Add /autoTriggers to TriggerInPredicate's RUN specification

3 files changed, 9 insertions, 5 deletions

diff --git a/Test/new-tests/trigger-in-predicate.dfy b/Test/dafny0/TriggerInPredicate.dfy
index 880d3d1d..3f2eac2c 100644
--- a/Test/new-tests/trigger-in-predicate.dfy
+++ b/Test/dafny0/TriggerInPredicate.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"

 // RUN: %diff "%s.expect" "%t"

 

 predicate A(x: bool, y: bool) { x }

@@ -13,3 +13,7 @@ method C'() requires B(true, true) {}
 

 // Inlining should work fine here

 method C''() requires B(true, true && false) {}

+

+// Local Variables:

+// dafny-prover-local-args: ("/autoTriggers:1")

+// End:

diff --git a/Test/dafny0/TriggerInPredicate.dfy.expect b/Test/dafny0/TriggerInPredicate.dfy.expect
new file mode 100644
index 00000000..47b3bdf9
--- /dev/null
+++ b/Test/dafny0/TriggerInPredicate.dfy.expect
@@ -0,0 +1,4 @@
+TriggerInPredicate.dfy(9,20): Info: This call cannot be safely inlined.

+TriggerInPredicate.dfy(9,20): Info: This call cannot be safely inlined.

+

+Dafny program verifier finished with 8 verified, 0 errors

diff --git a/Test/new-tests/trigger-in-predicate.dfy.expect b/Test/new-tests/trigger-in-predicate.dfy.expect
deleted file mode 100644
index 211bc9a2..00000000
--- a/Test/new-tests/trigger-in-predicate.dfy.expect
+++ /dev/null
@@ -1,4 +0,0 @@
-c:/MSR/dafny-triggers/Test/new-tests/trigger-in-predicate.dfy(9,21): Info: This call cannot be safely inlined.

-c:/MSR/dafny-triggers/Test/new-tests/trigger-in-predicate.dfy(9,21): Info: This call cannot be safely inlined.

-

-Dafny program verifier finished with 8 verified, 0 errors