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/dafny0/SeqFromArray.dfy | |
| 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/dafny0/SeqFromArray.dfy')
| -rw-r--r-- | Test/dafny0/SeqFromArray.dfy | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/Test/dafny0/SeqFromArray.dfy b/Test/dafny0/SeqFromArray.dfy index 629c5045..cf889804 100644 --- a/Test/dafny0/SeqFromArray.dfy +++ b/Test/dafny0/SeqFromArray.dfy @@ -53,7 +53,7 @@ method L(a: array<int>, c: array<int>, n: nat) case A == C =>
assert forall i :: 0 <= i < h ==> A[i] == C[i];
case A == C =>
- assert forall i :: 0 <= i < h ==> a[n+i] == c[n+i];
+ assert forall i :: n <= i < n + h ==> a[i] == c[i];
case true =>
}
}
@@ -73,13 +73,13 @@ method M(a: array<int>, c: array<int>, m: nat, n: nat, k: nat, l: nat) } else if * {
assert forall i :: 0 <= i < n ==> A[i] == C[i];
} else if * {
- assert forall i :: k <= i < k+n ==> A[i-k] == C[i-k];
+ assert forall i {:nowarn} :: k <= i < k+n ==> A[i-k] == C[i-k];
} else if * {
assert forall i :: 0 <= i < n ==> A[i] == a[k+i];
} else if * {
assert forall i :: 0 <= i < n ==> C[i] == c[l+i];
} else if * {
- assert forall i :: 0 <= i < n ==> a[k+i] == c[l+i];
+ assert forall i {:nowarn} :: 0 <= i < n ==> a[k+i] == c[l+i];
}
}
case l+m <= c.Length && forall i :: 0 <= i < m ==> a[i] == c[l+i] =>
|