Added more tests for the more advanced verification result caching.

4 files changed, 39 insertions, 2 deletions

diff --git a/Test/dafny0/snapshots/Snapshots4.v0.dfy b/Test/dafny0/snapshots/Snapshots4.v0.dfy
new file mode 100644
index 00000000..beaadfeb
--- /dev/null
+++ b/Test/dafny0/snapshots/Snapshots4.v0.dfy
@@ -0,0 +1,11 @@
+method M()

+{

+  if (*)

+  {

+

+  }

+  else

+  {

+    assert 0 == 0;

+  }

+}

diff --git a/Test/dafny0/snapshots/Snapshots4.v1.dfy b/Test/dafny0/snapshots/Snapshots4.v1.dfy
new file mode 100644
index 00000000..cf9ae753
--- /dev/null
+++ b/Test/dafny0/snapshots/Snapshots4.v1.dfy
@@ -0,0 +1,12 @@
+method M()

+{

+  if (*)

+  {

+    assert 1 != 1;  // error

+  }

+  else

+  {

+    assert 0 == 0;

+    assert 2 != 2;  // error

+  }

+}

diff --git a/Test/dafny0/snapshots/runtest.snapshot b/Test/dafny0/snapshots/runtest.snapshot
index 2d1cbe02..8c49e6ef 100644
--- a/Test/dafny0/snapshots/runtest.snapshot
+++ b/Test/dafny0/snapshots/runtest.snapshot
@@ -1,2 +1,2 @@
-// RUN: %dafny /compile:0 /verifySnapshots:2 /verifySeparately Snapshots0.dfy Snapshots1.dfy Snapshots2.dfy Snapshots3.dfy > "%t"
+// RUN: %dafny /compile:0 /verifySnapshots:2 /verifySeparately Snapshots0.dfy Snapshots1.dfy Snapshots2.dfy Snapshots3.dfy Snapshots4.dfy > "%t"
 // RUN: %diff "%s.expect" "%t"
diff --git a/Test/dafny0/snapshots/runtest.snapshot.expect b/Test/dafny0/snapshots/runtest.snapshot.expect
index 963ba754..7a93dece 100644
--- a/Test/dafny0/snapshots/runtest.snapshot.expect
+++ b/Test/dafny0/snapshots/runtest.snapshot.expect
@@ -33,9 +33,23 @@ Execution trace:
     (0,0): anon3_Else

 

 Dafny program verifier finished with 1 verified, 1 error

-Snapshots3.v1.dfy(9,14): Error: assertion violation

+Snapshots3.v0.dfy(9,14): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Else

 

 Dafny program verifier finished with 1 verified, 1 error

+

+-------------------- Snapshots4.dfy --------------------

+

+Dafny program verifier finished with 2 verified, 0 errors

+Snapshots4.v1.dfy(5,14): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Then

+Snapshots4.v1.dfy(10,14): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Else

+

+Dafny program verifier finished with 1 verified, 2 errors