98 files changed, 2458 insertions, 1975 deletions
diff --git a/Test/snapshots/Snapshots0.v0.bpl b/Test/snapshots/Snapshots0.v0.bpl
index c75e9520..68143cdf 100644
--- a/Test/snapshots/Snapshots0.v0.bpl
+++ b/Test/snapshots/Snapshots0.v0.bpl
@@ -1,42 +1,42 @@
-// id = "P1:0"
-// priority = 3
-// checksum = "123"
-// 
-// Action: verify
-procedure {:priority 3} {:checksum "123"} P1()
-{
-    assert false;
-}
-
-
-// id = "P2:0"
-// priority = 3
-// checksum = null
-//
-// Action: verify
-procedure {:priority 3} P2()
-{
-    assert false;
-}
-
-
-// id = "P3:0"
-// priority = 1
-// checksum = null
-//
-// Action: verify
-procedure P3()
-{
-    assert false;
-}
-
-
-// id = "P0:1"
-// priority = 5
-// checksum = "012"
-//
-// Action: verify
-procedure {:id "P0:1"} {:priority 5} {:checksum "012"} P0()
-{
-    assert false;
-}
+// id = "P1:0"
+// priority = 3
+// checksum = "123"
+// 
+// Action: verify
+procedure {:priority 3} {:checksum "123"} P1()
+{
+    assert false;
+}
+
+
+// id = "P2:0"
+// priority = 3
+// checksum = null
+//
+// Action: verify
+procedure {:priority 3} P2()
+{
+    assert false;
+}
+
+
+// id = "P3:0"
+// priority = 1
+// checksum = null
+//
+// Action: verify
+procedure P3()
+{
+    assert false;
+}
+
+
+// id = "P0:1"
+// priority = 5
+// checksum = "012"
+//
+// Action: verify
+procedure {:id "P0:1"} {:priority 5} {:checksum "012"} P0()
+{
+    assert false;
+}
diff --git a/Test/snapshots/Snapshots0.v1.bpl b/Test/snapshots/Snapshots0.v1.bpl
index efd30c8f..2be6ec1c 100644
--- a/Test/snapshots/Snapshots0.v1.bpl
+++ b/Test/snapshots/Snapshots0.v1.bpl
@@ -1,42 +1,42 @@
-// id = "P0:1"
-// priority = 5
-// checksum = "012"
-//
-// Action: skip
-procedure {:id "P0:1"} {:priority 5} {:checksum "012"} P0()
-{
-    assert false;
-}
-
-
-// id = "P1:0"
-// priority = 5
-// checksum = "234"
-//
-// Action: verify (unknown checksum)
-procedure {:priority 5} {:checksum "234"} P1()
-{
-    assert true;
-}
-
-
-// id = "P2:0"
-// priority = 3
-// checksum = null
-//
-// Action: verify (no checksum)
-procedure {:priority 3} P2()
-{
-    assert false;
-}
-
-
-// id = "P3:0"
-// priority = 1
-// checksum = "234"
-//
-// Action: verify (unknown checksum)
-procedure {:checksum "234"} P3()
-{
-    assert true;
-}
+// id = "P0:1"
+// priority = 5
+// checksum = "012"
+//
+// Action: skip
+procedure {:id "P0:1"} {:priority 5} {:checksum "012"} P0()
+{
+    assert false;
+}
+
+
+// id = "P1:0"
+// priority = 5
+// checksum = "234"
+//
+// Action: verify (unknown checksum)
+procedure {:priority 5} {:checksum "234"} P1()
+{
+    assert true;
+}
+
+
+// id = "P2:0"
+// priority = 3
+// checksum = null
+//
+// Action: verify (no checksum)
+procedure {:priority 3} P2()
+{
+    assert false;
+}
+
+
+// id = "P3:0"
+// priority = 1
+// checksum = "234"
+//
+// Action: verify (unknown checksum)
+procedure {:checksum "234"} P3()
+{
+    assert true;
+}
diff --git a/Test/snapshots/Snapshots0.v2.bpl b/Test/snapshots/Snapshots0.v2.bpl
index 156977f7..8c7efe24 100644
--- a/Test/snapshots/Snapshots0.v2.bpl
+++ b/Test/snapshots/Snapshots0.v2.bpl
@@ -1,31 +1,31 @@
-// id = "P0:1"
-// priority = 5
-// checksum = "012"
-//
-// Action: skip
-procedure {:id "P0:1"} {:priority 5} {:checksum "012"} P0()
-{
-    assert false;
-}
-
-
-// id = "P1:0"
-// priority = 1
-// checksum = "234"
-//
-// Action: skip
-procedure {:priority 1} {:checksum "234"} P1()
-{
-    assert true;
-}
-
-
-// id = "P3:0"
-// priority = 1
-// checksum = "234"
-//
-// Action: skip
-procedure {:checksum "234"} P3()
-{
-    assert true;
-}
+// id = "P0:1"
+// priority = 5
+// checksum = "012"
+//
+// Action: skip
+procedure {:id "P0:1"} {:priority 5} {:checksum "012"} P0()
+{
+    assert false;
+}
+
+
+// id = "P1:0"
+// priority = 1
+// checksum = "234"
+//
+// Action: skip
+procedure {:priority 1} {:checksum "234"} P1()
+{
+    assert true;
+}
+
+
+// id = "P3:0"
+// priority = 1
+// checksum = "234"
+//
+// Action: skip
+procedure {:checksum "234"} P3()
+{
+    assert true;
+}
diff --git a/Test/snapshots/Snapshots1.v0.bpl b/Test/snapshots/Snapshots1.v0.bpl
index ea2c06bb..749db7af 100644
--- a/Test/snapshots/Snapshots1.v0.bpl
+++ b/Test/snapshots/Snapshots1.v0.bpl
@@ -1,14 +1,14 @@
-procedure {:checksum "P1$proc#0"} P1();
-// Action: verify
-implementation {:id "P1"} {:checksum "P1$impl#0"} P1()
-{
-    call P2();
-}
-
-
-procedure {:checksum "P2$proc#0"} P2();
-// Action: verify
-implementation {:id "P2"} {:checksum "P2$impl#0"} P2()
-{
-    assert 1 != 1;
-}
+procedure {:checksum "P1$proc#0"} P1();
+// Action: verify
+implementation {:id "P1"} {:checksum "P1$impl#0"} P1()
+{
+    call P2();
+}
+
+
+procedure {:checksum "P2$proc#0"} P2();
+// Action: verify
+implementation {:id "P2"} {:checksum "P2$impl#0"} P2()
+{
+    assert 1 != 1;
+}
diff --git a/Test/snapshots/Snapshots1.v1.bpl b/Test/snapshots/Snapshots1.v1.bpl
index 9fbe44af..9dc8b779 100644
--- a/Test/snapshots/Snapshots1.v1.bpl
+++ b/Test/snapshots/Snapshots1.v1.bpl
@@ -1,14 +1,14 @@
-procedure {:checksum "P1$proc#0"} P1();
-// Action: skip
-implementation {:id "P1"} {:checksum "P1$impl#0"} P1()
-{
-    call P2();
-}
-
-
-procedure {:checksum "P2$proc#0"} P2();
-// Action: verify
-implementation {:id "P2"} {:checksum "P2$impl#1"} P2()
-{
-    assert 2 != 2;
-}
+procedure {:checksum "P1$proc#0"} P1();
+// Action: skip
+implementation {:id "P1"} {:checksum "P1$impl#0"} P1()
+{
+    call P2();
+}
+
+
+procedure {:checksum "P2$proc#0"} P2();
+// Action: verify
+implementation {:id "P2"} {:checksum "P2$impl#1"} P2()
+{
+    assert 2 != 2;
+}
diff --git a/Test/snapshots/Snapshots1.v2.bpl b/Test/snapshots/Snapshots1.v2.bpl
index c699631e..9d399207 100644
--- a/Test/snapshots/Snapshots1.v2.bpl
+++ b/Test/snapshots/Snapshots1.v2.bpl
@@ -1,15 +1,15 @@
-procedure {:checksum "P1$proc#0"} P1();
-// Action: verify
-implementation {:id "P1"} {:checksum "P1$impl#0"} P1()
-{
-    call P2();
-}
-
-
-procedure {:checksum "P2$proc#1"} P2();
-  requires false;
-// Action: verify
-implementation {:id "P2"} {:checksum "P2$impl#1"} P2()
-{
-    assert 2 != 2;
-}
+procedure {:checksum "P1$proc#0"} P1();
+// Action: verify
+implementation {:id "P1"} {:checksum "P1$impl#0"} P1()
+{
+    call P2();
+}
+
+
+procedure {:checksum "P2$proc#1"} P2();
+  requires false;
+// Action: verify
+implementation {:id "P2"} {:checksum "P2$impl#1"} P2()
+{
+    assert 2 != 2;
+}
diff --git a/Test/snapshots/Snapshots10.v0.bpl b/Test/snapshots/Snapshots10.v0.bpl
index bdbb6b63..80471302 100644
--- a/Test/snapshots/Snapshots10.v0.bpl
+++ b/Test/snapshots/Snapshots10.v0.bpl
@@ -1,20 +1,20 @@
-procedure {:checksum "0"} M(n: int);
-  requires 0 < n;
-
-implementation {:id "M"} {:checksum "1"} M(n: int)
-{
-    var x: int;
-
-    call x := N(n);
-
-    call O();
-
-    assert 0 <= x;
-}
-
-procedure {:checksum "2"} N(n: int) returns (r: int);
-  requires 0 < n;
-  ensures 0 < r;
-
-procedure {:checksum "3"} O();
-  ensures true;
+procedure {:checksum "0"} M(n: int);
+  requires 0 < n;
+
+implementation {:id "M"} {:checksum "1"} M(n: int)
+{
+    var x: int;
+
+    call x := N(n);
+
+    call O();
+
+    assert 0 <= x;
+}
+
+procedure {:checksum "2"} N(n: int) returns (r: int);
+  requires 0 < n;
+  ensures 0 < r;
+
+procedure {:checksum "3"} O();
+  ensures true;
diff --git a/Test/snapshots/Snapshots10.v1.bpl b/Test/snapshots/Snapshots10.v1.bpl
index d4c09a5f..afc47e4c 100644
--- a/Test/snapshots/Snapshots10.v1.bpl
+++ b/Test/snapshots/Snapshots10.v1.bpl
@@ -1,21 +1,21 @@
-procedure {:checksum "0"} M(n: int);
-  requires 0 < n;
-
-implementation {:id "M"} {:checksum "1"} M(n: int)
-{
-    var x: int;
-
-    call x := N(n);
-
-    call O();
-
-    assert 0 <= x;
-}
-
-procedure {:checksum "4"} N(n: int) returns (r: int);
-  requires 0 < n;
-  // Change: stronger postcondition
-  ensures 42 < r;
-
-procedure {:checksum "3"} O();
-  ensures true;
+procedure {:checksum "0"} M(n: int);
+  requires 0 < n;
+
+implementation {:id "M"} {:checksum "1"} M(n: int)
+{
+    var x: int;
+
+    call x := N(n);
+
+    call O();
+
+    assert 0 <= x;
+}
+
+procedure {:checksum "4"} N(n: int) returns (r: int);
+  requires 0 < n;
+  // Change: stronger postcondition
+  ensures 42 < r;
+
+procedure {:checksum "3"} O();
+  ensures true;
diff --git a/Test/snapshots/Snapshots11.v0.bpl b/Test/snapshots/Snapshots11.v0.bpl
index 10b4ed43..89634552 100644
--- a/Test/snapshots/Snapshots11.v0.bpl
+++ b/Test/snapshots/Snapshots11.v0.bpl
@@ -1,14 +1,14 @@
-procedure {:checksum "0"} M(n: int);
-
-implementation {:id "M"} {:checksum "1"} M(n: int)
-{
-    var x: int;
-
-    call x := N(n);
-
-    assert 0 <= x;
-}
-
-procedure {:checksum "2"} N(n: int) returns (r: int);
-  requires 0 < n;
-  ensures 0 < r;
+procedure {:checksum "0"} M(n: int);
+
+implementation {:id "M"} {:checksum "1"} M(n: int)
+{
+    var x: int;
+
+    call x := N(n);
+
+    assert 0 <= x;
+}
+
+procedure {:checksum "2"} N(n: int) returns (r: int);
+  requires 0 < n;
+  ensures 0 < r;
diff --git a/Test/snapshots/Snapshots11.v1.bpl b/Test/snapshots/Snapshots11.v1.bpl
index 3c3ea476..a6e6c64a 100644
--- a/Test/snapshots/Snapshots11.v1.bpl
+++ b/Test/snapshots/Snapshots11.v1.bpl
@@ -1,15 +1,15 @@
-procedure {:checksum "0"} M(n: int);
-
-implementation {:id "M"} {:checksum "1"} M(n: int)
-{
-    var x: int;
-
-    call x := N(n);
-
-    assert 0 <= x;
-}
-
-procedure {:checksum "3"} N(n: int) returns (r: int);
-  requires 0 < n;
-  // Change: weaker postcondition
-  ensures 0 <= r;
+procedure {:checksum "0"} M(n: int);
+
+implementation {:id "M"} {:checksum "1"} M(n: int)
+{
+    var x: int;
+
+    call x := N(n);
+
+    assert 0 <= x;
+}
+
+procedure {:checksum "3"} N(n: int) returns (r: int);
+  requires 0 < n;
+  // Change: weaker postcondition
+  ensures 0 <= r;
diff --git a/Test/snapshots/Snapshots12.v0.bpl b/Test/snapshots/Snapshots12.v0.bpl
index da219bfd..56205ec8 100644
--- a/Test/snapshots/Snapshots12.v0.bpl
+++ b/Test/snapshots/Snapshots12.v0.bpl
@@ -1,16 +1,16 @@
-procedure {:checksum "0"} M();
-
-implementation {:id "M"} {:checksum "1"} M()
-{
-    call N();
-
-    assert false;
-}
-
-procedure {:checksum "2"} N();
-  ensures F();
-
-function {:checksum "3"} F() : bool
-{
-    false
-}
+procedure {:checksum "0"} M();
+
+implementation {:id "M"} {:checksum "1"} M()
+{
+    call N();
+
+    assert false;
+}
+
+procedure {:checksum "2"} N();
+  ensures F();
+
+function {:checksum "3"} F() : bool
+{
+    false
+}
diff --git a/Test/snapshots/Snapshots12.v1.bpl b/Test/snapshots/Snapshots12.v1.bpl
index f71e3c5f..d3747c5f 100644
--- a/Test/snapshots/Snapshots12.v1.bpl
+++ b/Test/snapshots/Snapshots12.v1.bpl
@@ -1,16 +1,16 @@
-procedure {:checksum "0"} M();
-
-implementation {:id "M"} {:checksum "1"} M()
-{
-    call N();
-
-    assert false;
-}
-
-procedure {:checksum "2"} N();
-  ensures F();
-
-function {:checksum "4"} F() : bool
-{
-    true
-}
+procedure {:checksum "0"} M();
+
+implementation {:id "M"} {:checksum "1"} M()
+{
+    call N();
+
+    assert false;
+}
+
+procedure {:checksum "2"} N();
+  ensures F();
+
+function {:checksum "4"} F() : bool
+{
+    true
+}
diff --git a/Test/snapshots/Snapshots13.v0.bpl b/Test/snapshots/Snapshots13.v0.bpl
index 79dfe2c3..e4f80c70 100644
--- a/Test/snapshots/Snapshots13.v0.bpl
+++ b/Test/snapshots/Snapshots13.v0.bpl
@@ -1,21 +1,21 @@
-procedure {:checksum "0"} M();
-
-implementation {:id "M"} {:checksum "1"} M()
-{
-    call N();
-
-    assert false;
-}
-
-procedure {:checksum "2"} N();
-  ensures F() && G();
-
-function {:checksum "3"} F() : bool
-{
-    true
-}
-
-function {:checksum "4"} G() : bool
-{
-    false
-}
+procedure {:checksum "0"} M();
+
+implementation {:id "M"} {:checksum "1"} M()
+{
+    call N();
+
+    assert false;
+}
+
+procedure {:checksum "2"} N();
+  ensures F() && G();
+
+function {:checksum "3"} F() : bool
+{
+    true
+}
+
+function {:checksum "4"} G() : bool
+{
+    false
+}
diff --git a/Test/snapshots/Snapshots13.v1.bpl b/Test/snapshots/Snapshots13.v1.bpl
index a7ec6bfb..4c74d06e 100644
--- a/Test/snapshots/Snapshots13.v1.bpl
+++ b/Test/snapshots/Snapshots13.v1.bpl
@@ -1,16 +1,16 @@
-procedure {:checksum "0"} M();
-
-implementation {:id "M"} {:checksum "1"} M()
-{
-    call N();
-
-    assert false;
-}
-
-procedure {:checksum "2"} N();
-  ensures F();
-
-function {:checksum "3"} F() : bool
-{
-    true
-}
+procedure {:checksum "0"} M();
+
+implementation {:id "M"} {:checksum "1"} M()
+{
+    call N();
+
+    assert false;
+}
+
+procedure {:checksum "2"} N();
+  ensures F();
+
+function {:checksum "3"} F() : bool
+{
+    true
+}
diff --git a/Test/snapshots/Snapshots14.v0.bpl b/Test/snapshots/Snapshots14.v0.bpl
index 79dfe2c3..e4f80c70 100644
--- a/Test/snapshots/Snapshots14.v0.bpl
+++ b/Test/snapshots/Snapshots14.v0.bpl
@@ -1,21 +1,21 @@
-procedure {:checksum "0"} M();
-
-implementation {:id "M"} {:checksum "1"} M()
-{
-    call N();
-
-    assert false;
-}
-
-procedure {:checksum "2"} N();
-  ensures F() && G();
-
-function {:checksum "3"} F() : bool
-{
-    true
-}
-
-function {:checksum "4"} G() : bool
-{
-    false
-}
+procedure {:checksum "0"} M();
+
+implementation {:id "M"} {:checksum "1"} M()
+{
+    call N();
+
+    assert false;
+}
+
+procedure {:checksum "2"} N();
+  ensures F() && G();
+
+function {:checksum "3"} F() : bool
+{
+    true
+}
+
+function {:checksum "4"} G() : bool
+{
+    false
+}
diff --git a/Test/snapshots/Snapshots14.v1.bpl b/Test/snapshots/Snapshots14.v1.bpl
index b33c3430..b8c6c061 100644
--- a/Test/snapshots/Snapshots14.v1.bpl
+++ b/Test/snapshots/Snapshots14.v1.bpl
@@ -1,21 +1,21 @@
-procedure {:checksum "0"} M();
-
-implementation {:id "M"} {:checksum "1"} M()
-{
-    call N();
-
-    assert false;
-}
-
-procedure {:checksum "2"} N();
-  ensures F();
-
-function {:checksum "3"} F() : bool
-{
-    true
-}
-
-function {:checksum "4"} G() : bool
-{
-    false
-}
+procedure {:checksum "0"} M();
+
+implementation {:id "M"} {:checksum "1"} M()
+{
+    call N();
+
+    assert false;
+}
+
+procedure {:checksum "2"} N();
+  ensures F();
+
+function {:checksum "3"} F() : bool
+{
+    true
+}
+
+function {:checksum "4"} G() : bool
+{
+    false
+}
diff --git a/Test/snapshots/Snapshots15.v0.bpl b/Test/snapshots/Snapshots15.v0.bpl
index a947157d..e3dfb3f3 100644
--- a/Test/snapshots/Snapshots15.v0.bpl
+++ b/Test/snapshots/Snapshots15.v0.bpl
@@ -1,17 +1,17 @@
-procedure {:checksum "0"} M();
-
-implementation {:id "M"} {:checksum "1"} M()
-{
-    assert true;
-
-    call N();
-
-    assert true;
-
-    call N();
-
-    assert false;
-}
-
-procedure {:checksum "2"} N();
-  ensures false;
+procedure {:checksum "0"} M();
+
+implementation {:id "M"} {:checksum "1"} M()
+{
+    assert true;
+
+    call N();
+
+    assert true;
+
+    call N();
+
+    assert false;
+}
+
+procedure {:checksum "2"} N();
+  ensures false;
diff --git a/Test/snapshots/Snapshots15.v1.bpl b/Test/snapshots/Snapshots15.v1.bpl
index a797ab6c..94c3ec4d 100644
--- a/Test/snapshots/Snapshots15.v1.bpl
+++ b/Test/snapshots/Snapshots15.v1.bpl
@@ -1,17 +1,17 @@
-procedure {:checksum "0"} M();
-
-implementation {:id "M"} {:checksum "1"} M()
-{
-    assert true;
-
-    call N();
-
-    assert true;
-
-    call N();
-
-    assert false;
-}
-
-procedure {:checksum "3"} N();
-  ensures true;
+procedure {:checksum "0"} M();
+
+implementation {:id "M"} {:checksum "1"} M()
+{
+    assert true;
+
+    call N();
+
+    assert true;
+
+    call N();
+
+    assert false;
+}
+
+procedure {:checksum "3"} N();
+  ensures true;
diff --git a/Test/snapshots/Snapshots16.v0.bpl b/Test/snapshots/Snapshots16.v0.bpl
index 45cb4a76..3ab51400 100644
--- a/Test/snapshots/Snapshots16.v0.bpl
+++ b/Test/snapshots/Snapshots16.v0.bpl
@@ -1,15 +1,15 @@
-function {:checksum "1"} PlusOne(n: int) : int
-{
-    n + 1
-}
-
-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;
-}
+function {:checksum "1"} PlusOne(n: int) : int
+{
+    n + 1
+}
+
+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;
+}
diff --git a/Test/snapshots/Snapshots16.v1.bpl b/Test/snapshots/Snapshots16.v1.bpl
index 4d7cc354..ab6a8ace 100644
--- a/Test/snapshots/Snapshots16.v1.bpl
+++ b/Test/snapshots/Snapshots16.v1.bpl
@@ -1,15 +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
-}
+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
+}
diff --git a/Test/snapshots/Snapshots17.v0.bpl b/Test/snapshots/Snapshots17.v0.bpl
index 58ef53e7..55992c79 100644
--- a/Test/snapshots/Snapshots17.v0.bpl
+++ b/Test/snapshots/Snapshots17.v0.bpl
@@ -1,32 +1,32 @@
-procedure {:checksum "0"} M();
-
-implementation {:id "M"} {:checksum "1"} M()
-{
-    var x: int;
-
-    x := 0;
-    while (*)
-    {
-        while (*)
-        {
-            assert true;
-
-            call N();
-
-            call N();
-
-            x := x + 1;
-
-            assert x == 1;
-        }
-
-        call N();
-
-        assert false;
-    }
-
-    assert true;
-}
-
-procedure {:checksum "2"} N();
-  ensures false;
+procedure {:checksum "0"} M();
+
+implementation {:id "M"} {:checksum "1"} M()
+{
+    var x: int;
+
+    x := 0;
+    while (*)
+    {
+        while (*)
+        {
+            assert true;
+
+            call N();
+
+            call N();
+
+            x := x + 1;
+
+            assert x == 1;
+        }
+
+        call N();
+
+        assert false;
+    }
+
+    assert true;
+}
+
+procedure {:checksum "2"} N();
+  ensures false;
diff --git a/Test/snapshots/Snapshots17.v1.bpl b/Test/snapshots/Snapshots17.v1.bpl
index 4d22ab3d..66d0341a 100644
--- a/Test/snapshots/Snapshots17.v1.bpl
+++ b/Test/snapshots/Snapshots17.v1.bpl
@@ -1,32 +1,32 @@
-procedure {:checksum "0"} M();
-
-implementation {:id "M"} {:checksum "1"} M()
-{
-    var x: int;
-
-    x := 0;
-    while (*)
-    {
-        while (*)
-        {
-            assert true;
-
-            call N();
-
-            call N();
-
-            x := x + 1;
-
-            assert x == 1;  // error
-        }
-
-        call N();
-
-        assert false;  // error
-    }
-
-    assert true;
-}
-
-procedure {:checksum "3"} N();
-  ensures true;
+procedure {:checksum "0"} M();
+
+implementation {:id "M"} {:checksum "1"} M()
+{
+    var x: int;
+
+    x := 0;
+    while (*)
+    {
+        while (*)
+        {
+            assert true;
+
+            call N();
+
+            call N();
+
+            x := x + 1;
+
+            assert x == 1;  // error
+        }
+
+        call N();
+
+        assert false;  // error
+    }
+
+    assert true;
+}
+
+procedure {:checksum "3"} N();
+  ensures true;
diff --git a/Test/snapshots/Snapshots18.v0.bpl b/Test/snapshots/Snapshots18.v0.bpl
index d37d9546..750c6891 100644
--- a/Test/snapshots/Snapshots18.v0.bpl
+++ b/Test/snapshots/Snapshots18.v0.bpl
@@ -1,24 +1,24 @@
-procedure {:checksum "0"} M();
-
-implementation {:id "M"} {:checksum "1"} M()
-{
-    while (true)
-    {
-        assert 0 == 0;
-        
-        call N();
-        call N();
-
-        if (*)
-        {
-            break;
-        }
-
-        assert 1 != 1;
-    }
-
-    assert 2 != 2;
-}
-
-procedure {:checksum "2"} N();
-  ensures false;
+procedure {:checksum "0"} M();
+
+implementation {:id "M"} {:checksum "1"} M()
+{
+    while (true)
+    {
+        assert 0 == 0;
+        
+        call N();
+        call N();
+
+        if (*)
+        {
+            break;
+        }
+
+        assert 1 != 1;
+    }
+
+    assert 2 != 2;
+}
+
+procedure {:checksum "2"} N();
+  ensures false;
diff --git a/Test/snapshots/Snapshots18.v1.bpl b/Test/snapshots/Snapshots18.v1.bpl
index 76f8c597..262b5e4f 100644
--- a/Test/snapshots/Snapshots18.v1.bpl
+++ b/Test/snapshots/Snapshots18.v1.bpl
@@ -1,24 +1,24 @@
-procedure {:checksum "0"} M();
-
-implementation {:id "M"} {:checksum "1"} M()
-{
-    while (true)
-    {
-        assert 0 == 0;
-        
-        call N();
-        call N();
-
-        if (*)
-        {
-            break;
-        }
-
-        assert 1 != 1;  // error
-    }
-
-    assert 2 != 2;  // error
-}
-
-procedure {:checksum "3"} N();
-  ensures true;
+procedure {:checksum "0"} M();
+
+implementation {:id "M"} {:checksum "1"} M()
+{
+    while (true)
+    {
+        assert 0 == 0;
+        
+        call N();
+        call N();
+
+        if (*)
+        {
+            break;
+        }
+
+        assert 1 != 1;  // error
+    }
+
+    assert 2 != 2;  // error
+}
+
+procedure {:checksum "3"} N();
+  ensures true;
diff --git a/Test/snapshots/Snapshots19.v0.bpl b/Test/snapshots/Snapshots19.v0.bpl
index 935ee793..fb8f4524 100644
--- a/Test/snapshots/Snapshots19.v0.bpl
+++ b/Test/snapshots/Snapshots19.v0.bpl
@@ -1,11 +1,11 @@
-procedure {:checksum "0"} M();
-
-implementation {:id "M"} {:checksum "1"} M()
-{
-    call N();
-
-    assert 1 != 1;
-}
-
-procedure {:checksum "2"} N();
-  requires 2 == 2;
+procedure {:checksum "0"} M();
+
+implementation {:id "M"} {:checksum "1"} M()
+{
+    call N();
+
+    assert 1 != 1;
+}
+
+procedure {:checksum "2"} N();
+  requires 2 == 2;
diff --git a/Test/snapshots/Snapshots19.v1.bpl b/Test/snapshots/Snapshots19.v1.bpl
index 2afdd641..9e959b68 100644
--- a/Test/snapshots/Snapshots19.v1.bpl
+++ b/Test/snapshots/Snapshots19.v1.bpl
@@ -1,11 +1,11 @@
-procedure {:checksum "0"} M();
-
-implementation {:id "M"} {:checksum "1"} M()
-{
-    call N();
-
-    assert 1 != 1;
-}
-
-procedure {:checksum "3"} N();
-  requires 2 == 2;
+procedure {:checksum "0"} M();
+
+implementation {:id "M"} {:checksum "1"} M()
+{
+    call N();
+
+    assert 1 != 1;
+}
+
+procedure {:checksum "3"} N();
+  requires 2 == 2;
diff --git a/Test/snapshots/Snapshots2.v0.bpl b/Test/snapshots/Snapshots2.v0.bpl
index 91f05a0d..061f2c6c 100644
--- a/Test/snapshots/Snapshots2.v0.bpl
+++ b/Test/snapshots/Snapshots2.v0.bpl
@@ -1,12 +1,12 @@
-procedure {:checksum "P0$proc#0"} P0();
-// Action: verify
-implementation {:id "P0"} {:checksum "P0$impl#0"} P0()
-{
-    call P0();
-}
-
-
-function F0() : bool
-{
-    true
-}
+procedure {:checksum "P0$proc#0"} P0();
+// Action: verify
+implementation {:id "P0"} {: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
index 1dec4954..93c0e5d8 100644
--- a/Test/snapshots/Snapshots2.v1.bpl
+++ b/Test/snapshots/Snapshots2.v1.bpl
@@ -1,12 +1,12 @@
-procedure {:checksum "P0$proc#0"} P0();
-// Action: skip
-implementation {:id "P0"} {:checksum "P0$impl#0"} P0()
-{
-    call P0();
-}
-
-
-function F0() : bool
-{
-    true
-}
+procedure {:checksum "P0$proc#0"} P0();
+// Action: skip
+implementation {:id "P0"} {: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
index 567191d3..88865e75 100644
--- a/Test/snapshots/Snapshots2.v2.bpl
+++ b/Test/snapshots/Snapshots2.v2.bpl
@@ -1,13 +1,13 @@
-procedure {:checksum "P0$proc#2"} P0();
-requires F0();
-// Action: verify (procedure changed)
-implementation {:id "P0"} {:checksum "P0$impl#0"} P0()
-{
-    call P0();
-}
-
-
-function {:checksum "F0#0"} F0() : bool
-{
-    true
-}
+procedure {:checksum "P0$proc#2"} P0();
+requires F0();
+// Action: verify (procedure changed)
+implementation {:id "P0"} {: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
index 7f6c4a82..fd06e335 100644
--- a/Test/snapshots/Snapshots2.v3.bpl
+++ b/Test/snapshots/Snapshots2.v3.bpl
@@ -1,13 +1,13 @@
-procedure {:checksum "P0$proc#2"} P0();
-requires F0();
-// Action: verify (function changed)
-implementation {:id "P0"} {:checksum "P0$impl#0"} P0()
-{
-    call P0();
-}
-
-
-function {:checksum "F0#1"} F0() : bool
-{
-    false
-}
+procedure {:checksum "P0$proc#2"} P0();
+requires F0();
+// Action: verify (function changed)
+implementation {:id "P0"} {: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
index abbf5e86..eb183a1d 100644
--- a/Test/snapshots/Snapshots2.v4.bpl
+++ b/Test/snapshots/Snapshots2.v4.bpl
@@ -1,13 +1,13 @@
-procedure {:checksum "P0$proc#2"} P0();
-requires F0();
-// Action: skip
-implementation {:id "P0"} {:checksum "P0$impl#0"} P0()
-{
-    call P0();
-}
-
-
-function {:checksum "F0#1"} F0() : bool
-{
-    false
-}
+procedure {:checksum "P0$proc#2"} P0();
+requires F0();
+// Action: skip
+implementation {:id "P0"} {: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
index 55d08527..ea2904e9 100644
--- a/Test/snapshots/Snapshots2.v5.bpl
+++ b/Test/snapshots/Snapshots2.v5.bpl
@@ -1,14 +1,14 @@
-procedure {:checksum "P0$proc#5"} P0();
-requires F0();
-ensures F0();
-// Action: verify (procedure changed)
-implementation {:id "P0"} {:checksum "P0$impl#0"} P0()
-{
-    call P0();
-}
-
-
-function {:checksum "F0#1"} F0() : bool
-{
-    false
-}
+procedure {:checksum "P0$proc#5"} P0();
+requires F0();
+ensures F0();
+// Action: verify (procedure changed)
+implementation {:id "P0"} {:checksum "P0$impl#0"} P0()
+{
+    call P0();
+}
+
+
+function {:checksum "F0#1"} F0() : bool
+{
+    false
+}
diff --git a/Test/snapshots/Snapshots20.v0.bpl b/Test/snapshots/Snapshots20.v0.bpl
index 54934a05..d7544ec5 100644
--- a/Test/snapshots/Snapshots20.v0.bpl
+++ b/Test/snapshots/Snapshots20.v0.bpl
@@ -1,20 +1,20 @@
-procedure {:checksum "0"} M();
-
-implementation {:id "M"} {:checksum "1"} M()
-{
-    if (*)
-    {
-        call N();
-
-        assert 1 != 1;
-    }
-    else
-    {
-        assert 2 != 2;  // error
-    }
-
-    assert 3 != 3;
-}
-
-procedure {:checksum "2"} N();
-  ensures 0 != 0;
+procedure {:checksum "0"} M();
+
+implementation {:id "M"} {:checksum "1"} M()
+{
+    if (*)
+    {
+        call N();
+
+        assert 1 != 1;
+    }
+    else
+    {
+        assert 2 != 2;  // error
+    }
+
+    assert 3 != 3;
+}
+
+procedure {:checksum "2"} N();
+  ensures 0 != 0;
diff --git a/Test/snapshots/Snapshots20.v1.bpl b/Test/snapshots/Snapshots20.v1.bpl
index 04fd0a6e..7e4970e7 100644
--- a/Test/snapshots/Snapshots20.v1.bpl
+++ b/Test/snapshots/Snapshots20.v1.bpl
@@ -1,20 +1,20 @@
-procedure {:checksum "0"} M();
-
-implementation {:id "M"} {:checksum "1"} M()
-{
-    if (*)
-    {
-        call N();
-
-        assert 1 != 1;  // error
-    }
-    else
-    {
-        assert 2 != 2;  // error
-    }
-
-    assert 3 != 3;
-}
-
-procedure {:checksum "3"} N();
-  ensures 0 == 0;
+procedure {:checksum "0"} M();
+
+implementation {:id "M"} {:checksum "1"} M()
+{
+    if (*)
+    {
+        call N();
+
+        assert 1 != 1;  // error
+    }
+    else
+    {
+        assert 2 != 2;  // error
+    }
+
+    assert 3 != 3;
+}
+
+procedure {:checksum "3"} N();
+  ensures 0 == 0;
diff --git a/Test/snapshots/Snapshots21.v0.bpl b/Test/snapshots/Snapshots21.v0.bpl
index 4a4080f5..ef2c99eb 100644
--- a/Test/snapshots/Snapshots21.v0.bpl
+++ b/Test/snapshots/Snapshots21.v0.bpl
@@ -1,15 +1,15 @@
-procedure {:checksum "0"} M();
-
-implementation {:id "M"} {:checksum "1"} M()
-{
-    if (*)
-    {
-        assert 1 != 1;  // error
-    }
-    else
-    {
-        assert 2 != 2;  // error
-    }
-
-    assert 3 != 3;
-}
+procedure {:checksum "0"} M();
+
+implementation {:id "M"} {:checksum "1"} M()
+{
+    if (*)
+    {
+        assert 1 != 1;  // error
+    }
+    else
+    {
+        assert 2 != 2;  // error
+    }
+
+    assert 3 != 3;
+}
diff --git a/Test/snapshots/Snapshots21.v1.bpl b/Test/snapshots/Snapshots21.v1.bpl
index ef51e5ac..e1fec0ed 100644
--- a/Test/snapshots/Snapshots21.v1.bpl
+++ b/Test/snapshots/Snapshots21.v1.bpl
@@ -1,15 +1,15 @@
-procedure {:checksum "0"} M();
-
-implementation {:id "M"} {:checksum "2"} M()
-{
-    if (*)
-    {
-        assert 1 == 1;
-    }
-    else
-    {
-        assert 2 != 2;  // error
-    }
-
-    assert 3 != 3;  // error
-}
+procedure {:checksum "0"} M();
+
+implementation {:id "M"} {:checksum "2"} M()
+{
+    if (*)
+    {
+        assert 1 == 1;
+    }
+    else
+    {
+        assert 2 != 2;  // error
+    }
+
+    assert 3 != 3;  // error
+}
diff --git a/Test/snapshots/Snapshots22.v0.bpl b/Test/snapshots/Snapshots22.v0.bpl
index c2be13de..94968c33 100644
--- a/Test/snapshots/Snapshots22.v0.bpl
+++ b/Test/snapshots/Snapshots22.v0.bpl
@@ -1,15 +1,15 @@
-procedure {:checksum "0"} M();
-
-implementation {:id "M"} {:checksum "1"} M()
-{
-    if (*)
-    {
-        assert 1 != 1;  // error
-    }
-    else
-    {
-        assert 2 == 2;
-    }
-
-    assert 3 == 3;
-}
+procedure {:checksum "0"} M();
+
+implementation {:id "M"} {:checksum "1"} M()
+{
+    if (*)
+    {
+        assert 1 != 1;  // error
+    }
+    else
+    {
+        assert 2 == 2;
+    }
+
+    assert 3 == 3;
+}
diff --git a/Test/snapshots/Snapshots22.v1.bpl b/Test/snapshots/Snapshots22.v1.bpl
index 9d43f2c2..78b5da9a 100644
--- a/Test/snapshots/Snapshots22.v1.bpl
+++ b/Test/snapshots/Snapshots22.v1.bpl
@@ -1,15 +1,15 @@
-procedure {:checksum "0"} M();
-
-implementation {:id "M"} {:checksum "2"} M()
-{
-    if (*)
-    {
-        assert 1 == 1;
-    }
-    else
-    {
-        assert 2 == 2;
-    }
-
-    assert 3 == 3;
-}
+procedure {:checksum "0"} M();
+
+implementation {:id "M"} {:checksum "2"} M()
+{
+    if (*)
+    {
+        assert 1 == 1;
+    }
+    else
+    {
+        assert 2 == 2;
+    }
+
+    assert 3 == 3;
+}
diff --git a/Test/snapshots/Snapshots23.v0.bpl b/Test/snapshots/Snapshots23.v0.bpl
index 8f637d19..740afa6a 100644
--- a/Test/snapshots/Snapshots23.v0.bpl
+++ b/Test/snapshots/Snapshots23.v0.bpl
@@ -1,22 +1,22 @@
-procedure {:checksum "0"} M();
-
-implementation {:id "M"} {:checksum "1"} M()
-{
-    if (*)
-    {
-        assert 1 != 1;  // error
-    }
-    else
-    {
-        assert 2 == 2;
-    }
-
-    assert 3 == 3;
-}
-
-
-procedure {:checksum "2"} N();
-
-implementation {:id "N"} {:checksum "3"} N()
-{
-}
+procedure {:checksum "0"} M();
+
+implementation {:id "M"} {:checksum "1"} M()
+{
+    if (*)
+    {
+        assert 1 != 1;  // error
+    }
+    else
+    {
+        assert 2 == 2;
+    }
+
+    assert 3 == 3;
+}
+
+
+procedure {:checksum "2"} N();
+
+implementation {:id "N"} {:checksum "3"} N()
+{
+}
diff --git a/Test/snapshots/Snapshots23.v1.bpl b/Test/snapshots/Snapshots23.v1.bpl
index e13116dc..9e57a201 100644
--- a/Test/snapshots/Snapshots23.v1.bpl
+++ b/Test/snapshots/Snapshots23.v1.bpl
@@ -1,23 +1,23 @@
-procedure {:checksum "0"} M();
-
-implementation {:id "M"} {:checksum "1"} M()
-{
-    if (*)
-    {
-        assert 1 != 1;  // error
-    }
-    else
-    {
-        assert 2 == 2;
-    }
-
-    assert 3 == 3;
-}
-
-
-procedure {:checksum "2"} N();
-
-implementation {:id "N"} {:checksum "4"} N()
-{
-    assert 4 == 4;
-}
+procedure {:checksum "0"} M();
+
+implementation {:id "M"} {:checksum "1"} M()
+{
+    if (*)
+    {
+        assert 1 != 1;  // error
+    }
+    else
+    {
+        assert 2 == 2;
+    }
+
+    assert 3 == 3;
+}
+
+
+procedure {:checksum "2"} N();
+
+implementation {:id "N"} {:checksum "4"} N()
+{
+    assert 4 == 4;
+}
diff --git a/Test/snapshots/Snapshots23.v2.bpl b/Test/snapshots/Snapshots23.v2.bpl
index 144a0922..e076b618 100644
--- a/Test/snapshots/Snapshots23.v2.bpl
+++ b/Test/snapshots/Snapshots23.v2.bpl
@@ -1,22 +1,22 @@
-procedure {:checksum "0"} M();
-
-implementation {:id "M"} {:checksum "5"} M()
-{
-    if (*)
-    {
-        // Don't remove this comment.
-        assert 1 != 1;  // error
-    }
-    else
-    {
-        assert 2 == 2;
-    }
-}
-
-
-procedure {:checksum "2"} N();
-
-implementation {:id "N"} {:checksum "4"} N()
-{
-    assert 4 == 4;
-}
+procedure {:checksum "0"} M();
+
+implementation {:id "M"} {:checksum "5"} M()
+{
+    if (*)
+    {
+        // Don't remove this comment.
+        assert 1 != 1;  // error
+    }
+    else
+    {
+        assert 2 == 2;
+    }
+}
+
+
+procedure {:checksum "2"} N();
+
+implementation {:id "N"} {:checksum "4"} N()
+{
+    assert 4 == 4;
+}
diff --git a/Test/snapshots/Snapshots24.v0.bpl b/Test/snapshots/Snapshots24.v0.bpl
index 1289399b..5d038779 100644
--- a/Test/snapshots/Snapshots24.v0.bpl
+++ b/Test/snapshots/Snapshots24.v0.bpl
@@ -1,25 +1,25 @@
-procedure {:checksum "0"} M();
-
-implementation {:id "M"} {:checksum "1"} M()
-{
-    if (*)
-    {
-        assert {:subsumption 0} 1 != 1;  // error
-    }
-    else if (*)
-    {
-        assert {:subsumption 1} 5 != 5;  // error
-    }
-    else if (*)
-    {
-        assert {:subsumption 2} 6 != 6;  // error
-    }
-    else
-    {
-        assert {:subsumption 1} 2 == 2;
-        assert {:subsumption 2} 4 == 4;
-        assert 5 == 5;
-    }
-
-    assert {:subsumption 0} 3 == 3;
-}
+procedure {:checksum "0"} M();
+
+implementation {:id "M"} {:checksum "1"} M()
+{
+    if (*)
+    {
+        assert {:subsumption 0} 1 != 1;  // error
+    }
+    else if (*)
+    {
+        assert {:subsumption 1} 5 != 5;  // error
+    }
+    else if (*)
+    {
+        assert {:subsumption 2} 6 != 6;  // error
+    }
+    else
+    {
+        assert {:subsumption 1} 2 == 2;
+        assert {:subsumption 2} 4 == 4;
+        assert 5 == 5;
+    }
+
+    assert {:subsumption 0} 3 == 3;
+}
diff --git a/Test/snapshots/Snapshots24.v1.bpl b/Test/snapshots/Snapshots24.v1.bpl
index 00d65961..382dc6dc 100644
--- a/Test/snapshots/Snapshots24.v1.bpl
+++ b/Test/snapshots/Snapshots24.v1.bpl
@@ -1,25 +1,25 @@
-procedure {:checksum "0"} M();
-
-implementation {:id "M"} {:checksum "2"} M()
-{
-    if (*)
-    {
-        assert {:subsumption 0} 1 == 1;
-    }
-    else if (*)
-    {
-        assert {:subsumption 1} 5 == 5;
-    }
-    else if (*)
-    {
-        assert {:subsumption 2} 6 != 6;  // error
-    }
-    else
-    {
-        assert {:subsumption 1} 2 == 2;
-        assert {:subsumption 2} 4 == 4;
-        assert 5 == 5;
-    }
-
-    assert {:subsumption 0} 3 == 3;
-}
+procedure {:checksum "0"} M();
+
+implementation {:id "M"} {:checksum "2"} M()
+{
+    if (*)
+    {
+        assert {:subsumption 0} 1 == 1;
+    }
+    else if (*)
+    {
+        assert {:subsumption 1} 5 == 5;
+    }
+    else if (*)
+    {
+        assert {:subsumption 2} 6 != 6;  // error
+    }
+    else
+    {
+        assert {:subsumption 1} 2 == 2;
+        assert {:subsumption 2} 4 == 4;
+        assert 5 == 5;
+    }
+
+    assert {:subsumption 0} 3 == 3;
+}
diff --git a/Test/snapshots/Snapshots25.v0.bpl b/Test/snapshots/Snapshots25.v0.bpl
index 5276f1dd..514ba3fa 100644
--- a/Test/snapshots/Snapshots25.v0.bpl
+++ b/Test/snapshots/Snapshots25.v0.bpl
@@ -1,14 +1,14 @@
-procedure {:checksum "0"} M();
-
-implementation {:id "M"} {:checksum "1"} M()
-{
-    var x: int;
-
-    while (*)
-    {
-        x := 0;
-    }
-
-    assert 0 == 0;
-    assert x != x;
-}
+procedure {:checksum "0"} M();
+
+implementation {:id "M"} {:checksum "1"} M()
+{
+    var x: int;
+
+    while (*)
+    {
+        x := 0;
+    }
+
+    assert 0 == 0;
+    assert x != x;
+}
diff --git a/Test/snapshots/Snapshots25.v1.bpl b/Test/snapshots/Snapshots25.v1.bpl
index fb735930..1cf2dc6e 100644
--- a/Test/snapshots/Snapshots25.v1.bpl
+++ b/Test/snapshots/Snapshots25.v1.bpl
@@ -1,14 +1,14 @@
-procedure {:checksum "0"} M();
-
-implementation {:id "M"} {:checksum "2"} M()
-{
-    var x: int;
-
-    while (*)
-    {
-        x := 1;
-    }
-
-    assert 0 == 0;
-    assert x != x;
-}
+procedure {:checksum "0"} M();
+
+implementation {:id "M"} {:checksum "2"} M()
+{
+    var x: int;
+
+    while (*)
+    {
+        x := 1;
+    }
+
+    assert 0 == 0;
+    assert x != x;
+}
diff --git a/Test/snapshots/Snapshots26.v0.bpl b/Test/snapshots/Snapshots26.v0.bpl
index 5276f1dd..514ba3fa 100644
--- a/Test/snapshots/Snapshots26.v0.bpl
+++ b/Test/snapshots/Snapshots26.v0.bpl
@@ -1,14 +1,14 @@
-procedure {:checksum "0"} M();
-
-implementation {:id "M"} {:checksum "1"} M()
-{
-    var x: int;
-
-    while (*)
-    {
-        x := 0;
-    }
-
-    assert 0 == 0;
-    assert x != x;
-}
+procedure {:checksum "0"} M();
+
+implementation {:id "M"} {:checksum "1"} M()
+{
+    var x: int;
+
+    while (*)
+    {
+        x := 0;
+    }
+
+    assert 0 == 0;
+    assert x != x;
+}
diff --git a/Test/snapshots/Snapshots26.v1.bpl b/Test/snapshots/Snapshots26.v1.bpl
index 7c2e3292..c17596c7 100644
--- a/Test/snapshots/Snapshots26.v1.bpl
+++ b/Test/snapshots/Snapshots26.v1.bpl
@@ -1,15 +1,15 @@
-procedure {:checksum "0"} M();
-
-implementation {:id "M"} {:checksum "2"} M()
-{
-    var x: int;
-
-    while (*)
-    {
-        x := 0;
-        x := x + 1;
-    }
-
-    assert 0 == 0;
-    assert x != x;
-}
+procedure {:checksum "0"} M();
+
+implementation {:id "M"} {:checksum "2"} M()
+{
+    var x: int;
+
+    while (*)
+    {
+        x := 0;
+        x := x + 1;
+    }
+
+    assert 0 == 0;
+    assert x != x;
+}
diff --git a/Test/snapshots/Snapshots27.v0.bpl b/Test/snapshots/Snapshots27.v0.bpl
index 5276f1dd..514ba3fa 100644
--- a/Test/snapshots/Snapshots27.v0.bpl
+++ b/Test/snapshots/Snapshots27.v0.bpl
@@ -1,14 +1,14 @@
-procedure {:checksum "0"} M();
-
-implementation {:id "M"} {:checksum "1"} M()
-{
-    var x: int;
-
-    while (*)
-    {
-        x := 0;
-    }
-
-    assert 0 == 0;
-    assert x != x;
-}
+procedure {:checksum "0"} M();
+
+implementation {:id "M"} {:checksum "1"} M()
+{
+    var x: int;
+
+    while (*)
+    {
+        x := 0;
+    }
+
+    assert 0 == 0;
+    assert x != x;
+}
diff --git a/Test/snapshots/Snapshots27.v1.bpl b/Test/snapshots/Snapshots27.v1.bpl
index 4d60e149..7221721d 100644
--- a/Test/snapshots/Snapshots27.v1.bpl
+++ b/Test/snapshots/Snapshots27.v1.bpl
@@ -1,16 +1,16 @@
-procedure {:checksum "0"} M();
-
-implementation {:id "M"} {:checksum "2"} M()
-{
-    var x: int;
-    var y: int;
-
-    while (*)
-    {
-        x := 0;
-        y := 0;
-    }
-
-    assert 0 == 0;
-    assert x != x;
-}
+procedure {:checksum "0"} M();
+
+implementation {:id "M"} {:checksum "2"} M()
+{
+    var x: int;
+    var y: int;
+
+    while (*)
+    {
+        x := 0;
+        y := 0;
+    }
+
+    assert 0 == 0;
+    assert x != x;
+}
diff --git a/Test/snapshots/Snapshots28.v0.bpl b/Test/snapshots/Snapshots28.v0.bpl
index b74b5013..8bce51fa 100644
--- a/Test/snapshots/Snapshots28.v0.bpl
+++ b/Test/snapshots/Snapshots28.v0.bpl
@@ -1,15 +1,15 @@
-procedure {:checksum "0"} M();
-
-implementation {:id "M"} {:checksum "1"} M()
-{
-    var x: int;
-
-    assume x == 0;
-
-    while (*)
-    {
-    }
-
-    assert 0 == 0;
-    assert x == 0;
-}
+procedure {:checksum "0"} M();
+
+implementation {:id "M"} {:checksum "1"} M()
+{
+    var x: int;
+
+    assume x == 0;
+
+    while (*)
+    {
+    }
+
+    assert 0 == 0;
+    assert x == 0;
+}
diff --git a/Test/snapshots/Snapshots28.v1.bpl b/Test/snapshots/Snapshots28.v1.bpl
index 0312b6a6..205515f5 100644
--- a/Test/snapshots/Snapshots28.v1.bpl
+++ b/Test/snapshots/Snapshots28.v1.bpl
@@ -1,16 +1,16 @@
-procedure {:checksum "0"} M();
-
-implementation {:id "M"} {:checksum "2"} M()
-{
-    var x: int;
-
-    assume x == 0;
-
-    while (*)
-    {
-        x := 1;
-    }
-
-    assert 0 == 0;
-    assert x == 0;
-}
+procedure {:checksum "0"} M();
+
+implementation {:id "M"} {:checksum "2"} M()
+{
+    var x: int;
+
+    assume x == 0;
+
+    while (*)
+    {
+        x := 1;
+    }
+
+    assert 0 == 0;
+    assert x == 0;
+}
diff --git a/Test/snapshots/Snapshots29.v0.bpl b/Test/snapshots/Snapshots29.v0.bpl
index f4087f90..840aed82 100644
--- a/Test/snapshots/Snapshots29.v0.bpl
+++ b/Test/snapshots/Snapshots29.v0.bpl
@@ -1,15 +1,15 @@
-procedure {:checksum "0"} P();
-
-implementation {:id "P"} {:checksum "1"} P()
-{
-    var i: int;
-
-    i := 0;
-
-    while (*)
-    {
-        i := 0;
-    }
-
-    assert i == 0;
-}
+procedure {:checksum "0"} P();
+
+implementation {:id "P"} {:checksum "1"} P()
+{
+    var i: int;
+
+    i := 0;
+
+    while (*)
+    {
+        i := 0;
+    }
+
+    assert i == 0;
+}
diff --git a/Test/snapshots/Snapshots29.v1.bpl b/Test/snapshots/Snapshots29.v1.bpl
index 5211f832..59a607ea 100644
--- a/Test/snapshots/Snapshots29.v1.bpl
+++ b/Test/snapshots/Snapshots29.v1.bpl
@@ -1,15 +1,15 @@
-procedure {:checksum "0"} P();
-
-implementation {:id "P"} {:checksum "2"} P()
-{
-    var i: int;
-
-    i := 0;
-
-    while (*)
-    {
-        i := 1;
-    }
-
-    assert i == 0;
-}
+procedure {:checksum "0"} P();
+
+implementation {:id "P"} {:checksum "2"} P()
+{
+    var i: int;
+
+    i := 0;
+
+    while (*)
+    {
+        i := 1;
+    }
+
+    assert i == 0;
+}
diff --git a/Test/snapshots/Snapshots3.v0.bpl b/Test/snapshots/Snapshots3.v0.bpl
index 7ab7aa5c..118f28d7 100644
--- a/Test/snapshots/Snapshots3.v0.bpl
+++ b/Test/snapshots/Snapshots3.v0.bpl
@@ -1,18 +1,18 @@
-procedure {:checksum "P0$proc#0"} P0();
-ensures G();
-// Action: verify
-implementation {:id "P0"} {:checksum "P0$impl#0"} P0()
-{
-}
-
-
-function {:checksum "F#0"} F() : bool
-{
-    true
-}
-
-
-function {:checksum "G#0"} G() : bool
-{
-    F()
-}
+procedure {:checksum "P0$proc#0"} P0();
+ensures G();
+// Action: verify
+implementation {:id "P0"} {:checksum "P0$impl#0"} P0()
+{
+}
+
+
+function {:checksum "F#0"} F() : bool
+{
+    true
+}
+
+
+function {:checksum "G#0"} G() : bool
+{
+    F()
+}
diff --git a/Test/snapshots/Snapshots3.v1.bpl b/Test/snapshots/Snapshots3.v1.bpl
index 5eb57e78..a764c773 100644
--- a/Test/snapshots/Snapshots3.v1.bpl
+++ b/Test/snapshots/Snapshots3.v1.bpl
@@ -1,18 +1,18 @@
-procedure {:checksum "P0$proc#0"} P0();
-ensures G();
-// Action: verify
-implementation {:id "P0"} {:checksum "P0$impl#0"} P0()
-{
-}
-
-
-function {:checksum "F#1"} F() : bool
-{
-    false
-}
-
-
-function {:checksum "G#0"} G() : bool
-{
-    F()
-}
+procedure {:checksum "P0$proc#0"} P0();
+ensures G();
+// Action: verify
+implementation {:id "P0"} {:checksum "P0$impl#0"} P0()
+{
+}
+
+
+function {:checksum "F#1"} F() : bool
+{
+    false
+}
+
+
+function {:checksum "G#0"} G() : bool
+{
+    F()
+}
diff --git a/Test/snapshots/Snapshots30.v0.bpl b/Test/snapshots/Snapshots30.v0.bpl
index 459c4007..d4eb4502 100644
--- a/Test/snapshots/Snapshots30.v0.bpl
+++ b/Test/snapshots/Snapshots30.v0.bpl
@@ -1,13 +1,13 @@
-procedure {:checksum "0"} P();
-
-implementation {:id "P"} {:checksum "1"} P()
-{
-    call Q();
-}
-
-procedure {:checksum "2"} Q();
-  requires 0 == 0;
-  requires 1 == 1;
-  requires 2 != 2;
-  requires 3 == 3;
-  requires 4 == 4;
+procedure {:checksum "0"} P();
+
+implementation {:id "P"} {:checksum "1"} P()
+{
+    call Q();
+}
+
+procedure {:checksum "2"} Q();
+  requires 0 == 0;
+  requires 1 == 1;
+  requires 2 != 2;
+  requires 3 == 3;
+  requires 4 == 4;
diff --git a/Test/snapshots/Snapshots30.v1.bpl b/Test/snapshots/Snapshots30.v1.bpl
index 089a1939..dbf2ec72 100644
--- a/Test/snapshots/Snapshots30.v1.bpl
+++ b/Test/snapshots/Snapshots30.v1.bpl
@@ -1,14 +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;
+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;
diff --git a/Test/snapshots/Snapshots31.v0.bpl b/Test/snapshots/Snapshots31.v0.bpl
index 845a6cef..df8bbcbb 100644
--- a/Test/snapshots/Snapshots31.v0.bpl
+++ b/Test/snapshots/Snapshots31.v0.bpl
@@ -1,15 +1,15 @@
-var g: int;
-
-procedure {:checksum "0"} P();
-  requires g == 0;
-  modifies g;
-
-implementation {:id "P"} {:checksum "1"} P()
-{
-    call Q();
-    assert 0 < g;
-}
-
-procedure {:checksum "2"} Q();
-  modifies g;
-  ensures old(g) < g;
+var g: int;
+
+procedure {:checksum "0"} P();
+  requires g == 0;
+  modifies g;
+
+implementation {:id "P"} {:checksum "1"} P()
+{
+    call Q();
+    assert 0 < g;
+}
+
+procedure {:checksum "2"} Q();
+  modifies g;
+  ensures old(g) < g;
diff --git a/Test/snapshots/Snapshots31.v1.bpl b/Test/snapshots/Snapshots31.v1.bpl
index a3b37168..26469d83 100644
--- a/Test/snapshots/Snapshots31.v1.bpl
+++ b/Test/snapshots/Snapshots31.v1.bpl
@@ -1,14 +1,14 @@
-var g: int;
-
-procedure {:checksum "0"} P();
-  requires g == 0;
-  modifies g;
-
-implementation {:id "P"} {:checksum "1"} P()
-{
-    call Q();
-    assert 0 < g;
-}
-
-procedure {:checksum "3"} Q();
-  modifies g;
+var g: int;
+
+procedure {:checksum "0"} P();
+  requires g == 0;
+  modifies g;
+
+implementation {:id "P"} {:checksum "1"} P()
+{
+    call Q();
+    assert 0 < g;
+}
+
+procedure {:checksum "3"} Q();
+  modifies g;
diff --git a/Test/snapshots/Snapshots32.v0.bpl b/Test/snapshots/Snapshots32.v0.bpl
index 845a6cef..df8bbcbb 100644
--- a/Test/snapshots/Snapshots32.v0.bpl
+++ b/Test/snapshots/Snapshots32.v0.bpl
@@ -1,15 +1,15 @@
-var g: int;
-
-procedure {:checksum "0"} P();
-  requires g == 0;
-  modifies g;
-
-implementation {:id "P"} {:checksum "1"} P()
-{
-    call Q();
-    assert 0 < g;
-}
-
-procedure {:checksum "2"} Q();
-  modifies g;
-  ensures old(g) < g;
+var g: int;
+
+procedure {:checksum "0"} P();
+  requires g == 0;
+  modifies g;
+
+implementation {:id "P"} {:checksum "1"} P()
+{
+    call Q();
+    assert 0 < g;
+}
+
+procedure {:checksum "2"} Q();
+  modifies g;
+  ensures old(g) < g;
diff --git a/Test/snapshots/Snapshots32.v1.bpl b/Test/snapshots/Snapshots32.v1.bpl
index cbffe891..c0af5fb9 100644
--- a/Test/snapshots/Snapshots32.v1.bpl
+++ b/Test/snapshots/Snapshots32.v1.bpl
@@ -1,12 +1,12 @@
-var g: int;
-
-procedure {:checksum "0"} P();
-  requires g == 0;
-
-implementation {:id "P"} {:checksum "1"} P()
-{
-    call Q();
-    assert 0 < g;
-}
-
-procedure {:checksum "3"} Q();
+var g: int;
+
+procedure {:checksum "0"} P();
+  requires g == 0;
+
+implementation {:id "P"} {:checksum "1"} P()
+{
+    call Q();
+    assert 0 < g;
+}
+
+procedure {:checksum "3"} Q();
diff --git a/Test/snapshots/Snapshots33.v0.bpl b/Test/snapshots/Snapshots33.v0.bpl
index 845a6cef..df8bbcbb 100644
--- a/Test/snapshots/Snapshots33.v0.bpl
+++ b/Test/snapshots/Snapshots33.v0.bpl
@@ -1,15 +1,15 @@
-var g: int;
-
-procedure {:checksum "0"} P();
-  requires g == 0;
-  modifies g;
-
-implementation {:id "P"} {:checksum "1"} P()
-{
-    call Q();
-    assert 0 < g;
-}
-
-procedure {:checksum "2"} Q();
-  modifies g;
-  ensures old(g) < g;
+var g: int;
+
+procedure {:checksum "0"} P();
+  requires g == 0;
+  modifies g;
+
+implementation {:id "P"} {:checksum "1"} P()
+{
+    call Q();
+    assert 0 < g;
+}
+
+procedure {:checksum "2"} Q();
+  modifies g;
+  ensures old(g) < g;
diff --git a/Test/snapshots/Snapshots33.v1.bpl b/Test/snapshots/Snapshots33.v1.bpl
index 1c6d6dbf..3cc1de13 100644
--- a/Test/snapshots/Snapshots33.v1.bpl
+++ b/Test/snapshots/Snapshots33.v1.bpl
@@ -1,8 +1,8 @@
-procedure {:checksum "5"} P();
-
-implementation {:id "P"} {:checksum "4"} P()
-{
-    call Q();
-}
-
-procedure {:checksum "3"} Q();
+procedure {:checksum "5"} P();
+
+implementation {:id "P"} {:checksum "4"} P()
+{
+    call Q();
+}
+
+procedure {:checksum "3"} Q();
diff --git a/Test/snapshots/Snapshots34.v0.bpl b/Test/snapshots/Snapshots34.v0.bpl
new file mode 100644
index 00000000..5a996f40
--- /dev/null
+++ b/Test/snapshots/Snapshots34.v0.bpl
@@ -0,0 +1,7 @@
+procedure {:checksum "0"} P();
+  requires 0 != 0;
+
+implementation {:id "P"} {:checksum "1"} P()
+{
+    assert 1 != 1;
+}
diff --git a/Test/snapshots/Snapshots34.v1.bpl b/Test/snapshots/Snapshots34.v1.bpl
new file mode 100644
index 00000000..401b4f9e
--- /dev/null
+++ b/Test/snapshots/Snapshots34.v1.bpl
@@ -0,0 +1,6 @@
+procedure {:checksum "2"} P();
+
+implementation {:id "P"} {:checksum "1"} P()
+{
+    assert 1 != 1;
+}
diff --git a/Test/snapshots/Snapshots35.v0.bpl b/Test/snapshots/Snapshots35.v0.bpl
new file mode 100644
index 00000000..6377edaf
--- /dev/null
+++ b/Test/snapshots/Snapshots35.v0.bpl
@@ -0,0 +1,7 @@
+procedure {:checksum "0"} P(b: bool);
+  requires b;
+
+implementation {:id "P"} {:checksum "1"} P(p: bool)
+{
+    assert p;
+}
diff --git a/Test/snapshots/Snapshots35.v1.bpl b/Test/snapshots/Snapshots35.v1.bpl
new file mode 100644
index 00000000..605a862a
--- /dev/null
+++ b/Test/snapshots/Snapshots35.v1.bpl
@@ -0,0 +1,6 @@
+procedure {:checksum "2"} P(b: bool);
+
+implementation {:id "P"} {:checksum "1"} P(p: bool)
+{
+    assert p;
+}
diff --git a/Test/snapshots/Snapshots36.v0.bpl b/Test/snapshots/Snapshots36.v0.bpl
new file mode 100644
index 00000000..66c4ed85
--- /dev/null
+++ b/Test/snapshots/Snapshots36.v0.bpl
@@ -0,0 +1,14 @@
+function {:checksum "2"} F() : bool
+{
+    true
+}
+
+procedure {:checksum "0"} P(b: bool);
+
+implementation {:id "P"} {:checksum "1"} P(p: bool)
+{
+    var l: [int]bool;
+
+    l := (lambda n: int :: F());
+    assert l[0];
+}
diff --git a/Test/snapshots/Snapshots36.v1.bpl b/Test/snapshots/Snapshots36.v1.bpl
new file mode 100644
index 00000000..77172a3e
--- /dev/null
+++ b/Test/snapshots/Snapshots36.v1.bpl
@@ -0,0 +1,14 @@
+function {:checksum "3"} F() : bool
+{
+    false
+}
+
+procedure {:checksum "0"} P(b: bool);
+
+implementation {:id "P"} {:checksum "1"} P(p: bool)
+{
+    var l: [int]bool;
+
+    l := (lambda n: int :: F());
+    assert l[0];
+}
diff --git a/Test/snapshots/Snapshots37.v0.bpl b/Test/snapshots/Snapshots37.v0.bpl
new file mode 100644
index 00000000..a1b90fcc
--- /dev/null
+++ b/Test/snapshots/Snapshots37.v0.bpl
@@ -0,0 +1,9 @@
+procedure {:checksum "0"} P(b: bool);
+
+implementation {:id "P"} {:checksum "1"} P(p: bool)
+{
+    var l: [int]bool;
+
+    l := (lambda n: int :: true);
+    assert l[0];
+}
diff --git a/Test/snapshots/Snapshots37.v1.bpl b/Test/snapshots/Snapshots37.v1.bpl
new file mode 100644
index 00000000..825a16a0
--- /dev/null
+++ b/Test/snapshots/Snapshots37.v1.bpl
@@ -0,0 +1,9 @@
+procedure {:checksum "0"} P(b: bool);
+
+implementation {:id "P"} {:checksum "2"} P(p: bool)
+{
+    var l: [int]bool;
+
+    l := (lambda n: int :: false);
+    assert l[0];
+}
diff --git a/Test/snapshots/Snapshots38.v0.bpl b/Test/snapshots/Snapshots38.v0.bpl
new file mode 100644
index 00000000..496a75a9
--- /dev/null
+++ b/Test/snapshots/Snapshots38.v0.bpl
@@ -0,0 +1,13 @@
+procedure {:checksum "-1"} Callee();
+
+implementation {:id "Callee"} {:checksum "0"} Callee()
+{
+    var r: int;
+
+    call r := Sum(42);
+    assert r != 0;
+}
+
+procedure {:checksum "1"} Sum(n: int) returns (r: int);
+  requires 0 <= n;
+  ensures n != 0 ==> 1 <= r;
diff --git a/Test/snapshots/Snapshots38.v1.bpl b/Test/snapshots/Snapshots38.v1.bpl
new file mode 100644
index 00000000..062b22ea
--- /dev/null
+++ b/Test/snapshots/Snapshots38.v1.bpl
@@ -0,0 +1,14 @@
+procedure {:checksum "-1"} Callee();
+
+implementation {:id "Callee"} {:checksum "2"} Callee()
+{
+    var r: int;
+
+    call r := Sum(42);
+    assert r != 0;
+    assert 42 <= r;
+}
+
+procedure {:checksum "1"} Sum(n: int) returns (r: int);
+  requires 0 <= n;
+  ensures n != 0 ==> 1 <= r;
diff --git a/Test/snapshots/Snapshots38.v2.bpl b/Test/snapshots/Snapshots38.v2.bpl
new file mode 100644
index 00000000..5c4b69d6
--- /dev/null
+++ b/Test/snapshots/Snapshots38.v2.bpl
@@ -0,0 +1,14 @@
+procedure {:checksum "-1"} Callee();
+
+implementation {:id "Callee"} {:checksum "2"} Callee()
+{
+    var r: int;
+
+    call r := Sum(42);
+    assert r != 0;
+    assert 42 <= r;
+}
+
+procedure {:checksum "3"} Sum(n: int) returns (r: int);
+  requires 0 <= n;
+  ensures n != 0 ==> n <= r;
diff --git a/Test/snapshots/Snapshots39.v0.bpl b/Test/snapshots/Snapshots39.v0.bpl
new file mode 100644
index 00000000..083d497e
--- /dev/null
+++ b/Test/snapshots/Snapshots39.v0.bpl
@@ -0,0 +1,13 @@
+procedure {:checksum "-1"} Callee();
+
+implementation {:id "Callee"} {:checksum "0"} Callee()
+{
+    var r: int;
+
+    call r := Sum(42);
+    assert r != 0;
+}
+
+procedure {:checksum "1"} Sum(n: int) returns (r: int);
+  requires 0 <= n;
+  ensures n <= r;
diff --git a/Test/snapshots/Snapshots39.v1.bpl b/Test/snapshots/Snapshots39.v1.bpl
new file mode 100644
index 00000000..09850bfc
--- /dev/null
+++ b/Test/snapshots/Snapshots39.v1.bpl
@@ -0,0 +1,14 @@
+procedure {:checksum "-1"} Callee();
+
+implementation {:id "Callee"} {:checksum "2"} Callee()
+{
+    var r: int;
+
+    call r := Sum(42);
+    assert r != 0;
+    assert r == (42 * 43) div 2;
+}
+
+procedure {:checksum "1"} Sum(n: int) returns (r: int);
+  requires 0 <= n;
+  ensures n <= r;
diff --git a/Test/snapshots/Snapshots39.v2.bpl b/Test/snapshots/Snapshots39.v2.bpl
new file mode 100644
index 00000000..4bdc4b6e
--- /dev/null
+++ b/Test/snapshots/Snapshots39.v2.bpl
@@ -0,0 +1,14 @@
+procedure {:checksum "-1"} Callee();
+
+implementation {:id "Callee"} {:checksum "2"} Callee()
+{
+    var r: int;
+
+    call r := Sum(42);
+    assert r != 0;
+    assert r == (42 * 43) div 2;
+}
+
+procedure {:checksum "3"} Sum(n: int) returns (r: int);
+  requires 0 <= n;
+  ensures r == (n * (n + 1)) div 2;
diff --git a/Test/snapshots/Snapshots4.v0.bpl b/Test/snapshots/Snapshots4.v0.bpl
index 59a42289..db477aca 100644
--- a/Test/snapshots/Snapshots4.v0.bpl
+++ b/Test/snapshots/Snapshots4.v0.bpl
@@ -1,36 +1,36 @@
-procedure {:checksum "P0$proc#0"} P0();
-// Action: verify
-implementation {:id "P0"} {:checksum "P0$impl#0"} P0()
-{
-}
-
-
-procedure {:checksum "P1$proc#0"} P1();
-// Action: verify
-implementation {:id "P1"} {:checksum "P1$impl#0"} P1()
-{
-    call P2();
-}
-
-
-procedure {:checksum "P2$proc#0"} P2();
-  ensures G();
-
-
-procedure {:checksum "P3$proc#0"} P3();
-// Action: verify
-implementation {:id "P3"} {:checksum "P3$impl#0"} P3()
-{
-}
-
-
-function {:checksum "G#0"} G() : bool
-{
-    F()
-}
-
-
-function {:checksum "F#0"} F() : bool
-{
-    true
-}
+procedure {:checksum "P0$proc#0"} P0();
+// Action: verify
+implementation {:id "P0"} {:checksum "P0$impl#0"} P0()
+{
+}
+
+
+procedure {:checksum "P1$proc#0"} P1();
+// Action: verify
+implementation {:id "P1"} {:checksum "P1$impl#0"} P1()
+{
+    call P2();
+}
+
+
+procedure {:checksum "P2$proc#0"} P2();
+  ensures G();
+
+
+procedure {:checksum "P3$proc#0"} P3();
+// Action: verify
+implementation {:id "P3"} {:checksum "P3$impl#0"} P3()
+{
+}
+
+
+function {:checksum "G#0"} G() : bool
+{
+    F()
+}
+
+
+function {:checksum "F#0"} F() : bool
+{
+    true
+}
diff --git a/Test/snapshots/Snapshots4.v1.bpl b/Test/snapshots/Snapshots4.v1.bpl
index 392a1648..973d0104 100644
--- a/Test/snapshots/Snapshots4.v1.bpl
+++ b/Test/snapshots/Snapshots4.v1.bpl
@@ -1,45 +1,45 @@
-procedure {:checksum "P0$proc#0"} P0();
-// Action: skip
-// Priority: 0
-implementation {:id "P0"} {:checksum "P0$impl#0"} P0()
-{
-}
-
-
-procedure {:checksum "P1$proc#0"} P1();
-// Action: verify
-// Priority: 1
-implementation {:id "P1"} {:checksum "P1$impl#0"} P1()
-{
-    call P2();
-}
-
-
-procedure {:checksum "P3$proc#0"} P3();
-// Action: verify
-// Priority: 2
-implementation {:id "P3"} {:checksum "P3$impl#1"} P3()
-{
-    assert false;
-}
-
-
-procedure {:checksum "P2$proc#0"} P2();
-  ensures G();
-// Action: verify
-// Priority: 3
-implementation {:id "P2"} {:checksum "P2$impl#0"} P2()
-{
-}
-
-
-function {:checksum "G#0"} G() : bool
-{
-    F()
-}
-
-
-function {:checksum "F#1"} F() : bool
-{
-    false
-}
+procedure {:checksum "P0$proc#0"} P0();
+// Action: skip
+// Priority: 0
+implementation {:id "P0"} {:checksum "P0$impl#0"} P0()
+{
+}
+
+
+procedure {:checksum "P1$proc#0"} P1();
+// Action: verify
+// Priority: 1
+implementation {:id "P1"} {:checksum "P1$impl#0"} P1()
+{
+    call P2();
+}
+
+
+procedure {:checksum "P3$proc#0"} P3();
+// Action: verify
+// Priority: 2
+implementation {:id "P3"} {:checksum "P3$impl#1"} P3()
+{
+    assert false;
+}
+
+
+procedure {:checksum "P2$proc#0"} P2();
+  ensures G();
+// Action: verify
+// Priority: 3
+implementation {:id "P2"} {:checksum "P2$impl#0"} P2()
+{
+}
+
+
+function {:checksum "G#0"} G() : bool
+{
+    F()
+}
+
+
+function {:checksum "F#1"} F() : bool
+{
+    false
+}
diff --git a/Test/snapshots/Snapshots40.v0.bpl b/Test/snapshots/Snapshots40.v0.bpl
new file mode 100644
index 00000000..27839752
--- /dev/null
+++ b/Test/snapshots/Snapshots40.v0.bpl
@@ -0,0 +1,14 @@
+procedure {:checksum "-1"} Foo(b: bool);
+
+implementation {:id "Foo"} {:checksum "0"} Foo(b: bool)
+{
+    var r: int;
+
+    assert b;
+    call r := Sum(42);
+    assert r != 0;
+}
+
+procedure {:checksum "1"} Sum(n: int) returns (r: int);
+  requires 0 <= n;
+  ensures n <= r;
diff --git a/Test/snapshots/Snapshots40.v1.bpl b/Test/snapshots/Snapshots40.v1.bpl
new file mode 100644
index 00000000..e1c505f8
--- /dev/null
+++ b/Test/snapshots/Snapshots40.v1.bpl
@@ -0,0 +1,15 @@
+procedure {:checksum "-1"} Foo(b: bool);
+
+implementation {:id "Foo"} {:checksum "2"} Foo(b: bool)
+{
+    var r: int;
+
+    assert b;
+    call r := Sum(42);
+    assert r != 0;
+    assert r == (42 * 43) div 2;
+}
+
+procedure {:checksum "1"} Sum(n: int) returns (r: int);
+  requires 0 <= n;
+  ensures n <= r;
diff --git a/Test/snapshots/Snapshots40.v2.bpl b/Test/snapshots/Snapshots40.v2.bpl
new file mode 100644
index 00000000..842d33f5
--- /dev/null
+++ b/Test/snapshots/Snapshots40.v2.bpl
@@ -0,0 +1,15 @@
+procedure {:checksum "-1"} Foo(b: bool);
+
+implementation {:id "Foo"} {:checksum "2"} Foo(b: bool)
+{
+    var r: int;
+
+    assert b;
+    call r := Sum(42);
+    assert r != 0;
+    assert r == (42 * 43) div 2;
+}
+
+procedure {:checksum "3"} Sum(n: int) returns (r: int);
+  requires 0 <= n;
+  ensures r == (n * (n + 1)) div 2;
diff --git a/Test/snapshots/Snapshots41.v0.bpl b/Test/snapshots/Snapshots41.v0.bpl
new file mode 100644
index 00000000..dbfe3e2d
--- /dev/null
+++ b/Test/snapshots/Snapshots41.v0.bpl
@@ -0,0 +1,35 @@
+procedure {:checksum "0"} M(x: int);
+implementation {:id "M"} {:checksum "1"} M(x: int)
+{                     assert x < 20 || 10 <= x;  // always true
+  assert x < 10;  // error
+  call Other(x);  // error: precondition violation
+}
+
+procedure {:checksum "10"} Other(y: int);
+  requires 0 <= y;
+implementation {:id "Other"} {:checksum "11"} Other(y: int)
+{
+}
+
+procedure {:checksum "20"} Posty() returns (z: int);
+  ensures 2 <= z;  // error: postcondition violation
+implementation {:id "Posty"} {:checksum "21"} Posty() returns (z: int)
+{
+  var t: int;
+  t := 20;
+  if (t < z) {
+  } else {  // the postcondition violation occurs on this 'else' branch
+  }
+}
+
+procedure {:checksum "30"} NoChangeWhazzoeva(u: int);
+implementation {:id "NoChangeWhazzoeva"} {:checksum "3"} NoChangeWhazzoeva(u: int)
+{
+  assert u != 53;  // error
+}
+
+procedure {:checksum "40"} NoChangeAndCorrect();
+implementation {:id "NoChangeAndCorrect"} {:checksum "41"} NoChangeAndCorrect()
+{
+  assert true;
+}
diff --git a/Test/snapshots/Snapshots41.v1.bpl b/Test/snapshots/Snapshots41.v1.bpl
new file mode 100644
index 00000000..9864e0e4
--- /dev/null
+++ b/Test/snapshots/Snapshots41.v1.bpl
@@ -0,0 +1,39 @@
+procedure {:checksum "0"} M(x: int);
+implementation {:id "M"} {:checksum "1"} M(x: int)
+{
+assert x < 20 || 10 <= x;  // always true
+  
+       assert x < 10;  // error
+  call Other(x);  // error: precondition violation
+  assert x == 7;  // error: this is a new error in v1
+}
+
+
+       procedure {:checksum "10"} Other(y: int);
+         requires 0 <= y;
+       implementation {:id "Other"} {:checksum "11"} Other(y: int)
+       {
+       }
+
+
+
+procedure {:checksum "20"} Posty() returns (z: int);
+  ensures 2 <= z;  // error: postcondition violation
+implementation {:id "Posty"} {:checksum "21"} Posty() returns (z: int)
+{
+  var t: int;
+  t := 20;
+  if (t < z) {
+    assert true;  // this is a new assert
+  } else {  // the postcondition violation occurs on this 'else' branch
+  }
+}
+
+  procedure   {:checksum "30"} NoChangeWhazzoeva(u: int);
+  implementation {:id "NoChangeWhazzoeva"} {:checksum "3"} NoChangeWhazzoeva(u: int)
+  {
+       assert u != 53;  // error
+  }
+
+procedure {:checksum "40"} NoChangeAndCorrect();
+implementation {:id "NoChangeAndCorrect"} {:checksum "41"} NoChangeAndCorrect() { assert true; }
diff --git a/Test/snapshots/Snapshots5.v0.bpl b/Test/snapshots/Snapshots5.v0.bpl
index b8652c7b..ea59bed5 100644
--- a/Test/snapshots/Snapshots5.v0.bpl
+++ b/Test/snapshots/Snapshots5.v0.bpl
@@ -1,11 +1,11 @@
-procedure {:checksum "P0$proc#0"} P0(n: int where F(n));
-// Action: verify
-implementation {:id "P0"} {:checksum "P0$impl#0"} P0(n: int)
-{
-    assert false;
-}
-
-function {:checksum "F#1"} F(n: int) : bool
-{
-    false
-}
+procedure {:checksum "P0$proc#0"} P0(n: int where F(n));
+// Action: verify
+implementation {:id "P0"} {:checksum "P0$impl#0"} P0(n: int)
+{
+    assert false;
+}
+
+function {:checksum "F#1"} F(n: int) : bool
+{
+    false
+}
diff --git a/Test/snapshots/Snapshots5.v1.bpl b/Test/snapshots/Snapshots5.v1.bpl
index b42b1576..12895df6 100644
--- a/Test/snapshots/Snapshots5.v1.bpl
+++ b/Test/snapshots/Snapshots5.v1.bpl
@@ -1,11 +1,11 @@
-procedure {:checksum "P0$proc#0"} P0(n: int where F(n));
-// Action: verify
-implementation {:id "P0"} {:checksum "P0$impl#0"} P0(n: int)
-{
-    assert false;
-}
-
-function {:checksum "F#0"} F(n: int) : bool
-{
-    true
-}
+procedure {:checksum "P0$proc#0"} P0(n: int where F(n));
+// Action: verify
+implementation {:id "P0"} {:checksum "P0$impl#0"} P0(n: int)
+{
+    assert false;
+}
+
+function {:checksum "F#0"} F(n: int) : bool
+{
+    true
+}
diff --git a/Test/snapshots/Snapshots6.v0.bpl b/Test/snapshots/Snapshots6.v0.bpl
index bdf9c14a..f255c020 100644
--- a/Test/snapshots/Snapshots6.v0.bpl
+++ b/Test/snapshots/Snapshots6.v0.bpl
@@ -1,17 +1,17 @@
-var x: int;
-var y: int;
-
-procedure {:checksum "0"} M();
-  modifies x, y;
-
-implementation {:id "M"} {:checksum "1"} M()
-{
-    y := 0;
-
-    call N();
-
-    assert y == 0;
-}
-
-procedure {:checksum "2"} N();
-  modifies x;
+var x: int;
+var y: int;
+
+procedure {:checksum "0"} M();
+  modifies x, y;
+
+implementation {:id "M"} {:checksum "1"} M()
+{
+    y := 0;
+
+    call N();
+
+    assert y == 0;
+}
+
+procedure {:checksum "2"} N();
+  modifies x;
diff --git a/Test/snapshots/Snapshots6.v1.bpl b/Test/snapshots/Snapshots6.v1.bpl
index be8b699d..73e280d2 100644
--- a/Test/snapshots/Snapshots6.v1.bpl
+++ b/Test/snapshots/Snapshots6.v1.bpl
@@ -1,18 +1,18 @@
-var x: int;
-var y: int;
-
-procedure {:checksum "0"} M();
-  modifies x, y;
-
-implementation {:id "M"} {:checksum "1"} M()
-{
-    y := 0;
-
-    call N();
-
-    assert y == 0;
-}
-
-procedure {:checksum "3"} N();
-  // Change: more modified variables
-  modifies x, y;
+var x: int;
+var y: int;
+
+procedure {:checksum "0"} M();
+  modifies x, y;
+
+implementation {:id "M"} {:checksum "1"} M()
+{
+    y := 0;
+
+    call N();
+
+    assert y == 0;
+}
+
+procedure {:checksum "3"} N();
+  // Change: more modified variables
+  modifies x, y;
diff --git a/Test/snapshots/Snapshots7.v0.bpl b/Test/snapshots/Snapshots7.v0.bpl
index 6e0932c8..400b209c 100644
--- a/Test/snapshots/Snapshots7.v0.bpl
+++ b/Test/snapshots/Snapshots7.v0.bpl
@@ -1,19 +1,19 @@
-var x: int;
-var y: int;
-var z: int;
-
-procedure {:checksum "0"} M();
-  modifies x, y, z;
-
-implementation {:id "M"} {:checksum "1"} M()
-{
-    z := 0;
-
-    call N();
-
-    assert y < 0;
-}
-
-procedure {:checksum "2"} N();
-  modifies x, y;
-  ensures y < z;
+var x: int;
+var y: int;
+var z: int;
+
+procedure {:checksum "0"} M();
+  modifies x, y, z;
+
+implementation {:id "M"} {:checksum "1"} M()
+{
+    z := 0;
+
+    call N();
+
+    assert y < 0;
+}
+
+procedure {:checksum "2"} N();
+  modifies x, y;
+  ensures y < z;
diff --git a/Test/snapshots/Snapshots7.v1.bpl b/Test/snapshots/Snapshots7.v1.bpl
index 8700e91c..ad3f1f27 100644
--- a/Test/snapshots/Snapshots7.v1.bpl
+++ b/Test/snapshots/Snapshots7.v1.bpl
@@ -1,20 +1,20 @@
-var x: int;
-var y: int;
-var z: int;
-
-procedure {:checksum "0"} M();
-  modifies x, y, z;
-
-implementation {:id "M"} {:checksum "1"} M()
-{
-    z := 0;
-
-    call N();
-
-    assert y < 0;
-}
-
-procedure {:checksum "3"} N();
-  // Change: fewer modified variables
-  modifies x;
-  ensures y < z;
+var x: int;
+var y: int;
+var z: int;
+
+procedure {:checksum "0"} M();
+  modifies x, y, z;
+
+implementation {:id "M"} {:checksum "1"} M()
+{
+    z := 0;
+
+    call N();
+
+    assert y < 0;
+}
+
+procedure {:checksum "3"} N();
+  // Change: fewer modified variables
+  modifies x;
+  ensures y < z;
diff --git a/Test/snapshots/Snapshots8.v0.bpl b/Test/snapshots/Snapshots8.v0.bpl
index 73dcd9aa..0d33d81a 100644
--- a/Test/snapshots/Snapshots8.v0.bpl
+++ b/Test/snapshots/Snapshots8.v0.bpl
@@ -1,15 +1,15 @@
-procedure {:checksum "0"} M(n: int);
-  requires 0 < n;
-
-implementation {:id "M"} {:checksum "1"} M(n: int)
-{
-    var x: int;
-
-    call x := N(n);
-
-    assert 0 <= x;
-}
-
-procedure {:checksum "2"} N(n: int) returns (r: int);
-  requires 0 < n;
-  ensures 0 < r;
+procedure {:checksum "0"} M(n: int);
+  requires 0 < n;
+
+implementation {:id "M"} {:checksum "1"} M(n: int)
+{
+    var x: int;
+
+    call x := N(n);
+
+    assert 0 <= x;
+}
+
+procedure {:checksum "2"} N(n: int) returns (r: int);
+  requires 0 < n;
+  ensures 0 < r;
diff --git a/Test/snapshots/Snapshots8.v1.bpl b/Test/snapshots/Snapshots8.v1.bpl
index de241c24..a886d3bd 100644
--- a/Test/snapshots/Snapshots8.v1.bpl
+++ b/Test/snapshots/Snapshots8.v1.bpl
@@ -1,16 +1,16 @@
-procedure {:checksum "0"} M(n: int);
-  requires 0 < n;
-
-implementation {:id "M"} {:checksum "1"} M(n: int)
-{
-    var x: int;
-
-    call x := N(n);
-
-    assert 0 <= x;
-}
-
-procedure {:checksum "3"} N(n: int) returns (r: int);
-  requires 0 < n;
-  // Change: stronger postcondition
-  ensures 42 < r;
+procedure {:checksum "0"} M(n: int);
+  requires 0 < n;
+
+implementation {:id "M"} {:checksum "1"} M(n: int)
+{
+    var x: int;
+
+    call x := N(n);
+
+    assert 0 <= x;
+}
+
+procedure {:checksum "3"} N(n: int) returns (r: int);
+  requires 0 < n;
+  // Change: stronger postcondition
+  ensures 42 < r;
diff --git a/Test/snapshots/Snapshots9.v0.bpl b/Test/snapshots/Snapshots9.v0.bpl
index 5b2cf68c..58839cbc 100644
--- a/Test/snapshots/Snapshots9.v0.bpl
+++ b/Test/snapshots/Snapshots9.v0.bpl
@@ -1,17 +1,17 @@
-procedure {:checksum "0"} M(n: int);
-  requires 0 < n;
-
-implementation {:id "M"} {:checksum "1"} M(n: int)
-{
-    var x: int;
-
-    call x := N(n);
-
-    assert 0 <= x;
-}
-
-procedure {:checksum "2"} N(n: int) returns (r: int);
-  requires 0 < n;
-  requires true;
-  ensures 0 < r;
-  ensures true;
+procedure {:checksum "0"} M(n: int);
+  requires 0 < n;
+
+implementation {:id "M"} {:checksum "1"} M(n: int)
+{
+    var x: int;
+
+    call x := N(n);
+
+    assert 0 <= x;
+}
+
+procedure {:checksum "2"} N(n: int) returns (r: int);
+  requires 0 < n;
+  requires true;
+  ensures 0 < r;
+  ensures true;
diff --git a/Test/snapshots/Snapshots9.v1.bpl b/Test/snapshots/Snapshots9.v1.bpl
index d1886a6d..c35653fe 100644
--- a/Test/snapshots/Snapshots9.v1.bpl
+++ b/Test/snapshots/Snapshots9.v1.bpl
@@ -1,16 +1,16 @@
-procedure {:checksum "0"} M(n: int);
-  requires 0 < n;
-
-implementation {:id "M"} {:checksum "1"} M(n: int)
-{
-    var x: int;
-
-    call x := N(n);
-
-    assert 0 <= x;
-}
-
-procedure {:checksum "3"} N(n: int) returns (r: int);
-  requires 0 < n;
-  // Change: weaker postcondition
-  ensures 0 <= r;
+procedure {:checksum "0"} M(n: int);
+  requires 0 < n;
+
+implementation {:id "M"} {:checksum "1"} M(n: int)
+{
+    var x: int;
+
+    call x := N(n);
+
+    assert 0 <= x;
+}
+
+procedure {:checksum "3"} N(n: int) returns (r: int);
+  requires 0 < n;
+  // Change: weaker postcondition
+  ensures 0 <= r;
diff --git a/Test/snapshots/runtest.AI.snapshot b/Test/snapshots/runtest.AI.snapshot
index 51de91e8..116920b5 100644
--- a/Test/snapshots/runtest.AI.snapshot
+++ b/Test/snapshots/runtest.AI.snapshot
@@ -1,2 +1,2 @@
-// RUN: %boogie -errorTrace:0 -traceCaching:1 -verifySnapshots:2 -verifySeparately Snapshots29.bpl > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %boogie -errorTrace:0 -traceCaching:1 -verifySnapshots:2 -verifySeparately Snapshots29.bpl > "%t"
+// RUN: %diff "%s.expect" "%t"
diff --git a/Test/snapshots/runtest.AI.snapshot.expect b/Test/snapshots/runtest.AI.snapshot.expect
index 7b0288bb..f9e4dc32 100644
--- a/Test/snapshots/runtest.AI.snapshot.expect
+++ b/Test/snapshots/runtest.AI.snapshot.expect
@@ -1,9 +1,9 @@
-Processing command (at Snapshots29.v0.bpl(14,5)) assert i == 0;
-  >>> DoNothingToAssert
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing command (at Snapshots29.v1.bpl(14,5)) assert i == 0;
-  >>> DoNothingToAssert
-Snapshots29.v1.bpl(14,5): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots29.v0.bpl(14,5)) assert i == 0;
+  >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing command (at Snapshots29.v1.bpl(14,5)) assert i == 0;
+  >>> DoNothingToAssert
+Snapshots29.v1.bpl(14,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/snapshots/runtest.snapshot b/Test/snapshots/runtest.snapshot
index a203ffac..1d6e7c95 100644
--- a/Test/snapshots/runtest.snapshot
+++ b/Test/snapshots/runtest.snapshot
@@ -1,2 +1,3 @@
-// RUN: %boogie -errorTrace:0 -traceCaching:1 -verifySnapshots:2 -verifySeparately -noinfer Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl Snapshots6.bpl Snapshots7.bpl Snapshots8.bpl Snapshots9.bpl Snapshots10.bpl Snapshots11.bpl Snapshots12.bpl Snapshots13.bpl Snapshots14.bpl Snapshots15.bpl Snapshots16.bpl Snapshots17.bpl Snapshots18.bpl Snapshots19.bpl Snapshots20.bpl Snapshots21.bpl Snapshots22.bpl Snapshots23.bpl Snapshots24.bpl Snapshots25.bpl Snapshots26.bpl Snapshots27.bpl Snapshots28.bpl Snapshots30.bpl Snapshots31.bpl Snapshots32.bpl Snapshots33.bpl > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %boogie -errorTrace:0 -traceCaching:1 -verifySnapshots:2 -verifySeparately -noinfer Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl Snapshots6.bpl Snapshots7.bpl Snapshots8.bpl Snapshots9.bpl Snapshots10.bpl Snapshots11.bpl Snapshots12.bpl Snapshots13.bpl Snapshots14.bpl Snapshots15.bpl Snapshots16.bpl Snapshots17.bpl Snapshots18.bpl Snapshots19.bpl Snapshots20.bpl Snapshots21.bpl Snapshots22.bpl Snapshots23.bpl Snapshots24.bpl Snapshots25.bpl Snapshots26.bpl Snapshots27.bpl Snapshots28.bpl Snapshots30.bpl Snapshots31.bpl Snapshots32.bpl Snapshots33.bpl Snapshots34.bpl Snapshots35.bpl Snapshots36.bpl Snapshots37.bpl Snapshots38.bpl Snapshots39.bpl Snapshots40.bpl > "%t"
+// RUN: %boogie -errorTrace:0 -traceCaching:1 -verifySnapshots:3 -verifySeparately -noinfer Snapshots41.bpl >> "%t"
+// RUN: %diff "%s.expect" "%t"
diff --git a/Test/snapshots/runtest.snapshot.expect b/Test/snapshots/runtest.snapshot.expect
index 8f3c2015..393c9330 100644
--- a/Test/snapshots/runtest.snapshot.expect
+++ b/Test/snapshots/runtest.snapshot.expect
@@ -1,600 +1,810 @@
-Processing command (at Snapshots0.v0.bpl(41,5)) assert false;
-  >>> DoNothingToAssert
-Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold.
-Processing command (at Snapshots0.v0.bpl(8,5)) assert false;
-  >>> DoNothingToAssert
-Snapshots0.v0.bpl(8,5): Error BP5001: This assertion might not hold.
-Processing command (at Snapshots0.v0.bpl(19,5)) assert false;
-  >>> DoNothingToAssert
-Snapshots0.v0.bpl(19,5): Error BP5001: This assertion might not hold.
-Processing command (at Snapshots0.v0.bpl(30,5)) assert false;
-  >>> DoNothingToAssert
-Snapshots0.v0.bpl(30,5): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 4 errors
-Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold.
-Processing command (at Snapshots0.v1.bpl(19,5)) assert true;
-  >>> DoNothingToAssert
-Processing command (at Snapshots0.v1.bpl(30,5)) assert false;
-  >>> DoNothingToAssert
-Snapshots0.v1.bpl(30,5): Error BP5001: This assertion might not hold.
-Processing command (at Snapshots0.v1.bpl(41,5)) assert true;
-  >>> DoNothingToAssert
-
-Boogie program verifier finished with 2 verified, 2 errors
-Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold.
-Processing command (at Snapshots0.v2.bpl(19,5)) assert true;
-  >>> DoNothingToAssert
-Processing command (at Snapshots0.v2.bpl(30,5)) assert true;
-  >>> DoNothingToAssert
-
-Boogie program verifier finished with 2 verified, 1 error
-Processing command (at Snapshots1.v0.bpl(13,5)) assert 1 != 1;
-  >>> DoNothingToAssert
-Snapshots1.v0.bpl(13,5): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 1 verified, 1 error
-Processing command (at Snapshots1.v1.bpl(13,5)) assert 2 != 2;
-  >>> DoNothingToAssert
-Snapshots1.v1.bpl(13,5): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 1 verified, 1 error
-Processing call to procedure P2 in implementation P1 (at Snapshots1.v2.bpl(5,5)):
-Processing command (at Snapshots1.v2.bpl(5,5)) assert false;
-  >>> DoNothingToAssert
-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.
-Processing command (at Snapshots1.v2.bpl(14,5)) assert 2 != 2;
-  >>> DoNothingToAssert
-
-Boogie program verifier finished with 1 verified, 1 error
-
-Boogie program verifier finished with 1 verified, 0 errors
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing call to procedure P0 in implementation P0 (at Snapshots2.v2.bpl(6,5)):
-Processing command (at Snapshots2.v2.bpl(6,5)) assert F0();
-  >>> DoNothingToAssert
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing call to procedure P0 in implementation P0 (at Snapshots2.v3.bpl(6,5)):
-  >>> added after: a##post##0 := a##post##0 && false;
-Processing command (at Snapshots2.v3.bpl(6,5)) assert F0();
-  >>> DoNothingToAssert
-
-Boogie program verifier finished with 1 verified, 0 errors
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing call to procedure P0 in implementation P0 (at Snapshots2.v5.bpl(7,5)):
-  >>> added axiom: ##extracted_function##1() == F0()
-  >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1();
-Processing command (at Snapshots2.v5.bpl(7,5)) assume {:precondition_previous_snapshot} ##extracted_function##1();
-  >>> MarkAsFullyVerified
-Processing command (at Snapshots2.v5.bpl(7,5)) assert F0();
-  >>> MarkAsFullyVerified
-Processing command (at Snapshots2.v5.bpl(3,1)) assert F0();
-  >>> MarkAsFullyVerified
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing command (at Snapshots3.v0.bpl(2,1)) assert G();
-  >>> DoNothingToAssert
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing command (at Snapshots3.v1.bpl(2,1)) assert G();
-  >>> DoNothingToAssert
-Snapshots3.v1.bpl(6,1): Error BP5003: A postcondition might not hold on this return path.
-Snapshots3.v1.bpl(2,1): Related location: This is the postcondition that might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-
-Boogie program verifier finished with 3 verified, 0 errors
-Processing call to procedure P2 in implementation P1 (at Snapshots4.v1.bpl(14,5)):
-  >>> added after: a##post##0 := a##post##0 && false;
-Processing command (at Snapshots4.v1.bpl(23,5)) assert false;
-  >>> DoNothingToAssert
-Snapshots4.v1.bpl(23,5): Error BP5001: This assertion might not hold.
-Processing command (at Snapshots4.v1.bpl(28,3)) assert G();
-  >>> DoNothingToAssert
-Snapshots4.v1.bpl(33,1): Error BP5003: A postcondition might not hold on this return path.
-Snapshots4.v1.bpl(28,3): Related location: This is the postcondition that might not hold.
-
-Boogie program verifier finished with 2 verified, 2 errors
-Processing command (at Snapshots5.v0.bpl(5,5)) assert false;
-  >>> DoNothingToAssert
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing command (at Snapshots5.v1.bpl(5,5)) assert false;
-  >>> DoNothingToAssert
-Snapshots5.v1.bpl(5,5): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing command (at Snapshots6.v0.bpl(13,5)) assert y == 0;
-  >>> DoNothingToAssert
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing call to procedure N in implementation M (at Snapshots6.v1.bpl(11,5)):
-  >>> added axiom: (forall y##old##0: int, y: int :: {:weight 30} { ##extracted_function##1(y##old##0, y) } ##extracted_function##1(y##old##0, y) == (y##old##0 == y))
-  >>> added before: y##old##0 := y;
-  >>> added after: a##post##0 := a##post##0 && ##extracted_function##1(y##old##0, y);
-Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##1(y##old##0, y);
-  >>> AssumeNegationOfAssumptionVariable
-Processing command (at Snapshots6.v1.bpl(13,5)) assert y == 0;
-  >>> MarkAsPartiallyVerified
-Snapshots6.v1.bpl(13,5): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing command (at Snapshots7.v0.bpl(14,5)) assert y < 0;
-  >>> DoNothingToAssert
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing call to procedure N in implementation M (at Snapshots7.v1.bpl(12,5)):
-  >>> added axiom: (forall y: int, z: int :: {:weight 30} { ##extracted_function##1(y, z) } ##extracted_function##1(y, z) == (y < z))
-  >>> added before: y##old##0 := y;
-  >>> added after: a##post##0 := a##post##0 && ##extracted_function##1(y, z);
-Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##1(y, z);
-  >>> AssumeNegationOfAssumptionVariable
-Processing command (at Snapshots7.v1.bpl(14,5)) assert y < 0;
-  >>> MarkAsPartiallyVerified
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing command (at Snapshots8.v0.bpl(8,5)) assert 0 < call0formal#AT#n;
-  >>> DoNothingToAssert
-Processing command (at Snapshots8.v0.bpl(10,5)) assert 0 <= x;
-  >>> DoNothingToAssert
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing call to procedure N in implementation M (at Snapshots8.v1.bpl(8,5)):
-  >>> added axiom: (forall call0formal#AT#n: int :: {:weight 30} { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 < call0formal#AT#n))
-  >>> added axiom: (forall call1formal#AT#r: int :: {:weight 30} { ##extracted_function##2(call1formal#AT#r) } ##extracted_function##2(call1formal#AT#r) == (0 < call1formal#AT#r))
-  >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
-  >>> added after: a##post##0 := a##post##0 && ##extracted_function##2(call1formal#AT#r);
-Processing command (at Snapshots8.v1.bpl(8,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
-  >>> MarkAsFullyVerified
-Processing command (at Snapshots8.v1.bpl(8,5)) assert 0 < call0formal#AT#n;
-  >>> MarkAsFullyVerified
-Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##2(call1formal#AT#r);
-  >>> AssumeNegationOfAssumptionVariable
-Processing command (at Snapshots8.v1.bpl(10,5)) assert 0 <= x;
-  >>> MarkAsPartiallyVerified
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing command (at Snapshots9.v0.bpl(8,5)) assert 0 < call0formal#AT#n;
-  >>> DoNothingToAssert
-Processing command (at Snapshots9.v0.bpl(8,5)) assert true;
-  >>> DoNothingToAssert
-Processing command (at Snapshots9.v0.bpl(10,5)) assert 0 <= x;
-  >>> DoNothingToAssert
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing call to procedure N in implementation M (at Snapshots9.v1.bpl(8,5)):
-  >>> added axiom: (forall call0formal#AT#n: int :: {:weight 30} { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 < call0formal#AT#n && true))
-  >>> added axiom: (forall call1formal#AT#r: int :: {:weight 30} { ##extracted_function##2(call1formal#AT#r) } ##extracted_function##2(call1formal#AT#r) == (0 < call1formal#AT#r && true))
-  >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
-  >>> added after: a##post##0 := a##post##0 && ##extracted_function##2(call1formal#AT#r);
-Processing command (at Snapshots9.v1.bpl(8,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
-  >>> MarkAsFullyVerified
-Processing command (at Snapshots9.v1.bpl(8,5)) assert 0 < call0formal#AT#n;
-  >>> MarkAsFullyVerified
-Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##2(call1formal#AT#r);
-  >>> AssumeNegationOfAssumptionVariable
-Processing command (at Snapshots9.v1.bpl(10,5)) assert 0 <= x;
-  >>> MarkAsPartiallyVerified
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing command (at Snapshots10.v0.bpl(8,5)) assert 0 < call0formal#AT#n;
-  >>> DoNothingToAssert
-Processing command (at Snapshots10.v0.bpl(12,5)) assert 0 <= x;
-  >>> DoNothingToAssert
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing call to procedure N in implementation M (at Snapshots10.v1.bpl(8,5)):
-  >>> added axiom: (forall call0formal#AT#n: int :: {:weight 30} { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 < call0formal#AT#n))
-  >>> added axiom: (forall call1formal#AT#r: int :: {:weight 30} { ##extracted_function##2(call1formal#AT#r) } ##extracted_function##2(call1formal#AT#r) == (0 < call1formal#AT#r))
-  >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
-  >>> added after: a##post##0 := a##post##0 && ##extracted_function##2(call1formal#AT#r);
-Processing command (at Snapshots10.v1.bpl(8,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
-  >>> MarkAsFullyVerified
-Processing command (at Snapshots10.v1.bpl(8,5)) assert 0 < call0formal#AT#n;
-  >>> MarkAsFullyVerified
-Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##2(call1formal#AT#r);
-  >>> AssumeNegationOfAssumptionVariable
-Processing command (at Snapshots10.v1.bpl(12,5)) assert 0 <= x;
-  >>> MarkAsPartiallyVerified
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing command (at Snapshots11.v0.bpl(7,5)) assert 0 < call0formal#AT#n;
-  >>> DoNothingToAssert
-Processing command (at Snapshots11.v0.bpl(9,5)) assert 0 <= x;
-  >>> DoNothingToAssert
-Snapshots11.v0.bpl(7,5): Error BP5002: A precondition for this call might not hold.
-Snapshots11.v0.bpl(13,3): Related location: This is the precondition that might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing call to procedure N in implementation M (at Snapshots11.v1.bpl(7,5)):
-  >>> added axiom: (forall call0formal#AT#n: int :: {:weight 30} { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 < call0formal#AT#n))
-  >>> added axiom: (forall call1formal#AT#r: int :: {:weight 30} { ##extracted_function##2(call1formal#AT#r) } ##extracted_function##2(call1formal#AT#r) == (0 < call1formal#AT#r))
-  >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
-  >>> added after: a##post##0 := a##post##0 && ##extracted_function##2(call1formal#AT#r);
-Processing command (at Snapshots11.v1.bpl(7,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
-  >>> DropAssume
-Processing command (at Snapshots11.v1.bpl(7,5)) assert 0 < call0formal#AT#n;
-  >>> RecycleError
-Processing command (at Snapshots11.v1.bpl(9,5)) assert 0 <= x;
-  >>> MarkAsPartiallyVerified
-Snapshots11.v0.bpl(7,5): Error BP5002: A precondition for this call might not hold.
-Snapshots11.v0.bpl(13,3): Related location: This is the precondition that might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing command (at Snapshots12.v0.bpl(7,5)) assert false;
-  >>> DoNothingToAssert
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing call to procedure N in implementation M (at Snapshots12.v1.bpl(5,5)):
-  >>> added after: a##post##0 := a##post##0 && false;
-Processing command (at Snapshots12.v1.bpl(7,5)) assert false;
-  >>> DoNothingToAssert
-Snapshots12.v1.bpl(7,5): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing command (at Snapshots13.v0.bpl(7,5)) assert false;
-  >>> DoNothingToAssert
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing call to procedure N in implementation M (at Snapshots13.v1.bpl(5,5)):
-  >>> added after: a##post##0 := a##post##0 && false;
-Processing command (at Snapshots13.v1.bpl(7,5)) assert false;
-  >>> DoNothingToAssert
-Snapshots13.v1.bpl(7,5): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing command (at Snapshots14.v0.bpl(7,5)) assert false;
-  >>> DoNothingToAssert
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing call to procedure N in implementation M (at Snapshots14.v1.bpl(5,5)):
-  >>> added axiom: ##extracted_function##1() == (F() && G())
-  >>> added after: a##post##0 := a##post##0 && ##extracted_function##1();
-Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##1();
-  >>> AssumeNegationOfAssumptionVariable
-Processing command (at Snapshots14.v1.bpl(7,5)) assert false;
-  >>> MarkAsPartiallyVerified
-Snapshots14.v1.bpl(7,5): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing command (at Snapshots15.v0.bpl(5,5)) assert true;
-  >>> DoNothingToAssert
-Processing command (at Snapshots15.v0.bpl(9,5)) assert true;
-  >>> DoNothingToAssert
-Processing command (at Snapshots15.v0.bpl(13,5)) assert false;
-  >>> DoNothingToAssert
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing call to procedure N in implementation M (at Snapshots15.v1.bpl(7,5)):
-  >>> added after: a##post##0 := a##post##0 && false;
-Processing call to procedure N in implementation M (at Snapshots15.v1.bpl(11,5)):
-  >>> added after: a##post##1 := a##post##1 && false;
-Processing command (at Snapshots15.v1.bpl(5,5)) assert true;
-  >>> MarkAsFullyVerified
-Processing command (at Snapshots15.v1.bpl(9,5)) assert true;
-  >>> MarkAsPartiallyVerified
-Processing command (at Snapshots15.v1.bpl(13,5)) assert false;
-  >>> MarkAsPartiallyVerified
-Snapshots15.v1.bpl(13,5): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing command (at Snapshots16.v0.bpl(14,5)) assert F(0) == 1;
-  >>> DoNothingToAssert
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing command (at Snapshots16.v1.bpl(14,5)) assert F(0) == 1;
-  >>> DoNothingToAssert
-Snapshots16.v1.bpl(14,5): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing command (at Snapshots17.v0.bpl(28,5)) assert true;
-  >>> DoNothingToAssert
-Processing command (at Snapshots17.v0.bpl(25,9)) assert false;
-  >>> DoNothingToAssert
-Processing command (at Snapshots17.v0.bpl(12,13)) assert true;
-  >>> DoNothingToAssert
-Processing command (at Snapshots17.v0.bpl(20,13)) assert x == 1;
-  >>> DoNothingToAssert
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing call to procedure N in implementation M (at Snapshots17.v1.bpl(14,13)):
-  >>> added after: a##post##0 := a##post##0 && false;
-Processing call to procedure N in implementation M (at Snapshots17.v1.bpl(16,13)):
-  >>> added after: a##post##1 := a##post##1 && false;
-Processing call to procedure N in implementation M (at Snapshots17.v1.bpl(23,9)):
-  >>> added after: a##post##2 := a##post##2 && false;
-Processing command (at Snapshots17.v1.bpl(28,5)) assert true;
-  >>> MarkAsFullyVerified
-Processing command (at Snapshots17.v1.bpl(25,9)) assert false;
-  >>> MarkAsPartiallyVerified
-Processing command (at Snapshots17.v1.bpl(12,13)) assert true;
-  >>> MarkAsFullyVerified
-Processing command (at Snapshots17.v1.bpl(20,13)) assert x == 1;
-  >>> MarkAsPartiallyVerified
-Snapshots17.v1.bpl(20,13): Error BP5001: This assertion might not hold.
-Snapshots17.v1.bpl(25,9): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 2 errors
-Processing command (at Snapshots18.v0.bpl(7,9)) assert 0 == 0;
-  >>> DoNothingToAssert
-Processing command (at Snapshots18.v0.bpl(17,9)) assert 1 != 1;
-  >>> DoNothingToAssert
-Processing command (at Snapshots18.v0.bpl(20,5)) assert 2 != 2;
-  >>> DoNothingToAssert
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing call to procedure N in implementation M (at Snapshots18.v1.bpl(9,9)):
-  >>> added after: a##post##0 := a##post##0 && false;
-Processing call to procedure N in implementation M (at Snapshots18.v1.bpl(10,9)):
-  >>> added after: a##post##1 := a##post##1 && false;
-Processing command (at Snapshots18.v1.bpl(7,9)) assert 0 == 0;
-  >>> MarkAsFullyVerified
-Processing command (at Snapshots18.v1.bpl(17,9)) assert 1 != 1;
-  >>> MarkAsPartiallyVerified
-Processing command (at Snapshots18.v1.bpl(20,5)) assert 2 != 2;
-  >>> MarkAsPartiallyVerified
-Snapshots18.v1.bpl(17,9): Error BP5001: This assertion might not hold.
-Snapshots18.v1.bpl(20,5): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 2 errors
-Processing command (at Snapshots19.v0.bpl(5,5)) assert 2 == 2;
-  >>> DoNothingToAssert
-Processing command (at Snapshots19.v0.bpl(7,5)) assert 1 != 1;
-  >>> DoNothingToAssert
-Snapshots19.v0.bpl(7,5): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing call to procedure N in implementation M (at Snapshots19.v1.bpl(5,5)):
-  >>> added axiom: ##extracted_function##1() == (2 == 2)
-  >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1();
-Processing command (at Snapshots19.v1.bpl(5,5)) assume {:precondition_previous_snapshot} ##extracted_function##1();
-  >>> MarkAsFullyVerified
-Processing command (at Snapshots19.v1.bpl(5,5)) assert 2 == 2;
-  >>> MarkAsFullyVerified
-Processing command (at Snapshots19.v1.bpl(7,5)) assert 1 != 1;
-  >>> RecycleError
-Snapshots19.v0.bpl(7,5): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing command (at Snapshots20.v0.bpl(9,9)) assert 1 != 1;
-  >>> DoNothingToAssert
-Processing command (at Snapshots20.v0.bpl(13,9)) assert 2 != 2;
-  >>> DoNothingToAssert
-Processing command (at Snapshots20.v0.bpl(16,5)) assert 3 != 3;
-  >>> DoNothingToAssert
-Snapshots20.v0.bpl(13,9): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing call to procedure N in implementation M (at Snapshots20.v1.bpl(7,9)):
-  >>> added axiom: ##extracted_function##1() == (0 != 0)
-  >>> added after: a##post##0 := a##post##0 && ##extracted_function##1();
-Processing command (at Snapshots20.v1.bpl(9,9)) assert 1 != 1;
-  >>> MarkAsPartiallyVerified
-Processing command (at Snapshots20.v1.bpl(13,9)) assert 2 != 2;
-  >>> RecycleError
-Processing command (at Snapshots20.v1.bpl(16,5)) assert 3 != 3;
-  >>> MarkAsPartiallyVerified
-Snapshots20.v1.bpl(9,9): Error BP5001: This assertion might not hold.
-Snapshots20.v0.bpl(13,9): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 2 errors
-Processing command (at Snapshots21.v0.bpl(7,9)) assert 1 != 1;
-  >>> DoNothingToAssert
-Processing command (at Snapshots21.v0.bpl(11,9)) assert 2 != 2;
-  >>> DoNothingToAssert
-Processing command (at Snapshots21.v0.bpl(14,5)) assert 3 != 3;
-  >>> DoNothingToAssert
-Snapshots21.v0.bpl(7,9): Error BP5001: This assertion might not hold.
-Snapshots21.v0.bpl(11,9): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 2 errors
-Processing command (at Snapshots21.v1.bpl(7,9)) assert 1 == 1;
-  >>> DoNothingToAssert
-Processing command (at Snapshots21.v1.bpl(11,9)) assert 2 != 2;
-  >>> RecycleError
-Processing command (at Snapshots21.v1.bpl(14,5)) assert 3 != 3;
-  >>> DoNothingToAssert
-Snapshots21.v0.bpl(11,9): Error BP5001: This assertion might not hold.
-Snapshots21.v1.bpl(14,5): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 2 errors
-Processing command (at Snapshots22.v0.bpl(7,9)) assert 1 != 1;
-  >>> DoNothingToAssert
-Processing command (at Snapshots22.v0.bpl(11,9)) assert 2 == 2;
-  >>> DoNothingToAssert
-Processing command (at Snapshots22.v0.bpl(14,5)) assert 3 == 3;
-  >>> DoNothingToAssert
-Snapshots22.v0.bpl(7,9): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing command (at Snapshots22.v1.bpl(7,9)) assert 1 == 1;
-  >>> DoNothingToAssert
-Processing command (at Snapshots22.v1.bpl(11,9)) assert 2 == 2;
-  >>> MarkAsFullyVerified
-Processing command (at Snapshots22.v1.bpl(14,5)) assert 3 == 3;
-  >>> DoNothingToAssert
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing command (at Snapshots23.v0.bpl(7,9)) assert 1 != 1;
-  >>> DoNothingToAssert
-Processing command (at Snapshots23.v0.bpl(11,9)) assert 2 == 2;
-  >>> DoNothingToAssert
-Processing command (at Snapshots23.v0.bpl(14,5)) assert 3 == 3;
-  >>> DoNothingToAssert
-Snapshots23.v0.bpl(7,9): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 1 verified, 1 error
-Snapshots23.v0.bpl(7,9): Error BP5001: This assertion might not hold.
-Processing command (at Snapshots23.v1.bpl(22,5)) assert 4 == 4;
-  >>> DoNothingToAssert
-
-Boogie program verifier finished with 1 verified, 1 error
-Processing command (at Snapshots23.v2.bpl(8,9)) assert 1 != 1;
-  >>> RecycleError
-Processing command (at Snapshots23.v2.bpl(12,9)) assert 2 == 2;
-  >>> MarkAsFullyVerified
-Snapshots23.v0.bpl(7,9): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 1 verified, 1 error
-Processing command (at Snapshots24.v0.bpl(7,9)) assert {:subsumption 0} 1 != 1;
-  >>> DoNothingToAssert
-Processing command (at Snapshots24.v0.bpl(11,9)) assert {:subsumption 1} 5 != 5;
-  >>> DoNothingToAssert
-Processing command (at Snapshots24.v0.bpl(15,9)) assert {:subsumption 2} 6 != 6;
-  >>> DoNothingToAssert
-Processing command (at Snapshots24.v0.bpl(19,9)) assert {:subsumption 1} 2 == 2;
-  >>> DoNothingToAssert
-Processing command (at Snapshots24.v0.bpl(20,9)) assert {:subsumption 2} 4 == 4;
-  >>> DoNothingToAssert
-Processing command (at Snapshots24.v0.bpl(21,9)) assert 5 == 5;
-  >>> DoNothingToAssert
-Processing command (at Snapshots24.v0.bpl(24,5)) assert {:subsumption 0} 3 == 3;
-  >>> DoNothingToAssert
-Snapshots24.v0.bpl(7,9): Error BP5001: This assertion might not hold.
-Snapshots24.v0.bpl(11,9): Error BP5001: This assertion might not hold.
-Snapshots24.v0.bpl(15,9): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 3 errors
-Processing command (at Snapshots24.v1.bpl(7,9)) assert {:subsumption 0} 1 == 1;
-  >>> DoNothingToAssert
-Processing command (at Snapshots24.v1.bpl(11,9)) assert {:subsumption 1} 5 == 5;
-  >>> DoNothingToAssert
-Processing command (at Snapshots24.v1.bpl(15,9)) assert {:subsumption 2} 6 != 6;
-  >>> RecycleError
-Processing command (at Snapshots24.v1.bpl(19,9)) assert {:subsumption 1} 2 == 2;
-  >>> MarkAsFullyVerified
-Processing command (at Snapshots24.v1.bpl(20,9)) assert {:subsumption 2} 4 == 4;
-  >>> MarkAsFullyVerified
-Processing command (at Snapshots24.v1.bpl(21,9)) assert 5 == 5;
-  >>> MarkAsFullyVerified
-Processing command (at Snapshots24.v1.bpl(24,5)) assert {:subsumption 0} 3 == 3;
-  >>> DoNothingToAssert
-Snapshots24.v0.bpl(15,9): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing command (at Snapshots25.v0.bpl(12,5)) assert 0 == 0;
-  >>> DoNothingToAssert
-Processing command (at Snapshots25.v0.bpl(13,5)) assert x != x;
-  >>> DoNothingToAssert
-Snapshots25.v0.bpl(13,5): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing command (at Snapshots25.v1.bpl(12,5)) assert 0 == 0;
-  >>> MarkAsFullyVerified
-Processing command (at Snapshots25.v1.bpl(13,5)) assert x != x;
-  >>> RecycleError
-Snapshots25.v0.bpl(13,5): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing command (at Snapshots26.v0.bpl(12,5)) assert 0 == 0;
-  >>> DoNothingToAssert
-Processing command (at Snapshots26.v0.bpl(13,5)) assert x != x;
-  >>> DoNothingToAssert
-Snapshots26.v0.bpl(13,5): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing command (at Snapshots26.v1.bpl(13,5)) assert 0 == 0;
-  >>> MarkAsFullyVerified
-Processing command (at Snapshots26.v1.bpl(14,5)) assert x != x;
-  >>> RecycleError
-Snapshots26.v0.bpl(13,5): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing command (at Snapshots27.v0.bpl(12,5)) assert 0 == 0;
-  >>> DoNothingToAssert
-Processing command (at Snapshots27.v0.bpl(13,5)) assert x != x;
-  >>> DoNothingToAssert
-Snapshots27.v0.bpl(13,5): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing command (at Snapshots27.v1.bpl(14,5)) assert 0 == 0;
-  >>> MarkAsFullyVerified
-Processing command (at Snapshots27.v1.bpl(15,5)) assert x != x;
-  >>> RecycleError
-Snapshots27.v0.bpl(13,5): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing command (at Snapshots28.v0.bpl(13,5)) assert 0 == 0;
-  >>> DoNothingToAssert
-Processing command (at Snapshots28.v0.bpl(14,5)) assert x == 0;
-  >>> DoNothingToAssert
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing command (at Snapshots28.v1.bpl(14,5)) assert 0 == 0;
-  >>> DoNothingToAssert
-Processing command (at Snapshots28.v1.bpl(15,5)) assert x == 0;
-  >>> DoNothingToAssert
-Snapshots28.v1.bpl(15,5): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing command (at Snapshots30.v0.bpl(5,5)) assert 0 == 0;
-  >>> DoNothingToAssert
-Processing command (at Snapshots30.v0.bpl(5,5)) assert 1 == 1;
-  >>> DoNothingToAssert
-Processing command (at Snapshots30.v0.bpl(5,5)) assert 2 != 2;
-  >>> DoNothingToAssert
-Processing command (at Snapshots30.v0.bpl(5,5)) assert 3 == 3;
-  >>> DoNothingToAssert
-Processing command (at Snapshots30.v0.bpl(5,5)) assert 4 == 4;
-  >>> DoNothingToAssert
-Snapshots30.v0.bpl(5,5): Error BP5002: A precondition for this call might not hold.
-Snapshots30.v0.bpl(11,3): Related location: This is the precondition that might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing command (at Snapshots30.v1.bpl(5,5)) assert 0 == 0;
-  >>> MarkAsFullyVerified
-Processing command (at Snapshots30.v1.bpl(5,5)) assert 1 == 1;
-  >>> MarkAsFullyVerified
-Processing command (at Snapshots30.v1.bpl(5,5)) assert 2 != 2;
-  >>> RecycleError
-Processing command (at Snapshots30.v1.bpl(5,5)) assert 3 == 3;
-  >>> MarkAsFullyVerified
-Processing command (at Snapshots30.v1.bpl(5,5)) assert 4 == 4;
-  >>> MarkAsFullyVerified
-Processing command (at Snapshots30.v1.bpl(6,5)) assert 5 == 5;
-  >>> DoNothingToAssert
-Snapshots30.v0.bpl(5,5): Error BP5002: A precondition for this call might not hold.
-Snapshots30.v0.bpl(11,3): Related location: This is the precondition that might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing command (at Snapshots31.v0.bpl(10,5)) assert 0 < g;
-  >>> DoNothingToAssert
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing call to procedure Q in implementation P (at Snapshots31.v1.bpl(9,5)):
-  >>> added axiom: (forall call0old#AT#g: int, g: int :: {:weight 30} { ##extracted_function##1(call0old#AT#g, g) } ##extracted_function##1(call0old#AT#g, g) == (call0old#AT#g < g))
-  >>> added after: a##post##0 := a##post##0 && ##extracted_function##1(call0old#AT#g, g);
-Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##1(call0old#AT#g, g);
-  >>> AssumeNegationOfAssumptionVariable
-Processing command (at Snapshots31.v1.bpl(10,5)) assert 0 < g;
-  >>> MarkAsPartiallyVerified
-Snapshots31.v1.bpl(10,5): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing command (at Snapshots32.v0.bpl(10,5)) assert 0 < g;
-  >>> DoNothingToAssert
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing call to procedure Q in implementation P (at Snapshots32.v1.bpl(8,5)):
-  >>> added axiom: (forall g##old##0: int, g: int :: {:weight 30} { ##extracted_function##1(g##old##0, g) } ##extracted_function##1(g##old##0, g) == (g##old##0 < g))
-  >>> added before: g##old##0 := g;
-  >>> added after: a##post##0 := a##post##0 && ##extracted_function##1(g##old##0, g);
-Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##1(g##old##0, g);
-  >>> AssumeNegationOfAssumptionVariable
-Processing command (at Snapshots32.v1.bpl(9,5)) assert 0 < g;
-  >>> MarkAsPartiallyVerified
-Snapshots32.v1.bpl(9,5): Error BP5001: This assertion might not hold.
-
-Boogie program verifier finished with 0 verified, 1 error
-Processing command (at Snapshots33.v0.bpl(10,5)) assert 0 < g;
-  >>> DoNothingToAssert
-
-Boogie program verifier finished with 1 verified, 0 errors
-Processing call to procedure Q in implementation P (at Snapshots33.v1.bpl(5,5)):
-  >>> added after: a##post##0 := a##post##0 && false;
-
-Boogie program verifier finished with 1 verified, 0 errors
+Processing command (at Snapshots0.v0.bpl(41,5)) assert false;
+  >>> DoNothingToAssert
+Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold.
+Processing command (at Snapshots0.v0.bpl(8,5)) assert false;
+  >>> DoNothingToAssert
+Snapshots0.v0.bpl(8,5): Error BP5001: This assertion might not hold.
+Processing command (at Snapshots0.v0.bpl(19,5)) assert false;
+  >>> DoNothingToAssert
+Snapshots0.v0.bpl(19,5): Error BP5001: This assertion might not hold.
+Processing command (at Snapshots0.v0.bpl(30,5)) assert false;
+  >>> DoNothingToAssert
+Snapshots0.v0.bpl(30,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 4 errors
+Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold.
+Processing command (at Snapshots0.v1.bpl(19,5)) assert true;
+  >>> DoNothingToAssert
+Processing command (at Snapshots0.v1.bpl(30,5)) assert false;
+  >>> DoNothingToAssert
+Snapshots0.v1.bpl(30,5): Error BP5001: This assertion might not hold.
+Processing command (at Snapshots0.v1.bpl(41,5)) assert true;
+  >>> DoNothingToAssert
+
+Boogie program verifier finished with 2 verified, 2 errors
+Snapshots0.v0.bpl(41,5): Error BP5001: This assertion might not hold.
+Processing command (at Snapshots0.v2.bpl(19,5)) assert true;
+  >>> DoNothingToAssert
+Processing command (at Snapshots0.v2.bpl(30,5)) assert true;
+  >>> DoNothingToAssert
+
+Boogie program verifier finished with 2 verified, 1 error
+Processing command (at Snapshots1.v0.bpl(13,5)) assert 1 != 1;
+  >>> DoNothingToAssert
+Snapshots1.v0.bpl(13,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 1 verified, 1 error
+Processing command (at Snapshots1.v1.bpl(13,5)) assert 2 != 2;
+  >>> DoNothingToAssert
+Snapshots1.v1.bpl(13,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 1 verified, 1 error
+Processing call to procedure P2 in implementation P1 (at Snapshots1.v2.bpl(5,5)):
+  >>> added after: a##cached##0 := a##cached##0 && true;
+Processing implementation P2 (at Snapshots1.v2.bpl(12,51)):
+  >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && true;
+Processing command (at Snapshots1.v2.bpl(5,5)) assert false;
+  >>> DoNothingToAssert
+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && true;
+  >>> AssumeNegationOfAssumptionVariable
+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.
+Processing command (at Snapshots1.v2.bpl(14,5)) assert 2 != 2;
+  >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 1 error
+
+Boogie program verifier finished with 1 verified, 0 errors
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing implementation P0 (at Snapshots2.v2.bpl(4,51)):
+  >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && true;
+Processing call to procedure P0 in implementation P0 (at Snapshots2.v2.bpl(6,5)):
+  >>> added after: a##cached##1 := a##cached##1 && true;
+Processing command (at Snapshots2.v2.bpl(6,5)) assert F0();
+  >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing implementation P0 (at Snapshots2.v3.bpl(4,51)):
+  >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && false;
+Processing call to procedure P0 in implementation P0 (at Snapshots2.v3.bpl(6,5)):
+  >>> added after: a##cached##1 := a##cached##1 && false;
+Processing command (at Snapshots2.v3.bpl(6,5)) assert F0();
+  >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing implementation P0 (at Snapshots2.v5.bpl(5,51)):
+  >>> added axiom: ##extracted_function##1() == F0()
+  >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##1();
+Processing call to procedure P0 in implementation P0 (at Snapshots2.v5.bpl(7,5)):
+  >>> added axiom: ##extracted_function##2() == F0()
+  >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##2();
+  >>> added after: a##cached##1 := a##cached##1 && true;
+Processing command (at Snapshots2.v5.bpl(7,5)) assume {:precondition_previous_snapshot} ##extracted_function##2();
+  >>> MarkAsPartiallyVerified
+Processing command (at Snapshots2.v5.bpl(7,5)) assert F0();
+  >>> MarkAsPartiallyVerified
+Processing command (at Snapshots2.v5.bpl(3,1)) assert F0();
+  >>> MarkAsPartiallyVerified
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing command (at Snapshots3.v0.bpl(2,1)) assert G();
+  >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing implementation P0 (at Snapshots3.v1.bpl(4,51)):
+  >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && false;
+Processing command (at Snapshots3.v1.bpl(2,1)) assert G();
+  >>> DoNothingToAssert
+Snapshots3.v1.bpl(6,1): Error BP5003: A postcondition might not hold on this return path.
+Snapshots3.v1.bpl(2,1): Related location: This is the postcondition that might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+
+Boogie program verifier finished with 3 verified, 0 errors
+Processing call to procedure P2 in implementation P1 (at Snapshots4.v1.bpl(14,5)):
+  >>> added after: a##cached##0 := a##cached##0 && false;
+Processing command (at Snapshots4.v1.bpl(23,5)) assert false;
+  >>> DoNothingToAssert
+Snapshots4.v1.bpl(23,5): Error BP5001: This assertion might not hold.
+Processing command (at Snapshots4.v1.bpl(28,3)) assert G();
+  >>> DoNothingToAssert
+Snapshots4.v1.bpl(33,1): Error BP5003: A postcondition might not hold on this return path.
+Snapshots4.v1.bpl(28,3): Related location: This is the postcondition that might not hold.
+
+Boogie program verifier finished with 2 verified, 2 errors
+Processing command (at Snapshots5.v0.bpl(5,5)) assert false;
+  >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing implementation P0 (at Snapshots5.v1.bpl(3,51)):
+  >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && false;
+Processing command (at Snapshots5.v1.bpl(5,5)) assert false;
+  >>> DoNothingToAssert
+Snapshots5.v1.bpl(5,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots6.v0.bpl(13,5)) assert y == 0;
+  >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing call to procedure N in implementation M (at Snapshots6.v1.bpl(11,5)):
+  >>> added axiom: (forall y##old##0: int, y: int :: {:weight 30} { ##extracted_function##1(y##old##0, y) } ##extracted_function##1(y##old##0, y) == (y##old##0 == y))
+  >>> added before: y##old##0 := y;
+  >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##1(y##old##0, y);
+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##1(y##old##0, y);
+  >>> AssumeNegationOfAssumptionVariable
+Processing command (at Snapshots6.v1.bpl(13,5)) assert y == 0;
+  >>> MarkAsPartiallyVerified
+Snapshots6.v1.bpl(13,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots7.v0.bpl(14,5)) assert y < 0;
+  >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing call to procedure N in implementation M (at Snapshots7.v1.bpl(12,5)):
+  >>> added axiom: (forall y: int, z: int :: {:weight 30} { ##extracted_function##1(y, z) } ##extracted_function##1(y, z) == (y < z))
+  >>> added before: y##old##0 := y;
+  >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##1(y, z);
+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##1(y, z);
+  >>> AssumeNegationOfAssumptionVariable
+Processing command (at Snapshots7.v1.bpl(14,5)) assert y < 0;
+  >>> MarkAsPartiallyVerified
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing command (at Snapshots8.v0.bpl(8,5)) assert 0 < call0formal#AT#n;
+  >>> DoNothingToAssert
+Processing command (at Snapshots8.v0.bpl(10,5)) assert 0 <= x;
+  >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing call to procedure N in implementation M (at Snapshots8.v1.bpl(8,5)):
+  >>> added axiom: (forall call0formal#AT#n: int :: {:weight 30} { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 < call0formal#AT#n))
+  >>> added axiom: (forall call1formal#AT#r: int :: {:weight 30} { ##extracted_function##2(call1formal#AT#r) } ##extracted_function##2(call1formal#AT#r) == (0 < call1formal#AT#r))
+  >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
+  >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##2(call1formal#AT#r);
+Processing command (at Snapshots8.v1.bpl(8,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots8.v1.bpl(8,5)) assert 0 < call0formal#AT#n;
+  >>> MarkAsFullyVerified
+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##2(call1formal#AT#r);
+  >>> AssumeNegationOfAssumptionVariable
+Processing command (at Snapshots8.v1.bpl(10,5)) assert 0 <= x;
+  >>> MarkAsPartiallyVerified
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing command (at Snapshots9.v0.bpl(8,5)) assert 0 < call0formal#AT#n;
+  >>> DoNothingToAssert
+Processing command (at Snapshots9.v0.bpl(8,5)) assert true;
+  >>> DoNothingToAssert
+Processing command (at Snapshots9.v0.bpl(10,5)) assert 0 <= x;
+  >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing call to procedure N in implementation M (at Snapshots9.v1.bpl(8,5)):
+  >>> added axiom: (forall call0formal#AT#n: int :: {:weight 30} { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 < call0formal#AT#n && true))
+  >>> added axiom: (forall call1formal#AT#r: int :: {:weight 30} { ##extracted_function##2(call1formal#AT#r) } ##extracted_function##2(call1formal#AT#r) == (0 < call1formal#AT#r && true))
+  >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
+  >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##2(call1formal#AT#r);
+Processing command (at Snapshots9.v1.bpl(8,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots9.v1.bpl(8,5)) assert 0 < call0formal#AT#n;
+  >>> MarkAsFullyVerified
+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##2(call1formal#AT#r);
+  >>> AssumeNegationOfAssumptionVariable
+Processing command (at Snapshots9.v1.bpl(10,5)) assert 0 <= x;
+  >>> MarkAsPartiallyVerified
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing command (at Snapshots10.v0.bpl(8,5)) assert 0 < call0formal#AT#n;
+  >>> DoNothingToAssert
+Processing command (at Snapshots10.v0.bpl(12,5)) assert 0 <= x;
+  >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing call to procedure N in implementation M (at Snapshots10.v1.bpl(8,5)):
+  >>> added axiom: (forall call0formal#AT#n: int :: {:weight 30} { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 < call0formal#AT#n))
+  >>> added axiom: (forall call1formal#AT#r: int :: {:weight 30} { ##extracted_function##2(call1formal#AT#r) } ##extracted_function##2(call1formal#AT#r) == (0 < call1formal#AT#r))
+  >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
+  >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##2(call1formal#AT#r);
+Processing command (at Snapshots10.v1.bpl(8,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots10.v1.bpl(8,5)) assert 0 < call0formal#AT#n;
+  >>> MarkAsFullyVerified
+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##2(call1formal#AT#r);
+  >>> AssumeNegationOfAssumptionVariable
+Processing command (at Snapshots10.v1.bpl(12,5)) assert 0 <= x;
+  >>> MarkAsPartiallyVerified
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing command (at Snapshots11.v0.bpl(7,5)) assert 0 < call0formal#AT#n;
+  >>> DoNothingToAssert
+Processing command (at Snapshots11.v0.bpl(9,5)) assert 0 <= x;
+  >>> DoNothingToAssert
+Snapshots11.v0.bpl(7,5): Error BP5002: A precondition for this call might not hold.
+Snapshots11.v0.bpl(13,3): Related location: This is the precondition that might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing call to procedure N in implementation M (at Snapshots11.v1.bpl(7,5)):
+  >>> added axiom: (forall call0formal#AT#n: int :: {:weight 30} { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 < call0formal#AT#n))
+  >>> added axiom: (forall call1formal#AT#r: int :: {:weight 30} { ##extracted_function##2(call1formal#AT#r) } ##extracted_function##2(call1formal#AT#r) == (0 < call1formal#AT#r))
+  >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
+  >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##2(call1formal#AT#r);
+Processing command (at Snapshots11.v1.bpl(7,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
+  >>> DropAssume
+Processing command (at Snapshots11.v1.bpl(7,5)) assert 0 < call0formal#AT#n;
+  >>> RecycleError
+Processing command (at Snapshots11.v1.bpl(9,5)) assert 0 <= x;
+  >>> MarkAsPartiallyVerified
+Snapshots11.v0.bpl(7,5): Error BP5002: A precondition for this call might not hold.
+Snapshots11.v0.bpl(13,3): Related location: This is the precondition that might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots12.v0.bpl(7,5)) assert false;
+  >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing call to procedure N in implementation M (at Snapshots12.v1.bpl(5,5)):
+  >>> added after: a##cached##0 := a##cached##0 && false;
+Processing command (at Snapshots12.v1.bpl(7,5)) assert false;
+  >>> DoNothingToAssert
+Snapshots12.v1.bpl(7,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots13.v0.bpl(7,5)) assert false;
+  >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing call to procedure N in implementation M (at Snapshots13.v1.bpl(5,5)):
+  >>> added after: a##cached##0 := a##cached##0 && false;
+Processing command (at Snapshots13.v1.bpl(7,5)) assert false;
+  >>> DoNothingToAssert
+Snapshots13.v1.bpl(7,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots14.v0.bpl(7,5)) assert false;
+  >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing call to procedure N in implementation M (at Snapshots14.v1.bpl(5,5)):
+  >>> added axiom: ##extracted_function##1() == (F() && G())
+  >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##1();
+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##1();
+  >>> AssumeNegationOfAssumptionVariable
+Processing command (at Snapshots14.v1.bpl(7,5)) assert false;
+  >>> MarkAsPartiallyVerified
+Snapshots14.v1.bpl(7,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots15.v0.bpl(5,5)) assert true;
+  >>> DoNothingToAssert
+Processing command (at Snapshots15.v0.bpl(9,5)) assert true;
+  >>> DoNothingToAssert
+Processing command (at Snapshots15.v0.bpl(13,5)) assert false;
+  >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing call to procedure N in implementation M (at Snapshots15.v1.bpl(7,5)):
+  >>> added after: a##cached##0 := a##cached##0 && false;
+Processing call to procedure N in implementation M (at Snapshots15.v1.bpl(11,5)):
+  >>> added after: a##cached##1 := a##cached##1 && false;
+Processing command (at Snapshots15.v1.bpl(5,5)) assert true;
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots15.v1.bpl(9,5)) assert true;
+  >>> MarkAsPartiallyVerified
+Processing command (at Snapshots15.v1.bpl(13,5)) assert false;
+  >>> MarkAsPartiallyVerified
+Snapshots15.v1.bpl(13,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots16.v0.bpl(14,5)) assert F(0) == 1;
+  >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing command (at Snapshots16.v1.bpl(14,5)) assert F(0) == 1;
+  >>> DoNothingToAssert
+Snapshots16.v1.bpl(14,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots17.v0.bpl(28,5)) assert true;
+  >>> DoNothingToAssert
+Processing command (at Snapshots17.v0.bpl(25,9)) assert false;
+  >>> DoNothingToAssert
+Processing command (at Snapshots17.v0.bpl(12,13)) assert true;
+  >>> DoNothingToAssert
+Processing command (at Snapshots17.v0.bpl(20,13)) assert x == 1;
+  >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing call to procedure N in implementation M (at Snapshots17.v1.bpl(14,13)):
+  >>> added after: a##cached##0 := a##cached##0 && false;
+Processing call to procedure N in implementation M (at Snapshots17.v1.bpl(16,13)):
+  >>> added after: a##cached##1 := a##cached##1 && false;
+Processing call to procedure N in implementation M (at Snapshots17.v1.bpl(23,9)):
+  >>> added after: a##cached##2 := a##cached##2 && false;
+Processing command (at Snapshots17.v1.bpl(28,5)) assert true;
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots17.v1.bpl(25,9)) assert false;
+  >>> MarkAsPartiallyVerified
+Processing command (at Snapshots17.v1.bpl(12,13)) assert true;
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots17.v1.bpl(20,13)) assert x == 1;
+  >>> MarkAsPartiallyVerified
+Snapshots17.v1.bpl(20,13): Error BP5001: This assertion might not hold.
+Snapshots17.v1.bpl(25,9): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 2 errors
+Processing command (at Snapshots18.v0.bpl(7,9)) assert 0 == 0;
+  >>> DoNothingToAssert
+Processing command (at Snapshots18.v0.bpl(17,9)) assert 1 != 1;
+  >>> DoNothingToAssert
+Processing command (at Snapshots18.v0.bpl(20,5)) assert 2 != 2;
+  >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing call to procedure N in implementation M (at Snapshots18.v1.bpl(9,9)):
+  >>> added after: a##cached##0 := a##cached##0 && false;
+Processing call to procedure N in implementation M (at Snapshots18.v1.bpl(10,9)):
+  >>> added after: a##cached##1 := a##cached##1 && false;
+Processing command (at Snapshots18.v1.bpl(7,9)) assert 0 == 0;
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots18.v1.bpl(17,9)) assert 1 != 1;
+  >>> MarkAsPartiallyVerified
+Processing command (at Snapshots18.v1.bpl(20,5)) assert 2 != 2;
+  >>> MarkAsPartiallyVerified
+Snapshots18.v1.bpl(17,9): Error BP5001: This assertion might not hold.
+Snapshots18.v1.bpl(20,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 2 errors
+Processing command (at Snapshots19.v0.bpl(5,5)) assert 2 == 2;
+  >>> DoNothingToAssert
+Processing command (at Snapshots19.v0.bpl(7,5)) assert 1 != 1;
+  >>> DoNothingToAssert
+Snapshots19.v0.bpl(7,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing call to procedure N in implementation M (at Snapshots19.v1.bpl(5,5)):
+  >>> added axiom: ##extracted_function##1() == (2 == 2)
+  >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1();
+  >>> added after: a##cached##0 := a##cached##0 && true;
+Processing command (at Snapshots19.v1.bpl(5,5)) assume {:precondition_previous_snapshot} ##extracted_function##1();
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots19.v1.bpl(5,5)) assert 2 == 2;
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots19.v1.bpl(7,5)) assert 1 != 1;
+  >>> DoNothingToAssert
+Snapshots19.v1.bpl(7,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots20.v0.bpl(9,9)) assert 1 != 1;
+  >>> DoNothingToAssert
+Processing command (at Snapshots20.v0.bpl(13,9)) assert 2 != 2;
+  >>> DoNothingToAssert
+Processing command (at Snapshots20.v0.bpl(16,5)) assert 3 != 3;
+  >>> DoNothingToAssert
+Snapshots20.v0.bpl(13,9): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing call to procedure N in implementation M (at Snapshots20.v1.bpl(7,9)):
+  >>> added axiom: ##extracted_function##1() == (0 != 0)
+  >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##1();
+Processing command (at Snapshots20.v1.bpl(9,9)) assert 1 != 1;
+  >>> MarkAsPartiallyVerified
+Processing command (at Snapshots20.v1.bpl(13,9)) assert 2 != 2;
+  >>> RecycleError
+Processing command (at Snapshots20.v1.bpl(16,5)) assert 3 != 3;
+  >>> MarkAsPartiallyVerified
+Snapshots20.v1.bpl(9,9): Error BP5001: This assertion might not hold.
+Snapshots20.v0.bpl(13,9): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 2 errors
+Processing command (at Snapshots21.v0.bpl(7,9)) assert 1 != 1;
+  >>> DoNothingToAssert
+Processing command (at Snapshots21.v0.bpl(11,9)) assert 2 != 2;
+  >>> DoNothingToAssert
+Processing command (at Snapshots21.v0.bpl(14,5)) assert 3 != 3;
+  >>> DoNothingToAssert
+Snapshots21.v0.bpl(7,9): Error BP5001: This assertion might not hold.
+Snapshots21.v0.bpl(11,9): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 2 errors
+Processing command (at Snapshots21.v1.bpl(7,9)) assert 1 == 1;
+  >>> DoNothingToAssert
+Processing command (at Snapshots21.v1.bpl(11,9)) assert 2 != 2;
+  >>> RecycleError
+Processing command (at Snapshots21.v1.bpl(14,5)) assert 3 != 3;
+  >>> DoNothingToAssert
+Snapshots21.v0.bpl(11,9): Error BP5001: This assertion might not hold.
+Snapshots21.v1.bpl(14,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 2 errors
+Processing command (at Snapshots22.v0.bpl(7,9)) assert 1 != 1;
+  >>> DoNothingToAssert
+Processing command (at Snapshots22.v0.bpl(11,9)) assert 2 == 2;
+  >>> DoNothingToAssert
+Processing command (at Snapshots22.v0.bpl(14,5)) assert 3 == 3;
+  >>> DoNothingToAssert
+Snapshots22.v0.bpl(7,9): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots22.v1.bpl(7,9)) assert 1 == 1;
+  >>> DoNothingToAssert
+Processing command (at Snapshots22.v1.bpl(11,9)) assert 2 == 2;
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots22.v1.bpl(14,5)) assert 3 == 3;
+  >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing command (at Snapshots23.v0.bpl(7,9)) assert 1 != 1;
+  >>> DoNothingToAssert
+Processing command (at Snapshots23.v0.bpl(11,9)) assert 2 == 2;
+  >>> DoNothingToAssert
+Processing command (at Snapshots23.v0.bpl(14,5)) assert 3 == 3;
+  >>> DoNothingToAssert
+Snapshots23.v0.bpl(7,9): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 1 verified, 1 error
+Snapshots23.v0.bpl(7,9): Error BP5001: This assertion might not hold.
+Processing command (at Snapshots23.v1.bpl(22,5)) assert 4 == 4;
+  >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 1 error
+Processing command (at Snapshots23.v2.bpl(8,9)) assert 1 != 1;
+  >>> RecycleError
+Processing command (at Snapshots23.v2.bpl(12,9)) assert 2 == 2;
+  >>> MarkAsFullyVerified
+Snapshots23.v0.bpl(7,9): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 1 verified, 1 error
+Processing command (at Snapshots24.v0.bpl(7,9)) assert {:subsumption 0} 1 != 1;
+  >>> DoNothingToAssert
+Processing command (at Snapshots24.v0.bpl(11,9)) assert {:subsumption 1} 5 != 5;
+  >>> DoNothingToAssert
+Processing command (at Snapshots24.v0.bpl(15,9)) assert {:subsumption 2} 6 != 6;
+  >>> DoNothingToAssert
+Processing command (at Snapshots24.v0.bpl(19,9)) assert {:subsumption 1} 2 == 2;
+  >>> DoNothingToAssert
+Processing command (at Snapshots24.v0.bpl(20,9)) assert {:subsumption 2} 4 == 4;
+  >>> DoNothingToAssert
+Processing command (at Snapshots24.v0.bpl(21,9)) assert 5 == 5;
+  >>> DoNothingToAssert
+Processing command (at Snapshots24.v0.bpl(24,5)) assert {:subsumption 0} 3 == 3;
+  >>> DoNothingToAssert
+Snapshots24.v0.bpl(7,9): Error BP5001: This assertion might not hold.
+Snapshots24.v0.bpl(11,9): Error BP5001: This assertion might not hold.
+Snapshots24.v0.bpl(15,9): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 3 errors
+Processing command (at Snapshots24.v1.bpl(7,9)) assert {:subsumption 0} 1 == 1;
+  >>> DoNothingToAssert
+Processing command (at Snapshots24.v1.bpl(11,9)) assert {:subsumption 1} 5 == 5;
+  >>> DoNothingToAssert
+Processing command (at Snapshots24.v1.bpl(15,9)) assert {:subsumption 2} 6 != 6;
+  >>> RecycleError
+Processing command (at Snapshots24.v1.bpl(19,9)) assert {:subsumption 1} 2 == 2;
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots24.v1.bpl(20,9)) assert {:subsumption 2} 4 == 4;
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots24.v1.bpl(21,9)) assert 5 == 5;
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots24.v1.bpl(24,5)) assert {:subsumption 0} 3 == 3;
+  >>> DoNothingToAssert
+Snapshots24.v0.bpl(15,9): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots25.v0.bpl(12,5)) assert 0 == 0;
+  >>> DoNothingToAssert
+Processing command (at Snapshots25.v0.bpl(13,5)) assert x != x;
+  >>> DoNothingToAssert
+Snapshots25.v0.bpl(13,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots25.v1.bpl(12,5)) assert 0 == 0;
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots25.v1.bpl(13,5)) assert x != x;
+  >>> RecycleError
+Snapshots25.v0.bpl(13,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots26.v0.bpl(12,5)) assert 0 == 0;
+  >>> DoNothingToAssert
+Processing command (at Snapshots26.v0.bpl(13,5)) assert x != x;
+  >>> DoNothingToAssert
+Snapshots26.v0.bpl(13,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots26.v1.bpl(13,5)) assert 0 == 0;
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots26.v1.bpl(14,5)) assert x != x;
+  >>> RecycleError
+Snapshots26.v0.bpl(13,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots27.v0.bpl(12,5)) assert 0 == 0;
+  >>> DoNothingToAssert
+Processing command (at Snapshots27.v0.bpl(13,5)) assert x != x;
+  >>> DoNothingToAssert
+Snapshots27.v0.bpl(13,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots27.v1.bpl(14,5)) assert 0 == 0;
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots27.v1.bpl(15,5)) assert x != x;
+  >>> RecycleError
+Snapshots27.v0.bpl(13,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots28.v0.bpl(13,5)) assert 0 == 0;
+  >>> DoNothingToAssert
+Processing command (at Snapshots28.v0.bpl(14,5)) assert x == 0;
+  >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing command (at Snapshots28.v1.bpl(14,5)) assert 0 == 0;
+  >>> DoNothingToAssert
+Processing command (at Snapshots28.v1.bpl(15,5)) assert x == 0;
+  >>> DoNothingToAssert
+Snapshots28.v1.bpl(15,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots30.v0.bpl(5,5)) assert 0 == 0;
+  >>> DoNothingToAssert
+Processing command (at Snapshots30.v0.bpl(5,5)) assert 1 == 1;
+  >>> DoNothingToAssert
+Processing command (at Snapshots30.v0.bpl(5,5)) assert 2 != 2;
+  >>> DoNothingToAssert
+Processing command (at Snapshots30.v0.bpl(5,5)) assert 3 == 3;
+  >>> DoNothingToAssert
+Processing command (at Snapshots30.v0.bpl(5,5)) assert 4 == 4;
+  >>> DoNothingToAssert
+Snapshots30.v0.bpl(5,5): Error BP5002: A precondition for this call might not hold.
+Snapshots30.v0.bpl(11,3): Related location: This is the precondition that might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots30.v1.bpl(5,5)) assert 0 == 0;
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots30.v1.bpl(5,5)) assert 1 == 1;
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots30.v1.bpl(5,5)) assert 2 != 2;
+  >>> RecycleError
+Processing command (at Snapshots30.v1.bpl(5,5)) assert 3 == 3;
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots30.v1.bpl(5,5)) assert 4 == 4;
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots30.v1.bpl(6,5)) assert 5 == 5;
+  >>> DoNothingToAssert
+Snapshots30.v0.bpl(5,5): Error BP5002: A precondition for this call might not hold.
+Snapshots30.v0.bpl(11,3): Related location: This is the precondition that might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots31.v0.bpl(10,5)) assert 0 < g;
+  >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing call to procedure Q in implementation P (at Snapshots31.v1.bpl(9,5)):
+  >>> added axiom: (forall call0old#AT#g: int, g: int :: {:weight 30} { ##extracted_function##1(call0old#AT#g, g) } ##extracted_function##1(call0old#AT#g, g) == (call0old#AT#g < g))
+  >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##1(call0old#AT#g, g);
+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##1(call0old#AT#g, g);
+  >>> AssumeNegationOfAssumptionVariable
+Processing command (at Snapshots31.v1.bpl(10,5)) assert 0 < g;
+  >>> MarkAsPartiallyVerified
+Snapshots31.v1.bpl(10,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots32.v0.bpl(10,5)) assert 0 < g;
+  >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing call to procedure Q in implementation P (at Snapshots32.v1.bpl(8,5)):
+  >>> added axiom: (forall g##old##0: int, g: int :: {:weight 30} { ##extracted_function##1(g##old##0, g) } ##extracted_function##1(g##old##0, g) == (g##old##0 < g))
+  >>> added before: g##old##0 := g;
+  >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##1(g##old##0, g);
+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##1(g##old##0, g);
+  >>> AssumeNegationOfAssumptionVariable
+Processing command (at Snapshots32.v1.bpl(9,5)) assert 0 < g;
+  >>> MarkAsPartiallyVerified
+Snapshots32.v1.bpl(9,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots33.v0.bpl(10,5)) assert 0 < g;
+  >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing implementation P (at Snapshots33.v1.bpl(3,42)):
+  >>> added axiom: (forall g: int :: {:weight 30} { ##extracted_function##1(g) } ##extracted_function##1(g) == (g == 0))
+  >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##1(g);
+Processing call to procedure Q in implementation P (at Snapshots33.v1.bpl(5,5)):
+  >>> added after: a##cached##1 := a##cached##1 && false;
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing command (at Snapshots34.v0.bpl(6,5)) assert 1 != 1;
+  >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing implementation P (at Snapshots34.v1.bpl(3,42)):
+  >>> added axiom: ##extracted_function##1() == (0 != 0)
+  >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##1();
+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##1();
+  >>> AssumeNegationOfAssumptionVariable
+Processing command (at Snapshots34.v1.bpl(5,5)) assert 1 != 1;
+  >>> MarkAsPartiallyVerified
+Snapshots34.v1.bpl(5,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots35.v0.bpl(6,5)) assert p;
+  >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing implementation P (at Snapshots35.v1.bpl(3,42)):
+  >>> added axiom: (forall p: bool :: {:weight 30} { ##extracted_function##1(p) } ##extracted_function##1(p) == p)
+  >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##1(p);
+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##1(p);
+  >>> AssumeNegationOfAssumptionVariable
+Processing command (at Snapshots35.v1.bpl(5,5)) assert p;
+  >>> MarkAsPartiallyVerified
+Snapshots35.v1.bpl(5,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots36.v0.bpl(13,5)) assert l[0];
+  >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing command (at Snapshots36.v1.bpl(13,5)) assert l[0];
+  >>> DoNothingToAssert
+Snapshots36.v1.bpl(13,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots37.v0.bpl(8,5)) assert l[0];
+  >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing command (at Snapshots37.v1.bpl(8,5)) assert l[0];
+  >>> DoNothingToAssert
+Snapshots37.v1.bpl(8,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots38.v0.bpl(7,5)) assert 0 <= call0formal#AT#n;
+  >>> DoNothingToAssert
+Processing command (at Snapshots38.v0.bpl(8,5)) assert r != 0;
+  >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing command (at Snapshots38.v1.bpl(7,5)) assert 0 <= call0formal#AT#n;
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots38.v1.bpl(8,5)) assert r != 0;
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots38.v1.bpl(9,5)) assert 42 <= r;
+  >>> DoNothingToAssert
+Snapshots38.v1.bpl(9,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing call to procedure Sum in implementation Callee (at Snapshots38.v2.bpl(7,5)):
+  >>> added axiom: (forall call0formal#AT#n: int :: {:weight 30} { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 <= call0formal#AT#n))
+  >>> added axiom: (forall call0formal#AT#n: int, call1formal#AT#r: int :: {:weight 30} { ##extracted_function##2(call0formal#AT#n, call1formal#AT#r) } ##extracted_function##2(call0formal#AT#n, call1formal#AT#r) == (call0formal#AT#n != 0 ==> 1 <= call1formal#AT#r))
+  >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
+  >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##2(call0formal#AT#n, call1formal#AT#r);
+Processing command (at Snapshots38.v2.bpl(7,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots38.v2.bpl(7,5)) assert 0 <= call0formal#AT#n;
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots38.v2.bpl(8,5)) assert r != 0;
+  >>> MarkAsPartiallyVerified
+Processing command (at Snapshots38.v2.bpl(9,5)) assert 42 <= r;
+  >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing command (at Snapshots39.v0.bpl(7,5)) assert 0 <= call0formal#AT#n;
+  >>> DoNothingToAssert
+Processing command (at Snapshots39.v0.bpl(8,5)) assert r != 0;
+  >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing command (at Snapshots39.v1.bpl(7,5)) assert 0 <= call0formal#AT#n;
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots39.v1.bpl(8,5)) assert r != 0;
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots39.v1.bpl(9,5)) assert r == 42 * 43 div 2;
+  >>> DoNothingToAssert
+Snapshots39.v1.bpl(9,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing call to procedure Sum in implementation Callee (at Snapshots39.v2.bpl(7,5)):
+  >>> added axiom: (forall call0formal#AT#n: int :: {:weight 30} { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 <= call0formal#AT#n))
+  >>> added axiom: (forall call0formal#AT#n: int, call1formal#AT#r: int :: {:weight 30} { ##extracted_function##2(call0formal#AT#n, call1formal#AT#r) } ##extracted_function##2(call0formal#AT#n, call1formal#AT#r) == (call0formal#AT#n <= call1formal#AT#r))
+  >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
+  >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##2(call0formal#AT#n, call1formal#AT#r);
+Processing command (at Snapshots39.v2.bpl(7,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots39.v2.bpl(7,5)) assert 0 <= call0formal#AT#n;
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots39.v2.bpl(8,5)) assert r != 0;
+  >>> MarkAsPartiallyVerified
+Processing command (at Snapshots39.v2.bpl(9,5)) assert r == 42 * 43 div 2;
+  >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing command (at Snapshots40.v0.bpl(7,5)) assert b;
+  >>> DoNothingToAssert
+Processing command (at Snapshots40.v0.bpl(8,5)) assert 0 <= call0formal#AT#n;
+  >>> DoNothingToAssert
+Processing command (at Snapshots40.v0.bpl(9,5)) assert r != 0;
+  >>> DoNothingToAssert
+Snapshots40.v0.bpl(7,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots40.v1.bpl(7,5)) assert b;
+  >>> RecycleError
+Processing command (at Snapshots40.v1.bpl(8,5)) assert 0 <= call0formal#AT#n;
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots40.v1.bpl(9,5)) assert r != 0;
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots40.v1.bpl(10,5)) assert r == 42 * 43 div 2;
+  >>> DoNothingToAssert
+Snapshots40.v0.bpl(7,5): Error BP5001: This assertion might not hold.
+Snapshots40.v1.bpl(10,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 2 errors
+Processing call to procedure Sum in implementation Foo (at Snapshots40.v2.bpl(8,5)):
+  >>> added axiom: (forall call0formal#AT#n: int :: {:weight 30} { ##extracted_function##1(call0formal#AT#n) } ##extracted_function##1(call0formal#AT#n) == (0 <= call0formal#AT#n))
+  >>> added axiom: (forall call0formal#AT#n: int, call1formal#AT#r: int :: {:weight 30} { ##extracted_function##2(call0formal#AT#n, call1formal#AT#r) } ##extracted_function##2(call0formal#AT#n, call1formal#AT#r) == (call0formal#AT#n <= call1formal#AT#r))
+  >>> added before precondition check: assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
+  >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##2(call0formal#AT#n, call1formal#AT#r);
+Processing command (at Snapshots40.v2.bpl(7,5)) assert b;
+  >>> RecycleError
+Processing command (at Snapshots40.v2.bpl(8,5)) assume {:precondition_previous_snapshot} ##extracted_function##1(call0formal#AT#n);
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots40.v2.bpl(8,5)) assert 0 <= call0formal#AT#n;
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots40.v2.bpl(9,5)) assert r != 0;
+  >>> MarkAsPartiallyVerified
+Processing command (at Snapshots40.v2.bpl(10,5)) assert r == 42 * 43 div 2;
+  >>> DoNothingToAssert
+Snapshots40.v0.bpl(7,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots41.v0.bpl(3,23)) assert x < 20 || 10 <= x;
+  >>> DoNothingToAssert
+Processing command (at Snapshots41.v0.bpl(4,3)) assert x < 10;
+  >>> DoNothingToAssert
+Processing command (at Snapshots41.v0.bpl(5,3)) assert 0 <= call0formal#AT#y;
+  >>> DoNothingToAssert
+Snapshots41.v0.bpl(4,3): Error BP5001: This assertion might not hold.
+Snapshots41.v0.bpl(5,3): Error BP5002: A precondition for this call might not hold.
+Snapshots41.v0.bpl(9,3): Related location: This is the precondition that might not hold.
+Processing command (at Snapshots41.v0.bpl(15,3)) assert 2 <= z;
+  >>> DoNothingToAssert
+Snapshots41.v0.bpl(22,3): Error BP5003: A postcondition might not hold on this return path.
+Snapshots41.v0.bpl(15,3): Related location: This is the postcondition that might not hold.
+Processing command (at Snapshots41.v0.bpl(28,3)) assert u != 53;
+  >>> DoNothingToAssert
+Snapshots41.v0.bpl(28,3): Error BP5001: This assertion might not hold.
+Processing command (at Snapshots41.v0.bpl(34,3)) assert true;
+  >>> DoNothingToAssert
+
+Boogie program verifier finished with 2 verified, 4 errors
+Processing command (at Snapshots41.v1.bpl(4,1)) assert x < 20 || 10 <= x;
+  >>> MarkAsFullyVerified
+Processing command (at Snapshots41.v1.bpl(6,8)) assert x < 10;
+  >>> RecycleError
+Processing command (at Snapshots41.v1.bpl(7,3)) assert 0 <= call0formal#AT#y;
+  >>> RecycleError
+Processing command (at Snapshots41.v1.bpl(8,3)) assert x == 7;
+  >>> DoNothingToAssert
+Snapshots41.v1.bpl(6,8): Error BP5001: This assertion might not hold.
+Snapshots41.v1.bpl(7,3): Error BP5002: A precondition for this call might not hold.
+Snapshots41.v1.bpl(13,10): Related location: This is the precondition that might not hold.
+Snapshots41.v1.bpl(8,3): Error BP5001: This assertion might not hold.
+Processing command (at Snapshots41.v1.bpl(27,5)) assert true;
+  >>> DoNothingToAssert
+Processing command (at Snapshots41.v1.bpl(21,3)) assert 2 <= z;
+  >>> DoNothingToAssert
+Snapshots41.v1.bpl(29,3): Error BP5003: A postcondition might not hold on this return path.
+Snapshots41.v1.bpl(21,3): Related location: This is the postcondition that might not hold.
+Processing command (at Snapshots41.v1.bpl(35,8)) assert u != 53;
+  >>> RecycleError
+Snapshots41.v1.bpl(35,8): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 2 verified, 5 errors