1 files changed, 0 insertions, 92 deletions
diff --git a/Chalice/tests/general-tests/prog2.chalice b/Chalice/tests/general-tests/prog2.chalice
deleted file mode 100644
index 3b6f2783..00000000
--- a/Chalice/tests/general-tests/prog2.chalice
+++ /dev/null
@@ -1,92 +0,0 @@
-// 4 errors expected
-
-class C {
-  method M(x: int) returns (y: bool)
-    requires 0 <= x;
-    ensures y <==> x == 10;
-  {
-    y := true;
-    if (x != 10) { y := !y; }
-  }
-
-  method Caller0()
-  {
-    var b: bool;
-    call b := M(12);
-    assert !b;
-    call b := M(10);
-    assert b;
-  }
-  method Caller1()
-  {
-    var b: bool;
-    call b := M(11);
-    assert b; // error (258)
-  }
-
-  var F: int;
-
-  method P(n: int)
-    requires acc(F);
-    ensures F == old(F) + n;  // error
-  {
-    F := F + n;
-  }
-  method Caller2()
-    requires acc(F);
-  {
-    var prev := F;
-    call P(2);
-  }
-
-  method Q(n: int)
-    requires acc(F);
-    ensures acc(F) && F == old(F) + n;
-  {
-    F := F + n;
-  }
-  method Caller3()
-    requires acc(F);
-    ensures acc(F);
-  {
-    var prev := F;
-    call Q(2);
-    assert F == prev + 2;
-  }
-}
-
-class Consts {
-  method M0() returns (z: int)
-    ensures z == 5
-  {
-    const a := 5
-    z := a
-  }
-  method M1() {
-    ghost const a
-    a := 5
-  }
-  method M2() {
-    ghost const a
-    a := 5
-    a := 5  // error (569)
-  }
-  method M3(b: bool) {
-    ghost const a
-    if (b) { a := 5 }
-    assert a < 10  // error (611)
-  }
-  method M4(b: bool) {
-    ghost const a
-    if (b) { a := 5 }
-    ghost var x := a
-    if (!b) { a := 7 }
-    assert a < 10
-    assert b ==> x == 5  // cool, huh?
-  }
-  method M5(b: bool) {
-    ghost const a
-    if (b) { a := 5 }
-    assert assigned(a) ==> a == 5
-  }
-}