diff options
Diffstat (limited to 'Test/dafny2/COST-verif-comp-2011-3-TwoDuplicates.dfy')
| -rw-r--r-- | Test/dafny2/COST-verif-comp-2011-3-TwoDuplicates.dfy | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Test/dafny2/COST-verif-comp-2011-3-TwoDuplicates.dfy b/Test/dafny2/COST-verif-comp-2011-3-TwoDuplicates.dfy index 72a22cfd..4c702674 100644 --- a/Test/dafny2/COST-verif-comp-2011-3-TwoDuplicates.dfy +++ b/Test/dafny2/COST-verif-comp-2011-3-TwoDuplicates.dfy @@ -93,8 +93,8 @@ method Search(a: array<int>) returns (p: int, q: int) invariant forall j :: 0 <= j < d.Length ==>
(d[j] == -1 && forall k :: 0 <= k < i ==> a[k] != j) ||
(0 <= d[j] < i && a[d[j]] == j);
- invariant p == q ==> IsDuplicate(a, p);
- invariant forall k :: 0 <= k < i && IsPrefixDuplicate(a, i, a[k]) ==> p == q == a[k];
+ invariant p == q ==> IsDuplicate(a, p); //WISH remove the trigger on the next line
+ invariant forall k {:trigger old(a[k])} :: 0 <= k < i && IsPrefixDuplicate(a, i, a[k]) ==> p == q == a[k];
decreases a.Length - i;
{
var k := d[a[i]];
|