From 84b52a48efda3e9658b772dbc02d34a6f6c9d16b Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel <clement.pitclaudel@live.com>
Date: Fri, 21 Aug 2015 19:09:37 -0700
Subject: Adjust WF checks to use unsplit quantifiers.

The logic about split quantifiers is that Boogie (and z3) should never realize
that there was an unsplit quantifier. The WF check code does not produce a
quantifier, at least in it's checking part; thus, it should use original
quantifier. This fixes a problem in VerifyThis2015/Problem2.dfy with a null
check, and a problem spotted by Chris, made into a test case saved in
triggers/wf-checks-use-the-original-quantifier.dfy. The issue boiled down to
being able to verify (forall x :: x != null && x.a == 0).

Of course, the assumption that WF checks produce for a quantifier is a
quantifier, so it uses the split expression.
---
 .../wf-checks-use-the-original-quantifier.dfy.expect    | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 Test/triggers/wf-checks-use-the-original-quantifier.dfy.expect

(limited to 'Test/triggers/wf-checks-use-the-original-quantifier.dfy.expect')

diff --git a/Test/triggers/wf-checks-use-the-original-quantifier.dfy.expect b/Test/triggers/wf-checks-use-the-original-quantifier.dfy.expect
new file mode 100644
index 00000000..6b152262
--- /dev/null
+++ b/Test/triggers/wf-checks-use-the-original-quantifier.dfy.expect
@@ -0,0 +1,17 @@
+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))}:
+   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}:
+   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}:
+   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}:
+   Selected triggers:
+     {c'.x, c.x}, {c'.x, c in s}, {c.x, c' in s}, {c' in s, c in s}
+
+Dafny program verifier finished with 4 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/wf-checks-use-the-original-quantifier.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