1 files changed, 0 insertions, 136 deletions
diff --git a/Chalice/tests/refinements/experiments/CounterPredicate.chalice b/Chalice/tests/refinements/experiments/CounterPredicate.chalice
deleted file mode 100644
index fd35c18c..00000000
--- a/Chalice/tests/refinements/experiments/CounterPredicate.chalice
+++ /dev/null
@@ -1,136 +0,0 @@
-class Cell {
-  var n : int;
-}
-
-class A {
-  var x : int;
-
-  predicate valid { 
-    acc(x) && x >= 0 
-  }
-
-  function getX(): int requires valid 
-  { 
-    unfolding valid in x 
-  }
-
-  method init()
-    requires acc(this.*);
-    ensures valid;
-  {
-    x := 0;
-    fold valid;
-  }
-
-  method inc()
-    requires valid;
-    ensures valid && getX() == old(getX()) + 1;
-  {
-    unfold valid;
-    x := x + 1;
-    fold valid;
-  } 
-
-  method dec()
-    requires valid && getX() > 0;
-    ensures valid;
-  {    
-    unfold valid;
-    x := x - 1;
-    fold valid;
-  }
-
-  method magic() returns (c: Cell) 
-    requires valid;
-    ensures valid;
-  {
-  }
-}
-
-class C {
-  ghost var x : int;
-  var y : Cell;
-  var z : Cell;
-  
-  function getX() : int
-    requires valid;
-  { 
-    unfolding valid in y.n - z.n 
-  }
-
-  predicate valid {
-    acc(x) && acc(y) && acc(z) && acc(y.n) && acc(z.n) &&
-    y != null && z != null && 
-    y.n >= 0 && z.n >= 0 &&
-    y.n - z.n == x &&
-    x >= 0
-  }
-  
-  method init()
-    requires acc(this.*);
-    ensures valid;
-  {
-    x := 0;
-    //
-    y := new Cell;
-    z := new Cell;
-    y.n := 0;
-    z.n := 0;    
-    fold valid;
-  }
-
-  method inc() 
-    requires valid;
-    ensures valid && getX() == old(getX()) + 1;
-  {
-    unfold valid;
-    x := x + 1;
-    //
-    y.n := y.n + 1; 
-    fold valid;
-  }
-
-  method dec()
-    requires valid && getX() > 0;
-    ensures valid;
-  {
-    unfold valid;
-    x := x - 1;
-    //
-    z.n := z.n + 1;
-    fold valid;
-  }
-
-  method magic() returns (c: Cell)
-    requires valid;
-    ensures valid;
-  {
-    unfold valid;
-    c := y;
-    fold valid;
-  }
-}
-
-class Client {
-  method main() 
-  {
-    // Abstract program
-    var a := new A;    
-    call a.init();
-    call a.inc(); // problem is here
-    call a.inc();
-    call a.dec();
-    call ac := a.magic();
-    ac.n := 0; 
-  
-    // Concrete program
-    var c := new C;
-    call c.init();
-    call c.inc();
-    call c.inc();
-    call c.dec();
-    call cc := c.magic();
-    cc.n := 0; 
-  }
-}
-