1 files changed, 0 insertions, 9 deletions
diff --git a/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy b/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy
index 3f68ee5d..774008b8 100644
--- a/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy
+++ b/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy
@@ -205,7 +205,6 @@ class Node {
       invariant forall k,l :: 0 <= k < l < steps ==> Nexxxt(k, S) != Nexxxt(l, S);
       decreases S - Visited;
     {
-assume 2<2;  // TEMPORARY HACK
       p, steps, Visited := p.next, steps + 1, Visited + {p};
     }
     if (p == null) {
@@ -219,7 +218,6 @@ assume 2<2;  // TEMPORARY HACK
         invariant forall k :: 0 <= k < A ==> Nexxxt(k, S) != p;
         decreases steps - A;
       {
-assume 2<2;  // TEMPORARY HACK
         A := A + 1;
       }
       B := steps - A;
@@ -228,13 +226,6 @@ assume 2<2;  // TEMPORARY HACK
     }
   }
 
-/**  TEMPORARY
-  ghost method AnalyzeList_Aux(S: set<Node>, steps: int, p: Node) returns (A: int)
-    ensures 0 <= A < steps;
-    ensures forall k :: 0 <= k < A ==> Nexxxt(k, S) != p;
-    ensures Nexxxt(A, S) == p;
-**/
-
   ghost method CrucialLemma(a: int, b: int, S: set<Node>)
     requires IsClosed(S);
     requires 0 <= a && 1 <= b;