1 files changed, 0 insertions, 46 deletions
diff --git a/Chalice/tests/refinements/RecSqRoot.chalice b/Chalice/tests/refinements/RecSqRoot.chalice
deleted file mode 100644
index a10c1b55..00000000
--- a/Chalice/tests/refinements/RecSqRoot.chalice
+++ /dev/null
@@ -1,46 +0,0 @@
-class A0 {
-  method sqroot(n) returns (x)
-    requires n >= 0;
-  {
-    var x [x*x <= n && n < (x+1)*(x+1)];      
-  }  
-}
-
-class A1 refines A0 {
-  transforms sqroot(n) returns (x)
-  {        
-    replaces x by {call x := rec(n,0,n+1)}    
-  }
-  
-  method rec(n, l, r) returns (x)
-    requires l*l <= n && n < r*r;
-    requires l >= 0 && r >= 0;
-    ensures x*x <= n && n < (x+1)*(x+1);
-  {
-    if (l+1 == r) {
-      x := l;
-    } else {
-      var k [l < k && k < r];
-      if (n < k*k) {
-        call x := rec(n,l,k);
-      } else {
-        call x := rec(n,k,r);
-      }
-    }
-  }
-}
-
-class A2 refines A1 {
-  transforms rec(n, l, r) returns (x)
-  {    
-    if {
-      *
-    } else {
-      replaces k by {
-        assert l < r;
-        var k := l+1;
-      }
-      *
-    }    
-  }
-}