Make /autoTriggers:1 to be default. Add /autoTriggers:0 to tests that requires

it. Don't use pretty warning signs since we can't diff them correctly in the
test output from the test run.

29 files changed, 71 insertions, 28 deletions

diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs
index f3b38a84..607090eb 100644
--- a/Source/Dafny/DafnyOptions.cs
+++ b/Source/Dafny/DafnyOptions.cs
@@ -66,7 +66,7 @@ namespace Microsoft.Dafny
     public bool AllowGlobals = false;

     public bool CountVerificationErrors = true;

     public bool Optimize = false;

-    public bool AutoTriggers = false;

+    public bool AutoTriggers = true;

     public bool RewriteFocalPredicates = true;

     public bool PrintTooltips = false;

     public bool PrintStats = false;

@@ -386,8 +386,8 @@ namespace Microsoft.Dafny
                 1 (default) - If preprocessing succeeds, set exit code to the number of

                               verification errors.

   /autoTriggers:<n>

-                0 (default) - Do not generate {:trigger} annotations for user-level quantifiers.

-                1 - Add a {:trigger} to each user-level quantifier. Existing

+                0 - Do not generate {:trigger} annotations for user-level quantifiers.

+                1 (default) - Add a {:trigger} to each user-level quantifier. Existing

                               annotations are preserved.

   /rewriteFocalPredicates:<n>

                 0 - Don't rewrite predicates in the body of prefix lemmas.

diff --git a/Source/DafnyServer/Utilities.cs b/Source/DafnyServer/Utilities.cs
index 30d779e7..48bea01a 100644
--- a/Source/DafnyServer/Utilities.cs
+++ b/Source/DafnyServer/Utilities.cs
@@ -51,7 +51,7 @@ namespace Microsoft.Dafny {
         DafnyOptions.O.VerifySnapshots = 2; // Use caching

         DafnyOptions.O.VcsCores = Math.Max(1, System.Environment.ProcessorCount / 2); // Don't use too many cores

         DafnyOptions.O.PrintTooltips = true; // Dump tooptips (ErrorLevel.Info) to stdout

-        DafnyOptions.O.UnicodeOutput = true; // Use pretty warning signs

+        //DafnyOptions.O.UnicodeOutput = true; // Use pretty warning signs

         DafnyOptions.O.TraceProofObligations = true; // Show which method is being verified, but don't show duration of verification

       } else {

         throw new ServerException("Invalid command line options");

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(==)>