From f3cfd7a9994af3518655bc4d1d77eeb3619b0999 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Fri, 28 Aug 2015 21:05:19 -0700 Subject: Implement workarounds for some tests that fail with /autoTriggers. The issues here are mostly with induction (wrt. to trigger selection and quantifier splitting) and with expressions like P(i, j-1) where no good choices are available. --- Test/dafny2/COST-verif-comp-2011-3-TwoDuplicates.dfy | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'Test/dafny2/COST-verif-comp-2011-3-TwoDuplicates.dfy') 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) 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]]; -- cgit v1.2.3