27 files changed, 67 insertions, 24 deletions
diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy
index ea1911fe..a44ff5c3 100644
--- a/Test/VSI-Benchmarks/b8.dfy
+++ b/Test/VSI-Benchmarks/b8.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %dafny /compile:0 /autoTriggers:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // Benchmark 8
diff --git a/Test/VerifyThis2015/Problem3.dfy b/Test/VerifyThis2015/Problem3.dfy
index 21bdd4ed..60506a33 100644
--- a/Test/VerifyThis2015/Problem3.dfy
+++ b/Test/VerifyThis2015/Problem3.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // Rustan Leino
diff --git a/Test/cloudmake/CloudMake-CachedBuilds.dfy b/Test/cloudmake/CloudMake-CachedBuilds.dfy
index 9e1b511e..5f16da90 100644
--- a/Test/cloudmake/CloudMake-CachedBuilds.dfy
+++ b/Test/cloudmake/CloudMake-CachedBuilds.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // This module proves the correctness of the algorithms.  It leaves a number of things undefined.
diff --git a/Test/cloudmake/CloudMake-ConsistentBuilds.dfy b/Test/cloudmake/CloudMake-ConsistentBuilds.dfy
index 6d86607b..c2fa4205 100644
--- a/Test/cloudmake/CloudMake-ConsistentBuilds.dfy
+++ b/Test/cloudmake/CloudMake-ConsistentBuilds.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 /******* State *******/
diff --git a/Test/cloudmake/CloudMake-ParallelBuilds.dfy b/Test/cloudmake/CloudMake-ParallelBuilds.dfy
index 07cae317..5cc70994 100644
--- a/Test/cloudmake/CloudMake-ParallelBuilds.dfy
+++ b/Test/cloudmake/CloudMake-ParallelBuilds.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // This module proves the correctness of the algorithms.  It leaves a number of things undefined.
diff --git a/Test/dafny0/Basics.dfy b/Test/dafny0/Basics.dfy
index 89b0f02a..7b8b632b 100644
--- a/Test/dafny0/Basics.dfy
+++ b/Test/dafny0/Basics.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:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 class Global {
diff --git a/Test/dafny0/Calculations.dfy b/Test/dafny0/Calculations.dfy
index a7c8e06c..eb4ff1b9 100644
--- a/Test/dafny0/Calculations.dfy
+++ b/Test/dafny0/Calculations.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:0 "%s" > "%t"
 // RUN: %dafny /noVerify /compile:0 "%t.dprint.dfy" >> "%t"
 // RUN: %diff "%s.expect" "%t"
 
diff --git a/Test/dafny0/Compilation.dfy b/Test/dafny0/Compilation.dfy
index 7a443e47..213ace54 100644
--- a/Test/dafny0/Compilation.dfy
+++ b/Test/dafny0/Compilation.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 "%s" > "%t"
+// RUN: %dafny /compile:3 /autoTriggers:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // The tests in this file are designed to run through the compiler.  They contain
diff --git a/Test/dafny0/ForallCompilation.dfy b/Test/dafny0/ForallCompilation.dfy
index c812983a..4d89f70d 100644
--- a/Test/dafny0/ForallCompilation.dfy
+++ b/Test/dafny0/ForallCompilation.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 method Main() {
diff --git a/Test/dafny0/Fuel.dfy b/Test/dafny0/Fuel.dfy
index 6347e134..a768db02 100644
--- a/Test/dafny0/Fuel.dfy
+++ b/Test/dafny0/Fuel.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:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 module TestModule1 {
diff --git a/Test/dafny0/LetExpr.dfy b/Test/dafny0/LetExpr.dfy
index 000fce53..6a0ca66b 100644
--- a/Test/dafny0/LetExpr.dfy
+++ b/Test/dafny0/LetExpr.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:0 "%s" > "%t"
 // RUN: %dafny /noVerify /compile:0 "%t.dprint.dfy" >> "%t"
 // RUN: %diff "%s.expect" "%t"
 
diff --git a/Test/dafny0/LetExpr.dfy.expect b/Test/dafny0/LetExpr.dfy.expect
index f0f51274..8f365da3 100644
--- a/Test/dafny0/LetExpr.dfy.expect
+++ b/Test/dafny0/LetExpr.dfy.expect
@@ -35,5 +35,6 @@ Execution trace:
     (0,0): anon10_Then
 
 Dafny program verifier finished with 39 verified, 9 errors
+LetExpr.dfy.tmp.dprint.dfy(162,2): Warning: /!\ No terms found to trigger on.
 
 Dafny program verifier finished with 0 verified, 0 errors
diff --git a/Test/dafny0/LhsDuplicates.dfy b/Test/dafny0/LhsDuplicates.dfy
index 6a84c5a5..8a57f6ce 100644
--- a/Test/dafny0/LhsDuplicates.dfy
+++ b/Test/dafny0/LhsDuplicates.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:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 class MyClass<T> {
diff --git a/Test/dafny0/Parallel.dfy b/Test/dafny0/Parallel.dfy
index 93a16475..00a1514c 100644
--- a/Test/dafny0/Parallel.dfy
+++ b/Test/dafny0/Parallel.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:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 class C {
diff --git a/Test/dafny0/SmallTests.dfy.expect b/Test/dafny0/SmallTests.dfy.expect
index 6161c3dd..746e978a 100644
--- a/Test/dafny0/SmallTests.dfy.expect
+++ b/Test/dafny0/SmallTests.dfy.expect
@@ -197,5 +197,6 @@ Execution trace:
     (0,0): anon0
 
 Dafny program verifier finished with 104 verified, 35 errors
+SmallTests.dfy.tmp.dprint.dfy(369,4): Warning: /!\ No trigger covering all quantified variables found.
 
 Dafny program verifier finished with 0 verified, 0 errors
diff --git a/Test/dafny1/MoreInduction.dfy b/Test/dafny1/MoreInduction.dfy
index bd654db5..2b5187a4 100644
--- a/Test/dafny1/MoreInduction.dfy
+++ b/Test/dafny1/MoreInduction.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 datatype List<X> = Nil | Cons(Node<X>, List<X>)
diff --git a/Test/dafny1/SchorrWaite-stages.dfy b/Test/dafny1/SchorrWaite-stages.dfy
index 0eaed68c..a6e5e3aa 100644
--- a/Test/dafny1/SchorrWaite-stages.dfy
+++ b/Test/dafny1/SchorrWaite-stages.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // Schorr-Waite algorithms, written and verified in Dafny.
diff --git a/Test/dafny1/SchorrWaite.dfy b/Test/dafny1/SchorrWaite.dfy
index 50210eb1..b0877f9f 100644
--- a/Test/dafny1/SchorrWaite.dfy
+++ b/Test/dafny1/SchorrWaite.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // Rustan Leino
diff --git a/Test/dafny1/Substitution.dfy b/Test/dafny1/Substitution.dfy
index da64d004..b9c83aff 100644
--- a/Test/dafny1/Substitution.dfy
+++ b/Test/dafny1/Substitution.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 datatype List = Nil | Cons(Expr, List)
diff --git a/Test/dafny1/UltraFilter.dfy b/Test/dafny1/UltraFilter.dfy
index a32e6e0b..7ac4e749 100644
--- a/Test/dafny1/UltraFilter.dfy
+++ b/Test/dafny1/UltraFilter.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // ultra filter
diff --git a/Test/dafny2/SnapshotableTrees.dfy b/Test/dafny2/SnapshotableTrees.dfy
index 2bdfb83b..033c5db0 100644
--- a/Test/dafny2/SnapshotableTrees.dfy
+++ b/Test/dafny2/SnapshotableTrees.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:2 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /compile:2 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // Rustan Leino, September 2011.
diff --git a/Test/dafny3/Filter.dfy b/Test/dafny3/Filter.dfy
index 4f8b35ec..7473a580 100644
--- a/Test/dafny3/Filter.dfy
+++ b/Test/dafny3/Filter.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 codatatype Stream<T> = Cons(head: T, tail: Stream)
diff --git a/Test/dafny4/GHC-MergeSort.dfy b/Test/dafny4/GHC-MergeSort.dfy
index 976b8a27..24903d87 100644
--- a/Test/dafny4/GHC-MergeSort.dfy
+++ b/Test/dafny4/GHC-MergeSort.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // Rustan Leino
diff --git a/Test/dafny4/NumberRepresentations.dfy b/Test/dafny4/NumberRepresentations.dfy
index 0d6cffa1..c15f4987 100644
--- a/Test/dafny4/NumberRepresentations.dfy
+++ b/Test/dafny4/NumberRepresentations.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // We consider a number representation that consists of a sequence of digits.  The least
diff --git a/Test/dafny4/Primes.dfy b/Test/dafny4/Primes.dfy
index fd64b45e..0c2a64dd 100644
--- a/Test/dafny4/Primes.dfy
+++ b/Test/dafny4/Primes.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 predicate IsPrime(n: int)
diff --git a/Test/server/simple-session.transcript.expect b/Test/server/simple-session.transcript.expect
index 1aadca7f..a5f841bc 100644
--- a/Test/server/simple-session.transcript.expect
+++ b/Test/server/simple-session.transcript.expect
@@ -346,6 +346,7 @@ transcript(10,27): Error: invalid UnaryExpression
 Verification completed successfully!
 [SUCCESS] [[DAFNY-SERVER: EOM]]
 transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(10,9): Warning: /!\ No terms found to trigger on.
 
 Verifying CheckWellformed$$_module.__default.A ...
 Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
@@ -366,6 +367,7 @@ Execution trace:
 Verification completed successfully!
 [SUCCESS] [[DAFNY-SERVER: EOM]]
 transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(10,9): Warning: /!\ No terms found to trigger on.
 
 Verifying CheckWellformed$$_module.__default.A ...
 Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
@@ -383,6 +385,7 @@ Verifying Impl$$_module.__default.M_k ...
 Verification completed successfully!
 [SUCCESS] [[DAFNY-SERVER: EOM]]
 transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(10,9): Warning: /!\ No terms found to trigger on.
 
 Verifying CheckWellformed$$_module.__default.A ...
 Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
@@ -406,6 +409,7 @@ transcript(12,0): Error: invalid UpdateStmt
 Verification completed successfully!
 [SUCCESS] [[DAFNY-SERVER: EOM]]
 transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(10,9): Warning: /!\ No terms found to trigger on.
 
 Verifying CheckWellformed$$_module.__default.A ...
 Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
@@ -423,6 +427,7 @@ Verifying Impl$$_module.__default.M_k ...
 Verification completed successfully!
 [SUCCESS] [[DAFNY-SERVER: EOM]]
 transcript(5,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(10,9): Warning: /!\ No terms found to trigger on.
 
 Verifying CheckWellformed$$_module.__default.A ...
 Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
@@ -498,6 +503,10 @@ transcript(5,0): Warning: module-level methods are always non-instance, so the '
 transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
 transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
 transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(10,9): Warning: /!\ No terms found to trigger on.
+transcript(20,9): Warning: /!\ No terms found to trigger on.
+transcript(29,9): Warning: /!\ No terms found to trigger on.
+transcript(38,9): Warning: /!\ No terms found to trigger on.
 
 Verifying CheckWellformed$$_module.__default.A ...
 Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
@@ -538,6 +547,10 @@ transcript(5,0): Warning: module-level methods are always non-instance, so the '
 transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
 transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
 transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(10,9): Warning: /!\ No terms found to trigger on.
+transcript(20,9): Warning: /!\ No terms found to trigger on.
+transcript(29,9): Warning: /!\ No terms found to trigger on.
+transcript(38,9): Warning: /!\ No terms found to trigger on.
 
 Verifying CheckWellformed$$_module.__default.A ...
 Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
@@ -584,6 +597,10 @@ transcript(5,0): Warning: module-level methods are always non-instance, so the '
 transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
 transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
 transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(10,9): Warning: /!\ No terms found to trigger on.
+transcript(20,9): Warning: /!\ No terms found to trigger on.
+transcript(29,9): Warning: /!\ No terms found to trigger on.
+transcript(38,9): Warning: /!\ No terms found to trigger on.
 
 Verifying CheckWellformed$$_module.__default.A ...
 Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
@@ -638,6 +655,10 @@ transcript(5,0): Warning: module-level methods are always non-instance, so the '
 transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
 transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
 transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(10,9): Warning: /!\ No terms found to trigger on.
+transcript(20,9): Warning: /!\ No terms found to trigger on.
+transcript(29,9): Warning: /!\ No terms found to trigger on.
+transcript(38,9): Warning: /!\ No terms found to trigger on.
 
 Verifying CheckWellformed$$_module.__default.A ...
 Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
@@ -685,6 +706,10 @@ transcript(5,0): Warning: module-level methods are always non-instance, so the '
 transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
 transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
 transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(10,9): Warning: /!\ No terms found to trigger on.
+transcript(20,9): Warning: /!\ No terms found to trigger on.
+transcript(29,9): Warning: /!\ No terms found to trigger on.
+transcript(38,9): Warning: /!\ No terms found to trigger on.
 
 Verifying CheckWellformed$$_module.__default.A ...
 Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
@@ -729,6 +754,10 @@ transcript(5,0): Warning: module-level methods are always non-instance, so the '
 transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
 transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
 transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(10,9): Warning: /!\ No terms found to trigger on.
+transcript(20,9): Warning: /!\ No terms found to trigger on.
+transcript(29,9): Warning: /!\ No terms found to trigger on.
+transcript(38,9): Warning: /!\ No terms found to trigger on.
 
 Verifying CheckWellformed$$_module.__default.A ...
 Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
@@ -796,6 +825,10 @@ transcript(5,0): Warning: module-level methods are always non-instance, so the '
 transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
 transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
 transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(10,9): Warning: /!\ No terms found to trigger on.
+transcript(20,9): Warning: /!\ No terms found to trigger on.
+transcript(29,9): Warning: /!\ No terms found to trigger on.
+transcript(38,9): Warning: /!\ No terms found to trigger on.
 
 Verifying CheckWellformed$$_module.__default.A ...
 Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
@@ -861,6 +894,10 @@ transcript(5,0): Warning: module-level methods are always non-instance, so the '
 transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
 transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
 transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(10,9): Warning: /!\ No terms found to trigger on.
+transcript(20,9): Warning: /!\ No terms found to trigger on.
+transcript(29,9): Warning: /!\ No terms found to trigger on.
+transcript(38,9): Warning: /!\ No terms found to trigger on.
 
 Verifying CheckWellformed$$_module.__default.A ...
 Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
@@ -905,6 +942,10 @@ transcript(5,0): Warning: module-level methods are always non-instance, so the '
 transcript(15,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
 transcript(24,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
 transcript(33,0): Warning: module-level methods are always non-instance, so the 'static' keyword is not allowed here
+transcript(10,9): Warning: /!\ No terms found to trigger on.
+transcript(20,9): Warning: /!\ No terms found to trigger on.
+transcript(29,9): Warning: /!\ No terms found to trigger on.
+transcript(38,9): Warning: /!\ No terms found to trigger on.
 
 Verifying CheckWellformed$$_module.__default.A ...
 Retrieving cached verification result for implementation CheckWellformed$$_module.__default.A...
diff --git a/Test/vstte2012/BreadthFirstSearch.dfy b/Test/vstte2012/BreadthFirstSearch.dfy
index b111a438..375f4a09 100644
--- a/Test/vstte2012/BreadthFirstSearch.dfy
+++ b/Test/vstte2012/BreadthFirstSearch.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /dprint:"%t.dprint" /vcsMaxKeepGoingSplits:10 "%s" > "%t"
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" /vcsMaxKeepGoingSplits:10 /autoTriggers:0 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 class BreadthFirstSearch<Vertex(==)>