1 files changed, 0 insertions, 38 deletions
diff --git a/Chalice/tests/regressions/internal-bug-5.chalice b/Chalice/tests/regressions/internal-bug-5.chalice
deleted file mode 100644
index 35dfcb88..00000000
--- a/Chalice/tests/regressions/internal-bug-5.chalice
+++ /dev/null
@@ -1,38 +0,0 @@
-class Cell  {
-  var x: int;
-  var b: bool;
- 
-  predicate valid {
-    acc(this.b) && (this.b ==> acc(this.x,50))
-  }
-
-  method m()
-    requires this.valid && (unfolding valid in this.b) && acc(this.mu) && waitlevel << mu
-  {
-    acquire this;
-    
-    var c := (unfolding valid in this.x);
-    release this;
-    acquire this;
-    assert c == this.x;
-    call n();
-    c := (unfolding valid in this.x);
-    release this;
-    acquire this;
-    // ERROR: this is not supposed to verify (it did in previous versions of Chalice)
-    assert c == this.x;
-    release this;
-  }
-  
-  method n()
-    requires this.valid
-    ensures this.valid
-    {
-      unfold this.valid;
-      this.b := false;
-      fold this.valid;
-    }
-
-  invariant acc(this.x,50)
-}
-