1 files changed, 0 insertions, 82 deletions
diff --git a/Chalice/tests/general-tests/ll-lastnode.chalice b/Chalice/tests/general-tests/ll-lastnode.chalice
deleted file mode 100644
index f7a44cfe..00000000
--- a/Chalice/tests/general-tests/ll-lastnode.chalice
+++ /dev/null
@@ -1,82 +0,0 @@
-// This test case showed a triggering problem (and potentially a matching loop).
-// The quantified assertion and postcondition that did not verify are highlighted below.
-class Node
-{
-  var val:int
-  var next:Node
-  var break_here:bool
-  
-  predicate lseg
-  {
-    acc(break_here) && (!break_here ==> acc(val) && acc(next) && (next!=null ==> next.lseg))
-  }
-  
-  predicate xlseg
-  {
-    acc(val) && acc(next) && (next!=null ==> next.lseg)
-  }
-   
-  function length():int
-    requires lseg
-    ensures 0 <= result
-  {
-    unfolding lseg in (break_here ? 0 : (next==null ? 1 : 1+next.length()))
-  }   
-  
-  function xlength():int
-    requires xlseg
-    ensures 0 < result
-  {
-    unfolding xlseg in (next==null ? 1 : 1+next.length())
-  }
-    
-  function get(i:int):int
-    requires lseg && i>=0 && i<length()
-  {
-    unfolding lseg in i==0 ? val : next.get(i-1)
-  }
-        
-  function xget(i:int):int
-    requires xlseg && i>=0 && i<xlength()
-  {
-    unfolding xlseg in i==0 ? val : next.get(i-1)
-  }
-  
-   function get_next_seg():Node
-    requires lseg
-  {
-    unfolding lseg in break_here ? this : (next==null ? next : next.get_next_seg())
-  }
-  
-  method lastNode() returns(res:Node)
-    requires lseg && length()>0
-    ensures res != null && lseg && res.xlseg
-    ensures res.xlength()==1 && res.xget(0)==old(get(length()-1))
-    ensures length() == old(length()-1)
-    // Did not verify.
-    ensures (forall i:int :: 0<=i && i<length() ==> get(i) == old(get(i)))
-  {
-    var I:int
-	var h:Node
-	
-    res:=this
-	unfold lseg
-	break_here:=true
-	fold lseg
-	fold xlseg
-	
-    while(res.xlength()>1)
-      invariant res!=null && lseg && res.xlseg &&
-	            res==get_next_seg() && // new invariant
-                length() + res.xlength() == old(length()) &&
-                0 <= length() && length() < old(length()) && 
-                (forall i:int :: 0<=i && i<length() ==> get(i)==old(get(i))) &&
-                (forall i:int :: length()<=i && i<old(length()) ==> res.xget(i-length())==old(get(i)))
-    {
-        // We are not interested (at the moment) in verifying the loop.
-        assume false
-    }
-    // Did not verify.
-	assert (forall i:int :: length()<=i && i<old(length()) ==> res.xget(i-length())==old(get(i)))
-  }
-}
-\ No newline at end of file