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