Fix multiple tests that relied on z3 triggering on $Box

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

8 files changed, 23 insertions, 5 deletions

diff --git a/Test/dafny0/DeterministicPick.dfy b/Test/dafny0/DeterministicPick.dfy
index a7ec55fa..13db1bfc 100644
--- a/Test/dafny0/DeterministicPick.dfy
+++ b/Test/dafny0/DeterministicPick.dfy
@@ -29,6 +29,7 @@ module Attempt_Smallest refines Specification {
     var z :| z in s;

     if s != {z} {

       var s' := s - {z};

+      assert forall y :: y in s ==> y in s' || y == z;

       ASmallestToPick(s');

     }

   }

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index 45ef06f7..e9c2beb4 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -332,6 +332,7 @@ method TestSequences0()
     assert 1 !in s;

   } else {

     assert 2 in s;

+    assert 0 in s;

     assert exists n :: n in s && -3 <= n && n < 2;

   }

   assert 7 in s;  // error

diff --git a/Test/dafny1/BDD.dfy b/Test/dafny1/BDD.dfy
index 252164db..59dc3092 100644
--- a/Test/dafny1/BDD.dfy
+++ b/Test/dafny1/BDD.dfy
@@ -55,6 +55,7 @@ module SimpleBDD
 		 node := if s[n-i] then node.t else node.f;

 		 i := i - 1;

 	   }

+           assert s[n-i..] == [];

 	   b := node.b;

 	 }

    }

diff --git a/Test/dafny2/COST-verif-comp-2011-2-MaxTree-class.dfy b/Test/dafny2/COST-verif-comp-2011-2-MaxTree-class.dfy
index c752bd38..f691384c 100644
--- a/Test/dafny2/COST-verif-comp-2011-2-MaxTree-class.dfy
+++ b/Test/dafny2/COST-verif-comp-2011-2-MaxTree-class.dfy
@@ -117,6 +117,11 @@ class Tree {
     Repr := lft.Repr + {this} + rgt.Repr;

   }

 

+  lemma exists_intro<T>(P: T -> bool, x: T)

+    requires P.requires(x)

+    requires P(x)

+    ensures exists y :: P.requires(y) && P(y) { }

+

   method ComputeMax() returns (mx: int)

     requires Valid() && !IsEmpty();

     ensures forall x :: x in Contents ==> x <= mx;

@@ -124,13 +129,17 @@ class Tree {
     decreases Repr;

   {

     mx := value;

+

     if (!left.IsEmpty()) {

       var m := left.ComputeMax();

       mx := if mx < m  then m else mx;

     }

+

     if (!right.IsEmpty()) {

       var m := right.ComputeMax();

       mx := if mx < m then m else mx;

     }

+

+    exists_intro(x reads this => x in Contents && x == mx, mx);

   }

 }

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

     }