From 5f90de32e39ee691492048c08cb46215d2e9a062 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Wed, 7 Oct 2015 17:01:21 -0700
Subject: Renamed ExistentialGuards... to BindingGuards...

---
 Test/dafny0/BindingGuards.dfy                      | 159 ++++++++++++++++++
 Test/dafny0/BindingGuards.dfy.expect               | 183 +++++++++++++++++++++
 Test/dafny0/BindingGuardsResolution.dfy            | 154 +++++++++++++++++
 Test/dafny0/BindingGuardsResolution.dfy.expect     | 165 +++++++++++++++++++
 Test/dafny0/ExistentialGuards.dfy                  | 159 ------------------
 Test/dafny0/ExistentialGuards.dfy.expect           | 183 ---------------------
 Test/dafny0/ExistentialGuardsResolution.dfy        | 154 -----------------
 Test/dafny0/ExistentialGuardsResolution.dfy.expect | 165 -------------------
 8 files changed, 661 insertions(+), 661 deletions(-)
 create mode 100644 Test/dafny0/BindingGuards.dfy
 create mode 100644 Test/dafny0/BindingGuards.dfy.expect
 create mode 100644 Test/dafny0/BindingGuardsResolution.dfy
 create mode 100644 Test/dafny0/BindingGuardsResolution.dfy.expect
 delete mode 100644 Test/dafny0/ExistentialGuards.dfy
 delete mode 100644 Test/dafny0/ExistentialGuards.dfy.expect
 delete mode 100644 Test/dafny0/ExistentialGuardsResolution.dfy
 delete mode 100644 Test/dafny0/ExistentialGuardsResolution.dfy.expect

(limited to 'Test/dafny0')

diff --git a/Test/dafny0/BindingGuards.dfy b/Test/dafny0/BindingGuards.dfy
new file mode 100644
index 00000000..0706fc5b
--- /dev/null
+++ b/Test/dafny0/BindingGuards.dfy
@@ -0,0 +1,159 @@
+// RUN: %dafny /dprint:- /env:0 "%s" > "%t"
+// 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;
+  }
+}
+
+method M1()
+{
+  if x: int :| P(x) {
+  }
+}
+
+method M2()
+{
+  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;
+  }
+}
+
+method M4()
+{
+  if x, y: real :| P(x) && R(y) {
+  }
+}
+
+method M5()
+{
+  if x: int, y: real :| P(x) && R(y) {
+  }
+}
+
+method M6()
+{
+  if x {:myattribute x, "hello"} :| P(x) {
+  }
+  if x, y {:myattribute y, "sveika"} :| P(x) && R(y) {
+  }
+  if x: int {:myattribute x, "chello"} :| P(x) {
+  }
+  if x {:myattribute x, "hola"} {:yourattribute x + x, "hej"} :| P(x) {
+  }
+}
+
+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)
+{
+  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 :| m <= x < n && P(x) =>
+  }
+}
diff --git a/Test/dafny0/BindingGuards.dfy.expect b/Test/dafny0/BindingGuards.dfy.expect
new file mode 100644
index 00000000..b7da7b9e
--- /dev/null
+++ b/Test/dafny0/BindingGuards.dfy.expect
@@ -0,0 +1,183 @@
+// BindingGuards.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;
+  }
+}
+
+method M1()
+{
+  if x: int :| P(x) {
+  }
+}
+
+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;
+  }
+}
+
+method M4()
+{
+  if x, y: real :| P(x) && R(y) {
+  }
+}
+
+method M5()
+{
+  if x: int, y: real :| P(x) && R(y) {
+  }
+}
+
+method M6()
+{
+  if x {:myattribute x, "hello"} :| P(x) {
+  }
+  if x, y {:myattribute y, "sveika"} :| P(x) && R(y) {
+  }
+  if x: int {:myattribute x, "chello"} :| P(x) {
+  }
+  if x {:myattribute x, "hola"} {:yourattribute x + x, "hej"} :| P(x) {
+  }
+}
+
+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)
+{
+  if {
+    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) =>
+  }
+}
+BindingGuards.dfy(85,10): Error BP5003: A postcondition might not hold on this return path.
+BindingGuards.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
+BindingGuards.dfy(134,9): Error: assertion violation
+BindingGuards.dfy(6,8): Related location
+Execution trace:
+    (0,0): anon0
+    (0,0): anon20_Then
+    (0,0): anon21_Then
+    (0,0): anon5
+    (0,0): anon17
+BindingGuards.dfy(139,2): Error: alternative cases fail to cover all possibilties
+Execution trace:
+    (0,0): anon0
+    (0,0): anon7_Else
+BindingGuards.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 24 verified, 4 errors
diff --git a/Test/dafny0/BindingGuardsResolution.dfy b/Test/dafny0/BindingGuardsResolution.dfy
new file mode 100644
index 00000000..e2b55a99
--- /dev/null
+++ b/Test/dafny0/BindingGuardsResolution.dfy
@@ -0,0 +1,154 @@
+// RUN: %dafny /dprint:- /env:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+predicate P(n: int)
+
+predicate R(r: real)
+
+method M0()
+{
+  if x :| P(x) {
+    var y := x + 3;
+    var x := true;  // error: 'x' is already declared in this scope
+  }
+}
+
+method M1()
+{
+  if x: int :| P(x) {
+    x := x + 1;  // error: 'x' is an immutable variable
+  }
+}
+
+method M2()
+{
+  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 + int(y);
+    var w := real(x) + y;
+  }
+  var x := 0.0;  // error: 'x' is already declared in this scope
+}
+
+method M4()
+{
+  if x, y: real :| P(x) && R(y) {
+  }
+}
+
+method M5()
+{
+  if x: int, y: real :| P(x) && R(y) {
+  }
+}
+
+method M6()
+{
+  if x {:myattribute x, "hello"} :| P(x) {
+  }
+  if x, y {:myattribute y, "sveika"} :| P(x) && R(y) {
+  }
+  if x: int {:myattribute x, "chello"} :| P(x) {
+  }
+  if x {:myattribute x, "hola"} {:yourattribute x + x, "hej"} :| P(x) {
+  }
+}
+
+method M7()
+{
+  if x :| P(x) {
+  } else if * {
+  } else if y :| R(y) {
+  } else if y :| P(y) {
+  }
+}
+
+method P0(m: int, n: int)
+  requires m < n
+{
+  var x := true;
+  if {
+    case x :| P(x) =>
+      var t := 3 * x;
+    case x: int :| P(x) =>
+    case x, y :| P(x) && R(y) =>
+      y := y + 1.0;  // error: 'y' is an immutable variable
+    case x: int, y :| P(x) && R(y) =>
+    case m < n =>
+      x := x || m + 5 == n;
+    case x, y: real :| P(x) && R(y) =>
+    case x: int, y: real :| P(x) && R(y) =>
+  }
+  assert x;
+}
+
+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 =>
+  }
+}
+
+module TypesNotFullyDetermined {
+  method T0()
+  {
+    if x :| true {  // error: type not entirely resolved
+    }
+  }
+  method T1()
+  {
+    if x :| true {
+      var y := x + 3;
+    }
+  }
+}
+
+module Ghost {
+  predicate P(x: int)  // note, P is ghost
+  predicate method R(x: int)
+  method M7() returns (z: int, b: bool)
+  {
+    if * {
+      z := z + -z;
+    } else if y :| 1000 <= y < 2000 && R(y) {
+      z := y;
+    } else if y :| 0 <= y < 100 && P(y) {
+      z := y;  // error: not allowed, because the P in the guard makes this a ghost context
+    } else if y :| 0 <= y < 100 && R(y) {
+      z := y;  // error: this is also in a ghost context, because it depends on the P above
+    }
+
+    if * {
+      z := z + -z;
+    } else if exists y :: 1000 <= y < 2000 && R(y) {
+      z := 0;
+    } else if exists y :: 0 <= y < 100 && P(y) {
+      z := 0;  // error: not allowed, because the P in the guard makes this a ghost context
+    } else if exists y :: 0 <= y < 100 && R(y) {
+      z := 0;  // error: this is also in a ghost context, because it depends on the P above
+    }
+
+    if P(z) {
+      z := 20;  // error: blatant ghost context
+    }
+
+    b := exists y :: 0 <= y < 100 && P(y);  // error: assignment to non-ghost of something that depends on ghost
+    ghost var c;
+    c := exists y :: 0 <= y < 100 && P(y);
+    b := exists y {:myattribute P(y)} :: 0 <= y < 100;
+  }
+}
diff --git a/Test/dafny0/BindingGuardsResolution.dfy.expect b/Test/dafny0/BindingGuardsResolution.dfy.expect
new file mode 100644
index 00000000..b6f23805
--- /dev/null
+++ b/Test/dafny0/BindingGuardsResolution.dfy.expect
@@ -0,0 +1,165 @@
+// BindingGuardsResolution.dfy
+
+
+module TypesNotFullyDetermined {
+  method T0()
+  {
+    if x :| true {
+    }
+  }
+
+  method T1()
+  {
+    if x :| true {
+      var y := x + 3;
+    }
+  }
+}
+
+module Ghost {
+  predicate P(x: int)
+
+  predicate method R(x: int)
+
+  method M7() returns (z: int, b: bool)
+  {
+    if * {
+      z := z + -z;
+    } else if y :| 1000 <= y < 2000 && R(y) {
+      z := y;
+    } else if y :| 0 <= y < 100 && P(y) {
+      z := y;
+    } else if y :| 0 <= y < 100 && R(y) {
+      z := y;
+    }
+    if * {
+      z := z + -z;
+    } else if exists y :: 1000 <= y < 2000 && R(y) {
+      z := 0;
+    } else if exists y :: 0 <= y < 100 && P(y) {
+      z := 0;
+    } else if exists y :: 0 <= y < 100 && R(y) {
+      z := 0;
+    }
+    if P(z) {
+      z := 20;
+    }
+    b := exists y :: 0 <= y < 100 && P(y);
+    ghost var c;
+    c := exists y :: 0 <= y < 100 && P(y);
+    b := exists y {:myattribute P(y)} :: 0 <= y < 100;
+  }
+}
+predicate P(n: int)
+
+predicate R(r: real)
+
+method M0()
+{
+  if x :| P(x) {
+    var y := x + 3;
+    var x := true;
+  }
+}
+
+method M1()
+{
+  if x: int :| P(x) {
+    x := x + 1;
+  }
+}
+
+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 + int(y);
+    var w := real(x) + y;
+  }
+  var x := 0.0;
+}
+
+method M4()
+{
+  if x, y: real :| P(x) && R(y) {
+  }
+}
+
+method M5()
+{
+  if x: int, y: real :| P(x) && R(y) {
+  }
+}
+
+method M6()
+{
+  if x {:myattribute x, "hello"} :| P(x) {
+  }
+  if x, y {:myattribute y, "sveika"} :| P(x) && R(y) {
+  }
+  if x: int {:myattribute x, "chello"} :| P(x) {
+  }
+  if x {:myattribute x, "hola"} {:yourattribute x + x, "hej"} :| P(x) {
+  }
+}
+
+method M7()
+{
+  if x :| P(x) {
+  } else if * {
+  } else if y :| R(y) {
+  } else if y :| P(y) {
+  }
+}
+
+method P0(m: int, n: int)
+  requires m < n
+{
+  var x := true;
+  if {
+    case x :| P(x) =>
+      var t := 3 * x;
+    case x: int :| P(x) =>
+    case x, y :| P(x) && R(y) =>
+      y := y + 1.0;
+    case x: int, y :| P(x) && R(y) =>
+    case m < n =>
+      x := x || m + 5 == n;
+    case x, y: real :| P(x) && R(y) =>
+    case x: int, y: real :| P(x) && R(y) =>
+  }
+  assert x;
+}
+
+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 =>
+  }
+}
+BindingGuardsResolution.dfy(109,7): Error: type of bound variable 'x' could not be determined; please specify the type explicitly
+BindingGuardsResolution.dfy(130,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+BindingGuardsResolution.dfy(132,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+BindingGuardsResolution.dfy(140,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+BindingGuardsResolution.dfy(142,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+BindingGuardsResolution.dfy(146,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+BindingGuardsResolution.dfy(149,37): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
+BindingGuardsResolution.dfy(12,8): Error: Duplicate local-variable name: x
+BindingGuardsResolution.dfy(19,4): Error: LHS of assignment must denote a mutable variable
+BindingGuardsResolution.dfy(39,6): Error: Duplicate local-variable name: x
+BindingGuardsResolution.dfy(84,6): Error: LHS of assignment must denote a mutable variable
+11 resolution/type errors detected in BindingGuardsResolution.dfy
diff --git a/Test/dafny0/ExistentialGuards.dfy b/Test/dafny0/ExistentialGuards.dfy
deleted file mode 100644
index 0706fc5b..00000000
--- a/Test/dafny0/ExistentialGuards.dfy
+++ /dev/null
@@ -1,159 +0,0 @@
-// RUN: %dafny /dprint:- /env:0 "%s" > "%t"
-// 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;
-  }
-}
-
-method M1()
-{
-  if x: int :| P(x) {
-  }
-}
-
-method M2()
-{
-  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;
-  }
-}
-
-method M4()
-{
-  if x, y: real :| P(x) && R(y) {
-  }
-}
-
-method M5()
-{
-  if x: int, y: real :| P(x) && R(y) {
-  }
-}
-
-method M6()
-{
-  if x {:myattribute x, "hello"} :| P(x) {
-  }
-  if x, y {:myattribute y, "sveika"} :| P(x) && R(y) {
-  }
-  if x: int {:myattribute x, "chello"} :| P(x) {
-  }
-  if x {:myattribute x, "hola"} {:yourattribute x + x, "hej"} :| P(x) {
-  }
-}
-
-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)
-{
-  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 :| m <= x < n && P(x) =>
-  }
-}
diff --git a/Test/dafny0/ExistentialGuards.dfy.expect b/Test/dafny0/ExistentialGuards.dfy.expect
deleted file mode 100644
index 65e9f179..00000000
--- a/Test/dafny0/ExistentialGuards.dfy.expect
+++ /dev/null
@@ -1,183 +0,0 @@
-// 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;
-  }
-}
-
-method M1()
-{
-  if x: int :| P(x) {
-  }
-}
-
-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;
-  }
-}
-
-method M4()
-{
-  if x, y: real :| P(x) && R(y) {
-  }
-}
-
-method M5()
-{
-  if x: int, y: real :| P(x) && R(y) {
-  }
-}
-
-method M6()
-{
-  if x {:myattribute x, "hello"} :| P(x) {
-  }
-  if x, y {:myattribute y, "sveika"} :| P(x) && R(y) {
-  }
-  if x: int {:myattribute x, "chello"} :| P(x) {
-  }
-  if x {:myattribute x, "hola"} {:yourattribute x + x, "hej"} :| P(x) {
-  }
-}
-
-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)
-{
-  if {
-    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 24 verified, 4 errors
diff --git a/Test/dafny0/ExistentialGuardsResolution.dfy b/Test/dafny0/ExistentialGuardsResolution.dfy
deleted file mode 100644
index e2b55a99..00000000
--- a/Test/dafny0/ExistentialGuardsResolution.dfy
+++ /dev/null
@@ -1,154 +0,0 @@
-// RUN: %dafny /dprint:- /env:0 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-
-predicate P(n: int)
-
-predicate R(r: real)
-
-method M0()
-{
-  if x :| P(x) {
-    var y := x + 3;
-    var x := true;  // error: 'x' is already declared in this scope
-  }
-}
-
-method M1()
-{
-  if x: int :| P(x) {
-    x := x + 1;  // error: 'x' is an immutable variable
-  }
-}
-
-method M2()
-{
-  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 + int(y);
-    var w := real(x) + y;
-  }
-  var x := 0.0;  // error: 'x' is already declared in this scope
-}
-
-method M4()
-{
-  if x, y: real :| P(x) && R(y) {
-  }
-}
-
-method M5()
-{
-  if x: int, y: real :| P(x) && R(y) {
-  }
-}
-
-method M6()
-{
-  if x {:myattribute x, "hello"} :| P(x) {
-  }
-  if x, y {:myattribute y, "sveika"} :| P(x) && R(y) {
-  }
-  if x: int {:myattribute x, "chello"} :| P(x) {
-  }
-  if x {:myattribute x, "hola"} {:yourattribute x + x, "hej"} :| P(x) {
-  }
-}
-
-method M7()
-{
-  if x :| P(x) {
-  } else if * {
-  } else if y :| R(y) {
-  } else if y :| P(y) {
-  }
-}
-
-method P0(m: int, n: int)
-  requires m < n
-{
-  var x := true;
-  if {
-    case x :| P(x) =>
-      var t := 3 * x;
-    case x: int :| P(x) =>
-    case x, y :| P(x) && R(y) =>
-      y := y + 1.0;  // error: 'y' is an immutable variable
-    case x: int, y :| P(x) && R(y) =>
-    case m < n =>
-      x := x || m + 5 == n;
-    case x, y: real :| P(x) && R(y) =>
-    case x: int, y: real :| P(x) && R(y) =>
-  }
-  assert x;
-}
-
-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 =>
-  }
-}
-
-module TypesNotFullyDetermined {
-  method T0()
-  {
-    if x :| true {  // error: type not entirely resolved
-    }
-  }
-  method T1()
-  {
-    if x :| true {
-      var y := x + 3;
-    }
-  }
-}
-
-module Ghost {
-  predicate P(x: int)  // note, P is ghost
-  predicate method R(x: int)
-  method M7() returns (z: int, b: bool)
-  {
-    if * {
-      z := z + -z;
-    } else if y :| 1000 <= y < 2000 && R(y) {
-      z := y;
-    } else if y :| 0 <= y < 100 && P(y) {
-      z := y;  // error: not allowed, because the P in the guard makes this a ghost context
-    } else if y :| 0 <= y < 100 && R(y) {
-      z := y;  // error: this is also in a ghost context, because it depends on the P above
-    }
-
-    if * {
-      z := z + -z;
-    } else if exists y :: 1000 <= y < 2000 && R(y) {
-      z := 0;
-    } else if exists y :: 0 <= y < 100 && P(y) {
-      z := 0;  // error: not allowed, because the P in the guard makes this a ghost context
-    } else if exists y :: 0 <= y < 100 && R(y) {
-      z := 0;  // error: this is also in a ghost context, because it depends on the P above
-    }
-
-    if P(z) {
-      z := 20;  // error: blatant ghost context
-    }
-
-    b := exists y :: 0 <= y < 100 && P(y);  // error: assignment to non-ghost of something that depends on ghost
-    ghost var c;
-    c := exists y :: 0 <= y < 100 && P(y);
-    b := exists y {:myattribute P(y)} :: 0 <= y < 100;
-  }
-}
diff --git a/Test/dafny0/ExistentialGuardsResolution.dfy.expect b/Test/dafny0/ExistentialGuardsResolution.dfy.expect
deleted file mode 100644
index c9b62ff5..00000000
--- a/Test/dafny0/ExistentialGuardsResolution.dfy.expect
+++ /dev/null
@@ -1,165 +0,0 @@
-// ExistentialGuardsResolution.dfy
-
-
-module TypesNotFullyDetermined {
-  method T0()
-  {
-    if x :| true {
-    }
-  }
-
-  method T1()
-  {
-    if x :| true {
-      var y := x + 3;
-    }
-  }
-}
-
-module Ghost {
-  predicate P(x: int)
-
-  predicate method R(x: int)
-
-  method M7() returns (z: int, b: bool)
-  {
-    if * {
-      z := z + -z;
-    } else if y :| 1000 <= y < 2000 && R(y) {
-      z := y;
-    } else if y :| 0 <= y < 100 && P(y) {
-      z := y;
-    } else if y :| 0 <= y < 100 && R(y) {
-      z := y;
-    }
-    if * {
-      z := z + -z;
-    } else if exists y :: 1000 <= y < 2000 && R(y) {
-      z := 0;
-    } else if exists y :: 0 <= y < 100 && P(y) {
-      z := 0;
-    } else if exists y :: 0 <= y < 100 && R(y) {
-      z := 0;
-    }
-    if P(z) {
-      z := 20;
-    }
-    b := exists y :: 0 <= y < 100 && P(y);
-    ghost var c;
-    c := exists y :: 0 <= y < 100 && P(y);
-    b := exists y {:myattribute P(y)} :: 0 <= y < 100;
-  }
-}
-predicate P(n: int)
-
-predicate R(r: real)
-
-method M0()
-{
-  if x :| P(x) {
-    var y := x + 3;
-    var x := true;
-  }
-}
-
-method M1()
-{
-  if x: int :| P(x) {
-    x := x + 1;
-  }
-}
-
-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 + int(y);
-    var w := real(x) + y;
-  }
-  var x := 0.0;
-}
-
-method M4()
-{
-  if x, y: real :| P(x) && R(y) {
-  }
-}
-
-method M5()
-{
-  if x: int, y: real :| P(x) && R(y) {
-  }
-}
-
-method M6()
-{
-  if x {:myattribute x, "hello"} :| P(x) {
-  }
-  if x, y {:myattribute y, "sveika"} :| P(x) && R(y) {
-  }
-  if x: int {:myattribute x, "chello"} :| P(x) {
-  }
-  if x {:myattribute x, "hola"} {:yourattribute x + x, "hej"} :| P(x) {
-  }
-}
-
-method M7()
-{
-  if x :| P(x) {
-  } else if * {
-  } else if y :| R(y) {
-  } else if y :| P(y) {
-  }
-}
-
-method P0(m: int, n: int)
-  requires m < n
-{
-  var x := true;
-  if {
-    case x :| P(x) =>
-      var t := 3 * x;
-    case x: int :| P(x) =>
-    case x, y :| P(x) && R(y) =>
-      y := y + 1.0;
-    case x: int, y :| P(x) && R(y) =>
-    case m < n =>
-      x := x || m + 5 == n;
-    case x, y: real :| P(x) && R(y) =>
-    case x: int, y: real :| P(x) && R(y) =>
-  }
-  assert x;
-}
-
-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 =>
-  }
-}
-ExistentialGuardsResolution.dfy(109,7): Error: type of bound variable 'x' could not be determined; please specify the type explicitly
-ExistentialGuardsResolution.dfy(130,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
-ExistentialGuardsResolution.dfy(132,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
-ExistentialGuardsResolution.dfy(140,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
-ExistentialGuardsResolution.dfy(142,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
-ExistentialGuardsResolution.dfy(146,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
-ExistentialGuardsResolution.dfy(149,37): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
-ExistentialGuardsResolution.dfy(12,8): Error: Duplicate local-variable name: x
-ExistentialGuardsResolution.dfy(19,4): Error: LHS of assignment must denote a mutable variable
-ExistentialGuardsResolution.dfy(39,6): Error: Duplicate local-variable name: x
-ExistentialGuardsResolution.dfy(84,6): Error: LHS of assignment must denote a mutable variable
-11 resolution/type errors detected in ExistentialGuardsResolution.dfy
-- 
cgit v1.2.3