From 95a42a224dff8eae383d93beb37a3da6a28bb0f3 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Fri, 28 Aug 2015 20:50:50 -0700 Subject: Suppress many warnings in the test suite. We already have separate tests for those, and we want the output to be the same with and without /autoTriggers. --- Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'Test/dafny2') diff --git a/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy b/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy index 2aa14db7..72250f99 100644 --- a/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy +++ b/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy @@ -164,7 +164,7 @@ class Node { invariant 0 <= t < h && Nexxxt(t, S) == tortoise && Nexxxt(h, S) == hare; // What follows of the invariant is for proving termination: invariant h == 1 + 2*t && t <= A + B; - invariant forall k :: 0 <= k < t ==> Nexxxt(k, S) != Nexxxt(1+2*k, S); + invariant forall k {:nowarn} :: 0 <= k < t ==> Nexxxt(k, S) != Nexxxt(1+2*k, S); decreases A + B - t; { if hare == null || hare.next == null { @@ -225,7 +225,7 @@ class Node { requires 0 <= a && 1 <= b; requires forall k,l :: 0 <= k < l < a ==> Nexxxt(k, S) != Nexxxt(l, S); requires Nexxxt(a, S) == null || Nexxxt(a, S).Nexxxt(b, S) == Nexxxt(a, S); - ensures exists T :: 0 <= T < a+b && Nexxxt(T, S) == Nexxxt(1+2*T, S); + ensures exists T {:nowarn} :: 0 <= T < a+b && Nexxxt(T, S) == Nexxxt(1+2*T, S); { if Nexxxt(a, S) == null { Lemma_NullIsTerminal(1+2*a, S); -- cgit v1.2.3