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

---
 ...s-better-precondition-related-errors.dfy.expect | 32 ++++++++++++++++++++++
 1 file changed, 32 insertions(+)
 create mode 100644 Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy.expect

(limited to 'Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy.expect')

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
new file mode 100644
index 00000000..c8e1a5fa
--- /dev/null
+++ b/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy.expect
@@ -0,0 +1,32 @@
+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
+Execution trace:
+    (0,0): anon0
+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,25): Related location
+Execution trace:
+    (0,0): anon0
+splitting-triggers-yields-better-precondition-related-errors.dfy(20,2): Error: possible violation of function precondition
+splitting-triggers-yields-better-precondition-related-errors.dfy(15,11): Related location
+splitting-triggers-yields-better-precondition-related-errors.dfy(15,34): Related location
+Execution trace:
+    (0,0): anon0
+    (0,0): anon4_Else
+splitting-triggers-yields-better-precondition-related-errors.dfy(20,2): Error: possible violation of function precondition
+splitting-triggers-yields-better-precondition-related-errors.dfy(15,11): Related location
+splitting-triggers-yields-better-precondition-related-errors.dfy(15,25): Related location
+Execution trace:
+    (0,0): anon0
+    (0,0): anon4_Else
+
+Dafny program verifier finished with 4 verified, 4 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/splitting-triggers-yields-better-precondition-related-errors.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