1 files changed, 0 insertions, 75 deletions
diff --git a/Chalice/tests/examples/FictionallyDisjointCells.chalice b/Chalice/tests/examples/FictionallyDisjointCells.chalice
deleted file mode 100644
index d26dedbb..00000000
--- a/Chalice/tests/examples/FictionallyDisjointCells.chalice
+++ /dev/null
@@ -1,75 +0,0 @@
-class Cell
-{
-    var inner: InnerCell;
-    
-    predicate inv
-    {
-        acc(inner) && inner!=null && rd(inner.value,1) && rd*(inner.mu) && rd*(this.mu)
-    }
-    
-    method CellConstructor()
-        requires acc(inner) && acc(this.mu)
-        ensures inv && get()==0;
-    {
-        inner := new InnerCell;
-        call inner.InnerCellConstructor(0)
-        share inner;
-        fold inv;
-    }
-    
-    method CellConstructor2(other: Cell)
-        requires acc(inner) && acc(this.mu)
-        requires other != null && other.inv;
-        requires unfolding other.inv in waitlevel << other.inner.mu
-        ensures inv && other.inv && get()==other.get();
-    {
-        unfold other.inv;
-        inner := other.inner;
-        acquire inner;
-        inner.refCount := inner.refCount+1;
-        release inner;
-        fold other.inv;
-        fold inv;
-    }
-    
-    function get():int
-        requires inv;
-    { unfolding inv in inner.value }
-    
-    method set(x:int)
-        requires inv;
-        requires unfolding inv in waitlevel << inner.mu
-        ensures inv && get()==x;
-    {
-        var old_in: InnerCell;
-        unfold inv;
-        old_in := inner;
-        acquire old_in;
-        if (inner.refCount==1) { inner.value:=x; }
-        else
-        {
-            inner.refCount := inner.refCount-1;
-            inner := new InnerCell;
-            call inner.InnerCellConstructor(x)
-            share inner;
-        }
-        release old_in;
-        fold inv;
-    }
-}
-
-class InnerCell
-{
-    var value: int;
-    var refCount: int;
-    
-    invariant acc(refCount) && refCount > 0 && acc(value,100-rd(refCount));
-    
-    method InnerCellConstructor(val: int)
-        requires acc(refCount) && acc(value)
-        ensures acc(refCount) && acc(value) && refCount==1 && value == val;
-    {
-        refCount := 1;
-        value := val
-    }
-}