summaryrefslogtreecommitdiff
path: root/Test/snapshots
diff options
context:
space:
mode:
authorGravatar wuestholz <unknown>2013-06-03 10:21:39 -0700
committerGravatar wuestholz <unknown>2013-06-03 10:21:39 -0700
commit6c36ef17eef694a2c3b5b144d29a4e51b5102c7c (patch)
tree2097e901533d9535151ffe3a65fd602475db311a /Test/snapshots
parent734ee394898d9e37c784f32e0d105678f82d981a (diff)
Fixed an issue with discovering program snapshots.
Diffstat (limited to 'Test/snapshots')
-rw-r--r--Test/snapshots/Answer28
1 files changed, 14 insertions, 14 deletions
diff --git a/Test/snapshots/Answer b/Test/snapshots/Answer
index aac9cd03..434cdfda 100644
--- a/Test/snapshots/Answer
+++ b/Test/snapshots/Answer
@@ -1,27 +1,27 @@
-c:\dafny\boogie\Test\snapshots\Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold.
+Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold.
Execution trace:
- c:\dafny\boogie\Test\snapshots\Snapshots0.v0.bpl(41,5): anon0
-c:\dafny\boogie\Test\snapshots\Snapshots0.v0.bpl(8,5): Error BP5001: This assertion might not hold.
+ Snapshots0.v0.bpl(41,5): anon0
+Snapshots0.v0.bpl(8,5): Error BP5001: This assertion might not hold.
Execution trace:
- c:\dafny\boogie\Test\snapshots\Snapshots0.v0.bpl(8,5): anon0
-c:\dafny\boogie\Test\snapshots\Snapshots0.v0.bpl(19,5): Error BP5001: This assertion might not hold.
+ Snapshots0.v0.bpl(8,5): anon0
+Snapshots0.v0.bpl(19,5): Error BP5001: This assertion might not hold.
Execution trace:
- c:\dafny\boogie\Test\snapshots\Snapshots0.v0.bpl(19,5): anon0
-c:\dafny\boogie\Test\snapshots\Snapshots0.v0.bpl(30,5): Error BP5001: This assertion might not hold.
+ Snapshots0.v0.bpl(19,5): anon0
+Snapshots0.v0.bpl(30,5): Error BP5001: This assertion might not hold.
Execution trace:
- c:\dafny\boogie\Test\snapshots\Snapshots0.v0.bpl(30,5): anon0
+ Snapshots0.v0.bpl(30,5): anon0
Boogie program verifier finished with 0 verified, 4 errors
-c:\dafny\boogie\Test\snapshots\Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold.
+Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold.
Execution trace:
- c:\dafny\boogie\Test\snapshots\Snapshots0.v0.bpl(41,5): anon0
-c:\dafny\boogie\Test\snapshots\Snapshots0.v1.bpl(30,5): Error BP5001: This assertion might not hold.
+ Snapshots0.v0.bpl(41,5): anon0
+Snapshots0.v1.bpl(30,5): Error BP5001: This assertion might not hold.
Execution trace:
- c:\dafny\boogie\Test\snapshots\Snapshots0.v1.bpl(30,5): anon0
+ Snapshots0.v1.bpl(30,5): anon0
Boogie program verifier finished with 2 verified, 2 errors
-c:\dafny\boogie\Test\snapshots\Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold.
+Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold.
Execution trace:
- c:\dafny\boogie\Test\snapshots\Snapshots0.v0.bpl(41,5): anon0
+ Snapshots0.v0.bpl(41,5): anon0
Boogie program verifier finished with 2 verified, 1 error