From 3f886d1789d50400ffba2befdc2ae0e8d5c79cbe Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel <clement.pitclaudel@live.com>
Date: Thu, 23 Jul 2015 11:57:19 -0700
Subject: Fix: Unify column numbers in Dafny's errors

Dafny counts from 0, but Boogie counts from 1. Tokens are 1-based. Thus when we
print tokens, we need to decrement the column number. This was done for resolver
errors, but not for verification or parsing errors. In addition, parsing errors
were inconsistent with resolution errors case-wise.

Unfortunately, the fix affects the output of many tests.
---
 Test/dafny1/MoreInduction.dfy.expect | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

(limited to 'Test/dafny1/MoreInduction.dfy.expect')

diff --git a/Test/dafny1/MoreInduction.dfy.expect b/Test/dafny1/MoreInduction.dfy.expect
index c8785e56..5de0ace6 100644
--- a/Test/dafny1/MoreInduction.dfy.expect
+++ b/Test/dafny1/MoreInduction.dfy.expect
@@ -1,17 +1,17 @@
-MoreInduction.dfy(78,1): Error BP5003: A postcondition might not hold on this return path.
-MoreInduction.dfy(77,11): Related location: This is the postcondition that might not hold.
+MoreInduction.dfy(78,0): Error BP5003: A postcondition might not hold on this return path.
+MoreInduction.dfy(77,10): Related location: This is the postcondition that might not hold.
 Execution trace:
     (0,0): anon0
-MoreInduction.dfy(83,1): Error BP5003: A postcondition might not hold on this return path.
-MoreInduction.dfy(82,21): Related location: This is the postcondition that might not hold.
+MoreInduction.dfy(83,0): Error BP5003: A postcondition might not hold on this return path.
+MoreInduction.dfy(82,20): Related location: This is the postcondition that might not hold.
 Execution trace:
     (0,0): anon0
-MoreInduction.dfy(88,1): Error BP5003: A postcondition might not hold on this return path.
-MoreInduction.dfy(87,11): Related location: This is the postcondition that might not hold.
+MoreInduction.dfy(88,0): Error BP5003: A postcondition might not hold on this return path.
+MoreInduction.dfy(87,10): Related location: This is the postcondition that might not hold.
 Execution trace:
     (0,0): anon0
-MoreInduction.dfy(93,1): Error BP5003: A postcondition might not hold on this return path.
-MoreInduction.dfy(92,22): Related location: This is the postcondition that might not hold.
+MoreInduction.dfy(93,0): Error BP5003: A postcondition might not hold on this return path.
+MoreInduction.dfy(92,21): Related location: This is the postcondition that might not hold.
 Execution trace:
     (0,0): anon0
 
-- 
cgit v1.2.3


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 +++
 Test/dafny1/FindZero.dfy                           |  8 +-
 Test/dafny1/MoreInduction.dfy                      |  6 +-
 Test/dafny1/MoreInduction.dfy.expect               |  2 +
 Test/dafny1/PriorityQueue.dfy                      | 32 ++++----
 .../COST-verif-comp-2011-4-FloydCycleDetect.dfy    |  4 +-
 Test/dafny3/GenericSort.dfy                        |  2 +-
 Test/dafny4/Bug60.dfy                              |  4 +-
 Test/dafny4/Bug63.dfy                              |  4 +-
 Test/dafny4/Primes.dfy                             |  8 +-
 Test/vacid0/Composite.dfy                          |  2 +-
 Test/wishlist/exists-b-exists-not-b.dfy            |  4 +-
 28 files changed, 145 insertions(+), 136 deletions(-)

(limited to 'Test/dafny1/MoreInduction.dfy.expect')

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;
diff --git a/Test/dafny1/FindZero.dfy b/Test/dafny1/FindZero.dfy
index 0940d9e7..374555b0 100644
--- a/Test/dafny1/FindZero.dfy
+++ b/Test/dafny1/FindZero.dfy
@@ -3,7 +3,7 @@
 
 method FindZero(a: array<int>) returns (r: int)
   requires a != null && forall i :: 0 <= i < a.Length ==> 0 <= a[i];
-  requires forall i :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];
+  requires forall i {:nowarn} :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];
   ensures 0 <= r ==> r < a.Length && a[r] == 0;
   ensures r < 0 ==> forall i :: 0 <= i < a.Length ==> a[i] != 0;
 {
@@ -20,7 +20,7 @@ method FindZero(a: array<int>) returns (r: int)
 
 lemma Lemma(a: array<int>, k: int, m: int)
   requires a != null && forall i :: 0 <= i < a.Length ==> 0 <= a[i];
-  requires forall i :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];
+  requires forall i {:nowarn} :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];
   requires 0 <= k;
   requires k < a.Length ==> m <= a[k];
   ensures forall i :: k <= i < k+m && i < a.Length ==> a[i] != 0;
@@ -36,7 +36,7 @@ lemma Lemma(a: array<int>, k: int, m: int)
 
 method FindZero_GhostLoop(a: array<int>) returns (r: int)
   requires a != null && forall i :: 0 <= i < a.Length ==> 0 <= a[i];
-  requires forall i :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];
+  requires forall i {:nowarn} :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];
   ensures 0 <= r ==> r < a.Length && a[r] == 0;
   ensures r < 0 ==> forall i :: 0 <= i < a.Length ==> a[i] != 0;
 {
@@ -63,7 +63,7 @@ method FindZero_GhostLoop(a: array<int>) returns (r: int)
 
 method FindZero_Assert(a: array<int>) returns (r: int)
   requires a != null && forall i :: 0 <= i < a.Length ==> 0 <= a[i];
-  requires forall i :: 0 <= i-1 && i < a.Length ==> a[i-1]-1 <= a[i];
+  requires forall i {:nowarn} :: 0 <= i-1 && i < a.Length ==> a[i-1]-1 <= a[i];
   ensures 0 <= r ==> r < a.Length && a[r] == 0;
   ensures r < 0 ==> forall i :: 0 <= i < a.Length ==> a[i] != 0;
 {
diff --git a/Test/dafny1/MoreInduction.dfy b/Test/dafny1/MoreInduction.dfy
index 319bb8d0..bd654db5 100644
--- a/Test/dafny1/MoreInduction.dfy
+++ b/Test/dafny1/MoreInduction.dfy
@@ -83,12 +83,12 @@ lemma LemmaOne(n: int)
 {
 }
 
-lemma LemmaAll_Neg()
-  ensures forall n :: NegFac(-n) <= -1;  // error: fails to verify because of the minus in the trigger
+lemma LemmaAll_Neg() //FIXME I don't understand the comment below; what trigger?
+  ensures forall n {:nowarn} :: NegFac(-n) <= -1;  // error: fails to verify because of the minus in the trigger
 {
 }
 
-lemma LemmaOne_Neg(n: int)
+lemma LemmaOne_Neg(n: int) //FIXME What trigger?
   ensures NegFac(-n) <= -1;  // error: fails to verify because of the minus in the trigger
 {
 }
diff --git a/Test/dafny1/MoreInduction.dfy.expect b/Test/dafny1/MoreInduction.dfy.expect
index 5de0ace6..7da5e2ec 100644
--- a/Test/dafny1/MoreInduction.dfy.expect
+++ b/Test/dafny1/MoreInduction.dfy.expect
@@ -1,5 +1,6 @@
 MoreInduction.dfy(78,0): Error BP5003: A postcondition might not hold on this return path.
 MoreInduction.dfy(77,10): Related location: This is the postcondition that might not hold.
+MoreInduction.dfy(77,32): Related location
 Execution trace:
     (0,0): anon0
 MoreInduction.dfy(83,0): Error BP5003: A postcondition might not hold on this return path.
@@ -8,6 +9,7 @@ Execution trace:
     (0,0): anon0
 MoreInduction.dfy(88,0): Error BP5003: A postcondition might not hold on this return path.
 MoreInduction.dfy(87,10): Related location: This is the postcondition that might not hold.
+MoreInduction.dfy(87,43): Related location
 Execution trace:
     (0,0): anon0
 MoreInduction.dfy(93,0): Error BP5003: A postcondition might not hold on this return path.
diff --git a/Test/dafny1/PriorityQueue.dfy b/Test/dafny1/PriorityQueue.dfy
index 94223cba..3d2a5d78 100644
--- a/Test/dafny1/PriorityQueue.dfy
+++ b/Test/dafny1/PriorityQueue.dfy
@@ -12,7 +12,7 @@ class PriorityQueue {
     reads this, Repr;
   {
     MostlyValid() &&
-    (forall j :: 2 <= j && j <= n ==> a[j/2] <= a[j])
+    (forall j {:nowarn} :: 2 <= j && j <= n ==> a[j/2] <= a[j])
   }
 
   predicate MostlyValid()
@@ -50,8 +50,8 @@ class PriorityQueue {
   method SiftUp(k: int)
     requires 1 <= k && k <= n;
     requires MostlyValid();
-    requires (forall j :: 2 <= j && j <= n && j != k ==> a[j/2] <= a[j]);
-    requires (forall j :: 1 <= j && j <= n ==> j/2 != k);  // k is a leaf
+    requires (forall j {:nowarn} :: 2 <= j && j <= n && j != k ==> a[j/2] <= a[j]);
+    requires (forall j {:nowarn} :: 1 <= j && j <= n ==> j/2 != k);  // k is a leaf
     modifies a;
     ensures Valid();
   {
@@ -59,8 +59,8 @@ class PriorityQueue {
     assert MostlyValid();
     while (1 < i)
       invariant i <= k && MostlyValid();
-      invariant (forall j :: 2 <= j && j <= n && j != i ==> a[j/2] <= a[j]);
-      invariant (forall j :: 1 <= j/2/2 && j/2 == i && j <= n ==> a[j/2/2] <= a[j]);
+      invariant (forall j {:nowarn} :: 2 <= j && j <= n && j != i ==> a[j/2] <= a[j]);
+      invariant (forall j {:nowarn} :: 1 <= j/2/2 && j/2 == i && j <= n ==> a[j/2/2] <= a[j]);
     {
       if (a[i/2] <= a[i]) {
         return;
@@ -85,8 +85,8 @@ class PriorityQueue {
   method SiftDown(k: int)
     requires 1 <= k;
     requires MostlyValid();
-    requires (forall j :: 2 <= j && j <= n && j/2 != k ==> a[j/2] <= a[j]);
-    requires (forall j :: 2 <= j && j <= n && 1 <= j/2/2 && j/2/2 != k ==> a[j/2/2] <= a[j]);
+    requires (forall j {:nowarn} :: 2 <= j && j <= n && j/2 != k ==> a[j/2] <= a[j]);
+    requires (forall j {:nowarn} :: 2 <= j && j <= n && 1 <= j/2/2 && j/2/2 != k ==> a[j/2/2] <= a[j]);
     // Alternatively, the line above can be expressed as:
     //     requires (forall j :: 1 <= k/2 && j/2 == k && j <= n ==> a[j/2/2] <= a[j]);
     modifies a;
@@ -95,8 +95,8 @@ class PriorityQueue {
     var i := k;
     while (2*i <= n)  // while i is not a leaf
       invariant 1 <= i && MostlyValid();
-      invariant (forall j :: 2 <= j && j <= n && j/2 != i ==> a[j/2] <= a[j]);
-      invariant (forall j :: 2 <= j && j <= n && 1 <= j/2/2 && j/2/2 != i ==> a[j/2/2] <= a[j]);
+      invariant (forall j {:nowarn} :: 2 <= j && j <= n && j/2 != i ==> a[j/2] <= a[j]);
+      invariant (forall j {:nowarn} :: 2 <= j && j <= n && 1 <= j/2/2 && j/2/2 != i ==> a[j/2/2] <= a[j]);
     {
       var smallestChild;
       if (2*i + 1 <= n && a[2*i + 1] < a[2*i]) {
@@ -127,7 +127,7 @@ class PriorityQueue_Alternative {
     reads this, Repr;
   {
     MostlyValid() &&
-    (forall j :: 2 <= j && j <= n ==> a[j/2] <= a[j])
+    (forall j {:nowarn} :: 2 <= j && j <= n ==> a[j/2] <= a[j])
   }
 
   predicate MostlyValid()
@@ -164,7 +164,7 @@ class PriorityQueue_Alternative {
 
   method SiftUp()
     requires MostlyValid();
-    requires (forall j :: 2 <= j && j <= n && j != n ==> a[j/2] <= a[j]);
+    requires (forall j {:nowarn} :: 2 <= j && j <= n && j != n ==> a[j/2] <= a[j]);
     modifies a;
     ensures Valid();
   {
@@ -172,8 +172,8 @@ class PriorityQueue_Alternative {
     assert MostlyValid();
     while (1 < i)
       invariant i <= n && MostlyValid();
-      invariant (forall j :: 2 <= j && j <= n && j != i ==> a[j/2] <= a[j]);
-      invariant (forall j :: 1 <= j/2/2 && j/2 == i && j <= n ==> a[j/2/2] <= a[j]);
+      invariant (forall j {:nowarn} :: 2 <= j && j <= n && j != i ==> a[j/2] <= a[j]);
+      invariant (forall j {:nowarn} :: 1 <= j/2/2 && j/2 == i && j <= n ==> a[j/2/2] <= a[j]);
     {
       if (a[i/2] <= a[i]) {
         return;
@@ -197,15 +197,15 @@ class PriorityQueue_Alternative {
 
   method SiftDown()
     requires MostlyValid();
-    requires (forall j :: 4 <= j && j <= n ==> a[j/2] <= a[j]);
+    requires (forall j {:nowarn} :: 4 <= j && j <= n ==> a[j/2] <= a[j]);
     modifies a;
     ensures Valid();
   {
     var i := 1;
     while (2*i <= n)  // while i is not a leaf
       invariant 1 <= i && MostlyValid();
-      invariant (forall j :: 2 <= j && j <= n && j/2 != i ==> a[j/2] <= a[j]);
-      invariant (forall j :: 1 <= j/2/2 && j/2 == i && j <= n ==> a[j/2/2] <= a[j]);
+      invariant (forall j {:nowarn} :: 2 <= j && j <= n && j/2 != i ==> a[j/2] <= a[j]);
+      invariant (forall j {:nowarn} :: 1 <= j/2/2 && j/2 == i && j <= n ==> a[j/2/2] <= a[j]);
     {
       var smallestChild;
       if (2*i + 1 <= n && a[2*i + 1] < a[2*i]) {
diff --git a/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy b/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy
index 2aa14db7..72250f99 100644
--- a/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy
+++ b/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy
@@ -164,7 +164,7 @@ class Node {
       invariant 0 <= t < h && Nexxxt(t, S) == tortoise && Nexxxt(h, S) == hare;
       // What follows of the invariant is for proving termination:
       invariant h == 1 + 2*t && t <= A + B;
-      invariant forall k :: 0 <= k < t ==> Nexxxt(k, S) != Nexxxt(1+2*k, S);
+      invariant forall k {:nowarn} :: 0 <= k < t ==> Nexxxt(k, S) != Nexxxt(1+2*k, S);
       decreases A + B - t;
     {
       if hare == null || hare.next == null {
@@ -225,7 +225,7 @@ class Node {
     requires 0 <= a && 1 <= b;
     requires forall k,l :: 0 <= k < l < a ==> Nexxxt(k, S) != Nexxxt(l, S);
     requires Nexxxt(a, S) == null || Nexxxt(a, S).Nexxxt(b, S) == Nexxxt(a, S);
-    ensures exists T :: 0 <= T < a+b && Nexxxt(T, S) == Nexxxt(1+2*T, S);
+    ensures exists T {:nowarn} :: 0 <= T < a+b && Nexxxt(T, S) == Nexxxt(1+2*T, S);
   {
     if Nexxxt(a, S) == null {
       Lemma_NullIsTerminal(1+2*a, S);
diff --git a/Test/dafny3/GenericSort.dfy b/Test/dafny3/GenericSort.dfy
index 6bd06965..ea75c196 100644
--- a/Test/dafny3/GenericSort.dfy
+++ b/Test/dafny3/GenericSort.dfy
@@ -36,7 +36,7 @@ abstract module Sort {
     requires a != null && 0 <= low <= high <= a.Length
     reads a
   {
-    forall i :: low < i < high ==> O.Leq(a[i-1], a[i])
+    forall i {:nowarn} :: low < i < high ==> O.Leq(a[i-1], a[i])
   }
   // ...but we show that property to imply all pairs to be sorted.  The proof of this
   // lemma uses the transitivity property.
diff --git a/Test/dafny4/Bug60.dfy b/Test/dafny4/Bug60.dfy
index 5340ad6b..c433451c 100644
--- a/Test/dafny4/Bug60.dfy
+++ b/Test/dafny4/Bug60.dfy
@@ -9,5 +9,5 @@ method Main()
     print (s, m), "\n";
     print (|s|, |m|), "\n";
     print(set s | s in m), "\n";
-    print (forall x :: x in (map [1:=10, 2:=20]) ==> x > 0), "\n";
-}
\ No newline at end of file
+    print (forall x {:nowarn} :: x in (map [1:=10, 2:=20]) ==> x > 0), "\n";
+}
diff --git a/Test/dafny4/Bug63.dfy b/Test/dafny4/Bug63.dfy
index 86aad232..39cbae1b 100644
--- a/Test/dafny4/Bug63.dfy
+++ b/Test/dafny4/Bug63.dfy
@@ -8,6 +8,6 @@ method M()
 
 method Client()
 {
-  assume forall o: object :: o != null ==> false;
+  assume forall o: object {:nowarn} :: o != null ==> false;
   M();
-}
\ No newline at end of file
+}
diff --git a/Test/dafny4/Primes.dfy b/Test/dafny4/Primes.dfy
index b0bb7527..fd64b45e 100644
--- a/Test/dafny4/Primes.dfy
+++ b/Test/dafny4/Primes.dfy
@@ -3,7 +3,7 @@
 
 predicate IsPrime(n: int)
 {
-  2 <= n && forall m :: 2 <= m < n ==> n % m != 0
+  2 <= n && forall m {:nowarn} :: 2 <= m < n ==> n % m != 0 // WISH It would be great to think about the status of modulo as a trigger
 }
 
 // The following theorem shows that there is an infinite number of primes
@@ -167,8 +167,8 @@ lemma Composite(c: int) returns (a: int, b: int)
   calc {
     true;
     !IsPrime(c);
-    !(2 <= c && forall m :: 2 <= m < c ==> c % m != 0);
-    exists m :: 2 <= m < c && c % m == 0;
+    !(2 <= c && forall m {:nowarn} :: 2 <= m < c ==> c % m != 0);
+    exists m {:nowarn} :: 2 <= m < c && c % m == 0;
   }
   a :| 2 <= a < c && c % a == 0;
   b := c / a;
@@ -194,7 +194,7 @@ lemma LargestElementExists(s: set<int>)
   var s' := s;
   while true
     invariant s' != {} && s' <= s;
-    invariant forall x,y :: x in s' && y in s - s' ==> y <= x;
+    invariant forall x,y {:nowarn} :: x in s' && y in s - s' ==> y <= x;
     decreases s';
   {
     var x :| x in s';  // pick something
diff --git a/Test/vacid0/Composite.dfy b/Test/vacid0/Composite.dfy
index d5551d82..bc3b5baf 100644
--- a/Test/vacid0/Composite.dfy
+++ b/Test/vacid0/Composite.dfy
@@ -68,7 +68,7 @@ class Composite {
     // sets child.parent to this:
     ensures child.parent == this;
     // leaves everything in S+U valid:
-    ensures (forall c :: c in S+U ==> c.Valid(S+U));
+    ensures (forall c {:autotriggers false} :: c in S+U ==> c.Valid(S+U)); // We can't generate a trigger for this at the moment; if we did, we would still need to prevent TrSplitExpr from translating c in S+U to S[c] || U[c].
   {
     if (left == null) {
       left := child;
diff --git a/Test/wishlist/exists-b-exists-not-b.dfy b/Test/wishlist/exists-b-exists-not-b.dfy
index 711c5611..2573b2f2 100644
--- a/Test/wishlist/exists-b-exists-not-b.dfy
+++ b/Test/wishlist/exists-b-exists-not-b.dfy
@@ -5,6 +5,6 @@
 // otherwise, trigger splitting prevents `exists b :: b || not b` from verifying
 
 method M() {
-  assert exists b: bool :: b; // WISH
-  assert exists b: bool :: !b; // WISH
+  assert exists b : bool {:nowarn} :: b; // WISH
+  assert exists b : bool {:nowarn} :: !b; // WISH
 }
-- 
cgit v1.2.3


From 41ca5479952fc4dfaec72978a72327f2d534eee6 Mon Sep 17 00:00:00 2001
From: leino <unknown>
Date: Sun, 20 Sep 2015 21:57:39 -0700
Subject: Adjusted (corrected, I think) test output

---
 Test/dafny1/MoreInduction.dfy.expect | 2 --
 1 file changed, 2 deletions(-)

(limited to 'Test/dafny1/MoreInduction.dfy.expect')

diff --git a/Test/dafny1/MoreInduction.dfy.expect b/Test/dafny1/MoreInduction.dfy.expect
index 7da5e2ec..5de0ace6 100644
--- a/Test/dafny1/MoreInduction.dfy.expect
+++ b/Test/dafny1/MoreInduction.dfy.expect
@@ -1,6 +1,5 @@
 MoreInduction.dfy(78,0): Error BP5003: A postcondition might not hold on this return path.
 MoreInduction.dfy(77,10): Related location: This is the postcondition that might not hold.
-MoreInduction.dfy(77,32): Related location
 Execution trace:
     (0,0): anon0
 MoreInduction.dfy(83,0): Error BP5003: A postcondition might not hold on this return path.
@@ -9,7 +8,6 @@ Execution trace:
     (0,0): anon0
 MoreInduction.dfy(88,0): Error BP5003: A postcondition might not hold on this return path.
 MoreInduction.dfy(87,10): Related location: This is the postcondition that might not hold.
-MoreInduction.dfy(87,43): Related location
 Execution trace:
     (0,0): anon0
 MoreInduction.dfy(93,0): Error BP5003: A postcondition might not hold on this return path.
-- 
cgit v1.2.3