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.

7 files changed, 16 insertions, 11 deletions

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);

diff --git a/Test/dafny0/Array.dfy b/Test/dafny0/Array.dfy
index 391ca5f7..309e9248 100644
--- a/Test/dafny0/Array.dfy
+++ b/Test/dafny0/Array.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t"

 // RUN: %diff "%s.expect" "%t"

 

 class A {

@@ -327,3 +327,5 @@ module DtypeRegression {
     }

   }

 }

+

+// WISH: autoTriggers disabled because of induction

diff --git a/Test/dafny0/ComputationsNeg.dfy b/Test/dafny0/ComputationsNeg.dfy
index 0c539117..b9425d64 100644
--- a/Test/dafny0/ComputationsNeg.dfy
+++ b/Test/dafny0/ComputationsNeg.dfy
@@ -16,7 +16,7 @@ predicate ThProperty(step: nat, t: Nat, r: nat)
 {

   match t

   case Zero => true

-  case Succ(o) => step>0 && exists ro:nat :: ThProperty(step-1, o, ro)

+  case Succ(o) => step>0 && exists ro:nat, ss :: ss == step-1 ==> ThProperty(ss, o, ro) // WISH: auto-generate ss

 }

 ghost method test_ThProperty()

   ensures ThProperty(10, Succ(Zero), 0);

diff --git a/Test/dafny0/MultiSets.dfy b/Test/dafny0/MultiSets.dfy
index 3535f857..ba075fc3 100644
--- a/Test/dafny0/MultiSets.dfy
+++ b/Test/dafny0/MultiSets.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t"

 // RUN: %diff "%s.expect" "%t"

 

 method test1()

@@ -295,3 +295,6 @@ lemma Set_and_Multiset_Cardinalities(x: int, y: int)
     assert |multiset{x,y}| == 2;

   }

 }

+

+// AutoTriggers explicitly removed, as simplifications of set expressions such

+// as x in {1,2} cause invalid terms to appear in the triggers

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])

   }

 }

 

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]];

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.