1 files changed, 0 insertions, 153 deletions
diff --git a/Chalice/tests/general-tests/counter.chalice b/Chalice/tests/general-tests/counter.chalice
deleted file mode 100644
index c15ed36b..00000000
--- a/Chalice/tests/general-tests/counter.chalice
+++ /dev/null
@@ -1,153 +0,0 @@
-class Counter {
-  var value: int;
-
-  invariant acc(value) && old(value)<=value;
-}
-
-class Program {
-
-  method main1(){
-    var counter := new Counter;
-    counter.value := 0;
-    share counter;
-
-    acquire counter;
-    var tmp1 := counter.value;
-    release counter;
-    
-    acquire counter;
-    var tmp2 := counter.value;
-    release counter;
-
-    assert tmp1 <= tmp2;
-  }
-
-  method main2(){
-    var counter := new Counter;
-    counter.value := 0;
-    share counter;
-
-    acquire counter;
-    release counter;
-
-    call bar(counter);
-  }
-
-  method bar(c: Counter)
-    requires c!=null && acc(c.mu) && waitlevel << c.mu;
-    requires eval(c.release, acc(c.value) && 0<=c.value);
-  {
-    lock (c) {
-      assert 0 <= c.value; // ok, because of the lastSeen conjunct in the precondition
-    }
-  }
-
-  method main3() returns (counter: Counter)
-    lockchange counter;
-  {
-    counter := new Counter;
-    counter.value := 0;
-    share counter;
-    acquire counter;
-    call doRelease(counter, counter.value);
-  }
-
-  method doRelease(c: Counter, i: int)
-    requires c!=null && holds(c) && acc(c.value) && eval(c.acquire, acc(c.value) && c.value <= i);
-    lockchange c;
-  {
-    c.value := i+1
-    release c; // ok, because of atAcquire conjunct in the precondition
-  }
-
-  method main4(){
-    var counter := new Counter;
-    counter.value := 0;
-    share counter;
-
-    acquire counter;
-    counter.value := counter.value - 1;
-    release counter;  // error: should fail
-  }
-
-  method main5(){
-    var counter := new Counter;
-    counter.value := 10;
-    share counter;
-
-    call foo(counter);
-
-    unshare counter;
-    assert 10<=counter.value; // error: should fail
-  }
-
-  method foo(c: Counter)
-    requires c!=null && acc(c.mu) && waitlevel << c.mu && eval(c.release, acc(c.value) && 10<=c.value);
-    ensures c!=null && holds(c) && acc(c.mu) && acc(c.value);
-    lockchange c;
-  {
-    acquire c;
-    unshare c;
-    c.value := 5;
-    share c;
-    acquire c;
-  }
-
-  method nestedGood0(c: Counter)
-    requires c != null && acc(c.mu) && waitlevel << c.mu;
-  {
-    lock (c) {
-      release c
-      acquire c
-    }
-  }
-
-  method nestedGood1(c: Counter)
-    requires c != null && acc(c.mu) && waitlevel << c.mu;
-  {
-    var t: Counter := c
-    lock (t) {
-      t := new Counter
-      share t
-      acquire t
-    }  // this line releases the original value for t
-    release t
-  }
-
-  method nestedBad0(c: Counter)
-    requires c != null && acc(c.mu) && waitlevel << c.mu;
-  {
-    lock (c) {
-      release c
-    }  // error: no longer holds c
-  }
-
-  method nestedBad1(c: Counter)
-    requires c != null && acc(c.mu) && waitlevel << c.mu;
-  {
-    lock (c) {
-      acquire c  // error: already holds c
-    }
-  }
-
-  method nestedBad2(c: Counter)
-    requires c != null && acc(c.mu) && waitlevel << c.mu;
-  {
-    lock (c) {
-      lock (c) {  // error: already holds c
-      }
-    }
-  }
-
-  method nestedBad3(c: Counter)
-    requires c != null && acc(c.mu) && waitlevel << c.mu;
-  {
-    var t: Counter := c
-    lock (t) {
-      release t
-      t := new Counter
-      share t
-      acquire t
-    }  // error: this line attempts to release the original t
-  }
-}
-\ No newline at end of file