Fixed issue in the verification result caching.

1 files changed, 14 insertions, 0 deletions

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;