1 files changed, 0 insertions, 55 deletions
diff --git a/Chalice/tests/permission-model/peculiar.chalice b/Chalice/tests/permission-model/peculiar.chalice
deleted file mode 100644
index 31c4d259..00000000
--- a/Chalice/tests/permission-model/peculiar.chalice
+++ /dev/null
@@ -1,55 +0,0 @@
-class Cell {
-  var x: int;
-  
-  invariant rd(x);
-  
-  method t1()
-    requires acc(x);
-    ensures rd(x) && rd(x);
-  {
-  }
-  
-  method t2()
-    requires acc(x,1);
-    ensures rd(x);
-  {
-    call void();
-  }
-  
-  method t3()
-    requires rd(x);
-  {
-    call t3helper();
-  }
-  
-  method t3helper()
-    requires rd(x) && rd(x);
-    ensures rd(x) && rd(x);
-  {}
-  
-  method t4()
-    requires rd(x);
-  {
-    call dispose();
-    call void(); // call succeeds, even though the precondition is also rd(x), and the next assertion fails
-    assert(rd(x)); // ERROR: fails, as this check is done exactly (as it would in a postcondition)
-  }
-  
-  method t5(n: int)
-    requires acc(x);
-  {
-    var i: int := 0;
-    call req99();
-    while (i < n)
-      invariant rd*(x);
-    {
-      call dispose();
-      i := i+1
-    }
-  }
-    
-  method dispose() requires rd(x); {}
-  method void() requires rd(x); ensures rd(x); {}
-  method req99() requires acc(x,99); {}
-
-}