From c09814e1ae44a0bee53abb6e8e65b79c1da03d9e Mon Sep 17 00:00:00 2001
From: Valentin Wüstholz <wuestholz@gmail.com>
Date: Wed, 6 May 2015 17:52:52 +0200
Subject: Make it preserve the fact that the value of an assumption variable
 never becomes logically weaker after a havoc.

---
 Test/test2/AssumptionVariables0.bpl        | 41 +++++++++++++++++++++++++++---
 Test/test2/AssumptionVariables0.bpl.expect | 22 ++++++++--------
 2 files changed, 48 insertions(+), 15 deletions(-)

(limited to 'Test')

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
-- 
cgit v1.2.3