1 files changed, 0 insertions, 109 deletions
diff --git a/Chalice/tests/general-tests/prog0.chalice b/Chalice/tests/general-tests/prog0.chalice
deleted file mode 100644
index fb835a24..00000000
--- a/Chalice/tests/general-tests/prog0.chalice
+++ /dev/null
@@ -1,109 +0,0 @@
-class C {
-  method m() {
-    assert 4 + (a * 5) + (2 + 3) * (a + a);
-    a := a + 3;
-    b := a - b - c + 4 * d + 20 + --25;
-    b := ((((a - b) - c) + 4 * d) + 20) + --25;
-    c := a - (b - (c + (4 * d + (20 + 25))));
-    assert (X ==> Y) ==> Z <==> A ==> B ==> C;
-    assume A && B && (C || D || E) && F;
-    var x;
-    var y := 12 + !(x.f.g).h - (!x).f + (!x.f);
-    var z := new C;
-    y := new D;
-    o.f := 5;
-    (a + b).y := new T;
-    reorder (2 ==(O != 3)) != O between a,b,c and x,y,z;
-    reorder X ==> Y below x+5;
-    reorder o.f above this, null;
-    share o;
-    unshare o;
-    acquire o;
-    release o;
-    rd acquire o;
-    rd release o;
-    downgrade o;
-    var tok: token<C.m>;
-    fork tok := o.m();
-    join tok;
-    assert rd(x) + acc(y) + acc(z, 1/4) + old(old(k)) + null.f;
-    x := this.f;
-    call m(2,3,4);
-    call this.m(2,3,4);
-    call a,b,c := o.m();
-    call x := m(200);
-    reorder o above waitlevel;
-  }
-  method p(a,b,c) returns (x,y,z)
-    requires 8 + 2 == 10;
-    ensures 8 + 5 > 10;
-    requires x == y+1;
-    ensures old(x) < x;
-  {
-    if (x == 7) {
-      y := y + 1;  z := z + 2;
-    } else if (x == 8) {
-      y := 2;
-    } else {
-      z := 10;
-    }
-    {  // empty block
-    }
-    if (x == 9) { }
-    if (x == 10) { x := 10; } else { }
-    var n := 0;
-    while (n < 100) { n := n - 1; }
-    while (n != 0)
-      invariant n % 2 == 0;
-      invariant sqrt2 * sqrt2 == 2;
-    {
-      n := n - 2;
-    }
-    call v,x := s.M(65);
-  }
-}
-class D { }
-
-// ----- tests specifically of implicit locals in CALL and RECEIVE statements
-
-class ImplicitC {
-  var k: int;
-
-  method MyMethod() returns (x: int, y: ImplicitC)
-    requires acc(k)
-    ensures acc(y.k) && x < y.k
-  {
-    x := k - 15;
-    y := this;
-  }
-
-  method B0() {
-    var c := new ImplicitC;
-    call a, b := c.MyMethodX();  // error: method not found (so what is done with a,b?)
-    assert a < b.k;
-  }
-
-  method B1() {
-    var c := new ImplicitC;
-    call a, a := c.MyMethod();  // error: a occurs twice
-    assert a < b.k;
-  }
-
-  method D0() {
-    var ch := new Ch;
-    var c := new ImplicitC;
-    send ch(c.k - 15, c);  // give ourselves some credit
-    receive a, b := chX;  // error: channel not found (so what is done with a,b?)
-    assert a < b.k;
-  }
-
-  method D1() {
-    var ch := new Ch;
-    var c := new ImplicitC;
-    send ch(c.k - 15, c);  // give ourselves some credit
-    receive a, a := ch;  // error: a occurs twice
-    assert a < b.k;
-  }
-}
-
-channel Ch(x: int, y: ImplicitC) where acc(y.k) && x < y.k;