New logical encoding of types with Is and IsAlloc

1 files changed, 8 insertions, 0 deletions

diff --git a/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy b/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy
index 56f689da..ee56e14a 100644
--- a/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy
+++ b/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy
@@ -208,6 +208,14 @@ class Node {
       decreases S - Visited;

     {

       p, steps, Visited := p.next, steps + 1, Visited + {p};

+

+      // with all: 3s

+      // without this: 20s

+      assert forall t :: 0 <= t < steps ==> Nexxxt(t, S) in Visited;

+      // without this: 5s

+      assert forall q :: q in (Visited - {null}) ==> exists t :: 0 <= t < steps && Nexxxt(t, S) == q;

+      // without this: >60s

+      assert forall k,l :: 0 <= k < l < steps ==> Nexxxt(k, S) != Nexxxt(l, S);

     }

     if (p == null) {

       A, B := steps, 1;