From 82cd6194369a376e51a6b525e577f7cc8852ebef Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel <clement.pitclaudel@live.com>
Date: Mon, 20 Jul 2015 13:00:10 -0700
Subject: Split snapshot tests into separate files and add support for %S in
 runTests.py

---
 Test/dafny0/snapshots/Snapshots5.run.dfy | 2 ++
 1 file changed, 2 insertions(+)
 create mode 100644 Test/dafny0/snapshots/Snapshots5.run.dfy

(limited to 'Test/dafny0/snapshots/Snapshots5.run.dfy')

diff --git a/Test/dafny0/snapshots/Snapshots5.run.dfy b/Test/dafny0/snapshots/Snapshots5.run.dfy
new file mode 100644
index 00000000..4f26aac4
--- /dev/null
+++ b/Test/dafny0/snapshots/Snapshots5.run.dfy
@@ -0,0 +1,2 @@
+// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 %S/Inputs/Snapshots5.dfy > "%t"
+// RUN: %diff "%s.expect" "%t"
-- 
cgit v1.2.3


From 8c1a52e085aed20f62a5d24fb2af9bbd5cb3e469 Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel <clement.pitclaudel@live.com>
Date: Thu, 30 Jul 2015 14:56:08 -0700
Subject: Add quotes in snapshot tests.

Thanks Valentin for elucidating this issue!
---
 Test/dafny0/snapshots/Snapshots0.run.dfy | 2 +-
 Test/dafny0/snapshots/Snapshots1.run.dfy | 2 +-
 Test/dafny0/snapshots/Snapshots2.run.dfy | 2 +-
 Test/dafny0/snapshots/Snapshots3.run.dfy | 2 +-
 Test/dafny0/snapshots/Snapshots4.run.dfy | 2 +-
 Test/dafny0/snapshots/Snapshots5.run.dfy | 2 +-
 Test/dafny0/snapshots/Snapshots6.run.dfy | 2 +-
 Test/dafny0/snapshots/Snapshots7.run.dfy | 2 +-
 8 files changed, 8 insertions(+), 8 deletions(-)

(limited to 'Test/dafny0/snapshots/Snapshots5.run.dfy')

diff --git a/Test/dafny0/snapshots/Snapshots0.run.dfy b/Test/dafny0/snapshots/Snapshots0.run.dfy
index cb96468e..5e016c12 100644
--- a/Test/dafny0/snapshots/Snapshots0.run.dfy
+++ b/Test/dafny0/snapshots/Snapshots0.run.dfy
@@ -1,2 +1,2 @@
-// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 %S/Inputs/Snapshots0.dfy > "%t"
+// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 "%S/Inputs/Snapshots0.dfy" > "%t"
 // RUN: %diff "%s.expect" "%t"
diff --git a/Test/dafny0/snapshots/Snapshots1.run.dfy b/Test/dafny0/snapshots/Snapshots1.run.dfy
index 7c277b3e..1907f4a0 100644
--- a/Test/dafny0/snapshots/Snapshots1.run.dfy
+++ b/Test/dafny0/snapshots/Snapshots1.run.dfy
@@ -1,2 +1,2 @@
-// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 %S/Inputs/Snapshots1.dfy > "%t"
+// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 "%S/Inputs/Snapshots1.dfy" > "%t"
 // RUN: %diff "%s.expect" "%t"
diff --git a/Test/dafny0/snapshots/Snapshots2.run.dfy b/Test/dafny0/snapshots/Snapshots2.run.dfy
index 889a8153..71f3e18a 100644
--- a/Test/dafny0/snapshots/Snapshots2.run.dfy
+++ b/Test/dafny0/snapshots/Snapshots2.run.dfy
@@ -1,2 +1,2 @@
-// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 %S/Inputs/Snapshots2.dfy > "%t"
+// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 "%S/Inputs/Snapshots2.dfy" > "%t"
 // RUN: %diff "%s.expect" "%t"
diff --git a/Test/dafny0/snapshots/Snapshots3.run.dfy b/Test/dafny0/snapshots/Snapshots3.run.dfy
index 3df182d6..40dd1012 100644
--- a/Test/dafny0/snapshots/Snapshots3.run.dfy
+++ b/Test/dafny0/snapshots/Snapshots3.run.dfy
@@ -1,2 +1,2 @@
-// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 %S/Inputs/Snapshots3.dfy > "%t"
+// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 "%S/Inputs/Snapshots3.dfy" > "%t"
 // RUN: %diff "%s.expect" "%t"
diff --git a/Test/dafny0/snapshots/Snapshots4.run.dfy b/Test/dafny0/snapshots/Snapshots4.run.dfy
index fd6bef41..803403cf 100644
--- a/Test/dafny0/snapshots/Snapshots4.run.dfy
+++ b/Test/dafny0/snapshots/Snapshots4.run.dfy
@@ -1,2 +1,2 @@
-// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 %S/Inputs/Snapshots4.dfy > "%t"
+// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 "%S/Inputs/Snapshots4.dfy" > "%t"
 // RUN: %diff "%s.expect" "%t"
diff --git a/Test/dafny0/snapshots/Snapshots5.run.dfy b/Test/dafny0/snapshots/Snapshots5.run.dfy
index 4f26aac4..e0f3b16b 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" > "%t"
 // RUN: %diff "%s.expect" "%t"
diff --git a/Test/dafny0/snapshots/Snapshots6.run.dfy b/Test/dafny0/snapshots/Snapshots6.run.dfy
index 157fc5b7..8f958cb9 100644
--- a/Test/dafny0/snapshots/Snapshots6.run.dfy
+++ b/Test/dafny0/snapshots/Snapshots6.run.dfy
@@ -1,2 +1,2 @@
-// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 %S/Inputs/Snapshots6.dfy > "%t"
+// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 "%S/Inputs/Snapshots6.dfy" > "%t"
 // RUN: %diff "%s.expect" "%t"
diff --git a/Test/dafny0/snapshots/Snapshots7.run.dfy b/Test/dafny0/snapshots/Snapshots7.run.dfy
index b192f090..c84c41d2 100644
--- a/Test/dafny0/snapshots/Snapshots7.run.dfy
+++ b/Test/dafny0/snapshots/Snapshots7.run.dfy
@@ -1,2 +1,2 @@
-// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 %S/Inputs/Snapshots7.dfy > "%t"
+// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 "%S/Inputs/Snapshots7.dfy" > "%t"
 // RUN: %diff "%s.expect" "%t"
-- 
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/dafny0/snapshots/Snapshots5.run.dfy')

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