diff options
Diffstat (limited to 'Test/snapshots/runtest.snapshot.expect')
| -rw-r--r-- | Test/snapshots/runtest.snapshot.expect | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/Test/snapshots/runtest.snapshot.expect b/Test/snapshots/runtest.snapshot.expect index cf588e65..f34fefbe 100644 --- a/Test/snapshots/runtest.snapshot.expect +++ b/Test/snapshots/runtest.snapshot.expect @@ -203,7 +203,7 @@ Boogie program verifier finished with 0 verified, 1 error Processing call to procedure N in implementation M (at Snapshots11.v1.bpl(7,5)):
>>> added before precondition check: assume {:precondition_previous_snapshot} 0 < call0formal#AT#n;
>>> added after: a##post##0 := a##post##0 && 0 < call1formal#AT#r;
-Processing command (at Snapshots11.v1.bpl(7,5)) assume {:precondition_previous_snapshot} 0 < n;
+Processing command (at Snapshots11.v1.bpl(7,5)) assume {:precondition_previous_snapshot} 0 < call0formal#AT#n;
>>> DropAssume
Processing command (at Snapshots11.v1.bpl(7,5)) assert 0 < call0formal#AT#n;
>>> RecycleError
@@ -450,6 +450,8 @@ Processing command (at Snapshots24.v1.bpl(11,9)) assert {:subsumption 1} 5 == 5; >>> DoNothingToAssert
Processing command (at Snapshots24.v1.bpl(15,9)) assert {:subsumption 2} 6 != 6;
>>> RecycleError
+Processing command (at Snapshots24.v1.bpl(19,9)) assert {:subsumption 1} 2 == 2;
+ >>> DoNothingToAssert
Processing command (at Snapshots24.v1.bpl(20,9)) assert {:subsumption 2} 4 == 4;
>>> MarkAsFullyVerified
Processing command (at Snapshots24.v1.bpl(21,9)) assert 5 == 5;
|