2 files changed, 48 insertions, 15 deletions
diff --git a/Test/test2/AssumptionVariables0.bpl b/Test/test2/AssumptionVariables0.bpl
index cc73707c..766c9d1e 100644
--- a/Test/test2/AssumptionVariables0.bpl
+++ b/Test/test2/AssumptionVariables0.bpl
@@ -28,13 +28,46 @@ procedure Test2()
 }
 
 
-var {:assumption} a0: bool;
+var {:assumption} ga0: bool;
 
 
 procedure Test3()
-  modifies a0;
+  modifies ga0;
 {
-    a0 := a0 && true;
+    ga0 := ga0 && true;
 
-    assert a0;  // error
+    assert ga0;  // error
+}
+
+
+procedure Test4()
+{
+    var {:assumption} a0: bool;
+    var tmp: bool;
+
+    tmp := a0;
+
+    havoc a0;
+
+    assert a0 ==> tmp;
+}
+
+
+procedure Test5(A: bool)
+{
+    var {:assumption} a0: bool;
+    var tmp0, tmp1: bool;
+
+    a0 := a0 && A;
+    tmp0 := a0;
+
+    havoc a0;
+
+    assert a0 ==> tmp0;
+
+    tmp1 := a0;
+
+    havoc a0;
+
+    assert a0 ==> tmp1;
 }
diff --git a/Test/test2/AssumptionVariables0.bpl.expect b/Test/test2/AssumptionVariables0.bpl.expect
index 54ddb2a9..44292082 100644
--- a/Test/test2/AssumptionVariables0.bpl.expect
+++ b/Test/test2/AssumptionVariables0.bpl.expect
@@ -1,11 +1,11 @@
-AssumptionVariables0.bpl(17,5): Error BP5001: This assertion might not hold.
-Execution trace:
-    AssumptionVariables0.bpl(15,8): anon0
-AssumptionVariables0.bpl(27,5): Error BP5001: This assertion might not hold.
-Execution trace:
-    AssumptionVariables0.bpl(25,5): anon0
-AssumptionVariables0.bpl(39,5): Error BP5001: This assertion might not hold.
-Execution trace:
-    AssumptionVariables0.bpl(37,8): anon0
-
-Boogie program verifier finished with 1 verified, 3 errors
+AssumptionVariables0.bpl(17,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    AssumptionVariables0.bpl(15,8): anon0
+AssumptionVariables0.bpl(27,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    AssumptionVariables0.bpl(25,5): anon0
+AssumptionVariables0.bpl(39,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    AssumptionVariables0.bpl(37,9): anon0
+
+Boogie program verifier finished with 3 verified, 3 errors