Added a test for the verification result caching.

4 files changed, 41 insertions, 0 deletions

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

+

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

+{

+    var i: int;

+

+    i := 0;

+

+    while (*)

+    {

+        i := 0;

+    }

+

+    assert i == 0;

+}

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

+

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

+{

+    var i: int;

+

+    i := 0;

+

+    while (*)

+    {

+        i := 1;

+    }

+

+    assert i == 0;

+}

diff --git a/Test/snapshots/runtest.AI.snapshot b/Test/snapshots/runtest.AI.snapshot
new file mode 100644
index 00000000..51de91e8
--- /dev/null
+++ b/Test/snapshots/runtest.AI.snapshot
@@ -0,0 +1,2 @@
+// RUN: %boogie -errorTrace:0 -traceCaching:1 -verifySnapshots:2 -verifySeparately Snapshots29.bpl > "%t"

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

diff --git a/Test/snapshots/runtest.AI.snapshot.expect b/Test/snapshots/runtest.AI.snapshot.expect
new file mode 100644
index 00000000..be2666d4
--- /dev/null
+++ b/Test/snapshots/runtest.AI.snapshot.expect
@@ -0,0 +1,9 @@
+Processing command (at Snapshots29.v0.bpl(14,5)) assert i == 0 /* checksum: 15-7D-7A-B4-3A-9B-FD-1E-77-5A-56-1F-3A-18-C1-FD */ ;

+  >>> did nothing

+

+Boogie program verifier finished with 1 verified, 0 errors

+Processing command (at Snapshots29.v1.bpl(14,5)) assert i == 0 /* checksum: 8F-25-CD-62-0E-E2-33-AF-1A-28-E2-9A-F5-AC-02-2D */ ;

+  >>> did nothing

+Snapshots29.v1.bpl(14,5): Error BP5001: This assertion might not hold.

+

+Boogie program verifier finished with 0 verified, 1 error