Fixed issue in the verification result caching.

4 files changed, 59 insertions, 2 deletions

diff --git a/Test/snapshots/Snapshots30.v0.bpl b/Test/snapshots/Snapshots30.v0.bpl
new file mode 100644
index 00000000..459c4007
--- /dev/null
+++ b/Test/snapshots/Snapshots30.v0.bpl
@@ -0,0 +1,13 @@
+procedure {:checksum "0"} P();

+

+implementation {:id "P"} {:checksum "1"} P()

+{

+    call Q();

+}

+

+procedure {:checksum "2"} Q();

+  requires 0 == 0;

+  requires 1 == 1;

+  requires 2 != 2;

+  requires 3 == 3;

+  requires 4 == 4;

diff --git a/Test/snapshots/Snapshots30.v1.bpl b/Test/snapshots/Snapshots30.v1.bpl
new file mode 100644
index 00000000..089a1939
--- /dev/null
+++ b/Test/snapshots/Snapshots30.v1.bpl
@@ -0,0 +1,14 @@
+procedure {:checksum "0"} P();

+

+implementation {:id "P"} {:checksum "2"} P()

+{

+    call Q();

+    assert 5 == 5;

+}

+

+procedure {:checksum "2"} Q();

+  requires 0 == 0;

+  requires 1 == 1;

+  requires 2 != 2;

+  requires 3 == 3;

+  requires 4 == 4;

diff --git a/Test/snapshots/runtest.snapshot b/Test/snapshots/runtest.snapshot
index 484fa8e2..fb476128 100644
--- a/Test/snapshots/runtest.snapshot
+++ b/Test/snapshots/runtest.snapshot
@@ -1,2 +1,2 @@
-// RUN: %boogie -errorTrace:0 -traceCaching:1 -verifySnapshots:2 -verifySeparately -noinfer Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl Snapshots6.bpl Snapshots7.bpl Snapshots8.bpl Snapshots9.bpl Snapshots10.bpl Snapshots11.bpl Snapshots12.bpl Snapshots13.bpl Snapshots14.bpl Snapshots15.bpl Snapshots16.bpl Snapshots17.bpl Snapshots18.bpl Snapshots19.bpl Snapshots20.bpl Snapshots21.bpl Snapshots22.bpl Snapshots23.bpl Snapshots24.bpl Snapshots25.bpl Snapshots26.bpl Snapshots27.bpl Snapshots28.bpl > "%t"

+// RUN: %boogie -errorTrace:0 -traceCaching:1 -verifySnapshots:2 -verifySeparately -noinfer Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl Snapshots6.bpl Snapshots7.bpl Snapshots8.bpl Snapshots9.bpl Snapshots10.bpl Snapshots11.bpl Snapshots12.bpl Snapshots13.bpl Snapshots14.bpl Snapshots15.bpl Snapshots16.bpl Snapshots17.bpl Snapshots18.bpl Snapshots19.bpl Snapshots20.bpl Snapshots21.bpl Snapshots22.bpl Snapshots23.bpl Snapshots24.bpl Snapshots25.bpl Snapshots26.bpl Snapshots27.bpl Snapshots28.bpl Snapshots30.bpl > "%t"

 // RUN: %diff "%s.expect" "%t"

diff --git a/Test/snapshots/runtest.snapshot.expect b/Test/snapshots/runtest.snapshot.expect
index f34fefbe..d8642441 100644
--- a/Test/snapshots/runtest.snapshot.expect
+++ b/Test/snapshots/runtest.snapshot.expect
@@ -72,7 +72,7 @@ Processing command (at Snapshots2.v5.bpl(7,5)) assume {:precondition_previous_sn
 Processing command (at Snapshots2.v5.bpl(7,5)) assert F0();

   >>> MarkAsFullyVerified

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

-  >>> DoNothingToAssert

+  >>> MarkAsFullyVerified

 

 Boogie program verifier finished with 1 verified, 0 errors

 Processing command (at Snapshots3.v0.bpl(2,1)) assert G();

@@ -516,3 +516,33 @@ Processing command (at Snapshots28.v1.bpl(15,5)) assert x == 0;
 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