Fix multiple tests that relied on z3 triggering on $Box

Found by enabling auto-generated triggers and looking for failing tests

4 files changed, 11 insertions, 5 deletions

diff --git a/Test/dafny4/CoqArt-InsertionSort.dfy b/Test/dafny4/CoqArt-InsertionSort.dfy
index efd01537..99e0f0b1 100644
--- a/Test/dafny4/CoqArt-InsertionSort.dfy
+++ b/Test/dafny4/CoqArt-InsertionSort.dfy
@@ -151,6 +151,7 @@ lemma existence_proof(l: List<int>)
 {

   match l {

     case Nil =>

+      assert sorted(Nil);

     case Cons(x, m) =>

       existence_proof(m);

       var m' :| equiv(m, m') && sorted(m');

diff --git a/Test/dafny4/GHC-MergeSort.dfy b/Test/dafny4/GHC-MergeSort.dfy
index e06773eb..976b8a27 100644
--- a/Test/dafny4/GHC-MergeSort.dfy
+++ b/Test/dafny4/GHC-MergeSort.dfy
@@ -412,11 +412,8 @@ lemma sorted_replaceSuffix(xs: List<G>, ys: List<G>, zs: List<G>)
   match xs {

     case Nil =>

     case Cons(c, xs') =>

-      forall a,b | a in multiset_of(xs') && b in multiset_of(Cons(c, zs))

-        ensures Below(a, b);

-      {

-        sorted_reverse(xs', Cons(c, ys));

-      }

+      sorted_reverse(xs, ys);

+      sorted_reverse(xs', Cons(c, ys));

       sorted_replaceSuffix(xs', Cons(c, ys), Cons(c, zs));

   }

 }

diff --git a/Test/dafny4/NipkowKlein-chapter7.dfy b/Test/dafny4/NipkowKlein-chapter7.dfy
index 4756f5b1..7db31cbd 100644
--- a/Test/dafny4/NipkowKlein-chapter7.dfy
+++ b/Test/dafny4/NipkowKlein-chapter7.dfy
@@ -117,6 +117,7 @@ inductive lemma lemma_7_6(b: bexp, c: com, c': com, s: state, t: state)
   } else {

     var s' :| big_step#[_k-1](c, s, s') && big_step#[_k-1](While(b, c), s', t);

     lemma_7_6(b, c, c', s', t);  // induction hypothesis

+    assert big_step(While(b, c'), s', t);

   }

 }

 

diff --git a/Test/dafny4/Primes.dfy b/Test/dafny4/Primes.dfy
index 31e3a19b..b0bb7527 100644
--- a/Test/dafny4/Primes.dfy
+++ b/Test/dafny4/Primes.dfy
@@ -110,6 +110,13 @@ lemma RemoveFactor(x: int, s: set<int>)
       x * y * product(s - {y} - {x});

       { assert s - {y} - {x} == s - {x} - {y}; }

       x * y * product(s - {x} - {y});

+      /* FIXME: This annotation wasn't needed before the introduction

+       * of auto-triggers. It's not needed if one adds {:no_trigger}

+       * to the forall y :: y in s ==> y <= x part of PickLargest, but that

+       * boils down to z3 picking $Box(...) as good trigger

+       */

+      // FIXME: the parens shouldn't be needed around (s - {x})

+      { assert y in (s - {x}); }

       { assert y == PickLargest(s - {x}); }

       x * product(s - {x});

     }