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.

1 files changed, 4 insertions, 4 deletions

diff --git a/Test/dafny1/Induction.dfy b/Test/dafny1/Induction.dfy
index 3445dab9..e2cd4ade 100644
--- a/Test/dafny1/Induction.dfy
+++ b/Test/dafny1/Induction.dfy
@@ -53,7 +53,7 @@ class IntegerInduction {
   }

 

   lemma DoItAllInOneGo()

-    ensures (forall n :: 0 <= n ==>

+    ensures (forall n {:split false} :: 0 <= n ==> // WISH reenable quantifier splitting here. This will only work once we generate induction hypotheses at the Dafny level.

                 SumOfCubes(n) == Gauss(n) * Gauss(n) &&

                 2 * Gauss(n) == n*(n+1));

   {

@@ -148,11 +148,11 @@ class IntegerInduction {
   // Proving the "<==" case is simple; it's the "==>" case that requires induction.

   // The example uses an attribute that requests induction on just "j".  However, the proof also

   // goes through by applying induction on both bound variables.

-  function method IsSorted(s: seq<int>): bool

-    ensures IsSorted(s) ==> (forall i,j {:induction j} :: 0 <= i && i < j && j < |s| ==> s[i] <= s[j]);

+  function method IsSorted(s: seq<int>): bool //WISH remove autotriggers false

+    ensures IsSorted(s) ==> (forall i,j {:induction j} {:autotriggers false} :: 0 <= i < j < |s| ==> s[i] <= s[j]);

     ensures (forall i,j :: 0 <= i && i < j && j < |s| ==> s[i] <= s[j]) ==> IsSorted(s);

   {

-    (forall i :: 1 <= i && i < |s| ==> s[i-1] <= s[i])

+    (forall i {:nowarn} :: 1 <= i && i < |s| ==> s[i-1] <= s[i])

   }

 }