summaryrefslogtreecommitdiff
path: root/Test/snapshots/Answer
diff options
context:
space:
mode:
Diffstat (limited to 'Test/snapshots/Answer')
-rw-r--r--Test/snapshots/Answer8
1 files changed, 0 insertions, 8 deletions
diff --git a/Test/snapshots/Answer b/Test/snapshots/Answer
index 676f0323..dc0ee8c1 100644
--- a/Test/snapshots/Answer
+++ b/Test/snapshots/Answer
@@ -1,5 +1,3 @@
-
--------------------- Snapshots0 --------------------
Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold.
Execution trace:
Snapshots0.v0.bpl(41,5): anon0
@@ -27,8 +25,6 @@ Execution trace:
Snapshots0.v0.bpl(41,5): anon0
Boogie program verifier finished with 2 verified, 1 error
-
--------------------- Snapshots1 --------------------
Snapshots1.v0.bpl(13,5): Error BP5001: This assertion might not hold.
Execution trace:
Snapshots1.v0.bpl(13,5): anon0
@@ -46,8 +42,6 @@ Execution trace:
Boogie program verifier finished with 1 verified, 1 error
--------------------- Snapshots2 --------------------
-
Boogie program verifier finished with 1 verified, 0 errors
Boogie program verifier finished with 1 verified, 0 errors
@@ -60,8 +54,6 @@ Boogie program verifier finished with 1 verified, 0 errors
Boogie program verifier finished with 1 verified, 0 errors
--------------------- Snapshots3 --------------------
-
Boogie program verifier finished with 1 verified, 0 errors
Snapshots3.v1.bpl(6,1): Error BP5003: A postcondition might not hold on this return path.
Snapshots3.v1.bpl(2,1): Related location: This is the postcondition that might not hold.