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/dafny3/InductionVsCoinduction.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Test/dafny3/InductionVsCoinduction.dfy') diff --git a/Test/dafny3/InductionVsCoinduction.dfy b/Test/dafny3/InductionVsCoinduction.dfy index 89fa6cc8..0074b742 100644 --- a/Test/dafny3/InductionVsCoinduction.dfy +++ b/Test/dafny3/InductionVsCoinduction.dfy @@ -80,7 +80,7 @@ lemma SAppendIsAssociative(a:Stream, b:Stream, c:Stream) { forall k:nat { SAppendIsAssociativeK(k, a, b, c); } // assert for clarity only, postcondition follows directly from it - assert (forall k:nat :: SAppend(SAppend(a, b), c) ==#[k] SAppend(a, SAppend(b, c))); + assert (forall k:nat {:autotriggers false} :: SAppend(SAppend(a, b), c) ==#[k] SAppend(a, SAppend(b, c))); //FIXME: Should Dafny generate a trigger here? If so then which one? } // Equivalent proof using the colemma syntax. -- cgit v1.2.3