Make caching of verification results more fine-grained for changes that affect preconditions.

1 files changed, 88 insertions, 38 deletions

diff --git a/Test/snapshots/runtest.snapshot.expect b/Test/snapshots/runtest.snapshot.expect
index 8f3c2015..637dd088 100644
--- a/Test/snapshots/runtest.snapshot.expect
+++ b/Test/snapshots/runtest.snapshot.expect
@@ -40,8 +40,13 @@ 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;

@@ -52,34 +57,45 @@ 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##post##0 := a##post##0 && false;

+  >>> 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 call to procedure P0 in implementation P0 (at Snapshots2.v5.bpl(7,5)):

+Processing implementation P0 (at Snapshots2.v5.bpl(5,51)):

   >>> 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

+  >>> 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();

-  >>> MarkAsFullyVerified

+  >>> MarkAsPartiallyVerified

 Processing command (at Snapshots2.v5.bpl(3,1)) assert F0();

-  >>> MarkAsFullyVerified

+  >>> 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.

@@ -89,7 +105,7 @@ 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;

+  >>> 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.

@@ -103,6 +119,8 @@ 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.

@@ -115,8 +133,8 @@ 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);

+  >>> 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

@@ -130,8 +148,8 @@ 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);

+  >>> 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

@@ -147,12 +165,12 @@ 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);

+  >>> 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##post##0 := a##post##0 && ##extracted_function##2(call1formal#AT#r);

+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

@@ -170,12 +188,12 @@ 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);

+  >>> 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##post##0 := a##post##0 && ##extracted_function##2(call1formal#AT#r);

+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

@@ -191,12 +209,12 @@ 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);

+  >>> 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##post##0 := a##post##0 && ##extracted_function##2(call1formal#AT#r);

+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

@@ -214,7 +232,7 @@ 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);

+  >>> 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;

@@ -230,7 +248,7 @@ Processing command (at Snapshots12.v0.bpl(7,5)) assert false;
 

 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;

+  >>> 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.

@@ -241,7 +259,7 @@ Processing command (at Snapshots13.v0.bpl(7,5)) assert false;
 

 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;

+  >>> 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.

@@ -253,8 +271,8 @@ Processing command (at Snapshots14.v0.bpl(7,5)) assert false;
 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();

+  >>> 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

@@ -270,9 +288,9 @@ Processing command (at Snapshots15.v0.bpl(13,5)) assert false;
 

 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;

+  >>> 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##post##1 := a##post##1 && false;

+  >>> 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;

@@ -302,11 +320,11 @@ Processing command (at Snapshots17.v0.bpl(20,13)) assert x == 1;
 

 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;

+  >>> 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##post##1 := a##post##1 && false;

+  >>> 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##post##2 := a##post##2 && false;

+  >>> 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;

@@ -328,9 +346,9 @@ Processing command (at Snapshots18.v0.bpl(20,5)) assert 2 != 2;
 

 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;

+  >>> 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##post##1 := a##post##1 && false;

+  >>> 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;

@@ -351,13 +369,14 @@ 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;

-  >>> RecycleError

-Snapshots19.v0.bpl(7,5): Error BP5001: This assertion might not hold.

+  >>> 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;

@@ -371,7 +390,7 @@ 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();

+  >>> 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;

@@ -567,8 +586,8 @@ Processing command (at Snapshots31.v0.bpl(10,5)) assert 0 < g;
 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);

+  >>> 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

@@ -582,8 +601,8 @@ 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);

+  >>> 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

@@ -594,7 +613,38 @@ 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##post##0 := a##post##0 && false;

+  >>> 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