Did some refactoring, fixed minor issues, and made it apply the more advanced verification result caching even for implementations with errors.

1 files changed, 11 insertions, 0 deletions

diff --git a/Test/snapshots/Snapshots19.v1.bpl b/Test/snapshots/Snapshots19.v1.bpl
new file mode 100644
index 00000000..2afdd641
--- /dev/null
+++ b/Test/snapshots/Snapshots19.v1.bpl
@@ -0,0 +1,11 @@
+procedure {:checksum "0"} M();

+

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

+{

+    call N();

+

+    assert 1 != 1;

+}

+

+procedure {:checksum "3"} N();

+  requires 2 == 2;