diff options
author | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-28 20:50:50 -0700 |
---|---|---|
committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-28 20:50:50 -0700 |
commit | 95a42a224dff8eae383d93beb37a3da6a28bb0f3 (patch) | |
tree | 9a3b1f5fcba891aa5878a27528fa4ca619b8af6a /Test/dafny2 | |
parent | 3d45aa05a023c092167d938a72adf78cf1f76fdf (diff) |
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.
Diffstat (limited to 'Test/dafny2')
-rw-r--r-- | Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy | 4 |
1 files changed, 2 insertions, 2 deletions
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);
|