1 files changed, 0 insertions, 21 deletions
diff --git a/Chalice/tests/predicates/framing-fields.chalice b/Chalice/tests/predicates/framing-fields.chalice
deleted file mode 100644
index 6cfd4607..00000000
--- a/Chalice/tests/predicates/framing-fields.chalice
+++ /dev/null
@@ -1,21 +0,0 @@
-class List
-{
-  var value:int;
-  var next:List;
-  predicate valid { acc(value) && acc(next) && (next!=null ==> next.valid) }
- 
-  method set(x:int, y:int) requires valid; ensures valid; {}
-}
-
-class C
-{
-  method M (x:List, y:List)
-    requires x!=null && y!=null && x!=y && x.valid && y.valid;
-  {
-    var i: int := unfolding x.valid in x.value;
-    var j: int := unfolding y.valid in y.value;
-    call y.set(0,10);
-    assert unfolding x.valid in (i == x.value); // succeeds
-    assert unfolding y.valid in (j == y.value); // correctly fails to verify
- }
-}
-\ No newline at end of file