1 files changed, 0 insertions, 74 deletions
diff --git a/Chalice/tests/refinements/TestCoupling.chalice b/Chalice/tests/refinements/TestCoupling.chalice
deleted file mode 100644
index a178c9b4..00000000
--- a/Chalice/tests/refinements/TestCoupling.chalice
+++ /dev/null
@@ -1,74 +0,0 @@
-class A0 {
-  var x: int;
-  var n: int;
-  var k: int;
-  
-  method inc()
-    requires acc(x) && acc(n);
-    ensures acc(x) && x == old(x) + 1;
-  {
-    x := x + 1;
-    n := n + 1;
-  }
-
-  method error() 
-    requires acc(x)
-    ensures acc(x)
-  {
-    x := x + 1;
-  } 
-}
-
-class A1 refines A0 {
-  var y: int;
-  var z: int;  
-  replaces x by acc(y) && acc(z) && x == y - z && y >= 0 && z >= 0;
-  
-  refines inc()
-    ensures y == old(y) + 1
-  {
-    this.y := 1 + this.y;
-    this.n := this.n + 1;    
-  }
-
-  refines error()     
-    ensures acc(y)
-  {
-    this.y := 1 + this.y;
-  }
-}
-
-class B0 {
-  var x: int; 
-  var y: int;
-  
-  method error()
-    requires acc(x);
-    ensures acc(x);
-  {
-    x := x + 1;     
-  }
-  
-  method inc()
-    requires acc(x) && acc(y);
-    ensures acc(x) && acc(y);
-  { 
-    x := x + 1;
-  }
-}
-
-class B1 refines B0 {
-  var z: int;
-  replaces x,y by acc(z) && z == x + y;
-
-  refines error() 
-  {
-    this.z := this.z + 1;
-  }
-
-  refines inc() 
-  {
-    this.z := this.z + 1;
-  }
-}
-