summaryrefslogtreecommitdiff
path: root/Test/snapshots/runtest.snapshot.expect
diff options
context:
space:
mode:
Diffstat (limited to 'Test/snapshots/runtest.snapshot.expect')
-rw-r--r--Test/snapshots/runtest.snapshot.expect1410
1 files changed, 810 insertions, 600 deletions
diff --git a/Test/snapshots/runtest.snapshot.expect b/Test/snapshots/runtest.snapshot.expect
index 8f3c2015..393c9330 100644
--- a/Test/snapshots/runtest.snapshot.expect
+++ b/Test/snapshots/runtest.snapshot.expect
@@ -1,600 +1,810 @@
-Processing command (at Snapshots0.v0.bpl(41,5)) assert false;
- >>> DoNothingToAssert
-Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold.
-Processing command (at Snapshots0.v0.bpl(8,5)) assert false;
- >>> DoNothingToAssert
-Snapshots0.v0.bpl(8,5): Error BP5001: This assertion might not hold.
-Processing command (at Snapshots0.v0.bpl(19,5)) assert false;
- >>> DoNothingToAssert
-Snapshots0.v0.bpl(19,5): Error BP5001: This assertion might not hold.
-Processing command (at Snapshots0.v0.bpl(30,5)) assert false;
- >>> DoNothingToAssert
-Snapshots0.v0.bpl(30,5): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 4 errors
-Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold.
-Processing command (at Snapshots0.v1.bpl(19,5)) assert true;
- >>> DoNothingToAssert
-Processing command (at Snapshots0.v1.bpl(30,5)) assert false;
- >>> DoNothingToAssert
-Snapshots0.v1.bpl(30,5): Error BP5001: This assertion might not hold.
-Processing command (at Snapshots0.v1.bpl(41,5)) assert true;
- >>> DoNothingToAssert
-
-Boogie program verifier finished with 2 verified, 2 errors
-Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold.
-Processing command (at Snapshots0.v2.bpl(19,5)) assert true;
- >>> DoNothingToAssert
-Processing command (at Snapshots0.v2.bpl(30,5)) assert true;
- >>> DoNothingToAssert
-
-Boogie program verifier finished with 2 verified, 1 error
-Processing command (at Snapshots1.v0.bpl(13,5)) assert 1 != 1;
- >>> DoNothingToAssert
-Snapshots1.v0.bpl(13,5): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 1 verified, 1 error
-Processing command (at Snapshots1.v1.bpl(13,5)) assert 2 != 2;
- >>> DoNothingToAssert
-Snapshots1.v1.bpl(13,5): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 1 verified, 1 error
-Processing call to procedure P2 in implementation P1 (at Snapshots1.v2.bpl(5,5)):
-Processing command (at Snapshots1.v2.bpl(5,5)) assert false;
- >>> DoNothingToAssert
-Snapshots1.v2.bpl(5,5): Error BP5002: A precondition for this call might not hold.
-Snapshots1.v2.bpl(10,3): Related location: This is the precondition that might not hold.
-Processing command (at Snapshots1.v2.bpl(14,5)) assert 2 != 2;
- >>> DoNothingToAssert
-
-Boogie program verifier finished with 1 verified, 1 error
-
-Boogie program verifier finished with 1 verified, 0 errors
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing call to procedure P0 in implementation P0 (at Snapshots2.v2.bpl(6,5)):
-Processing command (at Snapshots2.v2.bpl(6,5)) assert F0();
- >>> DoNothingToAssert
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing call to procedure P0 in implementation P0 (at Snapshots2.v3.bpl(6,5)):
- >>> added after: a##post##0 := a##post##0 && false;
-Processing command (at Snapshots2.v3.bpl(6,5)) assert F0();
- >>> DoNothingToAssert
-
-Boogie program verifier finished with 1 verified, 0 errors
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing call to procedure P0 in implementation P0 (at Snapshots2.v5.bpl(7,5)):
- >>> added axiom: ##extracted_function##1() == F0()
- >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1();
-Processing command (at Snapshots2.v5.bpl(7,5)) assume {:precondition_previous_snapshot} ##extracted_function##1();
- >>> MarkAsFullyVerified
-Processing command (at Snapshots2.v5.bpl(7,5)) assert F0();
- >>> MarkAsFullyVerified
-Processing command (at Snapshots2.v5.bpl(3,1)) assert F0();
- >>> MarkAsFullyVerified
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing command (at Snapshots3.v0.bpl(2,1)) assert G();
- >>> DoNothingToAssert
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing command (at Snapshots3.v1.bpl(2,1)) assert G();
- >>> DoNothingToAssert
-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.
-
-Boogie program verifier finished with 0 verified, 1 error
-
-Boogie program verifier finished with 3 verified, 0 errors
-Processing call to procedure P2 in implementation P1 (at Snapshots4.v1.bpl(14,5)):
- >>> added after: a##post##0 := a##post##0 && false;
-Processing command (at Snapshots4.v1.bpl(23,5)) assert false;
- >>> DoNothingToAssert
-Snapshots4.v1.bpl(23,5): Error BP5001: This assertion might not hold.
-Processing command (at Snapshots4.v1.bpl(28,3)) assert G();
- >>> DoNothingToAssert
-Snapshots4.v1.bpl(33,1): Error BP5003: A postcondition might not hold on this return path.
-Snapshots4.v1.bpl(28,3): Related location: This is the postcondition that might not hold.
-
-Boogie program verifier finished with 2 verified, 2 errors
-Processing command (at Snapshots5.v0.bpl(5,5)) assert false;
- >>> DoNothingToAssert
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing command (at Snapshots5.v1.bpl(5,5)) assert false;
- >>> DoNothingToAssert
-Snapshots5.v1.bpl(5,5): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing command (at Snapshots6.v0.bpl(13,5)) assert y == 0;
- >>> DoNothingToAssert
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing call to procedure N in implementation M (at Snapshots6.v1.bpl(11,5)):
- >>> added axiom: (forall y##old##0: int, y: int :: {:weight 30} { ##extracted_function##1(y##old##0, y) } ##extracted_function##1(y##old##0, y) == (y##old##0 == y))
- >>> added before: y##old##0 := y;
- >>> added after: a##post##0 := a##post##0 && ##extracted_function##1(y##old##0, y);
-Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##1(y##old##0, y);
- >>> AssumeNegationOfAssumptionVariable
-Processing command (at Snapshots6.v1.bpl(13,5)) assert y == 0;
- >>> MarkAsPartiallyVerified
-Snapshots6.v1.bpl(13,5): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing command (at Snapshots7.v0.bpl(14,5)) assert y < 0;
- >>> DoNothingToAssert
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing call to procedure N in implementation M (at Snapshots7.v1.bpl(12,5)):
- >>> added axiom: (forall y: int, z: int :: {:weight 30} { ##extracted_function##1(y, z) } ##extracted_function##1(y, z) == (y < z))
- >>> added before: y##old##0 := y;
- >>> added after: a##post##0 := a##post##0 && ##extracted_function##1(y, z);
-Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##1(y, z);
- >>> AssumeNegationOfAssumptionVariable
-Processing command (at Snapshots7.v1.bpl(14,5)) assert y < 0;
- >>> MarkAsPartiallyVerified
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing command (at Snapshots8.v0.bpl(8,5)) assert 0 < call0formal#AT#n;
- >>> DoNothingToAssert
-Processing command (at Snapshots8.v0.bpl(10,5)) assert 0 <= x;
- >>> DoNothingToAssert
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing call to procedure N in implementation M (at Snapshots8.v1.bpl(8,5)):
- >>> added axiom: (forall call0formal#AT#n: int :: {:weight 30} { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 < call0formal#AT#n))
- >>> added axiom: (forall call1formal#AT#r: int :: {:weight 30} { ##extracted_function##2(call1formal#AT#r) } ##extracted_function##2(call1formal#AT#r) == (0 < call1formal#AT#r))
- >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
- >>> added after: a##post##0 := a##post##0 && ##extracted_function##2(call1formal#AT#r);
-Processing command (at Snapshots8.v1.bpl(8,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
- >>> MarkAsFullyVerified
-Processing command (at Snapshots8.v1.bpl(8,5)) assert 0 < call0formal#AT#n;
- >>> MarkAsFullyVerified
-Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##2(call1formal#AT#r);
- >>> AssumeNegationOfAssumptionVariable
-Processing command (at Snapshots8.v1.bpl(10,5)) assert 0 <= x;
- >>> MarkAsPartiallyVerified
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing command (at Snapshots9.v0.bpl(8,5)) assert 0 < call0formal#AT#n;
- >>> DoNothingToAssert
-Processing command (at Snapshots9.v0.bpl(8,5)) assert true;
- >>> DoNothingToAssert
-Processing command (at Snapshots9.v0.bpl(10,5)) assert 0 <= x;
- >>> DoNothingToAssert
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing call to procedure N in implementation M (at Snapshots9.v1.bpl(8,5)):
- >>> added axiom: (forall call0formal#AT#n: int :: {:weight 30} { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 < call0formal#AT#n && true))
- >>> added axiom: (forall call1formal#AT#r: int :: {:weight 30} { ##extracted_function##2(call1formal#AT#r) } ##extracted_function##2(call1formal#AT#r) == (0 < call1formal#AT#r && true))
- >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
- >>> added after: a##post##0 := a##post##0 && ##extracted_function##2(call1formal#AT#r);
-Processing command (at Snapshots9.v1.bpl(8,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
- >>> MarkAsFullyVerified
-Processing command (at Snapshots9.v1.bpl(8,5)) assert 0 < call0formal#AT#n;
- >>> MarkAsFullyVerified
-Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##2(call1formal#AT#r);
- >>> AssumeNegationOfAssumptionVariable
-Processing command (at Snapshots9.v1.bpl(10,5)) assert 0 <= x;
- >>> MarkAsPartiallyVerified
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing command (at Snapshots10.v0.bpl(8,5)) assert 0 < call0formal#AT#n;
- >>> DoNothingToAssert
-Processing command (at Snapshots10.v0.bpl(12,5)) assert 0 <= x;
- >>> DoNothingToAssert
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing call to procedure N in implementation M (at Snapshots10.v1.bpl(8,5)):
- >>> added axiom: (forall call0formal#AT#n: int :: {:weight 30} { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 < call0formal#AT#n))
- >>> added axiom: (forall call1formal#AT#r: int :: {:weight 30} { ##extracted_function##2(call1formal#AT#r) } ##extracted_function##2(call1formal#AT#r) == (0 < call1formal#AT#r))
- >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
- >>> added after: a##post##0 := a##post##0 && ##extracted_function##2(call1formal#AT#r);
-Processing command (at Snapshots10.v1.bpl(8,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
- >>> MarkAsFullyVerified
-Processing command (at Snapshots10.v1.bpl(8,5)) assert 0 < call0formal#AT#n;
- >>> MarkAsFullyVerified
-Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##2(call1formal#AT#r);
- >>> AssumeNegationOfAssumptionVariable
-Processing command (at Snapshots10.v1.bpl(12,5)) assert 0 <= x;
- >>> MarkAsPartiallyVerified
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing command (at Snapshots11.v0.bpl(7,5)) assert 0 < call0formal#AT#n;
- >>> DoNothingToAssert
-Processing command (at Snapshots11.v0.bpl(9,5)) assert 0 <= x;
- >>> DoNothingToAssert
-Snapshots11.v0.bpl(7,5): Error BP5002: A precondition for this call might not hold.
-Snapshots11.v0.bpl(13,3): Related location: This is the precondition that might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing call to procedure N in implementation M (at Snapshots11.v1.bpl(7,5)):
- >>> added axiom: (forall call0formal#AT#n: int :: {:weight 30} { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 < call0formal#AT#n))
- >>> added axiom: (forall call1formal#AT#r: int :: {:weight 30} { ##extracted_function##2(call1formal#AT#r) } ##extracted_function##2(call1formal#AT#r) == (0 < call1formal#AT#r))
- >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
- >>> added after: a##post##0 := a##post##0 && ##extracted_function##2(call1formal#AT#r);
-Processing command (at Snapshots11.v1.bpl(7,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
- >>> DropAssume
-Processing command (at Snapshots11.v1.bpl(7,5)) assert 0 < call0formal#AT#n;
- >>> RecycleError
-Processing command (at Snapshots11.v1.bpl(9,5)) assert 0 <= x;
- >>> MarkAsPartiallyVerified
-Snapshots11.v0.bpl(7,5): Error BP5002: A precondition for this call might not hold.
-Snapshots11.v0.bpl(13,3): Related location: This is the precondition that might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing command (at Snapshots12.v0.bpl(7,5)) assert false;
- >>> DoNothingToAssert
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing call to procedure N in implementation M (at Snapshots12.v1.bpl(5,5)):
- >>> added after: a##post##0 := a##post##0 && false;
-Processing command (at Snapshots12.v1.bpl(7,5)) assert false;
- >>> DoNothingToAssert
-Snapshots12.v1.bpl(7,5): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing command (at Snapshots13.v0.bpl(7,5)) assert false;
- >>> DoNothingToAssert
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing call to procedure N in implementation M (at Snapshots13.v1.bpl(5,5)):
- >>> added after: a##post##0 := a##post##0 && false;
-Processing command (at Snapshots13.v1.bpl(7,5)) assert false;
- >>> DoNothingToAssert
-Snapshots13.v1.bpl(7,5): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing command (at Snapshots14.v0.bpl(7,5)) assert false;
- >>> DoNothingToAssert
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing call to procedure N in implementation M (at Snapshots14.v1.bpl(5,5)):
- >>> added axiom: ##extracted_function##1() == (F() && G())
- >>> added after: a##post##0 := a##post##0 && ##extracted_function##1();
-Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##1();
- >>> AssumeNegationOfAssumptionVariable
-Processing command (at Snapshots14.v1.bpl(7,5)) assert false;
- >>> MarkAsPartiallyVerified
-Snapshots14.v1.bpl(7,5): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing command (at Snapshots15.v0.bpl(5,5)) assert true;
- >>> DoNothingToAssert
-Processing command (at Snapshots15.v0.bpl(9,5)) assert true;
- >>> DoNothingToAssert
-Processing command (at Snapshots15.v0.bpl(13,5)) assert false;
- >>> DoNothingToAssert
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing call to procedure N in implementation M (at Snapshots15.v1.bpl(7,5)):
- >>> added after: a##post##0 := a##post##0 && false;
-Processing call to procedure N in implementation M (at Snapshots15.v1.bpl(11,5)):
- >>> added after: a##post##1 := a##post##1 && false;
-Processing command (at Snapshots15.v1.bpl(5,5)) assert true;
- >>> MarkAsFullyVerified
-Processing command (at Snapshots15.v1.bpl(9,5)) assert true;
- >>> MarkAsPartiallyVerified
-Processing command (at Snapshots15.v1.bpl(13,5)) assert false;
- >>> MarkAsPartiallyVerified
-Snapshots15.v1.bpl(13,5): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing command (at Snapshots16.v0.bpl(14,5)) assert F(0) == 1;
- >>> DoNothingToAssert
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing command (at Snapshots16.v1.bpl(14,5)) assert F(0) == 1;
- >>> DoNothingToAssert
-Snapshots16.v1.bpl(14,5): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing command (at Snapshots17.v0.bpl(28,5)) assert true;
- >>> DoNothingToAssert
-Processing command (at Snapshots17.v0.bpl(25,9)) assert false;
- >>> DoNothingToAssert
-Processing command (at Snapshots17.v0.bpl(12,13)) assert true;
- >>> DoNothingToAssert
-Processing command (at Snapshots17.v0.bpl(20,13)) assert x == 1;
- >>> DoNothingToAssert
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing call to procedure N in implementation M (at Snapshots17.v1.bpl(14,13)):
- >>> added after: a##post##0 := a##post##0 && false;
-Processing call to procedure N in implementation M (at Snapshots17.v1.bpl(16,13)):
- >>> added after: a##post##1 := a##post##1 && false;
-Processing call to procedure N in implementation M (at Snapshots17.v1.bpl(23,9)):
- >>> added after: a##post##2 := a##post##2 && false;
-Processing command (at Snapshots17.v1.bpl(28,5)) assert true;
- >>> MarkAsFullyVerified
-Processing command (at Snapshots17.v1.bpl(25,9)) assert false;
- >>> MarkAsPartiallyVerified
-Processing command (at Snapshots17.v1.bpl(12,13)) assert true;
- >>> MarkAsFullyVerified
-Processing command (at Snapshots17.v1.bpl(20,13)) assert x == 1;
- >>> MarkAsPartiallyVerified
-Snapshots17.v1.bpl(20,13): Error BP5001: This assertion might not hold.
-Snapshots17.v1.bpl(25,9): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 2 errors
-Processing command (at Snapshots18.v0.bpl(7,9)) assert 0 == 0;
- >>> DoNothingToAssert
-Processing command (at Snapshots18.v0.bpl(17,9)) assert 1 != 1;
- >>> DoNothingToAssert
-Processing command (at Snapshots18.v0.bpl(20,5)) assert 2 != 2;
- >>> DoNothingToAssert
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing call to procedure N in implementation M (at Snapshots18.v1.bpl(9,9)):
- >>> added after: a##post##0 := a##post##0 && false;
-Processing call to procedure N in implementation M (at Snapshots18.v1.bpl(10,9)):
- >>> added after: a##post##1 := a##post##1 && false;
-Processing command (at Snapshots18.v1.bpl(7,9)) assert 0 == 0;
- >>> MarkAsFullyVerified
-Processing command (at Snapshots18.v1.bpl(17,9)) assert 1 != 1;
- >>> MarkAsPartiallyVerified
-Processing command (at Snapshots18.v1.bpl(20,5)) assert 2 != 2;
- >>> MarkAsPartiallyVerified
-Snapshots18.v1.bpl(17,9): Error BP5001: This assertion might not hold.
-Snapshots18.v1.bpl(20,5): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 2 errors
-Processing command (at Snapshots19.v0.bpl(5,5)) assert 2 == 2;
- >>> DoNothingToAssert
-Processing command (at Snapshots19.v0.bpl(7,5)) assert 1 != 1;
- >>> DoNothingToAssert
-Snapshots19.v0.bpl(7,5): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing call to procedure N in implementation M (at Snapshots19.v1.bpl(5,5)):
- >>> added axiom: ##extracted_function##1() == (2 == 2)
- >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1();
-Processing command (at Snapshots19.v1.bpl(5,5)) assume {:precondition_previous_snapshot} ##extracted_function##1();
- >>> MarkAsFullyVerified
-Processing command (at Snapshots19.v1.bpl(5,5)) assert 2 == 2;
- >>> MarkAsFullyVerified
-Processing command (at Snapshots19.v1.bpl(7,5)) assert 1 != 1;
- >>> RecycleError
-Snapshots19.v0.bpl(7,5): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing command (at Snapshots20.v0.bpl(9,9)) assert 1 != 1;
- >>> DoNothingToAssert
-Processing command (at Snapshots20.v0.bpl(13,9)) assert 2 != 2;
- >>> DoNothingToAssert
-Processing command (at Snapshots20.v0.bpl(16,5)) assert 3 != 3;
- >>> DoNothingToAssert
-Snapshots20.v0.bpl(13,9): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing call to procedure N in implementation M (at Snapshots20.v1.bpl(7,9)):
- >>> added axiom: ##extracted_function##1() == (0 != 0)
- >>> added after: a##post##0 := a##post##0 && ##extracted_function##1();
-Processing command (at Snapshots20.v1.bpl(9,9)) assert 1 != 1;
- >>> MarkAsPartiallyVerified
-Processing command (at Snapshots20.v1.bpl(13,9)) assert 2 != 2;
- >>> RecycleError
-Processing command (at Snapshots20.v1.bpl(16,5)) assert 3 != 3;
- >>> MarkAsPartiallyVerified
-Snapshots20.v1.bpl(9,9): Error BP5001: This assertion might not hold.
-Snapshots20.v0.bpl(13,9): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 2 errors
-Processing command (at Snapshots21.v0.bpl(7,9)) assert 1 != 1;
- >>> DoNothingToAssert
-Processing command (at Snapshots21.v0.bpl(11,9)) assert 2 != 2;
- >>> DoNothingToAssert
-Processing command (at Snapshots21.v0.bpl(14,5)) assert 3 != 3;
- >>> DoNothingToAssert
-Snapshots21.v0.bpl(7,9): Error BP5001: This assertion might not hold.
-Snapshots21.v0.bpl(11,9): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 2 errors
-Processing command (at Snapshots21.v1.bpl(7,9)) assert 1 == 1;
- >>> DoNothingToAssert
-Processing command (at Snapshots21.v1.bpl(11,9)) assert 2 != 2;
- >>> RecycleError
-Processing command (at Snapshots21.v1.bpl(14,5)) assert 3 != 3;
- >>> DoNothingToAssert
-Snapshots21.v0.bpl(11,9): Error BP5001: This assertion might not hold.
-Snapshots21.v1.bpl(14,5): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 2 errors
-Processing command (at Snapshots22.v0.bpl(7,9)) assert 1 != 1;
- >>> DoNothingToAssert
-Processing command (at Snapshots22.v0.bpl(11,9)) assert 2 == 2;
- >>> DoNothingToAssert
-Processing command (at Snapshots22.v0.bpl(14,5)) assert 3 == 3;
- >>> DoNothingToAssert
-Snapshots22.v0.bpl(7,9): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing command (at Snapshots22.v1.bpl(7,9)) assert 1 == 1;
- >>> DoNothingToAssert
-Processing command (at Snapshots22.v1.bpl(11,9)) assert 2 == 2;
- >>> MarkAsFullyVerified
-Processing command (at Snapshots22.v1.bpl(14,5)) assert 3 == 3;
- >>> DoNothingToAssert
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing command (at Snapshots23.v0.bpl(7,9)) assert 1 != 1;
- >>> DoNothingToAssert
-Processing command (at Snapshots23.v0.bpl(11,9)) assert 2 == 2;
- >>> DoNothingToAssert
-Processing command (at Snapshots23.v0.bpl(14,5)) assert 3 == 3;
- >>> DoNothingToAssert
-Snapshots23.v0.bpl(7,9): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 1 verified, 1 error
-Snapshots23.v0.bpl(7,9): Error BP5001: This assertion might not hold.
-Processing command (at Snapshots23.v1.bpl(22,5)) assert 4 == 4;
- >>> DoNothingToAssert
-
-Boogie program verifier finished with 1 verified, 1 error
-Processing command (at Snapshots23.v2.bpl(8,9)) assert 1 != 1;
- >>> RecycleError
-Processing command (at Snapshots23.v2.bpl(12,9)) assert 2 == 2;
- >>> MarkAsFullyVerified
-Snapshots23.v0.bpl(7,9): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 1 verified, 1 error
-Processing command (at Snapshots24.v0.bpl(7,9)) assert {:subsumption 0} 1 != 1;
- >>> DoNothingToAssert
-Processing command (at Snapshots24.v0.bpl(11,9)) assert {:subsumption 1} 5 != 5;
- >>> DoNothingToAssert
-Processing command (at Snapshots24.v0.bpl(15,9)) assert {:subsumption 2} 6 != 6;
- >>> DoNothingToAssert
-Processing command (at Snapshots24.v0.bpl(19,9)) assert {:subsumption 1} 2 == 2;
- >>> DoNothingToAssert
-Processing command (at Snapshots24.v0.bpl(20,9)) assert {:subsumption 2} 4 == 4;
- >>> DoNothingToAssert
-Processing command (at Snapshots24.v0.bpl(21,9)) assert 5 == 5;
- >>> DoNothingToAssert
-Processing command (at Snapshots24.v0.bpl(24,5)) assert {:subsumption 0} 3 == 3;
- >>> DoNothingToAssert
-Snapshots24.v0.bpl(7,9): Error BP5001: This assertion might not hold.
-Snapshots24.v0.bpl(11,9): Error BP5001: This assertion might not hold.
-Snapshots24.v0.bpl(15,9): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 3 errors
-Processing command (at Snapshots24.v1.bpl(7,9)) assert {:subsumption 0} 1 == 1;
- >>> DoNothingToAssert
-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;
- >>> MarkAsFullyVerified
-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;
- >>> MarkAsFullyVerified
-Processing command (at Snapshots24.v1.bpl(24,5)) assert {:subsumption 0} 3 == 3;
- >>> DoNothingToAssert
-Snapshots24.v0.bpl(15,9): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing command (at Snapshots25.v0.bpl(12,5)) assert 0 == 0;
- >>> DoNothingToAssert
-Processing command (at Snapshots25.v0.bpl(13,5)) assert x != x;
- >>> DoNothingToAssert
-Snapshots25.v0.bpl(13,5): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing command (at Snapshots25.v1.bpl(12,5)) assert 0 == 0;
- >>> MarkAsFullyVerified
-Processing command (at Snapshots25.v1.bpl(13,5)) assert x != x;
- >>> RecycleError
-Snapshots25.v0.bpl(13,5): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing command (at Snapshots26.v0.bpl(12,5)) assert 0 == 0;
- >>> DoNothingToAssert
-Processing command (at Snapshots26.v0.bpl(13,5)) assert x != x;
- >>> DoNothingToAssert
-Snapshots26.v0.bpl(13,5): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing command (at Snapshots26.v1.bpl(13,5)) assert 0 == 0;
- >>> MarkAsFullyVerified
-Processing command (at Snapshots26.v1.bpl(14,5)) assert x != x;
- >>> RecycleError
-Snapshots26.v0.bpl(13,5): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing command (at Snapshots27.v0.bpl(12,5)) assert 0 == 0;
- >>> DoNothingToAssert
-Processing command (at Snapshots27.v0.bpl(13,5)) assert x != x;
- >>> DoNothingToAssert
-Snapshots27.v0.bpl(13,5): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing command (at Snapshots27.v1.bpl(14,5)) assert 0 == 0;
- >>> MarkAsFullyVerified
-Processing command (at Snapshots27.v1.bpl(15,5)) assert x != x;
- >>> RecycleError
-Snapshots27.v0.bpl(13,5): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing command (at Snapshots28.v0.bpl(13,5)) assert 0 == 0;
- >>> DoNothingToAssert
-Processing command (at Snapshots28.v0.bpl(14,5)) assert x == 0;
- >>> DoNothingToAssert
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing command (at Snapshots28.v1.bpl(14,5)) assert 0 == 0;
- >>> DoNothingToAssert
-Processing command (at Snapshots28.v1.bpl(15,5)) assert x == 0;
- >>> DoNothingToAssert
-Snapshots28.v1.bpl(15,5): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing command (at Snapshots30.v0.bpl(5,5)) assert 0 == 0;
- >>> DoNothingToAssert
-Processing command (at Snapshots30.v0.bpl(5,5)) assert 1 == 1;
- >>> DoNothingToAssert
-Processing command (at Snapshots30.v0.bpl(5,5)) assert 2 != 2;
- >>> DoNothingToAssert
-Processing command (at Snapshots30.v0.bpl(5,5)) assert 3 == 3;
- >>> DoNothingToAssert
-Processing command (at Snapshots30.v0.bpl(5,5)) assert 4 == 4;
- >>> DoNothingToAssert
-Snapshots30.v0.bpl(5,5): Error BP5002: A precondition for this call might not hold.
-Snapshots30.v0.bpl(11,3): Related location: This is the precondition that might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing command (at Snapshots30.v1.bpl(5,5)) assert 0 == 0;
- >>> MarkAsFullyVerified
-Processing command (at Snapshots30.v1.bpl(5,5)) assert 1 == 1;
- >>> MarkAsFullyVerified
-Processing command (at Snapshots30.v1.bpl(5,5)) assert 2 != 2;
- >>> RecycleError
-Processing command (at Snapshots30.v1.bpl(5,5)) assert 3 == 3;
- >>> MarkAsFullyVerified
-Processing command (at Snapshots30.v1.bpl(5,5)) assert 4 == 4;
- >>> MarkAsFullyVerified
-Processing command (at Snapshots30.v1.bpl(6,5)) assert 5 == 5;
- >>> DoNothingToAssert
-Snapshots30.v0.bpl(5,5): Error BP5002: A precondition for this call might not hold.
-Snapshots30.v0.bpl(11,3): Related location: This is the precondition that might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing command (at Snapshots31.v0.bpl(10,5)) assert 0 < g;
- >>> DoNothingToAssert
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing call to procedure Q in implementation P (at Snapshots31.v1.bpl(9,5)):
- >>> added axiom: (forall call0old#AT#g: int, g: int :: {:weight 30} { ##extracted_function##1(call0old#AT#g, g) } ##extracted_function##1(call0old#AT#g, g) == (call0old#AT#g < g))
- >>> added after: a##post##0 := a##post##0 && ##extracted_function##1(call0old#AT#g, g);
-Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##1(call0old#AT#g, g);
- >>> AssumeNegationOfAssumptionVariable
-Processing command (at Snapshots31.v1.bpl(10,5)) assert 0 < g;
- >>> MarkAsPartiallyVerified
-Snapshots31.v1.bpl(10,5): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing command (at Snapshots32.v0.bpl(10,5)) assert 0 < g;
- >>> DoNothingToAssert
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing call to procedure Q in implementation P (at Snapshots32.v1.bpl(8,5)):
- >>> added axiom: (forall g##old##0: int, g: int :: {:weight 30} { ##extracted_function##1(g##old##0, g) } ##extracted_function##1(g##old##0, g) == (g##old##0 < g))
- >>> added before: g##old##0 := g;
- >>> added after: a##post##0 := a##post##0 && ##extracted_function##1(g##old##0, g);
-Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##1(g##old##0, g);
- >>> AssumeNegationOfAssumptionVariable
-Processing command (at Snapshots32.v1.bpl(9,5)) assert 0 < g;
- >>> MarkAsPartiallyVerified
-Snapshots32.v1.bpl(9,5): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing command (at Snapshots33.v0.bpl(10,5)) assert 0 < g;
- >>> DoNothingToAssert
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing call to procedure Q in implementation P (at Snapshots33.v1.bpl(5,5)):
- >>> added after: a##post##0 := a##post##0 && false;
-
-Boogie program verifier finished with 1 verified, 0 errors
+Processing command (at Snapshots0.v0.bpl(41,5)) assert false;
+ >>> DoNothingToAssert
+Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold.
+Processing command (at Snapshots0.v0.bpl(8,5)) assert false;
+ >>> DoNothingToAssert
+Snapshots0.v0.bpl(8,5): Error BP5001: This assertion might not hold.
+Processing command (at Snapshots0.v0.bpl(19,5)) assert false;
+ >>> DoNothingToAssert
+Snapshots0.v0.bpl(19,5): Error BP5001: This assertion might not hold.
+Processing command (at Snapshots0.v0.bpl(30,5)) assert false;
+ >>> DoNothingToAssert
+Snapshots0.v0.bpl(30,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 4 errors
+Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold.
+Processing command (at Snapshots0.v1.bpl(19,5)) assert true;
+ >>> DoNothingToAssert
+Processing command (at Snapshots0.v1.bpl(30,5)) assert false;
+ >>> DoNothingToAssert
+Snapshots0.v1.bpl(30,5): Error BP5001: This assertion might not hold.
+Processing command (at Snapshots0.v1.bpl(41,5)) assert true;
+ >>> DoNothingToAssert
+
+Boogie program verifier finished with 2 verified, 2 errors
+Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold.
+Processing command (at Snapshots0.v2.bpl(19,5)) assert true;
+ >>> DoNothingToAssert
+Processing command (at Snapshots0.v2.bpl(30,5)) assert true;
+ >>> DoNothingToAssert
+
+Boogie program verifier finished with 2 verified, 1 error
+Processing command (at Snapshots1.v0.bpl(13,5)) assert 1 != 1;
+ >>> DoNothingToAssert
+Snapshots1.v0.bpl(13,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 1 verified, 1 error
+Processing command (at Snapshots1.v1.bpl(13,5)) assert 2 != 2;
+ >>> DoNothingToAssert
+Snapshots1.v1.bpl(13,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 1 verified, 1 error
+Processing call to procedure P2 in implementation P1 (at Snapshots1.v2.bpl(5,5)):
+ >>> added after: a##cached##0 := a##cached##0 && true;
+Processing implementation P2 (at Snapshots1.v2.bpl(12,51)):
+ >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && true;
+Processing command (at Snapshots1.v2.bpl(5,5)) assert false;
+ >>> DoNothingToAssert
+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && true;
+ >>> AssumeNegationOfAssumptionVariable
+Snapshots1.v2.bpl(5,5): Error BP5002: A precondition for this call might not hold.
+Snapshots1.v2.bpl(10,3): Related location: This is the precondition that might not hold.
+Processing command (at Snapshots1.v2.bpl(14,5)) assert 2 != 2;
+ >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 1 error
+
+Boogie program verifier finished with 1 verified, 0 errors
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing implementation P0 (at Snapshots2.v2.bpl(4,51)):
+ >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && true;
+Processing call to procedure P0 in implementation P0 (at Snapshots2.v2.bpl(6,5)):
+ >>> added after: a##cached##1 := a##cached##1 && true;
+Processing command (at Snapshots2.v2.bpl(6,5)) assert F0();
+ >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing implementation P0 (at Snapshots2.v3.bpl(4,51)):
+ >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && false;
+Processing call to procedure P0 in implementation P0 (at Snapshots2.v3.bpl(6,5)):
+ >>> added after: a##cached##1 := a##cached##1 && false;
+Processing command (at Snapshots2.v3.bpl(6,5)) assert F0();
+ >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing implementation P0 (at Snapshots2.v5.bpl(5,51)):
+ >>> added axiom: ##extracted_function##1() == F0()
+ >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##1();
+Processing call to procedure P0 in implementation P0 (at Snapshots2.v5.bpl(7,5)):
+ >>> added axiom: ##extracted_function##2() == F0()
+ >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##2();
+ >>> added after: a##cached##1 := a##cached##1 && true;
+Processing command (at Snapshots2.v5.bpl(7,5)) assume {:precondition_previous_snapshot} ##extracted_function##2();
+ >>> MarkAsPartiallyVerified
+Processing command (at Snapshots2.v5.bpl(7,5)) assert F0();
+ >>> MarkAsPartiallyVerified
+Processing command (at Snapshots2.v5.bpl(3,1)) assert F0();
+ >>> MarkAsPartiallyVerified
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing command (at Snapshots3.v0.bpl(2,1)) assert G();
+ >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing implementation P0 (at Snapshots3.v1.bpl(4,51)):
+ >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && false;
+Processing command (at Snapshots3.v1.bpl(2,1)) assert G();
+ >>> DoNothingToAssert
+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.
+
+Boogie program verifier finished with 0 verified, 1 error
+
+Boogie program verifier finished with 3 verified, 0 errors
+Processing call to procedure P2 in implementation P1 (at Snapshots4.v1.bpl(14,5)):
+ >>> added after: a##cached##0 := a##cached##0 && false;
+Processing command (at Snapshots4.v1.bpl(23,5)) assert false;
+ >>> DoNothingToAssert
+Snapshots4.v1.bpl(23,5): Error BP5001: This assertion might not hold.
+Processing command (at Snapshots4.v1.bpl(28,3)) assert G();
+ >>> DoNothingToAssert
+Snapshots4.v1.bpl(33,1): Error BP5003: A postcondition might not hold on this return path.
+Snapshots4.v1.bpl(28,3): Related location: This is the postcondition that might not hold.
+
+Boogie program verifier finished with 2 verified, 2 errors
+Processing command (at Snapshots5.v0.bpl(5,5)) assert false;
+ >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing implementation P0 (at Snapshots5.v1.bpl(3,51)):
+ >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && false;
+Processing command (at Snapshots5.v1.bpl(5,5)) assert false;
+ >>> DoNothingToAssert
+Snapshots5.v1.bpl(5,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots6.v0.bpl(13,5)) assert y == 0;
+ >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing call to procedure N in implementation M (at Snapshots6.v1.bpl(11,5)):
+ >>> added axiom: (forall y##old##0: int, y: int :: {:weight 30} { ##extracted_function##1(y##old##0, y) } ##extracted_function##1(y##old##0, y) == (y##old##0 == y))
+ >>> added before: y##old##0 := y;
+ >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##1(y##old##0, y);
+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##1(y##old##0, y);
+ >>> AssumeNegationOfAssumptionVariable
+Processing command (at Snapshots6.v1.bpl(13,5)) assert y == 0;
+ >>> MarkAsPartiallyVerified
+Snapshots6.v1.bpl(13,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots7.v0.bpl(14,5)) assert y < 0;
+ >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing call to procedure N in implementation M (at Snapshots7.v1.bpl(12,5)):
+ >>> added axiom: (forall y: int, z: int :: {:weight 30} { ##extracted_function##1(y, z) } ##extracted_function##1(y, z) == (y < z))
+ >>> added before: y##old##0 := y;
+ >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##1(y, z);
+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##1(y, z);
+ >>> AssumeNegationOfAssumptionVariable
+Processing command (at Snapshots7.v1.bpl(14,5)) assert y < 0;
+ >>> MarkAsPartiallyVerified
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing command (at Snapshots8.v0.bpl(8,5)) assert 0 < call0formal#AT#n;
+ >>> DoNothingToAssert
+Processing command (at Snapshots8.v0.bpl(10,5)) assert 0 <= x;
+ >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing call to procedure N in implementation M (at Snapshots8.v1.bpl(8,5)):
+ >>> added axiom: (forall call0formal#AT#n: int :: {:weight 30} { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 < call0formal#AT#n))
+ >>> added axiom: (forall call1formal#AT#r: int :: {:weight 30} { ##extracted_function##2(call1formal#AT#r) } ##extracted_function##2(call1formal#AT#r) == (0 < call1formal#AT#r))
+ >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
+ >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##2(call1formal#AT#r);
+Processing command (at Snapshots8.v1.bpl(8,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots8.v1.bpl(8,5)) assert 0 < call0formal#AT#n;
+ >>> MarkAsFullyVerified
+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##2(call1formal#AT#r);
+ >>> AssumeNegationOfAssumptionVariable
+Processing command (at Snapshots8.v1.bpl(10,5)) assert 0 <= x;
+ >>> MarkAsPartiallyVerified
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing command (at Snapshots9.v0.bpl(8,5)) assert 0 < call0formal#AT#n;
+ >>> DoNothingToAssert
+Processing command (at Snapshots9.v0.bpl(8,5)) assert true;
+ >>> DoNothingToAssert
+Processing command (at Snapshots9.v0.bpl(10,5)) assert 0 <= x;
+ >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing call to procedure N in implementation M (at Snapshots9.v1.bpl(8,5)):
+ >>> added axiom: (forall call0formal#AT#n: int :: {:weight 30} { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 < call0formal#AT#n && true))
+ >>> added axiom: (forall call1formal#AT#r: int :: {:weight 30} { ##extracted_function##2(call1formal#AT#r) } ##extracted_function##2(call1formal#AT#r) == (0 < call1formal#AT#r && true))
+ >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
+ >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##2(call1formal#AT#r);
+Processing command (at Snapshots9.v1.bpl(8,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots9.v1.bpl(8,5)) assert 0 < call0formal#AT#n;
+ >>> MarkAsFullyVerified
+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##2(call1formal#AT#r);
+ >>> AssumeNegationOfAssumptionVariable
+Processing command (at Snapshots9.v1.bpl(10,5)) assert 0 <= x;
+ >>> MarkAsPartiallyVerified
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing command (at Snapshots10.v0.bpl(8,5)) assert 0 < call0formal#AT#n;
+ >>> DoNothingToAssert
+Processing command (at Snapshots10.v0.bpl(12,5)) assert 0 <= x;
+ >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing call to procedure N in implementation M (at Snapshots10.v1.bpl(8,5)):
+ >>> added axiom: (forall call0formal#AT#n: int :: {:weight 30} { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 < call0formal#AT#n))
+ >>> added axiom: (forall call1formal#AT#r: int :: {:weight 30} { ##extracted_function##2(call1formal#AT#r) } ##extracted_function##2(call1formal#AT#r) == (0 < call1formal#AT#r))
+ >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
+ >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##2(call1formal#AT#r);
+Processing command (at Snapshots10.v1.bpl(8,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots10.v1.bpl(8,5)) assert 0 < call0formal#AT#n;
+ >>> MarkAsFullyVerified
+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##2(call1formal#AT#r);
+ >>> AssumeNegationOfAssumptionVariable
+Processing command (at Snapshots10.v1.bpl(12,5)) assert 0 <= x;
+ >>> MarkAsPartiallyVerified
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing command (at Snapshots11.v0.bpl(7,5)) assert 0 < call0formal#AT#n;
+ >>> DoNothingToAssert
+Processing command (at Snapshots11.v0.bpl(9,5)) assert 0 <= x;
+ >>> DoNothingToAssert
+Snapshots11.v0.bpl(7,5): Error BP5002: A precondition for this call might not hold.
+Snapshots11.v0.bpl(13,3): Related location: This is the precondition that might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing call to procedure N in implementation M (at Snapshots11.v1.bpl(7,5)):
+ >>> added axiom: (forall call0formal#AT#n: int :: {:weight 30} { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 < call0formal#AT#n))
+ >>> added axiom: (forall call1formal#AT#r: int :: {:weight 30} { ##extracted_function##2(call1formal#AT#r) } ##extracted_function##2(call1formal#AT#r) == (0 < call1formal#AT#r))
+ >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
+ >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##2(call1formal#AT#r);
+Processing command (at Snapshots11.v1.bpl(7,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
+ >>> DropAssume
+Processing command (at Snapshots11.v1.bpl(7,5)) assert 0 < call0formal#AT#n;
+ >>> RecycleError
+Processing command (at Snapshots11.v1.bpl(9,5)) assert 0 <= x;
+ >>> MarkAsPartiallyVerified
+Snapshots11.v0.bpl(7,5): Error BP5002: A precondition for this call might not hold.
+Snapshots11.v0.bpl(13,3): Related location: This is the precondition that might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots12.v0.bpl(7,5)) assert false;
+ >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing call to procedure N in implementation M (at Snapshots12.v1.bpl(5,5)):
+ >>> added after: a##cached##0 := a##cached##0 && false;
+Processing command (at Snapshots12.v1.bpl(7,5)) assert false;
+ >>> DoNothingToAssert
+Snapshots12.v1.bpl(7,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots13.v0.bpl(7,5)) assert false;
+ >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing call to procedure N in implementation M (at Snapshots13.v1.bpl(5,5)):
+ >>> added after: a##cached##0 := a##cached##0 && false;
+Processing command (at Snapshots13.v1.bpl(7,5)) assert false;
+ >>> DoNothingToAssert
+Snapshots13.v1.bpl(7,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots14.v0.bpl(7,5)) assert false;
+ >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing call to procedure N in implementation M (at Snapshots14.v1.bpl(5,5)):
+ >>> added axiom: ##extracted_function##1() == (F() && G())
+ >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##1();
+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##1();
+ >>> AssumeNegationOfAssumptionVariable
+Processing command (at Snapshots14.v1.bpl(7,5)) assert false;
+ >>> MarkAsPartiallyVerified
+Snapshots14.v1.bpl(7,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots15.v0.bpl(5,5)) assert true;
+ >>> DoNothingToAssert
+Processing command (at Snapshots15.v0.bpl(9,5)) assert true;
+ >>> DoNothingToAssert
+Processing command (at Snapshots15.v0.bpl(13,5)) assert false;
+ >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing call to procedure N in implementation M (at Snapshots15.v1.bpl(7,5)):
+ >>> added after: a##cached##0 := a##cached##0 && false;
+Processing call to procedure N in implementation M (at Snapshots15.v1.bpl(11,5)):
+ >>> added after: a##cached##1 := a##cached##1 && false;
+Processing command (at Snapshots15.v1.bpl(5,5)) assert true;
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots15.v1.bpl(9,5)) assert true;
+ >>> MarkAsPartiallyVerified
+Processing command (at Snapshots15.v1.bpl(13,5)) assert false;
+ >>> MarkAsPartiallyVerified
+Snapshots15.v1.bpl(13,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots16.v0.bpl(14,5)) assert F(0) == 1;
+ >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing command (at Snapshots16.v1.bpl(14,5)) assert F(0) == 1;
+ >>> DoNothingToAssert
+Snapshots16.v1.bpl(14,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots17.v0.bpl(28,5)) assert true;
+ >>> DoNothingToAssert
+Processing command (at Snapshots17.v0.bpl(25,9)) assert false;
+ >>> DoNothingToAssert
+Processing command (at Snapshots17.v0.bpl(12,13)) assert true;
+ >>> DoNothingToAssert
+Processing command (at Snapshots17.v0.bpl(20,13)) assert x == 1;
+ >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing call to procedure N in implementation M (at Snapshots17.v1.bpl(14,13)):
+ >>> added after: a##cached##0 := a##cached##0 && false;
+Processing call to procedure N in implementation M (at Snapshots17.v1.bpl(16,13)):
+ >>> added after: a##cached##1 := a##cached##1 && false;
+Processing call to procedure N in implementation M (at Snapshots17.v1.bpl(23,9)):
+ >>> added after: a##cached##2 := a##cached##2 && false;
+Processing command (at Snapshots17.v1.bpl(28,5)) assert true;
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots17.v1.bpl(25,9)) assert false;
+ >>> MarkAsPartiallyVerified
+Processing command (at Snapshots17.v1.bpl(12,13)) assert true;
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots17.v1.bpl(20,13)) assert x == 1;
+ >>> MarkAsPartiallyVerified
+Snapshots17.v1.bpl(20,13): Error BP5001: This assertion might not hold.
+Snapshots17.v1.bpl(25,9): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 2 errors
+Processing command (at Snapshots18.v0.bpl(7,9)) assert 0 == 0;
+ >>> DoNothingToAssert
+Processing command (at Snapshots18.v0.bpl(17,9)) assert 1 != 1;
+ >>> DoNothingToAssert
+Processing command (at Snapshots18.v0.bpl(20,5)) assert 2 != 2;
+ >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing call to procedure N in implementation M (at Snapshots18.v1.bpl(9,9)):
+ >>> added after: a##cached##0 := a##cached##0 && false;
+Processing call to procedure N in implementation M (at Snapshots18.v1.bpl(10,9)):
+ >>> added after: a##cached##1 := a##cached##1 && false;
+Processing command (at Snapshots18.v1.bpl(7,9)) assert 0 == 0;
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots18.v1.bpl(17,9)) assert 1 != 1;
+ >>> MarkAsPartiallyVerified
+Processing command (at Snapshots18.v1.bpl(20,5)) assert 2 != 2;
+ >>> MarkAsPartiallyVerified
+Snapshots18.v1.bpl(17,9): Error BP5001: This assertion might not hold.
+Snapshots18.v1.bpl(20,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 2 errors
+Processing command (at Snapshots19.v0.bpl(5,5)) assert 2 == 2;
+ >>> DoNothingToAssert
+Processing command (at Snapshots19.v0.bpl(7,5)) assert 1 != 1;
+ >>> DoNothingToAssert
+Snapshots19.v0.bpl(7,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing call to procedure N in implementation M (at Snapshots19.v1.bpl(5,5)):
+ >>> added axiom: ##extracted_function##1() == (2 == 2)
+ >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1();
+ >>> added after: a##cached##0 := a##cached##0 && true;
+Processing command (at Snapshots19.v1.bpl(5,5)) assume {:precondition_previous_snapshot} ##extracted_function##1();
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots19.v1.bpl(5,5)) assert 2 == 2;
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots19.v1.bpl(7,5)) assert 1 != 1;
+ >>> DoNothingToAssert
+Snapshots19.v1.bpl(7,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots20.v0.bpl(9,9)) assert 1 != 1;
+ >>> DoNothingToAssert
+Processing command (at Snapshots20.v0.bpl(13,9)) assert 2 != 2;
+ >>> DoNothingToAssert
+Processing command (at Snapshots20.v0.bpl(16,5)) assert 3 != 3;
+ >>> DoNothingToAssert
+Snapshots20.v0.bpl(13,9): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing call to procedure N in implementation M (at Snapshots20.v1.bpl(7,9)):
+ >>> added axiom: ##extracted_function##1() == (0 != 0)
+ >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##1();
+Processing command (at Snapshots20.v1.bpl(9,9)) assert 1 != 1;
+ >>> MarkAsPartiallyVerified
+Processing command (at Snapshots20.v1.bpl(13,9)) assert 2 != 2;
+ >>> RecycleError
+Processing command (at Snapshots20.v1.bpl(16,5)) assert 3 != 3;
+ >>> MarkAsPartiallyVerified
+Snapshots20.v1.bpl(9,9): Error BP5001: This assertion might not hold.
+Snapshots20.v0.bpl(13,9): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 2 errors
+Processing command (at Snapshots21.v0.bpl(7,9)) assert 1 != 1;
+ >>> DoNothingToAssert
+Processing command (at Snapshots21.v0.bpl(11,9)) assert 2 != 2;
+ >>> DoNothingToAssert
+Processing command (at Snapshots21.v0.bpl(14,5)) assert 3 != 3;
+ >>> DoNothingToAssert
+Snapshots21.v0.bpl(7,9): Error BP5001: This assertion might not hold.
+Snapshots21.v0.bpl(11,9): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 2 errors
+Processing command (at Snapshots21.v1.bpl(7,9)) assert 1 == 1;
+ >>> DoNothingToAssert
+Processing command (at Snapshots21.v1.bpl(11,9)) assert 2 != 2;
+ >>> RecycleError
+Processing command (at Snapshots21.v1.bpl(14,5)) assert 3 != 3;
+ >>> DoNothingToAssert
+Snapshots21.v0.bpl(11,9): Error BP5001: This assertion might not hold.
+Snapshots21.v1.bpl(14,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 2 errors
+Processing command (at Snapshots22.v0.bpl(7,9)) assert 1 != 1;
+ >>> DoNothingToAssert
+Processing command (at Snapshots22.v0.bpl(11,9)) assert 2 == 2;
+ >>> DoNothingToAssert
+Processing command (at Snapshots22.v0.bpl(14,5)) assert 3 == 3;
+ >>> DoNothingToAssert
+Snapshots22.v0.bpl(7,9): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots22.v1.bpl(7,9)) assert 1 == 1;
+ >>> DoNothingToAssert
+Processing command (at Snapshots22.v1.bpl(11,9)) assert 2 == 2;
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots22.v1.bpl(14,5)) assert 3 == 3;
+ >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing command (at Snapshots23.v0.bpl(7,9)) assert 1 != 1;
+ >>> DoNothingToAssert
+Processing command (at Snapshots23.v0.bpl(11,9)) assert 2 == 2;
+ >>> DoNothingToAssert
+Processing command (at Snapshots23.v0.bpl(14,5)) assert 3 == 3;
+ >>> DoNothingToAssert
+Snapshots23.v0.bpl(7,9): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 1 verified, 1 error
+Snapshots23.v0.bpl(7,9): Error BP5001: This assertion might not hold.
+Processing command (at Snapshots23.v1.bpl(22,5)) assert 4 == 4;
+ >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 1 error
+Processing command (at Snapshots23.v2.bpl(8,9)) assert 1 != 1;
+ >>> RecycleError
+Processing command (at Snapshots23.v2.bpl(12,9)) assert 2 == 2;
+ >>> MarkAsFullyVerified
+Snapshots23.v0.bpl(7,9): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 1 verified, 1 error
+Processing command (at Snapshots24.v0.bpl(7,9)) assert {:subsumption 0} 1 != 1;
+ >>> DoNothingToAssert
+Processing command (at Snapshots24.v0.bpl(11,9)) assert {:subsumption 1} 5 != 5;
+ >>> DoNothingToAssert
+Processing command (at Snapshots24.v0.bpl(15,9)) assert {:subsumption 2} 6 != 6;
+ >>> DoNothingToAssert
+Processing command (at Snapshots24.v0.bpl(19,9)) assert {:subsumption 1} 2 == 2;
+ >>> DoNothingToAssert
+Processing command (at Snapshots24.v0.bpl(20,9)) assert {:subsumption 2} 4 == 4;
+ >>> DoNothingToAssert
+Processing command (at Snapshots24.v0.bpl(21,9)) assert 5 == 5;
+ >>> DoNothingToAssert
+Processing command (at Snapshots24.v0.bpl(24,5)) assert {:subsumption 0} 3 == 3;
+ >>> DoNothingToAssert
+Snapshots24.v0.bpl(7,9): Error BP5001: This assertion might not hold.
+Snapshots24.v0.bpl(11,9): Error BP5001: This assertion might not hold.
+Snapshots24.v0.bpl(15,9): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 3 errors
+Processing command (at Snapshots24.v1.bpl(7,9)) assert {:subsumption 0} 1 == 1;
+ >>> DoNothingToAssert
+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;
+ >>> MarkAsFullyVerified
+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;
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots24.v1.bpl(24,5)) assert {:subsumption 0} 3 == 3;
+ >>> DoNothingToAssert
+Snapshots24.v0.bpl(15,9): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots25.v0.bpl(12,5)) assert 0 == 0;
+ >>> DoNothingToAssert
+Processing command (at Snapshots25.v0.bpl(13,5)) assert x != x;
+ >>> DoNothingToAssert
+Snapshots25.v0.bpl(13,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots25.v1.bpl(12,5)) assert 0 == 0;
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots25.v1.bpl(13,5)) assert x != x;
+ >>> RecycleError
+Snapshots25.v0.bpl(13,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots26.v0.bpl(12,5)) assert 0 == 0;
+ >>> DoNothingToAssert
+Processing command (at Snapshots26.v0.bpl(13,5)) assert x != x;
+ >>> DoNothingToAssert
+Snapshots26.v0.bpl(13,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots26.v1.bpl(13,5)) assert 0 == 0;
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots26.v1.bpl(14,5)) assert x != x;
+ >>> RecycleError
+Snapshots26.v0.bpl(13,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots27.v0.bpl(12,5)) assert 0 == 0;
+ >>> DoNothingToAssert
+Processing command (at Snapshots27.v0.bpl(13,5)) assert x != x;
+ >>> DoNothingToAssert
+Snapshots27.v0.bpl(13,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots27.v1.bpl(14,5)) assert 0 == 0;
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots27.v1.bpl(15,5)) assert x != x;
+ >>> RecycleError
+Snapshots27.v0.bpl(13,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots28.v0.bpl(13,5)) assert 0 == 0;
+ >>> DoNothingToAssert
+Processing command (at Snapshots28.v0.bpl(14,5)) assert x == 0;
+ >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing command (at Snapshots28.v1.bpl(14,5)) assert 0 == 0;
+ >>> DoNothingToAssert
+Processing command (at Snapshots28.v1.bpl(15,5)) assert x == 0;
+ >>> DoNothingToAssert
+Snapshots28.v1.bpl(15,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots30.v0.bpl(5,5)) assert 0 == 0;
+ >>> DoNothingToAssert
+Processing command (at Snapshots30.v0.bpl(5,5)) assert 1 == 1;
+ >>> DoNothingToAssert
+Processing command (at Snapshots30.v0.bpl(5,5)) assert 2 != 2;
+ >>> DoNothingToAssert
+Processing command (at Snapshots30.v0.bpl(5,5)) assert 3 == 3;
+ >>> DoNothingToAssert
+Processing command (at Snapshots30.v0.bpl(5,5)) assert 4 == 4;
+ >>> DoNothingToAssert
+Snapshots30.v0.bpl(5,5): Error BP5002: A precondition for this call might not hold.
+Snapshots30.v0.bpl(11,3): Related location: This is the precondition that might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots30.v1.bpl(5,5)) assert 0 == 0;
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots30.v1.bpl(5,5)) assert 1 == 1;
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots30.v1.bpl(5,5)) assert 2 != 2;
+ >>> RecycleError
+Processing command (at Snapshots30.v1.bpl(5,5)) assert 3 == 3;
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots30.v1.bpl(5,5)) assert 4 == 4;
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots30.v1.bpl(6,5)) assert 5 == 5;
+ >>> DoNothingToAssert
+Snapshots30.v0.bpl(5,5): Error BP5002: A precondition for this call might not hold.
+Snapshots30.v0.bpl(11,3): Related location: This is the precondition that might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots31.v0.bpl(10,5)) assert 0 < g;
+ >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing call to procedure Q in implementation P (at Snapshots31.v1.bpl(9,5)):
+ >>> added axiom: (forall call0old#AT#g: int, g: int :: {:weight 30} { ##extracted_function##1(call0old#AT#g, g) } ##extracted_function##1(call0old#AT#g, g) == (call0old#AT#g < g))
+ >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##1(call0old#AT#g, g);
+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##1(call0old#AT#g, g);
+ >>> AssumeNegationOfAssumptionVariable
+Processing command (at Snapshots31.v1.bpl(10,5)) assert 0 < g;
+ >>> MarkAsPartiallyVerified
+Snapshots31.v1.bpl(10,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots32.v0.bpl(10,5)) assert 0 < g;
+ >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing call to procedure Q in implementation P (at Snapshots32.v1.bpl(8,5)):
+ >>> added axiom: (forall g##old##0: int, g: int :: {:weight 30} { ##extracted_function##1(g##old##0, g) } ##extracted_function##1(g##old##0, g) == (g##old##0 < g))
+ >>> added before: g##old##0 := g;
+ >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##1(g##old##0, g);
+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##1(g##old##0, g);
+ >>> AssumeNegationOfAssumptionVariable
+Processing command (at Snapshots32.v1.bpl(9,5)) assert 0 < g;
+ >>> MarkAsPartiallyVerified
+Snapshots32.v1.bpl(9,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots33.v0.bpl(10,5)) assert 0 < g;
+ >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing implementation P (at Snapshots33.v1.bpl(3,42)):
+ >>> added axiom: (forall g: int :: {:weight 30} { ##extracted_function##1(g) } ##extracted_function##1(g) == (g == 0))
+ >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##1(g);
+Processing call to procedure Q in implementation P (at Snapshots33.v1.bpl(5,5)):
+ >>> added after: a##cached##1 := a##cached##1 && false;
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing command (at Snapshots34.v0.bpl(6,5)) assert 1 != 1;
+ >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing implementation P (at Snapshots34.v1.bpl(3,42)):
+ >>> added axiom: ##extracted_function##1() == (0 != 0)
+ >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##1();
+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##1();
+ >>> AssumeNegationOfAssumptionVariable
+Processing command (at Snapshots34.v1.bpl(5,5)) assert 1 != 1;
+ >>> MarkAsPartiallyVerified
+Snapshots34.v1.bpl(5,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots35.v0.bpl(6,5)) assert p;
+ >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing implementation P (at Snapshots35.v1.bpl(3,42)):
+ >>> added axiom: (forall p: bool :: {:weight 30} { ##extracted_function##1(p) } ##extracted_function##1(p) == p)
+ >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##1(p);
+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##1(p);
+ >>> AssumeNegationOfAssumptionVariable
+Processing command (at Snapshots35.v1.bpl(5,5)) assert p;
+ >>> MarkAsPartiallyVerified
+Snapshots35.v1.bpl(5,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots36.v0.bpl(13,5)) assert l[0];
+ >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing command (at Snapshots36.v1.bpl(13,5)) assert l[0];
+ >>> DoNothingToAssert
+Snapshots36.v1.bpl(13,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots37.v0.bpl(8,5)) assert l[0];
+ >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing command (at Snapshots37.v1.bpl(8,5)) assert l[0];
+ >>> DoNothingToAssert
+Snapshots37.v1.bpl(8,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots38.v0.bpl(7,5)) assert 0 <= call0formal#AT#n;
+ >>> DoNothingToAssert
+Processing command (at Snapshots38.v0.bpl(8,5)) assert r != 0;
+ >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing command (at Snapshots38.v1.bpl(7,5)) assert 0 <= call0formal#AT#n;
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots38.v1.bpl(8,5)) assert r != 0;
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots38.v1.bpl(9,5)) assert 42 <= r;
+ >>> DoNothingToAssert
+Snapshots38.v1.bpl(9,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing call to procedure Sum in implementation Callee (at Snapshots38.v2.bpl(7,5)):
+ >>> added axiom: (forall call0formal#AT#n: int :: {:weight 30} { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 <= call0formal#AT#n))
+ >>> added axiom: (forall call0formal#AT#n: int, call1formal#AT#r: int :: {:weight 30} { ##extracted_function##2(call0formal#AT#n, call1formal#AT#r) } ##extracted_function##2(call0formal#AT#n, call1formal#AT#r) == (call0formal#AT#n != 0 ==> 1 <= call1formal#AT#r))
+ >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
+ >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##2(call0formal#AT#n, call1formal#AT#r);
+Processing command (at Snapshots38.v2.bpl(7,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots38.v2.bpl(7,5)) assert 0 <= call0formal#AT#n;
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots38.v2.bpl(8,5)) assert r != 0;
+ >>> MarkAsPartiallyVerified
+Processing command (at Snapshots38.v2.bpl(9,5)) assert 42 <= r;
+ >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing command (at Snapshots39.v0.bpl(7,5)) assert 0 <= call0formal#AT#n;
+ >>> DoNothingToAssert
+Processing command (at Snapshots39.v0.bpl(8,5)) assert r != 0;
+ >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing command (at Snapshots39.v1.bpl(7,5)) assert 0 <= call0formal#AT#n;
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots39.v1.bpl(8,5)) assert r != 0;
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots39.v1.bpl(9,5)) assert r == 42 * 43 div 2;
+ >>> DoNothingToAssert
+Snapshots39.v1.bpl(9,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing call to procedure Sum in implementation Callee (at Snapshots39.v2.bpl(7,5)):
+ >>> added axiom: (forall call0formal#AT#n: int :: {:weight 30} { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 <= call0formal#AT#n))
+ >>> added axiom: (forall call0formal#AT#n: int, call1formal#AT#r: int :: {:weight 30} { ##extracted_function##2(call0formal#AT#n, call1formal#AT#r) } ##extracted_function##2(call0formal#AT#n, call1formal#AT#r) == (call0formal#AT#n <= call1formal#AT#r))
+ >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
+ >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##2(call0formal#AT#n, call1formal#AT#r);
+Processing command (at Snapshots39.v2.bpl(7,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots39.v2.bpl(7,5)) assert 0 <= call0formal#AT#n;
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots39.v2.bpl(8,5)) assert r != 0;
+ >>> MarkAsPartiallyVerified
+Processing command (at Snapshots39.v2.bpl(9,5)) assert r == 42 * 43 div 2;
+ >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing command (at Snapshots40.v0.bpl(7,5)) assert b;
+ >>> DoNothingToAssert
+Processing command (at Snapshots40.v0.bpl(8,5)) assert 0 <= call0formal#AT#n;
+ >>> DoNothingToAssert
+Processing command (at Snapshots40.v0.bpl(9,5)) assert r != 0;
+ >>> DoNothingToAssert
+Snapshots40.v0.bpl(7,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots40.v1.bpl(7,5)) assert b;
+ >>> RecycleError
+Processing command (at Snapshots40.v1.bpl(8,5)) assert 0 <= call0formal#AT#n;
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots40.v1.bpl(9,5)) assert r != 0;
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots40.v1.bpl(10,5)) assert r == 42 * 43 div 2;
+ >>> DoNothingToAssert
+Snapshots40.v0.bpl(7,5): Error BP5001: This assertion might not hold.
+Snapshots40.v1.bpl(10,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 2 errors
+Processing call to procedure Sum in implementation Foo (at Snapshots40.v2.bpl(8,5)):
+ >>> added axiom: (forall call0formal#AT#n: int :: {:weight 30} { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 <= call0formal#AT#n))
+ >>> added axiom: (forall call0formal#AT#n: int, call1formal#AT#r: int :: {:weight 30} { ##extracted_function##2(call0formal#AT#n, call1formal#AT#r) } ##extracted_function##2(call0formal#AT#n, call1formal#AT#r) == (call0formal#AT#n <= call1formal#AT#r))
+ >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
+ >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##2(call0formal#AT#n, call1formal#AT#r);
+Processing command (at Snapshots40.v2.bpl(7,5)) assert b;
+ >>> RecycleError
+Processing command (at Snapshots40.v2.bpl(8,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots40.v2.bpl(8,5)) assert 0 <= call0formal#AT#n;
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots40.v2.bpl(9,5)) assert r != 0;
+ >>> MarkAsPartiallyVerified
+Processing command (at Snapshots40.v2.bpl(10,5)) assert r == 42 * 43 div 2;
+ >>> DoNothingToAssert
+Snapshots40.v0.bpl(7,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots41.v0.bpl(3,23)) assert x < 20 || 10 <= x;
+ >>> DoNothingToAssert
+Processing command (at Snapshots41.v0.bpl(4,3)) assert x < 10;
+ >>> DoNothingToAssert
+Processing command (at Snapshots41.v0.bpl(5,3)) assert 0 <= call0formal#AT#y;
+ >>> DoNothingToAssert
+Snapshots41.v0.bpl(4,3): Error BP5001: This assertion might not hold.
+Snapshots41.v0.bpl(5,3): Error BP5002: A precondition for this call might not hold.
+Snapshots41.v0.bpl(9,3): Related location: This is the precondition that might not hold.
+Processing command (at Snapshots41.v0.bpl(15,3)) assert 2 <= z;
+ >>> DoNothingToAssert
+Snapshots41.v0.bpl(22,3): Error BP5003: A postcondition might not hold on this return path.
+Snapshots41.v0.bpl(15,3): Related location: This is the postcondition that might not hold.
+Processing command (at Snapshots41.v0.bpl(28,3)) assert u != 53;
+ >>> DoNothingToAssert
+Snapshots41.v0.bpl(28,3): Error BP5001: This assertion might not hold.
+Processing command (at Snapshots41.v0.bpl(34,3)) assert true;
+ >>> DoNothingToAssert
+
+Boogie program verifier finished with 2 verified, 4 errors
+Processing command (at Snapshots41.v1.bpl(4,1)) assert x < 20 || 10 <= x;
+ >>> MarkAsFullyVerified
+Processing command (at Snapshots41.v1.bpl(6,8)) assert x < 10;
+ >>> RecycleError
+Processing command (at Snapshots41.v1.bpl(7,3)) assert 0 <= call0formal#AT#y;
+ >>> RecycleError
+Processing command (at Snapshots41.v1.bpl(8,3)) assert x == 7;
+ >>> DoNothingToAssert
+Snapshots41.v1.bpl(6,8): Error BP5001: This assertion might not hold.
+Snapshots41.v1.bpl(7,3): Error BP5002: A precondition for this call might not hold.
+Snapshots41.v1.bpl(13,10): Related location: This is the precondition that might not hold.
+Snapshots41.v1.bpl(8,3): Error BP5001: This assertion might not hold.
+Processing command (at Snapshots41.v1.bpl(27,5)) assert true;
+ >>> DoNothingToAssert
+Processing command (at Snapshots41.v1.bpl(21,3)) assert 2 <= z;
+ >>> DoNothingToAssert
+Snapshots41.v1.bpl(29,3): Error BP5003: A postcondition might not hold on this return path.
+Snapshots41.v1.bpl(21,3): Related location: This is the postcondition that might not hold.
+Processing command (at Snapshots41.v1.bpl(35,8)) assert u != 53;
+ >>> RecycleError
+Snapshots41.v1.bpl(35,8): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 2 verified, 5 errors
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 03:22:27 +0000