Suppress many warnings in the test suite.

We already have separate tests for those, and we want the output to be the same
with and without /autoTriggers.

17 files changed, 106 insertions, 99 deletions

diff --git a/Test/dafny0/Comprehensions.dfy b/Test/dafny0/Comprehensions.dfy
index d0436815..dd83e46c 100644
--- a/Test/dafny0/Comprehensions.dfy
+++ b/Test/dafny0/Comprehensions.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:1 "%s" > "%t"

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

 

 method M()

@@ -19,18 +19,18 @@ datatype D = A | B
 // have to run the resulting program to check that the compiler is doing the right thing.

 method Main()

 {

-  var q := set i,j | 0 <= i && i < 10 && 0 <= j && j < 3 :: i+j;

+  var q := set i,j | 0 <= i < 10 && 0 <= j < 3 :: i+j;

   PrintSet(q);

   q := set b: bool | true :: if b then 3 else 7;

   var d := set b:D | true;

-  var test := forall d:D :: d == A || d == B;

+  var test := forall d:D {:nowarn} :: d == A || d == B; // Ignoring the warning as we're only compiling here

   PrintSet(q);

   var m := set k | k in q :: 2*k;

   PrintSet(m);

   PrintSet(set k | k in q && k % 2 == 0);

   var sq := [30, 40, 20];

-  PrintSet(set k, i | k in sq && 0 <= i && i < k && i % 7 == 0 :: k + i);

-  var bb := forall k, i | k in sq && 0 <= i && i < k && i % 7 == 0 :: k + i == 17;

+  PrintSet(set k, i | k in sq && 0 <= i < k && i % 7 == 0 :: k + i);

+  var bb := forall k, i {:nowarn} | k in sq && 0 <= i < k && i % 7 == 0 :: k + i == 17; // Ignoring the warning as we're only compiling here

 }

 

 method PrintSet<T>(s: set<T>) {

diff --git a/Test/dafny0/DTypes.dfy b/Test/dafny0/DTypes.dfy
index c8c893a0..9e36e64c 100644
--- a/Test/dafny0/DTypes.dfy
+++ b/Test/dafny0/DTypes.dfy
@@ -5,7 +5,7 @@ class C {
   var n: set<Node>;

 

   method M(v: Stack)

-    requires v != null;

+    requires v != null

   {

     var o: object := v;

     assert o !in n;  // should be known from the types involved

@@ -28,12 +28,12 @@ class C {
   method A1(a: CP<int,C>)

   {

     var x: object := a;

-    assert (forall b: CP<int,Stack> :: x == b ==> b == null);  // follows from type antecedents

+    assert (forall b: CP<int,Stack> {:nowarn} :: x == b ==> b == null);  // follows from type antecedents

   }

 

   var a2x: set<CP<C,Node>>;

   method A2(b: set<CP<Node,C>>)

-    requires null !in b;

+    requires null !in b

   {

     var x: set<object> := a2x;

     var y: set<object> := b;

@@ -81,7 +81,7 @@ class CP<T,U> {
 datatype Data = Lemon | Kiwi(int)

 

 function G(d: Data): int

-  requires d != Data.Lemon;

+  requires d != Data.Lemon

 {

   match d

   case Lemon => G(d)

@@ -101,28 +101,28 @@ class DatatypeInduction<T> {
   }

 

   method Theorem0(tree: Tree<T>)

-    ensures 1 <= LeafCount(tree);

+    ensures 1 <= LeafCount(tree)

   {

     assert (forall t: Tree<T> :: 1 <= LeafCount(t));

   }

 

   // also make sure it works for an instantiated generic datatype

   method Theorem1(bt: Tree<bool>, it: Tree<int>)

-    ensures 1 <= LeafCount(bt);

-    ensures 1 <= LeafCount(it);

+    ensures 1 <= LeafCount(bt)

+    ensures 1 <= LeafCount(it)

   {

     assert (forall t: Tree<bool> :: 1 <= LeafCount(t));

     assert (forall t: Tree<int> :: 1 <= LeafCount(t));

   }

 

   method NotATheorem0(tree: Tree<T>)

-    ensures LeafCount(tree) % 2 == 1;

+    ensures LeafCount(tree) % 2 == 1

   {

     assert (forall t: Tree<T> :: LeafCount(t) % 2 == 1);  // error: fails for Branch case

   }

 

   method NotATheorem1(tree: Tree<T>)

-    ensures 2 <= LeafCount(tree);

+    ensures 2 <= LeafCount(tree)

   {

     assert (forall t: Tree<T> :: 2 <= LeafCount(t));  // error: fails for Leaf case

   }

@@ -140,22 +140,22 @@ class DatatypeInduction<T> {
   // ----- here is a test for induction over integers

 

   method IntegerInduction_Succeeds(a: array<int>)

-    requires a != null;

-    requires a.Length == 0 || a[0] == 0;

-    requires forall j :: 1 <= j && j < a.Length ==> a[j] == a[j-1]+2*j-1;

+    requires a != null

+    requires a.Length == 0 || a[0] == 0

+    requires forall j {:nowarn} :: 1 <= j < a.Length ==> a[j] == a[j-1]+2*j-1 // WISH: If induction was more powerful, we wouldn't need to rely on the quantifier to produce the j-1 term.

   {

     // The following assertion can be proved by induction:

-    assert forall n {:induction} :: 0 <= n && n < a.Length ==> a[n] == n*n;

+    assert forall n {:induction} :: 0 <= n < a.Length ==> a[n] == n*n;

   }

 

   method IntegerInduction_Fails(a: array<int>)

-    requires a != null;

-    requires a.Length == 0 || a[0] == 0;

-    requires forall j :: 1 <= j && j < a.Length ==> a[j] == a[j-1]+2*j-1;

+    requires a != null

+    requires a.Length == 0 || a[0] == 0

+    requires forall j {:nowarn} :: 1 <= j < a.Length ==> a[j] == a[j-1]+2*j-1 // WISH: Same as above

   {

     // ...but the induction heuristics don't recognize the situation as one where

     // applying induction would be profitable:

-    assert forall n :: 0 <= n && n < a.Length ==> a[n] == n*n;  // error reported

+    assert forall n :: 0 <= n < a.Length ==> a[n] == n*n;  // error reported

   }

 }

 

@@ -171,7 +171,7 @@ abstract module OpaqueTypesWithParameters {
   }

 

   method DifferentTypes(a: array<P<int>>, b: array<P<bool>>)

-    requires a != null && b != null;

+    requires a != null && b != null

     // If P were a known type, then it would also be known that P<int> and P<bool>

     // would be different types, and then the types of 'a' and 'b' would be different,

     // which would imply that the following postcondition would hold.

diff --git a/Test/dafny0/Matrix-OOB.dfy b/Test/dafny0/Matrix-OOB.dfy
index 2e5c0366..d7aacd79 100644
--- a/Test/dafny0/Matrix-OOB.dfy
+++ b/Test/dafny0/Matrix-OOB.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /dprint:"%t.dprint" /printTooltips "%s" > "%t"

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

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

 

 // This is a regression test: OOB errors for matrices used to be reported on the

diff --git a/Test/dafny0/Matrix-OOB.dfy.expect b/Test/dafny0/Matrix-OOB.dfy.expect
index 94e77aa4..e2920445 100644
--- a/Test/dafny0/Matrix-OOB.dfy.expect
+++ b/Test/dafny0/Matrix-OOB.dfy.expect
@@ -1,3 +1,4 @@
+Matrix-OOB.dfy(12,10): Info: Selected triggers: {m[i, j]}

 Matrix-OOB.dfy(12,26): Error: index 0 out of range

 Execution trace:

     (0,0): anon0

@@ -6,6 +7,7 @@ Execution trace:
     (0,0): anon0

 Matrix-OOB.dfy(13,0): Error BP5003: A postcondition might not hold on this return path.

 Matrix-OOB.dfy(12,10): Related location: This is the postcondition that might not hold.

+Matrix-OOB.dfy(12,33): Related location

 Execution trace:

     (0,0): anon0

 

diff --git a/Test/dafny0/Modules1.dfy b/Test/dafny0/Modules1.dfy
index 505d9b74..3ffa5a23 100644
--- a/Test/dafny0/Modules1.dfy
+++ b/Test/dafny0/Modules1.dfy
@@ -125,7 +125,7 @@ abstract module Regression {
     predicate p<c,d>(m: map<c,d>)

 

     lemma m<a,b>(m: map<a,b>)

-      ensures exists m :: p(var m : map<a,b> := m; m);

+      ensures exists m {:nowarn} :: p(var m : map<a,b> := m; m) // WISH: Zeta-expanding the let binding would provide a good trigger

   }

 

   abstract module B

diff --git a/Test/dafny0/Parallel.dfy b/Test/dafny0/Parallel.dfy
index e0d6491b..93a16475 100644
--- a/Test/dafny0/Parallel.dfy
+++ b/Test/dafny0/Parallel.dfy
@@ -210,7 +210,7 @@ class TwoState_C { ghost var data: int }
 // contexts are not allowed to allocate state.  Callers of this ghost method will know

 // that the postcondition is tantamount to 'false'.

 ghost method TwoState0(y: int)

-  ensures exists o: TwoState_C :: o != null && fresh(o)

+  ensures exists o: TwoState_C {:nowarn} :: o != null && fresh(o)

 

 method TwoState_Main0() {

   forall x { TwoState0(x); }

@@ -236,7 +236,7 @@ method X_Legit(c: TwoState_C)
 method TwoState_Main2()

 {

   forall x: int

-    ensures exists o: TwoState_C :: o != null && fresh(o)

+    ensures exists o: TwoState_C {:nowarn} :: o != null && fresh(o)

   {

     TwoState0(x);

   }

@@ -252,7 +252,7 @@ method TwoState_Main2()
 method TwoState_Main3()

 {

   forall x: int

-    ensures exists o: TwoState_C :: o != null && fresh(o)

+    ensures exists o: TwoState_C {:nowarn} :: o != null && fresh(o)

   {

     assume false;  // (there's no other way to achieve this forall-statement postcondition)

   }

@@ -309,12 +309,12 @@ 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: ss should be autogrnerated. Note that step is not a bound variable.

 }

 

 lemma Th(step: nat, t: Nat, r: nat)

   requires t.Succ? && ThProperty(step, t, r)

   // the next line follows from the precondition and the definition of ThProperty

-  ensures exists ro:nat :: ThProperty(step-1, t.tail, ro)

+  ensures exists ro:nat, ss | ss == step-1 :: ThProperty(ss, t.tail, ro) //WISH same as above

 {

 }

diff --git a/Test/dafny0/Predicates.dfy b/Test/dafny0/Predicates.dfy
index 737dacd2..f8b3355d 100644
--- a/Test/dafny0/Predicates.dfy
+++ b/Test/dafny0/Predicates.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:1  "%s" > "%t"

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

 

 module A {

diff --git a/Test/dafny0/Predicates.dfy.expect b/Test/dafny0/Predicates.dfy.expect
index 2d7ea6f1..36c9dfdd 100644
--- a/Test/dafny0/Predicates.dfy.expect
+++ b/Test/dafny0/Predicates.dfy.expect
@@ -17,10 +17,12 @@ Execution trace:
     (0,0): anon0

 Predicates.dfy(164,4): Error BP5003: A postcondition might not hold on this return path.

 Predicates.dfy(163,14): Related location: This is the postcondition that might not hold.

+Predicates.dfy(163,42): Related location

 Execution trace:

     (0,0): anon0

 Predicates.dfy[Q1](154,4): Error BP5003: A postcondition might not hold on this return path.

 Predicates.dfy[Q1](153,14): Related location: This is the postcondition that might not hold.

+Predicates.dfy[Q1](153,45): Related location

 Execution trace:

     (0,0): anon0

 

diff --git a/Test/dafny0/SeqFromArray.dfy b/Test/dafny0/SeqFromArray.dfy
index 629c5045..cf889804 100644
--- a/Test/dafny0/SeqFromArray.dfy
+++ b/Test/dafny0/SeqFromArray.dfy
@@ -53,7 +53,7 @@ method L(a: array<int>, c: array<int>, n: nat)
     case A == C =>

       assert forall i :: 0 <= i < h ==> A[i] == C[i];

     case A == C =>

-      assert forall i :: 0 <= i < h ==> a[n+i] == c[n+i];

+      assert forall i :: n <= i < n + h ==> a[i] == c[i];

     case true =>

   }

 }

@@ -73,13 +73,13 @@ method M(a: array<int>, c: array<int>, m: nat, n: nat, k: nat, l: nat)
         } else if * {

           assert forall i :: 0 <= i < n ==> A[i] == C[i];

         } else if * {

-          assert forall i :: k <= i < k+n ==> A[i-k] == C[i-k];

+          assert forall i {:nowarn} :: k <= i < k+n ==> A[i-k] == C[i-k];

         } else if * {

           assert forall i :: 0 <= i < n ==> A[i] == a[k+i];

         } else if * {

           assert forall i :: 0 <= i < n ==> C[i] == c[l+i];

         } else if * {

-          assert forall i :: 0 <= i < n ==> a[k+i] == c[l+i];

+          assert forall i {:nowarn} :: 0 <= i < n ==> a[k+i] == c[l+i];

         }

       }

     case l+m <= c.Length && forall i :: 0 <= i < m ==> a[i] == c[l+i] =>

diff --git a/Test/dafny0/SeqFromArray.dfy.expect b/Test/dafny0/SeqFromArray.dfy.expect
index 5395e298..af845d3e 100644
--- a/Test/dafny0/SeqFromArray.dfy.expect
+++ b/Test/dafny0/SeqFromArray.dfy.expect
@@ -1,6 +1,3 @@
-SeqFromArray.dfy(56,13): Warning: (!) No terms found to trigger on.

-SeqFromArray.dfy(76,17): Warning: (!) No terms found to trigger on.

-SeqFromArray.dfy(82,17): Warning: (!) No terms found to trigger on.

 

 Dafny program verifier finished with 10 verified, 0 errors

 Program compiled successfully

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

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

 // RUN: %dafny /noVerify /compile:0 "%t.dprint.dfy" >> "%t"

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

 

@@ -35,11 +35,11 @@ class Node {
   }

 

   method Sequence(s: seq<bool>, j: int, b: bool, c: bool) returns (t: seq<bool>)

-    requires 10 <= |s|;

-    requires 8 <= j && j < |s|;

-    ensures |t| == |s|;

-    ensures t[8] == s[8] || t[9] == s[9];

-    ensures t[j] == b;

+    requires 10 <= |s|

+    requires 8 <= j < |s|

+    ensures |t| == |s|

+    ensures t[8] == s[8] || t[9] == s[9]

+    ensures t[j] == b

   {

     if (c) {

       t := s[j := b];

@@ -49,14 +49,14 @@ class Node {
   }

 

   method Max0(x: int, y: int) returns (r: int)

-    ensures r == (if x < y then y else x);

+    ensures r == (if x < y then y else x)

   {

     if (x < y) { r := y; } else { r := x; }

   }

 

   method Max1(x: int, y: int) returns (r: int)

-    ensures r == x || r == y;

-    ensures x <= r && y <= r;

+    ensures r == x || r == y

+    ensures x <= r && y <= r

   {

     r := if x < y then y else x;

   }

@@ -122,12 +122,12 @@ class Modifies {
 

   method C(b: bool)

     modifies this;

-    ensures !b ==> x == old(x) && next == old(next);

+    ensures !b ==> x == old(x) && next == old(next)

   {

   }

 

   method D(p: Modifies, y: int)

-    requires p != null;

+    requires p != null

   {

     if (y == 3) {

       p.C(true);  // error: may violate modifies clause

@@ -230,15 +230,15 @@ class InitCalls {
 

   method Init(y: int)

     modifies this;

-    ensures z == y;

+    ensures z == y

   {

     z := y;

   }

 

   method InitFromReference(q: InitCalls)

-    requires q != null && 15 <= q.z;

+    requires q != null && 15 <= q.z

     modifies this;

-    ensures p == q;

+    ensures p == q

   {

     p := q;

   }

@@ -265,35 +265,35 @@ class InitCalls {
 // --------------- some tests with quantifiers and ranges ----------------------

 

 method QuantifierRange0<T>(a: seq<T>, x: T, y: T, N: int)

-  requires 0 <= N && N <= |a|;

-  requires forall k | 0 <= k && k < N :: a[k] != x;

-  requires exists k | 0 <= k && k < N :: a[k] == y;

-  ensures forall k :: 0 <= k && k < N ==> a[k] != x;  // same as the precondition, but using ==> instead of |

-  ensures exists k :: 0 <= k && k < N && a[k] == y;  // same as the precondition, but using && instead of |

+  requires 0 <= N <= |a|

+  requires forall k | 0 <= k < N :: a[k] != x

+  requires exists k | 0 <= k < N :: a[k] == y

+  ensures forall k :: 0 <= k < N ==> a[k] != x;  // same as the precondition, but using ==> instead of |

+  ensures exists k :: 0 <= k < N && a[k] == y;  // same as the precondition, but using && instead of |

 {

   assert x != y;

 }

 

 method QuantifierRange1<T>(a: seq<T>, x: T, y: T, N: int)

-  requires 0 <= N && N <= |a|;

-  requires forall k :: 0 <= k && k < N ==> a[k] != x;

-  requires exists k :: 0 <= k && k < N && a[k] == y;

-  ensures forall k | 0 <= k && k < N :: a[k] != x;  // same as the precondition, but using | instead of ==>

-  ensures exists k | 0 <= k && k < N :: a[k] == y;  // same as the precondition, but using | instead of &&

+  requires 0 <= N <= |a|

+  requires forall k :: 0 <= k < N ==> a[k] != x

+  requires exists k :: 0 <= k < N && a[k] == y

+  ensures forall k | 0 <= k < N :: a[k] != x;  // same as the precondition, but using | instead of ==>

+  ensures exists k | 0 <= k < N :: a[k] == y;  // same as the precondition, but using | instead of &&

 {

   assert x != y;

 }

 

 method QuantifierRange2<T(==)>(a: seq<T>, x: T, y: T, N: int)

-  requires 0 <= N && N <= |a|;

-  requires exists k | 0 <= k && k < N :: a[k] == y;

-  ensures forall k | 0 <= k && k < N :: a[k] == y;  // error

+  requires 0 <= N <= |a|

+  requires exists k | 0 <= k < N :: a[k] == y

+  ensures forall k | 0 <= k < N :: a[k] == y;  // error

 {

   assert N != 0;

   if (N == 1) {

-    assert forall k | a[if 0 <= k && k < N then k else 0] != y :: k < 0 || N <= k;  // in this case, the precondition holds trivially

+    assert forall k {:nowarn} | a[if 0 <= k < N then k else 0] != y :: k < 0 || N <= k;  // in this case, the precondition holds trivially

   }

-  if (forall k | 0 <= k && k < N :: a[k] == x) {

+  if (forall k | 0 <= k < N :: a[k] == x) {

     assert x == y;

   }

 }

@@ -301,8 +301,8 @@ method QuantifierRange2<T(==)>(a: seq<T>, x: T, y: T, N: int)
 // ----------------------- tests that involve sequences of boxes --------

 

 ghost method M(zeros: seq<bool>, Z: bool)

-  requires 1 <= |zeros| && Z == false;

-  requires forall k :: 0 <= k && k < |zeros| ==> zeros[k] == Z;

+  requires 1 <= |zeros| && Z == false

+  requires forall k :: 0 <= k < |zeros| ==> zeros[k] == Z

 {

   var x := [Z];

   assert zeros[0..1] == [Z];

@@ -312,7 +312,7 @@ class SomeType
 {

   var x: int;

   method DoIt(stack: seq<SomeType>)

-    requires null !in stack;

+    requires null !in stack

     modifies stack;

   {

     forall n | n in stack {

@@ -333,7 +333,7 @@ method TestSequences0()
   } else {

     assert 2 in s;

     assert 0 in s;

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

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

   }

   assert 7 in s;  // error

 }

@@ -399,7 +399,7 @@ class Test {
 function F(b: bool): int

   // The if-then-else in the following line was once translated incorrectly,

   // incorrectly causing the postcondition to verify

-  ensures if b then F(b) == 5 else F(b) == 6;

+  ensures if b then F(b) == 5 else F(b) == 6

 {

   5

 }

@@ -430,10 +430,10 @@ class AttributeTests {
   }

 

   method testAttributes0() returns (r: AttributeTests)

-    ensures {:boolAttr true} true;

-    ensures {:boolAttr false} true;

-    ensures {:intAttr 0} true;

-    ensures {:intAttr 1} true;

+    ensures {:boolAttr true} true

+    ensures {:boolAttr false} true

+    ensures {:intAttr 0} true

+    ensures {:intAttr 1} true

     modifies {:boolAttr true} this`f;

     modifies {:boolAttr false} this`f;

     modifies {:intAttr 0} this`f;

@@ -541,7 +541,7 @@ method TestNotNot()
 // ----------------------- Assign-such-that statements -------

 

 method AssignSuchThat0(a: int, b: int) returns (x: int, y: int)

-  ensures x == a && y == b;

+  ensures x == a && y == b

 {

   if (*) {

     x, y :| a <= x < a + 1 && b + a <= y + a && y <= b;

@@ -635,7 +635,7 @@ method AssignSuchThat9() returns (q: QuiteFinite)
 function method LetSuchThat_P(x: int): bool

 

 method LetSuchThat0(ghost g: int)

-  requires LetSuchThat_P(g);

+  requires LetSuchThat_P(g)

 {

   var t :| LetSuchThat_P(t);  // assign-such-that statement

   ghost var u := var q :| LetSuchThat_P(q); q + 1;  // let-such-that expression

@@ -710,10 +710,10 @@ class GT {
   {

     if (*) {

       P0();

-      assert forall x: GT :: x != null ==> !fresh(x);  // error: method P2 may have allocated stuff

+      assert forall x: GT {:nowarn} :: x != null ==> !fresh(x);  // error: method P2 may have allocated stuff

     } else {

       P1();

-      assert forall x: GT :: x != null ==> !fresh(x);  // fine, because the ghost method does not allocate anything

+      assert forall x: GT {:nowarn} :: x != null ==> !fresh(x);  // fine, because the ghost method does not allocate anything

     }

   }

 }

@@ -777,20 +777,20 @@ module GenericPick {
     var x :| x in s; x

   }

   function SeqPick3<U>(s: seq<U>): U

-    requires exists i :: 0 <= i < |s|

+    requires exists i {:nowarn} :: 0 <= i < |s|

   {

     EquivalentWaysOfSayingSequenceIsNonempty(s);  // I wish this wasn't needed; see comment near Seq#Length axioms in DafnyPrelude.bpl

     var x :| x in s; x

   }

   function SeqPick4<U>(s: seq<U>): U

-    requires exists i :: 0 <= i < |s|

+    requires exists i {:nowarn} :: 0 <= i < |s|

   {

     var i :| 0 <= i < |s|; s[i]

   }

   lemma EquivalentWaysOfSayingSequenceIsNonempty<U>(s: seq<U>)

     requires s != []

           || |s| != 0

-          || exists i :: 0 <= i < |s|

+          || exists i {:nowarn} :: 0 <= i < |s|

     ensures exists x :: x in s

   {

     assert s[0] in s;

diff --git a/Test/dafny0/SmallTests.dfy.expect b/Test/dafny0/SmallTests.dfy.expect
index eee0d4f1..4bd12096 100644
--- a/Test/dafny0/SmallTests.dfy.expect
+++ b/Test/dafny0/SmallTests.dfy.expect
@@ -107,6 +107,7 @@ Execution trace:
     (0,0): anon3

 SmallTests.dfy(296,2): Error BP5003: A postcondition might not hold on this return path.

 SmallTests.dfy(290,10): Related location: This is the postcondition that might not hold.

+SmallTests.dfy(290,40): Related location

 Execution trace:

     (0,0): anon0

     (0,0): anon18_Else

@@ -117,8 +118,8 @@ Execution trace:
 SmallTests.dfy(338,11): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    (0,0): anon8_Then

-    (0,0): anon7

+    (0,0): anon7_Then

+    (0,0): anon6

 SmallTests.dfy(345,9): Error: assertion violation

 Execution trace:

     (0,0): anon0

diff --git a/Test/dafny0/TriggerInPredicate.dfy.expect b/Test/dafny0/TriggerInPredicate.dfy.expect
index 1cbd4034..b3fb9cc0 100644
--- a/Test/dafny0/TriggerInPredicate.dfy.expect
+++ b/Test/dafny0/TriggerInPredicate.dfy.expect
@@ -1,5 +1,5 @@
-TriggerInPredicate.dfy(6,32): Info: Not generating triggers for {A(x, y)}.

-TriggerInPredicate.dfy(6,32): Info: Not generating triggers for {z}.

+TriggerInPredicate.dfy(6,32): Info: Not generating triggers for "A(x, y)".

+TriggerInPredicate.dfy(6,32): Info: Not generating triggers for "z".

 TriggerInPredicate.dfy(9,20): Info: Some instances of this call cannot safely be inlined.

 TriggerInPredicate.dfy(9,20): Info: Some instances of this call cannot safely be inlined.

 

diff --git a/Test/dafny0/columns.dfy b/Test/dafny0/columns.dfy
index e36142be..72c9ab81 100644
--- a/Test/dafny0/columns.dfy
+++ b/Test/dafny0/columns.dfy
@@ -3,8 +3,10 @@
 

 // Dafny counts columns from 0, but Boogie from one, so for a while there were small bugs with that.

 

+predicate P(x: int)

+

 static method A(x:int) requires x > 0 { // error os 's'

-  assert (forall y :: y > x ==> y > 100); // error on '('

+  assert (forall y: int :: P(y)); // error on '('

   assert x != 1; // error on '!'

   assert x in {}; // error on 'i'

 }

diff --git a/Test/dafny0/columns.dfy.expect b/Test/dafny0/columns.dfy.expect
index 295ca351..0a99be69 100644
--- a/Test/dafny0/columns.dfy.expect
+++ b/Test/dafny0/columns.dfy.expect
@@ -1,18 +1,12 @@
-columns.dfy(6,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here

-columns.dfy(7,9): Error: assertion violation

+columns.dfy(8,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here

+columns.dfy(9,9): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Then

-    (0,0): anon2

-columns.dfy(8,11): Error: assertion violation

+columns.dfy(10,11): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Then

-    (0,0): anon2

-columns.dfy(9,11): Error: assertion violation

+columns.dfy(11,11): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Then

-    (0,0): anon2

 

-Dafny program verifier finished with 1 verified, 3 errors

+Dafny program verifier finished with 2 verified, 3 errors

diff --git a/Test/dafny0/snapshots/Snapshots5.run.dfy b/Test/dafny0/snapshots/Snapshots5.run.dfy
index e0f3b16b..096df53c 100644
--- a/Test/dafny0/snapshots/Snapshots5.run.dfy
+++ b/Test/dafny0/snapshots/Snapshots5.run.dfy
@@ -1,2 +1,2 @@
-// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 "%S/Inputs/Snapshots5.dfy" > "%t"

+// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 "%S/Inputs/Snapshots5.dfy" /autoTriggers:1 > "%t"

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

diff --git a/Test/dafny0/snapshots/Snapshots5.run.dfy.expect b/Test/dafny0/snapshots/Snapshots5.run.dfy.expect
index 8148a8cf..8cc44882 100644
--- a/Test/dafny0/snapshots/Snapshots5.run.dfy.expect
+++ b/Test/dafny0/snapshots/Snapshots5.run.dfy.expect
@@ -1,3 +1,7 @@
+Snapshots5.v0.dfy(10,12): Warning: /!\ No terms found to trigger on.

+Snapshots5.v0.dfy(13,10): Warning: /!\ No terms found to trigger on.

+Snapshots5.v0.dfy(20,12): Warning: /!\ No terms found to trigger on.

+Snapshots5.v0.dfy(26,11): Warning: /!\ No terms found to trigger on.

 Processing command (at Snapshots5.v0.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);

   >>> DoNothingToAssert

 Processing command (at Snapshots5.v0.dfy(10,40)) assert (forall b#1: bool :: true ==> b#1 || !b#1) || 0 != 0;

@@ -10,6 +14,11 @@ Processing command (at Snapshots5.v0.dfy(20,40)) assert (forall b#5: bool :: tru
   >>> DoNothingToAssert

 

 Dafny program verifier finished with 3 verified, 0 errors

+Snapshots5.v1.dfy(10,12): Warning: /!\ No terms found to trigger on.

+Snapshots5.v1.dfy(13,10): Warning: /!\ No terms found to trigger on.

+Snapshots5.v1.dfy(20,12): Warning: /!\ No terms found to trigger on.

+Snapshots5.v1.dfy(22,10): Warning: /!\ No terms found to trigger on.

+Snapshots5.v1.dfy(27,11): Warning: /!\ No terms found to trigger on.

 Processing command (at Snapshots5.v1.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);

   >>> MarkAsFullyVerified

 Processing command (at Snapshots5.v1.dfy(10,40)) assert (forall b#1: bool :: true ==> b#1 || !b#1) || 0 != 0;