From 19c70cd0d7a65c46bcaafa66b13bde43316bc081 Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel <clement.pitclaudel@live.com>
Date: Wed, 19 Aug 2015 22:16:02 -0700
Subject: Add tests for quantifier splitting and trigger generation

---
 Test/triggers/function-applications-are-triggers.dfy.expect | 2 ++
 1 file changed, 2 insertions(+)
 create mode 100644 Test/triggers/function-applications-are-triggers.dfy.expect

(limited to 'Test/triggers/function-applications-are-triggers.dfy.expect')

diff --git a/Test/triggers/function-applications-are-triggers.dfy.expect b/Test/triggers/function-applications-are-triggers.dfy.expect
new file mode 100644
index 00000000..069e7767
--- /dev/null
+++ b/Test/triggers/function-applications-are-triggers.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 2 verified, 0 errors
-- 
cgit v1.2.3


From af6f23ba1869c0450c44e917becc48263b565327 Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel <clement.pitclaudel@live.com>
Date: Fri, 21 Aug 2015 09:39:49 -0700
Subject: Add /printTooltips to trigger tests

---
 .../function-applications-are-triggers.dfy         |  2 +-
 .../function-applications-are-triggers.dfy.expect  | 11 ++++++++
 .../large-quantifiers-dont-break-dafny.dfy         |  2 +-
 .../large-quantifiers-dont-break-dafny.dfy.expect  |  2 ++
 Test/triggers/loop-detection-is-not-too-strict.dfy |  2 +-
 .../loop-detection-is-not-too-strict.dfy.expect    |  4 +++
 .../loop-detection-messages--unit-tests.dfy        |  2 +-
 .../loop-detection-messages--unit-tests.dfy.expect | 24 ++++++++++++++++++
 .../nested-quantifiers-all-get-triggers.dfy        |  2 +-
 .../nested-quantifiers-all-get-triggers.dfy.expect |  2 ++
 ...ms-do-not-look-like-the-triggers-they-match.dfy |  2 +-
 .../splitting-triggers-recovers-expressivity.dfy   |  2 +-
 ...tting-triggers-recovers-expressivity.dfy.expect | 29 ++++++++++++++++++++++
 ...s-yields-better-precondition-related-errors.dfy |  2 +-
 Test/triggers/triggers-prevent-some-inlining.dfy   |  2 +-
 .../triggers-prevent-some-inlining.dfy.expect      |  5 ++++
 Test/triggers/useless-triggers-are-removed.dfy     |  2 +-
 17 files changed, 87 insertions(+), 10 deletions(-)

(limited to 'Test/triggers/function-applications-are-triggers.dfy.expect')

diff --git a/Test/triggers/function-applications-are-triggers.dfy b/Test/triggers/function-applications-are-triggers.dfy
index 67ffe4e4..0aad9018 100644
--- a/Test/triggers/function-applications-are-triggers.dfy
+++ b/Test/triggers/function-applications-are-triggers.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // This file checks that function applications yield trigger candidates
diff --git a/Test/triggers/function-applications-are-triggers.dfy.expect b/Test/triggers/function-applications-are-triggers.dfy.expect
index 069e7767..7922e88d 100644
--- a/Test/triggers/function-applications-are-triggers.dfy.expect
+++ b/Test/triggers/function-applications-are-triggers.dfy.expect
@@ -1,2 +1,13 @@
+function-applications-are-triggers.dfy(9,9): Info: Selected triggers: {P.requires(f)}
+function-applications-are-triggers.dfy(10,9): Info: For expression {P(f) ==> f.requires(10)}:
+   Selected triggers:
+     {f(10)}, {f.requires(10)}, {P(f)}
+function-applications-are-triggers.dfy(10,9): Info: For expression {P(f) ==> f(10) == 0}:
+   Selected triggers:
+     {f(10)}, {f.requires(10)}, {P(f)}
+function-applications-are-triggers.dfy(11,9): Info: Selected triggers:
+   {f(10)}, {f.requires(10)}
+function-applications-are-triggers.dfy(12,5): Info: Selected triggers:
+   {g(x), f(x)}, {g(x), f.requires(x)}, {g(x)}, {f(x)}, {g.requires(x), f.requires(x)}, {g.requires(x)}, {f.requires(x)}
 
 Dafny program verifier finished with 2 verified, 0 errors
diff --git a/Test/triggers/large-quantifiers-dont-break-dafny.dfy b/Test/triggers/large-quantifiers-dont-break-dafny.dfy
index 8becae97..58eb56e1 100644
--- a/Test/triggers/large-quantifiers-dont-break-dafny.dfy
+++ b/Test/triggers/large-quantifiers-dont-break-dafny.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // This test ensures that the trigger  collector (the routine that picks trigger
diff --git a/Test/triggers/large-quantifiers-dont-break-dafny.dfy.expect b/Test/triggers/large-quantifiers-dont-break-dafny.dfy.expect
index c90560b0..5e7c14b9 100644
--- a/Test/triggers/large-quantifiers-dont-break-dafny.dfy.expect
+++ b/Test/triggers/large-quantifiers-dont-break-dafny.dfy.expect
@@ -1,2 +1,4 @@
+large-quantifiers-dont-break-dafny.dfy(60,9): Info: Selected triggers:
+   {P49(x)}, {P48(x)}, {P47(x)}, {P46(x)}, {P45(x)}, {P44(x)}, {P43(x)}, {P42(x)}, {P41(x)}, {P40(x)}, {P39(x)}, {P38(x)}, {P37(x)}, {P36(x)}, {P35(x)}, {P34(x)}, {P33(x)}, {P32(x)}, {P31(x)}, {P30(x)}, {P29(x)}, {P28(x)}, {P27(x)}, {P26(x)}, {P25(x)}, {P24(x)}, {P23(x)}, {P22(x)}, {P21(x)}, {P20(x)}, {P19(x)}, {P18(x)}, {P17(x)}, {P16(x)}, {P15(x)}, {P14(x)}, {P13(x)}, {P12(x)}, {P11(x)}, {P10(x)}, {P9(x)}, {P8(x)}, {P7(x)}, {P6(x)}, {P5(x)}, {P4(x)}, {P3(x)}, {P2(x)}, {P1(x)}, {P0(x)}
 
 Dafny program verifier finished with 52 verified, 0 errors
diff --git a/Test/triggers/loop-detection-is-not-too-strict.dfy b/Test/triggers/loop-detection-is-not-too-strict.dfy
index c6722399..a5a30c81 100644
--- a/Test/triggers/loop-detection-is-not-too-strict.dfy
+++ b/Test/triggers/loop-detection-is-not-too-strict.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // This test shows that the loop detection engine makes compromises when looking
diff --git a/Test/triggers/loop-detection-is-not-too-strict.dfy.expect b/Test/triggers/loop-detection-is-not-too-strict.dfy.expect
index 29882da7..270f7e57 100644
--- a/Test/triggers/loop-detection-is-not-too-strict.dfy.expect
+++ b/Test/triggers/loop-detection-is-not-too-strict.dfy.expect
@@ -1,3 +1,7 @@
+loop-detection-is-not-too-strict.dfy(14,9): Info: Selected triggers:
+   {P(y, x)}, {P(x, y)}
+loop-detection-is-not-too-strict.dfy(17,9): Info: Selected triggers:
+   {P(y, x)}, {P(x, y)}
 loop-detection-is-not-too-strict.dfy(20,9): Warning: Selected triggers: {P(x, y)} (loops with {P(x, y + 1)})
  (!) Suppressing loops would leave this expression without triggers.
 
diff --git a/Test/triggers/loop-detection-messages--unit-tests.dfy b/Test/triggers/loop-detection-messages--unit-tests.dfy
index d5439e09..c1560317 100644
--- a/Test/triggers/loop-detection-messages--unit-tests.dfy
+++ b/Test/triggers/loop-detection-messages--unit-tests.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // This file is a series of basic tests for loop detection, focusing on the
diff --git a/Test/triggers/loop-detection-messages--unit-tests.dfy.expect b/Test/triggers/loop-detection-messages--unit-tests.dfy.expect
index 1ebc0bce..89d7265c 100644
--- a/Test/triggers/loop-detection-messages--unit-tests.dfy.expect
+++ b/Test/triggers/loop-detection-messages--unit-tests.dfy.expect
@@ -1,13 +1,37 @@
+loop-detection-messages--unit-tests.dfy(11,9): Info: Selected triggers: {f(f(i))}
+ Rejected triggers: {f(i)} (loops with {f(f(i))})
 loop-detection-messages--unit-tests.dfy(12,9): Warning: Selected triggers: {f(i)} (loops with {f(i + 1)})
  (!) Suppressing loops would leave this expression without triggers.
+loop-detection-messages--unit-tests.dfy(13,9): Info: Selected triggers: {f(i)} (loops with {f(i + 1)})
+loop-detection-messages--unit-tests.dfy(15,9): Info: For expression {false ==> f(i) == f(i + 1)}:
+   Selected triggers: {g(i)}
+   Rejected triggers: {f(i)} (loops with {f(i + 1)})
+loop-detection-messages--unit-tests.dfy(15,9): Info: For expression {false ==> f(i) == g(i)}:
+   Selected triggers:
+     {g(i)}, {f(i)}
 loop-detection-messages--unit-tests.dfy(16,9): Warning: For expression {false ==> f(i) == f(i + 1)}:
    Selected triggers: {f(i)} (loops with {f(i + 1)})
    (!) Suppressing loops would leave this expression without triggers.
+loop-detection-messages--unit-tests.dfy(16,9): Info: For expression {false ==> f(i) == f(i)}:
+   Selected triggers: {f(i)}
+loop-detection-messages--unit-tests.dfy(17,9): Info: For expression {false ==> f(i) == f(i + 1)}:
+   Selected triggers: {f(i)} (loops with {f(i + 1)})
+loop-detection-messages--unit-tests.dfy(17,9): Info: For expression {false ==> f(i) == f(i)}:
+   Selected triggers: {f(i)}
+loop-detection-messages--unit-tests.dfy(19,9): Info: Selected triggers: {f(i)}
 loop-detection-messages--unit-tests.dfy(20,9): Warning: (!) No terms found to trigger on.
+loop-detection-messages--unit-tests.dfy(21,9): Info: Not generating triggers for {false ==> f(i + 1) == 0}.
+loop-detection-messages--unit-tests.dfy(23,9): Info: Selected triggers: {f(j), f(i)}
 loop-detection-messages--unit-tests.dfy(24,9): Warning: (!) No trigger covering all quantified variables found.
+loop-detection-messages--unit-tests.dfy(25,9): Info: For expression {false ==> f(i) == f(i)}:
+   Selected triggers: {g(j), f(i)}
+loop-detection-messages--unit-tests.dfy(25,9): Info: For expression {false ==> g(j) == 0}:
+   Selected triggers: {g(j), f(i)}
 loop-detection-messages--unit-tests.dfy(26,9): Warning: For expression {false ==> f(i) == f(i)}:
    (!) No trigger covering all quantified variables found.
 loop-detection-messages--unit-tests.dfy(26,9): Warning: For expression {false ==> g(j + 1) == 0}:
    (!) No trigger covering all quantified variables found.
+loop-detection-messages--unit-tests.dfy(27,9): Info: Not generating triggers for {false ==> f(i) == f(i)}.
+loop-detection-messages--unit-tests.dfy(28,9): Info: Not generating triggers for {false ==> f(i) == f(i)}.
 
 Dafny program verifier finished with 4 verified, 0 errors
diff --git a/Test/triggers/nested-quantifiers-all-get-triggers.dfy b/Test/triggers/nested-quantifiers-all-get-triggers.dfy
index c75cfab9..a55019db 100644
--- a/Test/triggers/nested-quantifiers-all-get-triggers.dfy
+++ b/Test/triggers/nested-quantifiers-all-get-triggers.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // This checks that nested quantifiers do get triggers, and that the parent
diff --git a/Test/triggers/nested-quantifiers-all-get-triggers.dfy.expect b/Test/triggers/nested-quantifiers-all-get-triggers.dfy.expect
index 069e7767..172f5607 100644
--- a/Test/triggers/nested-quantifiers-all-get-triggers.dfy.expect
+++ b/Test/triggers/nested-quantifiers-all-get-triggers.dfy.expect
@@ -1,2 +1,4 @@
+nested-quantifiers-all-get-triggers.dfy(8,17): Info: Selected triggers: {x in s}
+nested-quantifiers-all-get-triggers.dfy(8,59): Info: Selected triggers: {y in s}
 
 Dafny program verifier finished with 2 verified, 0 errors
diff --git a/Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy b/Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy
index 7423e086..d7636ea2 100644
--- a/Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy
+++ b/Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // This file shows how Dafny detects loops even for terms that are not literal
diff --git a/Test/triggers/splitting-triggers-recovers-expressivity.dfy b/Test/triggers/splitting-triggers-recovers-expressivity.dfy
index 79a0dc72..dd1bd81d 100644
--- a/Test/triggers/splitting-triggers-recovers-expressivity.dfy
+++ b/Test/triggers/splitting-triggers-recovers-expressivity.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 predicate P(i: int)
diff --git a/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect b/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect
index 8d7ff4ef..63cbc476 100644
--- a/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect
+++ b/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect
@@ -1,3 +1,32 @@
+splitting-triggers-recovers-expressivity.dfy(12,10): Info: Selected triggers: {Q(i)}
+ Rejected triggers: {P(i)} (loops with {P(i + 1)})
+splitting-triggers-recovers-expressivity.dfy(17,11): Info: Selected triggers: {Q(j)}
+ Rejected triggers: {P(j)} (loops with {P(j + 1)})
+splitting-triggers-recovers-expressivity.dfy(26,10): Info: Selected triggers: {Q(i)}
+ Rejected triggers: {P(i)} (loops with {P(i + 1)})
+splitting-triggers-recovers-expressivity.dfy(33,11): Info: Selected triggers: {Q(j)}
+ Rejected triggers: {P(j)} (loops with {P(j + 1)})
+splitting-triggers-recovers-expressivity.dfy(44,10): Info: For expression {P(i)}:
+   Selected triggers:
+     {Q(i)}, {P(i)}
+splitting-triggers-recovers-expressivity.dfy(44,10): Info: For expression {!Q(i)}:
+   Selected triggers:
+     {Q(i)}, {P(i)}
+splitting-triggers-recovers-expressivity.dfy(44,10): Info: For expression {P(i + 1)}:
+   Selected triggers: {Q(i)}
+   Rejected triggers: {P(i)} (loops with {P(i + 1)})
+splitting-triggers-recovers-expressivity.dfy(49,11): Info: For expression {j >= 0 ==> P(j)}:
+   Selected triggers:
+     {Q(j)}, {P(j)}
+splitting-triggers-recovers-expressivity.dfy(49,11): Info: For expression {j >= 0 ==> Q(j) ==> P(j + 1)}:
+   Selected triggers: {Q(j)}
+   Rejected triggers: {P(j)} (loops with {P(j + 1)})
+splitting-triggers-recovers-expressivity.dfy(58,11): Info: For expression {i >= 0 ==> Q(i)}:
+   Selected triggers:
+     {P(i)}, {Q(i)}
+splitting-triggers-recovers-expressivity.dfy(58,11): Info: For expression {i >= 0 ==> P(i) ==> P(i + 1)}:
+   Selected triggers:
+     {P(i)} (loops with {P(i + 1)}), {Q(i)}
 splitting-triggers-recovers-expressivity.dfy(12,63): Error BP5003: A postcondition might not hold on this return path.
 splitting-triggers-recovers-expressivity.dfy(12,10): Related location: This is the postcondition that might not hold.
 Execution trace:
diff --git a/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy b/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy
index f25a624e..20e90843 100644
--- a/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy
+++ b/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // This tests shows that, since quantifiers are split, it becomes possible to know more precisely what part of a precondition did not hold at the call site.
diff --git a/Test/triggers/triggers-prevent-some-inlining.dfy b/Test/triggers/triggers-prevent-some-inlining.dfy
index 04b8051c..90af62a3 100644
--- a/Test/triggers/triggers-prevent-some-inlining.dfy
+++ b/Test/triggers/triggers-prevent-some-inlining.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // This  file looks  at the  interactions  between inlining  and triggers.   The
diff --git a/Test/triggers/triggers-prevent-some-inlining.dfy.expect b/Test/triggers/triggers-prevent-some-inlining.dfy.expect
index 73ba063c..4c24893e 100644
--- a/Test/triggers/triggers-prevent-some-inlining.dfy.expect
+++ b/Test/triggers/triggers-prevent-some-inlining.dfy.expect
@@ -1,2 +1,7 @@
+triggers-prevent-some-inlining.dfy(17,2): Info: Selected triggers: {sum(a, b)}
+triggers-prevent-some-inlining.dfy(24,10): Info: Some instances of this call cannot safely be inlined.
+triggers-prevent-some-inlining.dfy(25,10): Info: Some instances of this call cannot safely be inlined.
+triggers-prevent-some-inlining.dfy(24,10): Info: Some instances of this call cannot safely be inlined.
+triggers-prevent-some-inlining.dfy(25,10): Info: Some instances of this call cannot safely be inlined.
 
 Dafny program verifier finished with 4 verified, 0 errors
diff --git a/Test/triggers/useless-triggers-are-removed.dfy b/Test/triggers/useless-triggers-are-removed.dfy
index 16458e41..658890f2 100644
--- a/Test/triggers/useless-triggers-are-removed.dfy
+++ b/Test/triggers/useless-triggers-are-removed.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /printTooltips /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // This file ensures that Dafny does get rid of redundant triggers before
-- 
cgit v1.2.3


From c55cb226f4de90b080aa809d883d52c3386db063 Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel <clement.pitclaudel@live.com>
Date: Wed, 26 Aug 2015 18:36:34 -0700
Subject: Improve the redundancy detection algorithm used while constructing
 sets of terms

Based on an issue noted by Chris with redundancy removal resuls being dependent
on the order of the terms. Interestingly, one of our tests already had an
instance of that problem.

Also fix the issue with nested quantifiers getting redundant triggers.
---
 Source/Dafny/DafnyAst.cs                           |   1 +
 Source/Dafny/Triggers/QuantifiersCollection.cs     |  17 ++--
 Source/Dafny/Triggers/TriggerUtils.cs              | 100 ++++++++++++++++++---
 Source/Dafny/Triggers/TriggersCollector.cs         |   5 ++
 .../function-applications-are-triggers.dfy.expect  |   2 +-
 .../redundancy-detection-is-bidirectional.dfy      |  29 ++++++
 ...edundancy-detection-is-bidirectional.dfy.expect |  12 +++
 7 files changed, 143 insertions(+), 23 deletions(-)
 create mode 100644 Test/triggers/redundancy-detection-is-bidirectional.dfy
 create mode 100644 Test/triggers/redundancy-detection-is-bidirectional.dfy.expect

(limited to 'Test/triggers/function-applications-are-triggers.dfy.expect')

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index c7aae173..9bff2038 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -2965,6 +2965,7 @@ namespace Microsoft.Dafny {
     }
   }
 
+  [DebuggerDisplay("Bound<{name}>")]
   public class BoundVar : NonglobalVariable {
     public override bool IsMutable {
       get {
diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs
index 6555b52a..114d5f5d 100644
--- a/Source/Dafny/Triggers/QuantifiersCollection.cs
+++ b/Source/Dafny/Triggers/QuantifiersCollection.cs
@@ -47,15 +47,9 @@ namespace Microsoft.Dafny.Triggers {
       SelectTriggers();
     }
     
-    private bool SubsetGenerationPredicate(List<TriggerTerm> terms, TriggerTerm additionalTerm) {
-      // Simple formulas like [P0(i) && P1(i) && P2(i) && P3(i) && P4(i)] yield very
-      // large numbers of multi-triggers, most of which are useless. This filter
-      // restricts subsets of terms so that we only generate sets of terms where each
-      // element contributes at least one variable. In the example above, we'll only
-      // get 5 triggers.
-      // Note that this may still be an over-approximation, as in the following example:
-      // forall a, b :: forall x :: a[x] || b[x] > 0.
-      return additionalTerm.Variables.Where(v => v is BoundVar && !terms.Any(t => t.Variables.Contains(v))).Any();
+    private bool SubsetGenerationPredicate(TriggerUtils.SetOfTerms terms, TriggerTerm additionalTerm) {
+      return true; // FIXME Remove this
+      //return additionalTerm.Variables.Where(v => v is BoundVar && !terms.Any(t => t.Variables.Contains(v))).Any();
     }
 
     /// <summary>
@@ -68,11 +62,10 @@ namespace Microsoft.Dafny.Triggers {
     void CollectAndShareTriggers(TriggersCollector triggersCollector) {
       var pool = quantifiers.SelectMany(q => triggersCollector.CollectTriggers(q.quantifier));
       var distinctPool = pool.Deduplicate(TriggerTerm.Eq);
-      var multiPool = TriggerUtils.AllNonEmptySubsets(distinctPool, SubsetGenerationPredicate).Select(candidates => new TriggerCandidate(candidates)).ToList();
 
       foreach (var q in quantifiers) {
-        q.CandidateTerms = distinctPool; //Candidate terms are immutable: no copy needed
-        q.Candidates = multiPool.Select(candidate => new TriggerCandidate(candidate)).ToList();
+        q.CandidateTerms = distinctPool; // The list of candidate terms is immutable
+        q.Candidates = TriggerUtils.AllNonEmptySubsets(distinctPool, SubsetGenerationPredicate, q.quantifier.BoundVars).Select(set => set.ToTriggerCandidate()).ToList();
       }
     }
 
diff --git a/Source/Dafny/Triggers/TriggerUtils.cs b/Source/Dafny/Triggers/TriggerUtils.cs
index 4fd139e2..efa1f167 100644
--- a/Source/Dafny/Triggers/TriggerUtils.cs
+++ b/Source/Dafny/Triggers/TriggerUtils.cs
@@ -15,29 +15,109 @@ namespace Microsoft.Dafny.Triggers {
       return copy;
     }
 
-    internal static IEnumerable<List<T>> AllSubsets<T>(IList<T> source, Func<List<T>, T, bool> predicate, int offset) {
+    internal class SetOfTerms {
+      internal bool IsRedundant { get; private set; }
+      internal List<TriggerTerm> Terms { get; set; }
+
+      private ISet<BoundVar> variables;
+      private Dictionary<BoundVar, TriggerTerm> termOwningAUniqueVar;
+      private Dictionary<TriggerTerm, ISet<BoundVar>> uniqueVarsOwnedByATerm;
+
+      public int Count { get { return Terms.Count; } }
+
+      private SetOfTerms() { }
+
+      internal TriggerCandidate ToTriggerCandidate() {
+        return new TriggerCandidate(Terms);
+      }
+      
+      internal static SetOfTerms Empty() {
+        var newSet = new SetOfTerms();
+        newSet.IsRedundant = false;
+        newSet.Terms = new List<TriggerTerm>();
+        newSet.variables = new HashSet<BoundVar>();
+        newSet.termOwningAUniqueVar = new Dictionary<BoundVar, TriggerTerm>();
+        newSet.uniqueVarsOwnedByATerm = new Dictionary<TriggerTerm, ISet<BoundVar>>();
+        return newSet;
+      }
+
+      /// <summary>
+      /// Simple formulas like [P0(i) && P1(i) && P2(i) && P3(i) && P4(i)] yield very
+      /// large numbers of multi-triggers, most of which are useless. As it copies its
+      /// argument, this method updates various datastructures that allow it to
+      /// efficiently track ownership relations between formulae and bound variables,
+      /// and sets the IsRedundant flag of the returned set, allowing the caller to
+      /// discard that set of terms, and the ones that would have been built on top of
+      /// it, thus ensuring that the only sets of terms produced in the end are sets
+      /// of terms in which each element contributes (owns) at least one variable.
+      ///
+      /// Note that this is trickier than just checking every term for new variables;
+      /// indeed, a new term that does bring new variables in can make an existing
+      /// term redundant (see redundancy-detection-does-its-job-properly.dfy).
+      /// </summary>
+      internal SetOfTerms CopyWithAdd(TriggerTerm term, ISet<BoundVar> relevantVariables) {
+        var copy = new SetOfTerms();
+        copy.Terms = new List<TriggerTerm>(Terms);
+        copy.variables = new HashSet<BoundVar>(variables);
+        copy.termOwningAUniqueVar = new Dictionary<BoundVar, TriggerTerm>(termOwningAUniqueVar);
+        copy.uniqueVarsOwnedByATerm = new Dictionary<TriggerTerm, ISet<BoundVar>>(uniqueVarsOwnedByATerm);
+
+        copy.Terms.Add(term);
+
+        var varsInNewTerm = new HashSet<BoundVar>(term.BoundVars);
+        varsInNewTerm.IntersectWith(relevantVariables);
+
+        var ownedByNewTerm = new HashSet<BoundVar>();
+
+        // Check #0: does this term bring anything new?
+        copy.IsRedundant = IsRedundant || varsInNewTerm.All(bv => copy.variables.Contains(bv));
+        copy.variables.UnionWith(varsInNewTerm);
+        
+        // Check #1: does this term claiming ownership of all its variables cause another term to become useless?
+        foreach (var v in varsInNewTerm) {
+          TriggerTerm originalOwner;
+          if (copy.termOwningAUniqueVar.TryGetValue(v, out originalOwner)) {
+            var alsoOwnedByOriginalOwner = copy.uniqueVarsOwnedByATerm[originalOwner];
+            alsoOwnedByOriginalOwner.Remove(v);
+            if (!alsoOwnedByOriginalOwner.Any()) {
+              copy.IsRedundant = true;
+            }
+          } else {
+            ownedByNewTerm.Add(v);
+            copy.termOwningAUniqueVar[v] = term;
+          }
+        }
+
+        // Actually claim ownership
+        copy.uniqueVarsOwnedByATerm[term] = ownedByNewTerm;
+
+        return copy;
+      }
+    }
+
+    internal static IEnumerable<SetOfTerms> AllSubsets(IList<TriggerTerm> source, Func<SetOfTerms, TriggerTerm, bool> predicate, int offset, ISet<BoundVar> relevantVariables) {
       if (offset >= source.Count) {
-        yield return new List<T>();
+        yield return SetOfTerms.Empty();
         yield break;
       }
 
-      foreach (var subset in AllSubsets<T>(source, predicate, offset + 1)) {
-        if (predicate(subset, source[offset])) {
-          yield return CopyAndAdd(subset, source[offset]);
+      foreach (var subset in AllSubsets(source, predicate, offset + 1, relevantVariables)) {
+        var newSet = subset.CopyWithAdd(source[offset], relevantVariables);
+        if (!newSet.IsRedundant && predicate(subset, source[offset])) { // Fixme remove the predicate?
+          yield return newSet;
         }
-        yield return new List<T>(subset);
+        yield return subset;
       }
     }
 
-    internal static IEnumerable<List<T>> AllNonEmptySubsets<T>(IEnumerable<T> source, Func<List<T>, T, bool> predicate) {
-      List<T> all = new List<T>(source);
-      foreach (var subset in AllSubsets(all, predicate, 0)) {
+    internal static IEnumerable<SetOfTerms> AllNonEmptySubsets(IList<TriggerTerm> source, Func<SetOfTerms, TriggerTerm, bool> predicate, IEnumerable<BoundVar> relevantVariables) {
+      foreach (var subset in AllSubsets(source, predicate, 0, new HashSet<BoundVar>(relevantVariables))) {
         if (subset.Count > 0) {
           yield return subset;
         }
       }
     }
-
+    
     internal static List<T> MergeAlterFirst<T>(List<T> a, List<T> b) {
       Contract.Requires(a != null);
       Contract.Requires(b != null);
diff --git a/Source/Dafny/Triggers/TriggersCollector.cs b/Source/Dafny/Triggers/TriggersCollector.cs
index 69c47d90..d78bcb9e 100644
--- a/Source/Dafny/Triggers/TriggersCollector.cs
+++ b/Source/Dafny/Triggers/TriggersCollector.cs
@@ -11,6 +11,11 @@ namespace Microsoft.Dafny.Triggers {
     internal Expression Expr { get; set; }
     internal Expression OriginalExpr { get; set; }
     internal ISet<IVariable> Variables { get; set; }
+    internal IEnumerable<BoundVar> BoundVars {
+      get {
+        return Variables.Select(v => v as BoundVar).Where(v => v != null);
+      }
+    }
 
     public override string ToString() {
       return Printer.ExprToString(Expr); 
diff --git a/Test/triggers/function-applications-are-triggers.dfy.expect b/Test/triggers/function-applications-are-triggers.dfy.expect
index 7922e88d..501cfa51 100644
--- a/Test/triggers/function-applications-are-triggers.dfy.expect
+++ b/Test/triggers/function-applications-are-triggers.dfy.expect
@@ -8,6 +8,6 @@ function-applications-are-triggers.dfy(10,9): Info: For expression {P(f) ==> f(1
 function-applications-are-triggers.dfy(11,9): Info: Selected triggers:
    {f(10)}, {f.requires(10)}
 function-applications-are-triggers.dfy(12,5): Info: Selected triggers:
-   {g(x), f(x)}, {g(x), f.requires(x)}, {g(x)}, {f(x)}, {g.requires(x), f.requires(x)}, {g.requires(x)}, {f.requires(x)}
+   {g(x)}, {f(x)}, {g.requires(x)}, {f.requires(x)}
 
 Dafny program verifier finished with 2 verified, 0 errors
diff --git a/Test/triggers/redundancy-detection-is-bidirectional.dfy b/Test/triggers/redundancy-detection-is-bidirectional.dfy
new file mode 100644
index 00000000..df1d78c3
--- /dev/null
+++ b/Test/triggers/redundancy-detection-is-bidirectional.dfy
@@ -0,0 +1,29 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// This tests checks for tricky cases of redundancy suppression when building
+// triggers.
+
+predicate P(x: int, y: int)
+predicate Q(x: int)
+predicate R(x: int)
+
+method M() {
+  // For this term, it is enough to order the terms by number of variables
+  assert forall x, y :: true || P(x, y) || Q(y) || R(x);
+  assert forall x, y :: true || Q(y) || P(x, y) || R(x);
+  assert forall x, y :: true || Q(y) || R(x) || P(x, y);
+}
+
+predicate PP(x: int, y: int, z: int)
+predicate QQ(x: int, y: int)
+predicate RR(x: int, y: int)
+predicate SS(x: int, y: int)
+
+method MM() {
+  // Not for this one, though
+  assert forall x, y, z, u, v, w :: true || PP(x, y, z) || QQ(x, u) || RR(y, v) || SS(z, w);
+  assert forall x, y, z, u, v, w :: true || QQ(x, u) || PP(x, y, z) || RR(y, v) || SS(z, w);
+  assert forall x, y, z, u, v, w :: true || QQ(x, u) || RR(y, v) || PP(x, y, z) || SS(z, w);
+  assert forall x, y, z, u, v, w :: true || QQ(x, u) || RR(y, v) || SS(z, w) || PP(x, y, z);
+}
diff --git a/Test/triggers/redundancy-detection-is-bidirectional.dfy.expect b/Test/triggers/redundancy-detection-is-bidirectional.dfy.expect
new file mode 100644
index 00000000..78c9e7ca
--- /dev/null
+++ b/Test/triggers/redundancy-detection-is-bidirectional.dfy.expect
@@ -0,0 +1,12 @@
+redundancy-detection-is-bidirectional.dfy(13,9): Info: Selected triggers:
+   {R(x), Q(y)}, {P(x, y)}
+redundancy-detection-is-bidirectional.dfy(14,9): Info: Selected triggers:
+   {R(x), Q(y)}, {P(x, y)}
+redundancy-detection-is-bidirectional.dfy(15,9): Info: Selected triggers:
+   {P(x, y)}, {R(x), Q(y)}
+redundancy-detection-is-bidirectional.dfy(25,9): Info: Selected triggers: {SS(z, w), RR(y, v), QQ(x, u)}
+redundancy-detection-is-bidirectional.dfy(26,9): Info: Selected triggers: {SS(z, w), RR(y, v), QQ(x, u)}
+redundancy-detection-is-bidirectional.dfy(27,9): Info: Selected triggers: {SS(z, w), RR(y, v), QQ(x, u)}
+redundancy-detection-is-bidirectional.dfy(28,9): Info: Selected triggers: {SS(z, w), RR(y, v), QQ(x, u)}
+
+Dafny program verifier finished with 11 verified, 0 errors
-- 
cgit v1.2.3


From 2db858bf6e72e521b49aa0ae3a993dc943b8c875 Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel <clement.pitclaudel@live.com>
Date: Fri, 28 Aug 2015 20:39:02 -0700
Subject: Implement {:nowarn}, clarify some messages, and add a few tests

---
 Source/Dafny/Triggers/QuantifiersCollection.cs     | 26 +++++++----
 Source/Dafny/Triggers/TriggerUtils.cs              | 11 +++--
 .../triggers/constructors-cause-matching-loops.dfy | 11 +++++
 .../constructors-cause-matching-loops.dfy.expect   |  6 +++
 .../function-applications-are-triggers.dfy.expect  |  4 +-
 .../loop-detection-is-not-too-strict.dfy.expect    |  8 ++--
 .../loop-detection-looks-at-ranges-too.dfy.expect  |  8 ++--
 .../loop-detection-messages--unit-tests.dfy.expect | 50 +++++++++++-----------
 ...ng-is-hard-to-decide-modulo-equality.dfy.expect |  4 +-
 .../matrix-accesses-are-triggers.dfy.expect        |  4 +-
 .../old-is-a-special-case-for-triggers.dfy.expect  | 10 ++---
 Test/triggers/regression-tests.dfy.expect          |  2 +-
 .../some-proofs-only-work-without-autoTriggers.dfy | 48 +++++++++++++++++++++
 ...roofs-only-work-without-autoTriggers.dfy.expect | 31 ++++++++++++++
 ...ot-look-like-the-triggers-they-match.dfy.expect | 16 +++----
 .../splitting-picks-the-right-tokens.dfy.expect    | 12 +++---
 ...tting-triggers-recovers-expressivity.dfy.expect | 28 ++++++------
 ...s-better-precondition-related-errors.dfy.expect | 16 +++----
 .../suppressing-warnings-behaves-properly.dfy      | 21 +++++++++
 ...uppressing-warnings-behaves-properly.dfy.expect | 14 ++++++
 .../useless-triggers-are-removed.dfy.expect        |  4 +-
 ...f-checks-use-the-original-quantifier.dfy.expect | 10 ++---
 22 files changed, 244 insertions(+), 100 deletions(-)
 create mode 100644 Test/triggers/constructors-cause-matching-loops.dfy
 create mode 100644 Test/triggers/constructors-cause-matching-loops.dfy.expect
 create mode 100644 Test/triggers/some-proofs-only-work-without-autoTriggers.dfy
 create mode 100644 Test/triggers/some-proofs-only-work-without-autoTriggers.dfy.expect
 create mode 100644 Test/triggers/suppressing-warnings-behaves-properly.dfy
 create mode 100644 Test/triggers/suppressing-warnings-behaves-properly.dfy.expect

(limited to 'Test/triggers/function-applications-are-triggers.dfy.expect')

diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs
index 50458ab7..f72dab7f 100644
--- a/Source/Dafny/Triggers/QuantifiersCollection.cs
+++ b/Source/Dafny/Triggers/QuantifiersCollection.cs
@@ -117,7 +117,7 @@ namespace Microsoft.Dafny.Triggers {
           (candidate, loopingSubterms) => !loopingSubterms.Any(),
           (candidate, loopingSubterms) => {
             looping.Add(candidate);
-            candidate.Annotation = "may loop with " + loopingSubterms.MapConcat(t => "{" + Printer.ExprToString(t.OriginalExpr) + "}", ", ");
+            candidate.Annotation = "may loop with " + loopingSubterms.MapConcat(t => "\"" + Printer.ExprToString(t.OriginalExpr) + "\"", ", ");
           }).ToList();
 
         q.CouldSuppressLoops = safe.Count > 0;
@@ -145,12 +145,14 @@ namespace Microsoft.Dafny.Triggers {
       var errorLevel = ErrorLevel.Info;
       var msg = new StringBuilder();
       var indent = addHeader ? "  " : "";
+      bool suppressWarnings = Attributes.Contains(q.quantifier.Attributes, "nowarn");
 
-      if (!TriggerUtils.NeedsAutoTriggers(q.quantifier)) { // NOTE: matchingloop, split and autotriggers attributes are passed down to Boogie
-        msg.AppendFormat("Not generating triggers for {{{0}}}.", Printer.ExprToString(q.quantifier.Term)).AppendLine(); 
+      if (!TriggerUtils.NeedsAutoTriggers(q.quantifier)) { // NOTE: split and autotriggers attributes are passed down to Boogie
+        var extraMsg = TriggerUtils.WantsAutoTriggers(q.quantifier) ? "" : " Note that {:autotriggers false} can cause instabilities. Consider using {:nowarn}, {:matchingloop} (not great either), or a manual trigger instead.";
+        msg.AppendFormat("Not generating triggers for \"{0}\".{1}", Printer.ExprToString(q.quantifier.Term), extraMsg).AppendLine(); 
       } else {
         if (addHeader) {
-          msg.AppendFormat("For expression {{{0}}}:", Printer.ExprToString(q.quantifier.Term)).AppendLine();
+          msg.AppendFormat("For expression \"{0}\":", Printer.ExprToString(q.quantifier.Term)).AppendLine();
         }
 
         foreach (var candidate in q.Candidates) {
@@ -161,20 +163,26 @@ namespace Microsoft.Dafny.Triggers {
         AddTriggersToMessage("Rejected triggers:", q.RejectedCandidates, msg, indent, true);
 
 #if QUANTIFIER_WARNINGS
-        string WARN = indent + (DafnyOptions.O.UnicodeOutput ? "⚠ " : "(!) ");
+        var WARN_TAG = DafnyOptions.O.UnicodeOutput ? "⚠ " : "/!\\ ";
+        var WARN_TAG_OVERRIDE = suppressWarnings ? "(Suppressed warning) " : WARN_TAG;
+        var WARN_LEVEL = suppressWarnings ? ErrorLevel.Info : ErrorLevel.Warning;
+        var WARN = indent + WARN_TAG_OVERRIDE;
         if (!q.CandidateTerms.Any()) {
-          errorLevel = ErrorLevel.Warning;
+          errorLevel = WARN_LEVEL;
           msg.Append(WARN).AppendLine("No terms found to trigger on.");
         } else if (!q.Candidates.Any()) {
-          errorLevel = ErrorLevel.Warning;
+          errorLevel = WARN_LEVEL;
           msg.Append(WARN).AppendLine("No trigger covering all quantified variables found.");
         } else if (!q.CouldSuppressLoops && !q.AllowsLoops) {
-          errorLevel = ErrorLevel.Warning;
+          errorLevel = WARN_LEVEL;
           msg.Append(WARN).AppendLine("Suppressing loops would leave this expression without triggers.");
+        } else if (suppressWarnings) {
+          errorLevel = ErrorLevel.Warning;
+          msg.Append(indent).Append(WARN_TAG).AppendLine("There is no warning here to suppress.");
         }
 #endif
       }
-      
+
       if (msg.Length > 0) {
         var msgStr = msg.ToString().TrimEnd("\r\n ".ToCharArray());
         reporter.Message(MessageSource.Rewriter, errorLevel, q.quantifier.tok, msgStr);
diff --git a/Source/Dafny/Triggers/TriggerUtils.cs b/Source/Dafny/Triggers/TriggerUtils.cs
index efa1f167..c16a3e44 100644
--- a/Source/Dafny/Triggers/TriggerUtils.cs
+++ b/Source/Dafny/Triggers/TriggerUtils.cs
@@ -183,14 +183,19 @@ namespace Microsoft.Dafny.Triggers {
 
     internal static bool AllowsMatchingLoops(QuantifierExpr quantifier) {
       Contract.Requires(quantifier.SplitQuantifier == null); // Don't call this on a quantifier with a Split clause: it's not a real quantifier
+      // This is different from nowarn: it won't remove loops at all, even if another trigger is available.
       return Attributes.Contains(quantifier.Attributes, "matchingloop");
     }
 
-    internal static bool NeedsAutoTriggers(QuantifierExpr quantifier) {
+    internal static bool WantsAutoTriggers(QuantifierExpr quantifier) {
       Contract.Requires(quantifier.SplitQuantifier == null); // Don't call this on a quantifier with a Split clause: it's not a real quantifier
       bool wantsAutoTriggers = true;
-      return !Attributes.Contains(quantifier.Attributes, "trigger") && 
-        (!Attributes.ContainsBool(quantifier.Attributes, "autotriggers", ref wantsAutoTriggers) || wantsAutoTriggers);
+      return !Attributes.ContainsBool(quantifier.Attributes, "autotriggers", ref wantsAutoTriggers) || wantsAutoTriggers;
+    }
+
+    internal static bool NeedsAutoTriggers(QuantifierExpr quantifier) {
+      Contract.Requires(quantifier.SplitQuantifier == null); // Don't call this on a quantifier with a Split clause: it's not a real quantifier
+      return !Attributes.Contains(quantifier.Attributes, "trigger") && WantsAutoTriggers(quantifier);
     }
 
     internal static BinaryExpr.ResolvedOpcode RemoveNotInBinaryExprIn(BinaryExpr.ResolvedOpcode opcode) {
diff --git a/Test/triggers/constructors-cause-matching-loops.dfy b/Test/triggers/constructors-cause-matching-loops.dfy
new file mode 100644
index 00000000..61e6a66b
--- /dev/null
+++ b/Test/triggers/constructors-cause-matching-loops.dfy
@@ -0,0 +1,11 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// This file is just a small test to check that constructors do cause loops
+
+datatype Nat = Zero | Succ(x: Nat)
+function f(n: Nat): Nat
+
+method M() {
+  assert forall s :: true || f(Succ(s)) == f(s);
+}
diff --git a/Test/triggers/constructors-cause-matching-loops.dfy.expect b/Test/triggers/constructors-cause-matching-loops.dfy.expect
new file mode 100644
index 00000000..e7a671ab
--- /dev/null
+++ b/Test/triggers/constructors-cause-matching-loops.dfy.expect
@@ -0,0 +1,6 @@
+constructors-cause-matching-loops.dfy(10,9): Info: Selected triggers: {Succ(s)}
+ Rejected triggers:
+   {f(s)} (may loop with "f(Succ(s))")
+   {f(Succ(s))} (more specific than {Succ(s)})
+
+Dafny program verifier finished with 3 verified, 0 errors
diff --git a/Test/triggers/function-applications-are-triggers.dfy.expect b/Test/triggers/function-applications-are-triggers.dfy.expect
index 501cfa51..1214536d 100644
--- a/Test/triggers/function-applications-are-triggers.dfy.expect
+++ b/Test/triggers/function-applications-are-triggers.dfy.expect
@@ -1,8 +1,8 @@
 function-applications-are-triggers.dfy(9,9): Info: Selected triggers: {P.requires(f)}
-function-applications-are-triggers.dfy(10,9): Info: For expression {P(f) ==> f.requires(10)}:
+function-applications-are-triggers.dfy(10,9): Info: For expression "P(f) ==> f.requires(10)":
    Selected triggers:
      {f(10)}, {f.requires(10)}, {P(f)}
-function-applications-are-triggers.dfy(10,9): Info: For expression {P(f) ==> f(10) == 0}:
+function-applications-are-triggers.dfy(10,9): Info: For expression "P(f) ==> f(10) == 0":
    Selected triggers:
      {f(10)}, {f.requires(10)}, {P(f)}
 function-applications-are-triggers.dfy(11,9): Info: Selected triggers:
diff --git a/Test/triggers/loop-detection-is-not-too-strict.dfy.expect b/Test/triggers/loop-detection-is-not-too-strict.dfy.expect
index 705c2a8c..65ea0d79 100644
--- a/Test/triggers/loop-detection-is-not-too-strict.dfy.expect
+++ b/Test/triggers/loop-detection-is-not-too-strict.dfy.expect
@@ -2,16 +2,16 @@ loop-detection-is-not-too-strict.dfy(15,9): Info: Selected triggers:
    {P(y, x)}, {P(x, y)}
 loop-detection-is-not-too-strict.dfy(18,9): Info: Selected triggers:
    {P(y, x)}, {P(x, y)}
-loop-detection-is-not-too-strict.dfy(21,9): Warning: Selected triggers: {P(x, y)} (may loop with {P(x, y + 1)})
- (!) Suppressing loops would leave this expression without triggers.
+loop-detection-is-not-too-strict.dfy(21,9): Warning: Selected triggers: {P(x, y)} (may loop with "P(x, y + 1)")
+ /!\ Suppressing loops would leave this expression without triggers.
 loop-detection-is-not-too-strict.dfy(26,9): Info: Selected triggers: {Q(x)}
 loop-detection-is-not-too-strict.dfy(27,9): Info: Selected triggers: {Q(x)}
 loop-detection-is-not-too-strict.dfy(28,9): Info: Selected triggers:
    {P(x, z)}, {P(x, 1)}
 loop-detection-is-not-too-strict.dfy(33,9): Info: Selected triggers: {Q(x)}
 loop-detection-is-not-too-strict.dfy(34,9): Info: Selected triggers: {Q(x)}
-loop-detection-is-not-too-strict.dfy(36,9): Warning: Selected triggers: {Q(x)} (may loop with {Q(if z > 1 then x else 3 * z + 1)})
- (!) Suppressing loops would leave this expression without triggers.
+loop-detection-is-not-too-strict.dfy(36,9): Warning: Selected triggers: {Q(x)} (may loop with "Q(if z > 1 then x else 3 * z + 1)")
+ /!\ Suppressing loops would leave this expression without triggers.
 loop-detection-is-not-too-strict.dfy(39,9): Info: Selected triggers: {Q(x)}
 
 Dafny program verifier finished with 4 verified, 0 errors
diff --git a/Test/triggers/loop-detection-looks-at-ranges-too.dfy.expect b/Test/triggers/loop-detection-looks-at-ranges-too.dfy.expect
index ce62d868..a32e4a60 100644
--- a/Test/triggers/loop-detection-looks-at-ranges-too.dfy.expect
+++ b/Test/triggers/loop-detection-looks-at-ranges-too.dfy.expect
@@ -1,6 +1,6 @@
-loop-detection-looks-at-ranges-too.dfy(11,17): Warning: Selected triggers: {P(x)} (may loop with {P(x + 1)})
- (!) Suppressing loops would leave this expression without triggers.
-loop-detection-looks-at-ranges-too.dfy(13,17): Warning: Selected triggers: {P(x)} (may loop with {P(x + 1)})
- (!) Suppressing loops would leave this expression without triggers.
+loop-detection-looks-at-ranges-too.dfy(11,17): Warning: Selected triggers: {P(x)} (may loop with "P(x + 1)")
+ /!\ Suppressing loops would leave this expression without triggers.
+loop-detection-looks-at-ranges-too.dfy(13,17): Warning: Selected triggers: {P(x)} (may loop with "P(x + 1)")
+ /!\ Suppressing loops would leave this expression without triggers.
 
 Dafny program verifier finished with 3 verified, 0 errors
diff --git a/Test/triggers/loop-detection-messages--unit-tests.dfy.expect b/Test/triggers/loop-detection-messages--unit-tests.dfy.expect
index 804a0116..eba8c179 100644
--- a/Test/triggers/loop-detection-messages--unit-tests.dfy.expect
+++ b/Test/triggers/loop-detection-messages--unit-tests.dfy.expect
@@ -1,37 +1,37 @@
 loop-detection-messages--unit-tests.dfy(11,9): Info: Selected triggers: {f(f(i))}
- Rejected triggers: {f(i)} (may loop with {f(f(i))})
-loop-detection-messages--unit-tests.dfy(12,9): Warning: Selected triggers: {f(i)} (may loop with {f(i + 1)})
- (!) Suppressing loops would leave this expression without triggers.
-loop-detection-messages--unit-tests.dfy(13,9): Info: Selected triggers: {f(i)} (may loop with {f(i + 1)})
-loop-detection-messages--unit-tests.dfy(15,9): Info: For expression {false ==> f(i) == f(i + 1)}:
+ Rejected triggers: {f(i)} (may loop with "f(f(i))")
+loop-detection-messages--unit-tests.dfy(12,9): Warning: Selected triggers: {f(i)} (may loop with "f(i + 1)")
+ /!\ Suppressing loops would leave this expression without triggers.
+loop-detection-messages--unit-tests.dfy(13,9): Info: Selected triggers: {f(i)} (may loop with "f(i + 1)")
+loop-detection-messages--unit-tests.dfy(15,9): Info: For expression "false ==> f(i) == f(i + 1)":
    Selected triggers: {g(i)}
-   Rejected triggers: {f(i)} (may loop with {f(i + 1)})
-loop-detection-messages--unit-tests.dfy(15,9): Info: For expression {false ==> f(i) == g(i)}:
+   Rejected triggers: {f(i)} (may loop with "f(i + 1)")
+loop-detection-messages--unit-tests.dfy(15,9): Info: For expression "false ==> f(i) == g(i)":
    Selected triggers:
      {g(i)}, {f(i)}
-loop-detection-messages--unit-tests.dfy(16,9): Warning: For expression {false ==> f(i) == f(i + 1)}:
-   Selected triggers: {f(i)} (may loop with {f(i + 1)})
-   (!) Suppressing loops would leave this expression without triggers.
-loop-detection-messages--unit-tests.dfy(16,9): Info: For expression {false ==> f(i) == f(i)}:
+loop-detection-messages--unit-tests.dfy(16,9): Warning: For expression "false ==> f(i) == f(i + 1)":
+   Selected triggers: {f(i)} (may loop with "f(i + 1)")
+   /!\ Suppressing loops would leave this expression without triggers.
+loop-detection-messages--unit-tests.dfy(16,9): Info: For expression "false ==> f(i) == f(i)":
    Selected triggers: {f(i)}
-loop-detection-messages--unit-tests.dfy(17,9): Info: For expression {false ==> f(i) == f(i + 1)}:
-   Selected triggers: {f(i)} (may loop with {f(i + 1)})
-loop-detection-messages--unit-tests.dfy(17,9): Info: For expression {false ==> f(i) == f(i)}:
+loop-detection-messages--unit-tests.dfy(17,9): Info: For expression "false ==> f(i) == f(i + 1)":
+   Selected triggers: {f(i)} (may loop with "f(i + 1)")
+loop-detection-messages--unit-tests.dfy(17,9): Info: For expression "false ==> f(i) == f(i)":
    Selected triggers: {f(i)}
 loop-detection-messages--unit-tests.dfy(19,9): Info: Selected triggers: {f(i)}
-loop-detection-messages--unit-tests.dfy(20,9): Warning: (!) No terms found to trigger on.
-loop-detection-messages--unit-tests.dfy(21,9): Info: Not generating triggers for {false ==> f(i + 1) == 0}.
+loop-detection-messages--unit-tests.dfy(20,9): Warning: /!\ No terms found to trigger on.
+loop-detection-messages--unit-tests.dfy(21,9): Info: Not generating triggers for "false ==> f(i + 1) == 0". Note that {:autotriggers false} can cause instabilities. Consider using {:nowarn}, {:matchingloop} (not great either), or a manual trigger instead.
 loop-detection-messages--unit-tests.dfy(23,9): Info: Selected triggers: {f(j), f(i)}
-loop-detection-messages--unit-tests.dfy(24,9): Warning: (!) No trigger covering all quantified variables found.
-loop-detection-messages--unit-tests.dfy(25,9): Info: For expression {false ==> f(i) == f(i)}:
+loop-detection-messages--unit-tests.dfy(24,9): Warning: /!\ No trigger covering all quantified variables found.
+loop-detection-messages--unit-tests.dfy(25,9): Info: For expression "false ==> f(i) == f(i)":
    Selected triggers: {g(j), f(i)}
-loop-detection-messages--unit-tests.dfy(25,9): Info: For expression {false ==> g(j) == 0}:
+loop-detection-messages--unit-tests.dfy(25,9): Info: For expression "false ==> g(j) == 0":
    Selected triggers: {g(j), f(i)}
-loop-detection-messages--unit-tests.dfy(26,9): Warning: For expression {false ==> f(i) == f(i)}:
-   (!) No trigger covering all quantified variables found.
-loop-detection-messages--unit-tests.dfy(26,9): Warning: For expression {false ==> g(j + 1) == 0}:
-   (!) No trigger covering all quantified variables found.
-loop-detection-messages--unit-tests.dfy(27,9): Info: Not generating triggers for {false ==> f(i) == f(i)}.
-loop-detection-messages--unit-tests.dfy(28,9): Info: Not generating triggers for {false ==> f(i) == f(i)}.
+loop-detection-messages--unit-tests.dfy(26,9): Warning: For expression "false ==> f(i) == f(i)":
+   /!\ No trigger covering all quantified variables found.
+loop-detection-messages--unit-tests.dfy(26,9): Warning: For expression "false ==> g(j + 1) == 0":
+   /!\ No trigger covering all quantified variables found.
+loop-detection-messages--unit-tests.dfy(27,9): Info: Not generating triggers for "false ==> f(i) == f(i)". Note that {:autotriggers false} can cause instabilities. Consider using {:nowarn}, {:matchingloop} (not great either), or a manual trigger instead.
+loop-detection-messages--unit-tests.dfy(28,9): Info: Not generating triggers for "false ==> f(i) == f(i)".
 
 Dafny program verifier finished with 4 verified, 0 errors
diff --git a/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy.expect b/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy.expect
index 58094110..e900c1f9 100644
--- a/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy.expect
+++ b/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy.expect
@@ -1,10 +1,10 @@
 looping-is-hard-to-decide-modulo-equality.dfy(21,9): Info: Selected triggers:
    {h(h(c, j), j)}, {h(c, i)}, {c in sc}
- Rejected triggers: {h(c, j)} (may loop with {h(h(c, j), j)})
+ Rejected triggers: {h(c, j)} (may loop with "h(h(c, j), j)")
 looping-is-hard-to-decide-modulo-equality.dfy(26,9): Info: Selected triggers: {f(x)}
  Rejected triggers: {g(f(x))} (more specific than {f(x)})
 looping-is-hard-to-decide-modulo-equality.dfy(31,9): Info: Selected triggers:
    {old(f(f(c)))}, {f(c)}, {c in sc}
- Rejected triggers: {old(f(c))} (may loop with {old(f(f(c)))})
+ Rejected triggers: {old(f(c))} (may loop with "old(f(f(c)))")
 
 Dafny program verifier finished with 9 verified, 0 errors
diff --git a/Test/triggers/matrix-accesses-are-triggers.dfy.expect b/Test/triggers/matrix-accesses-are-triggers.dfy.expect
index 35df02f5..572fc41f 100644
--- a/Test/triggers/matrix-accesses-are-triggers.dfy.expect
+++ b/Test/triggers/matrix-accesses-are-triggers.dfy.expect
@@ -1,5 +1,5 @@
-matrix-accesses-are-triggers.dfy(8,11): Warning: Selected triggers: {m[i, j]} (may loop with {m[j, i + 1]})
- (!) Suppressing loops would leave this expression without triggers.
+matrix-accesses-are-triggers.dfy(8,11): Warning: Selected triggers: {m[i, j]} (may loop with "m[j, i + 1]")
+ /!\ Suppressing loops would leave this expression without triggers.
 matrix-accesses-are-triggers.dfy(8,81): Error: index 0 out of range
 Execution trace:
     (0,0): anon0
diff --git a/Test/triggers/old-is-a-special-case-for-triggers.dfy.expect b/Test/triggers/old-is-a-special-case-for-triggers.dfy.expect
index 313d7c16..7388a911 100644
--- a/Test/triggers/old-is-a-special-case-for-triggers.dfy.expect
+++ b/Test/triggers/old-is-a-special-case-for-triggers.dfy.expect
@@ -2,14 +2,14 @@ old-is-a-special-case-for-triggers.dfy(15,10): Info: Selected triggers:
    {old(f(c))}, {c in sc}
 old-is-a-special-case-for-triggers.dfy(20,10): Info: Selected triggers:
    {old(f(f(c)))}, {f(c)}, {c in sc}
- Rejected triggers: {old(f(c))} (may loop with {old(f(f(c)))})
+ Rejected triggers: {old(f(c))} (may loop with "old(f(f(c)))")
 old-is-a-special-case-for-triggers.dfy(21,10): Info: Selected triggers:
    {f(g(c))}, {g(f(c))}, {old(f(g(c)))}, {old(g(f(c)))}, {old(f(f(c)))}, {c in sc}
  Rejected triggers:
-   {g(c)} (may loop with {g(f(c))})
-   {f(c)} (may loop with {f(g(c))})
-   {old(g(c))} (may loop with {old(g(f(c)))})
-   {old(f(c))} (may loop with {old(f(f(c)))}, {old(f(g(c)))})
+   {g(c)} (may loop with "g(f(c))")
+   {f(c)} (may loop with "f(g(c))")
+   {old(g(c))} (may loop with "old(g(f(c)))")
+   {old(f(c))} (may loop with "old(f(f(c)))", "old(f(g(c)))")
 old-is-a-special-case-for-triggers.dfy(25,10): Info: Selected triggers:
    {old(f(c))}, {f(c)}, {c in sc}
  Rejected triggers: {old(g(f(c)))} (more specific than {old(f(c))})
diff --git a/Test/triggers/regression-tests.dfy.expect b/Test/triggers/regression-tests.dfy.expect
index a03810fb..e780e966 100644
--- a/Test/triggers/regression-tests.dfy.expect
+++ b/Test/triggers/regression-tests.dfy.expect
@@ -1,3 +1,3 @@
-regression-tests.dfy(16,5): Warning: (!) No terms found to trigger on.
+regression-tests.dfy(16,5): Warning: /!\ No terms found to trigger on.
 
 Dafny program verifier finished with 2 verified, 0 errors
diff --git a/Test/triggers/some-proofs-only-work-without-autoTriggers.dfy b/Test/triggers/some-proofs-only-work-without-autoTriggers.dfy
new file mode 100644
index 00000000..98cea392
--- /dev/null
+++ b/Test/triggers/some-proofs-only-work-without-autoTriggers.dfy
@@ -0,0 +1,48 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// The examples below work nicely with /autoTriggers:0, but break when we ass
+// /autoTriggers.
+
+// The issue is that the axioms for sequences are missing a number of facts,
+// which was not a problem before /autoTriggers and /stricterTriggers, but has
+// become one. Here are examples of things that Dafny won’t prove with
+// /autoTriggers (I would expect it wouldn’t with stricterTriggers either,
+// though the second example is trickier than the first):
+
+method M(a: seq<int>) {
+  if * {
+    // This fails; it needs the following axiom:
+    //   axiom (forall<T> s: Seq T ::
+    //    { Seq#Take(s, Seq#Length(s)) }
+    //    Seq#Take(s, Seq#Length(s)) == s);
+    assume forall x :: x in a ==> x > 0;
+    assert forall x :: x in a[..|a|] ==> x > 0;
+  } else if * {
+    // This fails; it needs the following axiom:
+    //   axiom (forall<T> s: Seq T, i: int ::
+    //    { Seq#Index(s, i) }
+    //    0 <= i && i < Seq#Length(s) ==>
+    //    Seq#Contains(s, Seq#Index(s, i)));
+    assume forall x :: x in a ==> x > 0;
+    assert forall i | 0 <= i < |a| ::  a[i] > 0;
+  } else if * {
+    assume |a| > 3;
+    assume forall x | x in a[..3] :: x > 1;
+    // This fails, but here it's a lot harder to know what a good axiom would be.
+    assert forall x | x in a[..2] :: x > 1;
+  }
+}
+
+
+// In the first case, the Boogie version is
+//
+//   Seq#Contains(Seq#Take(a#0, Seq#Length(a#0)), $Box(x#0_1)) ⟹ x#0_1 > 0
+//
+// And of course Z3 picks $Box(x#0_1). The third case is similar.
+//
+// The problem is of course that knowing that x ∈ a[..2] doesn’t magically give
+// you a term that matches x ∈ a[..3]. One could imagine introducing an extra
+// symbol in the translation to put x and a together for triggering purposes,
+// but that would have the same sort of issues as adding symbols for arithmetic
+// operators.
diff --git a/Test/triggers/some-proofs-only-work-without-autoTriggers.dfy.expect b/Test/triggers/some-proofs-only-work-without-autoTriggers.dfy.expect
new file mode 100644
index 00000000..d48840b8
--- /dev/null
+++ b/Test/triggers/some-proofs-only-work-without-autoTriggers.dfy.expect
@@ -0,0 +1,31 @@
+some-proofs-only-work-without-autoTriggers.dfy(19,11): Info: Selected triggers: {x in a}
+some-proofs-only-work-without-autoTriggers.dfy(20,11): Info: Selected triggers: {x in a[..|a|]}
+some-proofs-only-work-without-autoTriggers.dfy(27,11): Info: Selected triggers: {x in a}
+some-proofs-only-work-without-autoTriggers.dfy(28,11): Info: Selected triggers: {a[i]}
+some-proofs-only-work-without-autoTriggers.dfy(31,11): Info: Selected triggers: {x in a[..3]}
+some-proofs-only-work-without-autoTriggers.dfy(33,11): Info: Selected triggers: {x in a[..2]}
+some-proofs-only-work-without-autoTriggers.dfy(20,11): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+    (0,0): anon22_Then
+    (0,0): anon3
+    (0,0): anon23_Then
+    (0,0): anon5
+some-proofs-only-work-without-autoTriggers.dfy(28,11): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+    (0,0): anon25_Then
+    (0,0): anon9
+    (0,0): anon26_Then
+    (0,0): anon27_Then
+    (0,0): anon13
+some-proofs-only-work-without-autoTriggers.dfy(33,11): Error: assertion violation
+Execution trace:
+    (0,0): anon0
+    (0,0): anon28_Then
+    (0,0): anon29_Then
+    (0,0): anon17
+    (0,0): anon30_Then
+    (0,0): anon19
+
+Dafny program verifier finished with 1 verified, 3 errors
diff --git a/Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy.expect b/Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy.expect
index f5e47454..1a143edb 100644
--- a/Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy.expect
+++ b/Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy.expect
@@ -1,10 +1,10 @@
-some-terms-do-not-look-like-the-triggers-they-match.dfy(12,17): Warning: Selected triggers: {s[x]} (may loop with {s[x + 1]})
- (!) Suppressing loops would leave this expression without triggers.
-some-terms-do-not-look-like-the-triggers-they-match.dfy(15,17): Warning: For expression {x in s ==> s[x + 1] > 0}:
-   Selected triggers: {s[x]} (may loop with {s[x + 1]})
-   (!) Suppressing loops would leave this expression without triggers.
-some-terms-do-not-look-like-the-triggers-they-match.dfy(15,17): Warning: For expression {x in s ==> x + 2 !in s}:
-   Selected triggers: {s[x]} (may loop with {x + 2 !in s})
-   (!) Suppressing loops would leave this expression without triggers.
+some-terms-do-not-look-like-the-triggers-they-match.dfy(12,17): Warning: Selected triggers: {s[x]} (may loop with "s[x + 1]")
+ /!\ Suppressing loops would leave this expression without triggers.
+some-terms-do-not-look-like-the-triggers-they-match.dfy(15,17): Warning: For expression "x in s ==> s[x + 1] > 0":
+   Selected triggers: {s[x]} (may loop with "s[x + 1]")
+   /!\ Suppressing loops would leave this expression without triggers.
+some-terms-do-not-look-like-the-triggers-they-match.dfy(15,17): Warning: For expression "x in s ==> x + 2 !in s":
+   Selected triggers: {s[x]} (may loop with "x + 2 !in s")
+   /!\ Suppressing loops would leave this expression without triggers.
 
 Dafny program verifier finished with 2 verified, 0 errors
diff --git a/Test/triggers/splitting-picks-the-right-tokens.dfy.expect b/Test/triggers/splitting-picks-the-right-tokens.dfy.expect
index af274e75..f01ed1a0 100644
--- a/Test/triggers/splitting-picks-the-right-tokens.dfy.expect
+++ b/Test/triggers/splitting-picks-the-right-tokens.dfy.expect
@@ -1,14 +1,14 @@
-splitting-picks-the-right-tokens.dfy(9,11): Info: For expression {Id(x) > 1}:
+splitting-picks-the-right-tokens.dfy(9,11): Info: For expression "Id(x) > 1":
    Selected triggers: {Id(x)}
-splitting-picks-the-right-tokens.dfy(9,11): Info: For expression {x > 2}:
+splitting-picks-the-right-tokens.dfy(9,11): Info: For expression "x > 2":
    Selected triggers: {Id(x)}
-splitting-picks-the-right-tokens.dfy(9,11): Info: For expression {x > -1}:
+splitting-picks-the-right-tokens.dfy(9,11): Info: For expression "x > -1":
    Selected triggers: {Id(x)}
-splitting-picks-the-right-tokens.dfy(16,11): Info: For expression {x > 0 ==> Id(x) > 1}:
+splitting-picks-the-right-tokens.dfy(16,11): Info: For expression "x > 0 ==> Id(x) > 1":
    Selected triggers: {Id(x)}
-splitting-picks-the-right-tokens.dfy(16,11): Info: For expression {x > 0 ==> x > 2}:
+splitting-picks-the-right-tokens.dfy(16,11): Info: For expression "x > 0 ==> x > 2":
    Selected triggers: {Id(x)}
-splitting-picks-the-right-tokens.dfy(16,11): Info: For expression {x > 0 ==> x > -1}:
+splitting-picks-the-right-tokens.dfy(16,11): Info: For expression "x > 0 ==> x > -1":
    Selected triggers: {Id(x)}
 splitting-picks-the-right-tokens.dfy(20,12): Error BP5002: A precondition for this call might not hold.
 splitting-picks-the-right-tokens.dfy(16,11): Related location: This is the precondition that might not hold.
diff --git a/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect b/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect
index 58c8dd2b..a8bb2345 100644
--- a/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect
+++ b/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect
@@ -1,32 +1,32 @@
 splitting-triggers-recovers-expressivity.dfy(12,10): Info: Selected triggers: {Q(i)}
- Rejected triggers: {P(i)} (may loop with {P(i + 1)})
+ Rejected triggers: {P(i)} (may loop with "P(i + 1)")
 splitting-triggers-recovers-expressivity.dfy(17,11): Info: Selected triggers: {Q(j)}
- Rejected triggers: {P(j)} (may loop with {P(j + 1)})
+ Rejected triggers: {P(j)} (may loop with "P(j + 1)")
 splitting-triggers-recovers-expressivity.dfy(26,10): Info: Selected triggers: {Q(i)}
- Rejected triggers: {P(i)} (may loop with {P(i + 1)})
+ Rejected triggers: {P(i)} (may loop with "P(i + 1)")
 splitting-triggers-recovers-expressivity.dfy(33,11): Info: Selected triggers: {Q(j)}
- Rejected triggers: {P(j)} (may loop with {P(j + 1)})
-splitting-triggers-recovers-expressivity.dfy(44,10): Info: For expression {P(i)}:
+ Rejected triggers: {P(j)} (may loop with "P(j + 1)")
+splitting-triggers-recovers-expressivity.dfy(44,10): Info: For expression "P(i)":
    Selected triggers:
      {Q(i)}, {P(i)}
-splitting-triggers-recovers-expressivity.dfy(44,10): Info: For expression {!Q(i)}:
+splitting-triggers-recovers-expressivity.dfy(44,10): Info: For expression "!Q(i)":
    Selected triggers:
      {Q(i)}, {P(i)}
-splitting-triggers-recovers-expressivity.dfy(44,10): Info: For expression {P(i + 1)}:
+splitting-triggers-recovers-expressivity.dfy(44,10): Info: For expression "P(i + 1)":
    Selected triggers: {Q(i)}
-   Rejected triggers: {P(i)} (may loop with {P(i + 1)})
-splitting-triggers-recovers-expressivity.dfy(49,11): Info: For expression {j >= 0 ==> P(j)}:
+   Rejected triggers: {P(i)} (may loop with "P(i + 1)")
+splitting-triggers-recovers-expressivity.dfy(49,11): Info: For expression "j >= 0 ==> P(j)":
    Selected triggers:
      {Q(j)}, {P(j)}
-splitting-triggers-recovers-expressivity.dfy(49,11): Info: For expression {j >= 0 ==> Q(j) ==> P(j + 1)}:
+splitting-triggers-recovers-expressivity.dfy(49,11): Info: For expression "j >= 0 ==> Q(j) ==> P(j + 1)":
    Selected triggers: {Q(j)}
-   Rejected triggers: {P(j)} (may loop with {P(j + 1)})
-splitting-triggers-recovers-expressivity.dfy(58,11): Info: For expression {i >= 0 ==> Q(i)}:
+   Rejected triggers: {P(j)} (may loop with "P(j + 1)")
+splitting-triggers-recovers-expressivity.dfy(58,11): Info: For expression "i >= 0 ==> Q(i)":
    Selected triggers:
      {P(i)}, {Q(i)}
-splitting-triggers-recovers-expressivity.dfy(58,11): Info: For expression {i >= 0 ==> P(i) ==> P(i + 1)}:
+splitting-triggers-recovers-expressivity.dfy(58,11): Info: For expression "i >= 0 ==> P(i) ==> P(i + 1)":
    Selected triggers:
-     {P(i)} (may loop with {P(i + 1)}), {Q(i)}
+     {P(i)} (may loop with "P(i + 1)"), {Q(i)}
 splitting-triggers-recovers-expressivity.dfy(12,63): Error BP5003: A postcondition might not hold on this return path.
 splitting-triggers-recovers-expressivity.dfy(12,10): Related location: This is the postcondition that might not hold.
 Execution trace:
diff --git a/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy.expect b/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy.expect
index c8e1a5fa..27548ac9 100644
--- a/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy.expect
+++ b/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy.expect
@@ -1,11 +1,11 @@
-splitting-triggers-yields-better-precondition-related-errors.dfy(7,11): Warning: For expression {y > 0}:
-   (!) No terms found to trigger on.
-splitting-triggers-yields-better-precondition-related-errors.dfy(7,11): Warning: For expression {y < 0}:
-   (!) No terms found to trigger on.
-splitting-triggers-yields-better-precondition-related-errors.dfy(15,11): Warning: For expression {y > 0}:
-   (!) No terms found to trigger on.
-splitting-triggers-yields-better-precondition-related-errors.dfy(15,11): Warning: For expression {y < 0}:
-   (!) No terms found to trigger on.
+splitting-triggers-yields-better-precondition-related-errors.dfy(7,11): Warning: For expression "y > 0":
+   /!\ No terms found to trigger on.
+splitting-triggers-yields-better-precondition-related-errors.dfy(7,11): Warning: For expression "y < 0":
+   /!\ No terms found to trigger on.
+splitting-triggers-yields-better-precondition-related-errors.dfy(15,11): Warning: For expression "y > 0":
+   /!\ No terms found to trigger on.
+splitting-triggers-yields-better-precondition-related-errors.dfy(15,11): Warning: For expression "y < 0":
+   /!\ No terms found to trigger on.
 splitting-triggers-yields-better-precondition-related-errors.dfy(11,3): Error BP5002: A precondition for this call might not hold.
 splitting-triggers-yields-better-precondition-related-errors.dfy(7,11): Related location: This is the precondition that might not hold.
 splitting-triggers-yields-better-precondition-related-errors.dfy(7,34): Related location
diff --git a/Test/triggers/suppressing-warnings-behaves-properly.dfy b/Test/triggers/suppressing-warnings-behaves-properly.dfy
new file mode 100644
index 00000000..237269e5
--- /dev/null
+++ b/Test/triggers/suppressing-warnings-behaves-properly.dfy
@@ -0,0 +1,21 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// This file checks that suppressing warnings works properly
+
+predicate f(x: int)
+predicate g(x: int)
+
+method M() {
+  assert forall n :: n >= 0 || n < 0;
+  assert forall n {:nowarn} :: n >= 0 || n < 0;
+  assert forall n {:autotriggers false} :: n >= 0 || n < 0;
+
+  assert forall n: nat :: (n != 0) == f(n) || true;
+  assert forall n: nat {:nowarn} :: (n != 0) == f(n) || true;
+  assert forall n: nat {:autotriggers false} :: (n != 0) == f(n) || true;
+
+  assert forall n: nat :: f(n) == f(n+1) || g(n) || true;
+  assert forall n: nat {:nowarn} :: (n != 0) == f(n) || true;
+  assert forall n: nat {:autotriggers false} :: (n != 0) == f(n) || true;
+}
diff --git a/Test/triggers/suppressing-warnings-behaves-properly.dfy.expect b/Test/triggers/suppressing-warnings-behaves-properly.dfy.expect
new file mode 100644
index 00000000..124984b1
--- /dev/null
+++ b/Test/triggers/suppressing-warnings-behaves-properly.dfy.expect
@@ -0,0 +1,14 @@
+suppressing-warnings-behaves-properly.dfy(10,9): Warning: /!\ No terms found to trigger on.
+suppressing-warnings-behaves-properly.dfy(11,9): Info: (Suppressed warning) No terms found to trigger on.
+suppressing-warnings-behaves-properly.dfy(12,9): Info: Not generating triggers for "n >= 0 || n < 0". Note that {:autotriggers false} can cause instabilities. Consider using {:nowarn}, {:matchingloop} (not great either), or a manual trigger instead.
+suppressing-warnings-behaves-properly.dfy(14,9): Info: Selected triggers: {f(n)}
+suppressing-warnings-behaves-properly.dfy(15,9): Warning: Selected triggers: {f(n)}
+ /!\ There is no warning here to suppress.
+suppressing-warnings-behaves-properly.dfy(16,9): Info: Not generating triggers for "(n != 0) == f(n) || true". Note that {:autotriggers false} can cause instabilities. Consider using {:nowarn}, {:matchingloop} (not great either), or a manual trigger instead.
+suppressing-warnings-behaves-properly.dfy(18,9): Info: Selected triggers: {g(n)}
+ Rejected triggers: {f(n)} (may loop with "f(n + 1)")
+suppressing-warnings-behaves-properly.dfy(19,9): Warning: Selected triggers: {f(n)}
+ /!\ There is no warning here to suppress.
+suppressing-warnings-behaves-properly.dfy(20,9): Info: Not generating triggers for "(n != 0) == f(n) || true". Note that {:autotriggers false} can cause instabilities. Consider using {:nowarn}, {:matchingloop} (not great either), or a manual trigger instead.
+
+Dafny program verifier finished with 4 verified, 0 errors
diff --git a/Test/triggers/useless-triggers-are-removed.dfy.expect b/Test/triggers/useless-triggers-are-removed.dfy.expect
index 2e9bbedf..d6b49a9e 100644
--- a/Test/triggers/useless-triggers-are-removed.dfy.expect
+++ b/Test/triggers/useless-triggers-are-removed.dfy.expect
@@ -5,11 +5,11 @@ useless-triggers-are-removed.dfy(16,11): Info: Selected triggers: {f(x)}
    {h(f(x))} (more specific than {f(x)})
    {g(f(x))} (more specific than {f(x)})
 useless-triggers-are-removed.dfy(20,11): Info: Selected triggers: {f(f(x))}
- Rejected triggers: {f(x)} (may loop with {f(f(x))})
+ Rejected triggers: {f(x)} (may loop with "f(f(x))")
 useless-triggers-are-removed.dfy(23,11): Info: Selected triggers:
    {g(f(x)), g(y)}, {f(y), f(x)}
  Rejected triggers:
-   {g(y), f(x)} (may loop with {g(f(y))}, {g(f(x))})
+   {g(y), f(x)} (may loop with "g(f(y))", "g(f(x))")
    {g(f(x)), g(f(y))} (more specific than {g(f(x)), f(y)}, {g(f(y)), f(x)}, {f(y), f(x)})
    {g(f(x)), f(y)} (more specific than {f(y), f(x)})
    {g(f(y)), f(x)} (more specific than {f(y), f(x)})
diff --git a/Test/triggers/wf-checks-use-the-original-quantifier.dfy.expect b/Test/triggers/wf-checks-use-the-original-quantifier.dfy.expect
index 6b152262..6c3e4853 100644
--- a/Test/triggers/wf-checks-use-the-original-quantifier.dfy.expect
+++ b/Test/triggers/wf-checks-use-the-original-quantifier.dfy.expect
@@ -1,16 +1,16 @@
-wf-checks-use-the-original-quantifier.dfy(26,11): Info: For expression {0 <= f(n)}:
+wf-checks-use-the-original-quantifier.dfy(26,11): Info: For expression "0 <= f(n)":
    Selected triggers: {f(n)}
    Rejected triggers: {P(f(n))} (more specific than {f(n)})
-wf-checks-use-the-original-quantifier.dfy(26,11): Info: For expression {P(f(n))}:
+wf-checks-use-the-original-quantifier.dfy(26,11): Info: For expression "P(f(n))":
    Selected triggers: {f(n)}
    Rejected triggers: {P(f(n))} (more specific than {f(n)})
-wf-checks-use-the-original-quantifier.dfy(27,11): Info: For expression {c != null}:
+wf-checks-use-the-original-quantifier.dfy(27,11): Info: For expression "c != null":
    Selected triggers:
      {c'.x, c.x}, {c'.x, c in s}, {c.x, c' in s}, {c' in s, c in s}
-wf-checks-use-the-original-quantifier.dfy(27,11): Info: For expression {c' != null}:
+wf-checks-use-the-original-quantifier.dfy(27,11): Info: For expression "c' != null":
    Selected triggers:
      {c'.x, c.x}, {c'.x, c in s}, {c.x, c' in s}, {c' in s, c in s}
-wf-checks-use-the-original-quantifier.dfy(27,11): Info: For expression {c.x == c'.x}:
+wf-checks-use-the-original-quantifier.dfy(27,11): Info: For expression "c.x == c'.x":
    Selected triggers:
      {c'.x, c.x}, {c'.x, c in s}, {c.x, c' in s}, {c' in s, c in s}
 
-- 
cgit v1.2.3