From 95a42a224dff8eae383d93beb37a3da6a28bb0f3 Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel <clement.pitclaudel@live.com>
Date: Fri, 28 Aug 2015 20:50:50 -0700
Subject: 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.
---
 Test/dafny0/Comprehensions.dfy                  | 10 +--
 Test/dafny0/DTypes.dfy                          | 36 +++++-----
 Test/dafny0/Matrix-OOB.dfy                      |  2 +-
 Test/dafny0/Matrix-OOB.dfy.expect               |  2 +
 Test/dafny0/Modules1.dfy                        |  2 +-
 Test/dafny0/Parallel.dfy                        | 10 +--
 Test/dafny0/Predicates.dfy                      |  2 +-
 Test/dafny0/Predicates.dfy.expect               |  2 +
 Test/dafny0/SeqFromArray.dfy                    |  6 +-
 Test/dafny0/SeqFromArray.dfy.expect             |  3 -
 Test/dafny0/SmallTests.dfy                      | 90 ++++++++++++-------------
 Test/dafny0/SmallTests.dfy.expect               |  5 +-
 Test/dafny0/TriggerInPredicate.dfy.expect       |  4 +-
 Test/dafny0/columns.dfy                         |  4 +-
 Test/dafny0/columns.dfy.expect                  | 16 ++---
 Test/dafny0/snapshots/Snapshots5.run.dfy        |  2 +-
 Test/dafny0/snapshots/Snapshots5.run.dfy.expect |  9 +++
 17 files changed, 106 insertions(+), 99 deletions(-)

(limited to 'Test/dafny0')

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;
-- 
cgit v1.2.3