Fixed issue involving axioms in the dependency analysis used for verification result caching.

1 files changed, 15 insertions, 0 deletions

diff --git a/Test/snapshots/Snapshots16.v1.bpl b/Test/snapshots/Snapshots16.v1.bpl
new file mode 100644
index 00000000..4d7cc354
--- /dev/null
+++ b/Test/snapshots/Snapshots16.v1.bpl
@@ -0,0 +1,15 @@
+function {:checksum "4"} PlusOne(n: int) : int

+{

+    n + 2

+}

+

+function {:checksum "0"} F(n: int) : int;

+

+axiom (forall n: int :: { F(n) } F(n) == PlusOne(n));

+

+procedure {:checksum "2"} M();

+

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

+{

+    assert F(0) == 1;  // error

+}