1 files changed, 78 insertions, 8 deletions
diff --git a/Test/dafny0/ExistentialGuards.dfy b/Test/dafny0/ExistentialGuards.dfy
index 001acb55..5afb3979 100644
--- a/Test/dafny0/ExistentialGuards.dfy
+++ b/Test/dafny0/ExistentialGuards.dfy
@@ -2,12 +2,19 @@
 // RUN: %diff "%s.expect" "%t"
 
 predicate P(n: int)
+{
+  n % 2 == 0
+}
 
 predicate R(r: real)
+{
+  0.0 <= r
+}
 
 method M0()
 {
   if x :| P(x) {
+    var y := x + 3;
   }
 }
 
@@ -19,13 +26,19 @@ method M1()
 
 method M2()
 {
-  if x, y :| P(x) && R(y) {
+  var x := true;
+  if x, y :| P(x) && R(y) {  // this declares a new 'x'
+    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;
   }
 }
 
@@ -53,37 +66,94 @@ method M6()
   }
 }
 
-method M7()
+ghost method M7() returns (z: real, w: real)
+  ensures -2.0 <= z
+  ensures z == w  // error: does not hold
 {
+  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;  // will never happen
+    }
+  }
+  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;  // this assigns to 'alsoEven' a possibly odd number
     case x: int, y :| P(x) && R(y) =>
+      even := x;
     case m < n =>  // just to be different
     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);  // error: may not hold
 }
 
 method P1(m: int, n: int)
-  requires m < n
 {
+  if {  // error: missing case
+    case x :| m <= x < n && P(x) =>
+  }
+}
+
+method P2(m: int, n: int)
+  requires forall y :: m <= y < n ==> P(y)
+{
+  if {  // error: missing case
+    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);  // lemma that proves that the following 'if' covers all possibilities
   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) =>
   }
 }