1 files changed, 0 insertions, 56 deletions
diff --git a/Chalice/tests/predicates/test4.chalice b/Chalice/tests/predicates/test4.chalice
deleted file mode 100644
index 201b643d..00000000
--- a/Chalice/tests/predicates/test4.chalice
+++ /dev/null
@@ -1,56 +0,0 @@
-class Cell
-{
-  var value:int;
-    
-  predicate P { acc(value,50) }
-    
-  function get():int
-    requires P;
-  {
-    unfolding P in value
-  }
-    
-  method boom(x:Cell, y:Cell)
-    requires x!=null && y!=null && x.P && y.P;
-	ensures x.P && y.P && (x==y ==> x.get()==100) && (x!=y ==> x.get()==old(x.get()));
-  {
-    if(x==y)
-	{
-	  unfold x.P; unfold x.P;
-	  y.value:=100;
-	  fold y.P; fold y.P;
-	}
-  }
-  
-  method skip()
-    requires P;
-	ensures P;
-  {}
-
-  // is the bookkeeping correct when calculating the secondary mask?
-  // fold happens once on a statically unknown object
-  // intermediate calls to skip happen in all examples to create artificial "changes" to the heap,
-  // thereby testing framing in the bookkeeping of folds/unfolds
-  method foo(z:Cell)
-    requires acc(value,50) && value==2 && z!=null && acc(z.value,50);
-  {	
-	fold z.P;
-	call z.skip();
-	fold P;
-	call boom(this, z);
-	assert this!=z ==> unfolding P in value==2;
-	assert this==z ==> unfolding P in value==100;
-  }
-  
-  // must fail: give away all permission, even in pieces, and you lose all information about value
-  method hoo()
-    requires acc(value);
-  {
-    fold P;
-	call skip();
-	fold P;
-	fork t:=skip();
-	call skip ();
-	assert unfolding P in value==old(value); // ERROR: should fail
-  }
-}
-\ No newline at end of file