1 files changed, 0 insertions, 43 deletions
diff --git a/Chalice/tests/refinements/LoopSqRoot.chalice b/Chalice/tests/refinements/LoopSqRoot.chalice
deleted file mode 100644
index 4ea9434d..00000000
--- a/Chalice/tests/refinements/LoopSqRoot.chalice
+++ /dev/null
@@ -1,43 +0,0 @@
-class A0 {
-  method sqroot(n) returns (x)
-    requires n >= 0;
-  { 
-    var x [x*x <= n && n < (x+1)*(x+1) && x >=0];    
-  }
-}
-
-class A1 refines A0 {
-  transforms sqroot(n) returns (x)
-  {
-    replaces x by {
-      var l := 0;
-      var r := n + 1;
-      while (l + 1 != r) 
-        invariant l >= 0 && r > l;
-        invariant l*l <= n && n < r*r;
-      {
-        var k [l < k && k < r];
-        if (k*k <= n) {
-          l := k;
-        } else {
-          r := k;
-        }
-      }
-      x := l;      
-    }
-  }
-}
-
-class A2 refines A1 {
-  transforms sqroot(n) returns (x)
-  {
-    _
-    while {
-      replaces k by {
-        var k [2*k <= l+r && l+r < 2*(k+1)]        
-      }
-      *
-    }
-    _
-  }
-}