Implement {:nowarn}, clarify some messages, and add a few tests

20 files changed, 219 insertions, 88 deletions

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}