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/VerifyThis2015/Problem2.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Test/VerifyThis2015') diff --git a/Test/VerifyThis2015/Problem2.dfy b/Test/VerifyThis2015/Problem2.dfy index 1c7deffd..86b4a019 100644 --- a/Test/VerifyThis2015/Problem2.dfy +++ b/Test/VerifyThis2015/Problem2.dfy @@ -315,7 +315,7 @@ lemma GcdDecrease(a: int, b: int) ensures Gcd(a, b) == Gcd(a - b, b) { var k := Gcd(a - b, b); - assert DividesBoth(k, a-b, b) && forall m :: DividesBoth(m, a-b, b) ==> m <= k; + assert DividesBoth(k, a-b, b) && forall m, mm :: mm == a - b ==> DividesBoth(m, mm, b) ==> m <= k; // WISH: auto-generate 'mm' var n := DividesProperty(k, a-b); assert n*k == a-b; var p := DividesProperty(k, b); -- cgit v1.2.3