11 files changed, 163 insertions, 0 deletions
diff --git a/Test/snapshots/Answer b/Test/snapshots/Answer
index 434cdfda..a7a6b0be 100644
--- a/Test/snapshots/Answer
+++ b/Test/snapshots/Answer
@@ -1,3 +1,4 @@
+-------------------- Snapshots0.bpl --------------------
 Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold.
 Execution trace:
     Snapshots0.v0.bpl(41,5): anon0
@@ -25,3 +26,35 @@ Execution trace:
     Snapshots0.v0.bpl(41,5): anon0
 
 Boogie program verifier finished with 2 verified, 1 error
+
+-------------------- Snapshots1.bpl --------------------
+Snapshots1.v0.bpl(13,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    Snapshots1.v0.bpl(13,5): anon0
+
+Boogie program verifier finished with 1 verified, 1 error
+Snapshots1.v1.bpl(13,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    Snapshots1.v1.bpl(13,5): anon0
+
+Boogie program verifier finished with 1 verified, 1 error
+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.
+Execution trace:
+    Snapshots1.v2.bpl(5,5): anon0
+
+Boogie program verifier finished with 1 verified, 1 error
+
+-------------------- Snapshots2.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
+
+Boogie program verifier finished with 1 verified, 0 errors
+
+Boogie program verifier finished with 1 verified, 0 errors
+
+Boogie program verifier finished with 1 verified, 0 errors
+
+Boogie program verifier finished with 1 verified, 0 errors
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/snapshots/Snapshots1.v0.bpl b/Test/snapshots/Snapshots1.v0.bpl
new file mode 100644
index 00000000..d6d4332e
--- /dev/null
+++ b/Test/snapshots/Snapshots1.v0.bpl
@@ -0,0 +1,14 @@
+procedure {:checksum "P1$proc#0"} P1();
+// Action: verify
+implementation {:checksum "P1$impl#0"} P1()
+{
+    call P2();
+}
+
+
+procedure {:checksum "P2$proc#0"} P2();
+// Action: verify
+implementation {:checksum "P2$impl#0"} P2()
+{
+    assert 1 != 1;
+}
diff --git a/Test/snapshots/Snapshots1.v1.bpl b/Test/snapshots/Snapshots1.v1.bpl
new file mode 100644
index 00000000..c0014a03
--- /dev/null
+++ b/Test/snapshots/Snapshots1.v1.bpl
@@ -0,0 +1,14 @@
+procedure {:checksum "P1$proc#0"} P1();
+// Action: skip
+implementation {:checksum "P1$impl#0"} P1()
+{
+    call P2();
+}
+
+
+procedure {:checksum "P2$proc#0"} P2();
+// Action: verify
+implementation {:checksum "P2$impl#1"} P2()
+{
+    assert 2 != 2;
+}
diff --git a/Test/snapshots/Snapshots1.v2.bpl b/Test/snapshots/Snapshots1.v2.bpl
new file mode 100644
index 00000000..49e8b389
--- /dev/null
+++ b/Test/snapshots/Snapshots1.v2.bpl
@@ -0,0 +1,15 @@
+procedure {:checksum "P1$proc#0"} P1();
+// Action: verify
+implementation {:checksum "P1$impl#0"} P1()
+{
+    call P2();
+}
+
+
+procedure {:checksum "P2$proc#1"} P2();
+  requires false;
+// Action: verify
+implementation {:checksum "P2$impl#1"} P2()
+{
+    assert 2 != 2;
+}
diff --git a/Test/snapshots/Snapshots2.v0.bpl b/Test/snapshots/Snapshots2.v0.bpl
new file mode 100644
index 00000000..63f1995d
--- /dev/null
+++ b/Test/snapshots/Snapshots2.v0.bpl
@@ -0,0 +1,12 @@
+procedure {:checksum "P0$proc#0"} P0();
+// Action: verify
+implementation {:checksum "P0$impl#0"} P0()
+{
+    call P0();
+}
+
+
+function F0() : bool
+{
+    true
+}
diff --git a/Test/snapshots/Snapshots2.v1.bpl b/Test/snapshots/Snapshots2.v1.bpl
new file mode 100644
index 00000000..a00bdecb
--- /dev/null
+++ b/Test/snapshots/Snapshots2.v1.bpl
@@ -0,0 +1,12 @@
+procedure {:checksum "P0$proc#0"} P0();
+// Action: skip
+implementation {:checksum "P0$impl#0"} P0()
+{
+    call P0();
+}
+
+
+function F0() : bool
+{
+    true
+}
diff --git a/Test/snapshots/Snapshots2.v2.bpl b/Test/snapshots/Snapshots2.v2.bpl
new file mode 100644
index 00000000..02c5e6df
--- /dev/null
+++ b/Test/snapshots/Snapshots2.v2.bpl
@@ -0,0 +1,13 @@
+procedure {:checksum "P0$proc#2"} P0();
+requires F0();
+// Action: verify (procedure changed)
+implementation {:checksum "P0$impl#0"} P0()
+{
+    call P0();
+}
+
+
+function {:checksum "F0#0"} F0() : bool
+{
+    true
+}
diff --git a/Test/snapshots/Snapshots2.v3.bpl b/Test/snapshots/Snapshots2.v3.bpl
new file mode 100644
index 00000000..5bf59435
--- /dev/null
+++ b/Test/snapshots/Snapshots2.v3.bpl
@@ -0,0 +1,13 @@
+procedure {:checksum "P0$proc#2"} P0();
+requires F0();
+// Action: verify (function changed)
+implementation {:checksum "P0$impl#0"} P0()
+{
+    call P0();
+}
+
+
+function {:checksum "F0#1"} F0() : bool
+{
+    false
+}
diff --git a/Test/snapshots/Snapshots2.v4.bpl b/Test/snapshots/Snapshots2.v4.bpl
new file mode 100644
index 00000000..3d11ee27
--- /dev/null
+++ b/Test/snapshots/Snapshots2.v4.bpl
@@ -0,0 +1,13 @@
+procedure {:checksum "P0$proc#2"} P0();
+requires F0();
+// Action: skip
+implementation {:checksum "P0$impl#0"} P0()
+{
+    call P0();
+}
+
+
+function {:checksum "F0#1"} F0() : bool
+{
+    false
+}
diff --git a/Test/snapshots/Snapshots2.v5.bpl b/Test/snapshots/Snapshots2.v5.bpl
new file mode 100644
index 00000000..5ff7bb4d
--- /dev/null
+++ b/Test/snapshots/Snapshots2.v5.bpl
@@ -0,0 +1,14 @@
+procedure {:checksum "P0$proc#5"} P0();
+requires F0();
+ensures F0();
+// Action: verify (procedure changed)
+implementation {:checksum "P0$impl#0"} P0()
+{
+    call P0();
+}
+
+
+function {:checksum "F0#1"} F0() : bool
+{
+    false
+}
diff --git a/Test/snapshots/runtest.bat b/Test/snapshots/runtest.bat
index 05421b85..fa45d56a 100644
--- a/Test/snapshots/runtest.bat
+++ b/Test/snapshots/runtest.bat
@@ -1,7 +1,17 @@
+
 @echo off
 setlocal
 
 set BOOGIEDIR=..\..\Binaries
 set BGEXE=%BOOGIEDIR%\Boogie.exe
 
+echo -------------------- Snapshots0.bpl --------------------
 %BGEXE% %* /verifySnapshots Snapshots0.bpl
+
+echo.
+echo -------------------- Snapshots1.bpl --------------------
+%BGEXE% %* /verifySnapshots Snapshots1.bpl
+
+echo.
+echo -------------------- Snapshots2.bpl --------------------
+%BGEXE% %* /verifySnapshots Snapshots2.bpl