diff options
author | wuestholz <unknown> | 2013-06-03 10:21:39 -0700 |
---|---|---|
committer | wuestholz <unknown> | 2013-06-03 10:21:39 -0700 |
commit | 6c36ef17eef694a2c3b5b144d29a4e51b5102c7c (patch) | |
tree | 2097e901533d9535151ffe3a65fd602475db311a /Test/snapshots | |
parent | 734ee394898d9e37c784f32e0d105678f82d981a (diff) |
Fixed an issue with discovering program snapshots.
Diffstat (limited to 'Test/snapshots')
-rw-r--r-- | Test/snapshots/Answer | 28 |
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
|