From 91cee1c2028f9ad995df863f2a4568d95f4ea1a8 Mon Sep 17 00:00:00 2001
From: qunyanm <unknown>
Date: Mon, 28 Mar 2016 12:02:37 -0700
Subject: 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.

---
 Test/dafny0/Basics.dfy            | 2 +-
 Test/dafny0/Calculations.dfy      | 2 +-
 Test/dafny0/Compilation.dfy       | 2 +-
 Test/dafny0/ForallCompilation.dfy | 2 +-
 Test/dafny0/Fuel.dfy              | 2 +-
 Test/dafny0/LetExpr.dfy           | 2 +-
 Test/dafny0/LetExpr.dfy.expect    | 1 +
 Test/dafny0/LhsDuplicates.dfy     | 2 +-
 Test/dafny0/Parallel.dfy          | 2 +-
 Test/dafny0/SmallTests.dfy.expect | 1 +
 10 files changed, 10 insertions(+), 8 deletions(-)

(limited to 'Test/dafny0')

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