1 files changed, 101 insertions, 10 deletions
diff --git a/Test/dafny0/ExistentialGuards.dfy.expect b/Test/dafny0/ExistentialGuards.dfy.expect
index cf229553..21461067 100644
--- a/Test/dafny0/ExistentialGuards.dfy.expect
+++ b/Test/dafny0/ExistentialGuards.dfy.expect
@@ -3,12 +3,19 @@
 // ExistentialGuards.dfy
 
 predicate P(n: int)
+{
+  n % 2 == 0
+}
 
 predicate R(r: real)
+{
+  0.0 <= r
+}
 
 method M0()
 {
   if x :| P(x) {
+    var y := x + 3;
   }
 }
 
@@ -20,13 +27,19 @@ method M1()
 
 method M2()
 {
+  var x := true;
   if x, y :| P(x) && R(y) {
+    var z := x + 12;
   }
+  x := x && false;
 }
 
 method M3()
 {
+  var x := true;
   if x: int, y :| P(x) && R(y) {
+    var z := x + y.Trunc;
+    var w := real(x) + y;
   }
 }
 
@@ -54,41 +67,119 @@ method M6()
   }
 }
 
-method M7()
+ghost method M7() returns (z: real, w: real)
+  ensures -2.0 <= z
+  ensures z == w
 {
+  var k;
   if x :| P(x) {
+    k, z := 4, 18.0;
   } else if * {
+    z := z + -z;
   } else if y :| R(y) {
+    z := y;
   } else if y :| P(y) {
+    k := y;
+  } else {
+    z :| R(z);
+  }
+  if P(k) {
+    z := 18.0;
   }
 }
 
+ghost method M8(m: int, n: int)
+  requires forall y :: m <= y < n ==> P(y)
+{
+  var t := -1;
+  var u;
+  if y :| m <= y < n && P(y) {
+    u := y;
+    if * {
+      t := n - y;
+    } else if * {
+      t := y - m;
+    } else if P(y) {
+      t := 8;
+    } else {
+      t := -100;
+    }
+  }
+  if t < 0 && m < n {
+    assert P(m) && !P(m);
+    assert false;
+  }
+  assert t < 0 ==> n <= m;
+}
+
 method P0(m: int, n: int)
   requires m < n
 {
+  ghost var even, alsoEven := 4, 8;
   if {
     case x :| P(x) =>
+      even := x;
     case x: int :| P(x) =>
+      even := x;
     case x, y :| P(x) && R(y) =>
+      even, alsoEven := x, y.Trunc;
     case x: int, y :| P(x) && R(y) =>
+      even := x;
     case m < n =>
     case x, y: real :| P(x) && R(y) =>
+      even := x;
     case x: int, y: real :| P(x) && R(y) =>
+      even := x;
   }
+  assert P(even);
+  assert P(alsoEven);
 }
 
 method P1(m: int, n: int)
-  requires m < n
 {
   if {
-    case x {:myattribute x, "hello"} :| P(x) =>
-    case x, y {:myattribute y, "sveika"} :| P(x) && R(y) =>
-    case x: int {:myattribute x, "chello"} :| P(x) =>
-    case x {:myattribute x, "hola"} {:yourattribute x + x, "hej"} :| P(x) =>
-    case m < n =>
+    case x :| m <= x < n && P(x) =>
+  }
+}
+
+method P2(m: int, n: int)
+  requires forall y :: m <= y < n ==> P(y)
+{
+  if {
+    case x :| m <= x < n && P(x) =>
+  }
+}
+
+method P3(m: int, n: int)
+  requires m < n && forall y :: m <= y < n ==> P(y)
+{
+  assert P(m);
+  if {
+    case x :| m <= x < n && P(x) =>
   }
 }
+ExistentialGuards.dfy(85,10): Error BP5003: A postcondition might not hold on this return path.
+ExistentialGuards.dfy(71,12): Related location: This is the postcondition that might not hold.
+Execution trace:
+    (0,0): anon0
+    (0,0): anon12_Then
+    (0,0): anon9
+    (0,0): anon16_Then
+ExistentialGuards.dfy(134,9): Error: assertion violation
+ExistentialGuards.dfy(6,8): Related location
+Execution trace:
+    (0,0): anon0
+    (0,0): anon20_Then
+    (0,0): anon21_Then
+    (0,0): anon5
+    (0,0): anon17
+ExistentialGuards.dfy(139,2): Error: alternative cases fail to cover all possibilties
+Execution trace:
+    (0,0): anon0
+    (0,0): anon7_Else
+ExistentialGuards.dfy(147,2): Error: alternative cases fail to cover all possibilties
+Execution trace:
+    (0,0): anon0
+    (0,0): anon7_Else
 
-Dafny program verifier finished with 22 verified, 0 errors
-Compilation error: Function _module._default.P has no body
-Compilation error: Function _module._default.R has no body
+Dafny program verifier finished with 24 verified, 4 errors