46 files changed, 968 insertions, 0 deletions
diff --git a/Test/triggers/auto-triggers-fix-an-issue-listed-in-the-ironclad-notebook.dfy b/Test/triggers/auto-triggers-fix-an-issue-listed-in-the-ironclad-notebook.dfy
new file mode 100644
index 00000000..09032453
--- /dev/null
+++ b/Test/triggers/auto-triggers-fix-an-issue-listed-in-the-ironclad-notebook.dfy
@@ -0,0 +1,23 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// This example was listed in IronClad's notebook as one place were z3 picked
+// much too liberal triggers. THe Boogie code for this is shown below:
+//
+// forall k#2: Seq Box :: $Is(k#2, TSeq(TInt)) && $IsAlloc(k#2, TSeq(TInt), $Heap)
+//                   ==> Seq#Equal(_module.__default.HashtableLookup($Heap, h1#0, k#2),
+//                                 _module.__default.HashtableLookup($Heap, h2#0, k#2))
+//
+// and z3 would pick $Is(k#2, TSeq(TInt)) or $IsAlloc(k#2, TSeq(TInt), $Heap) as
+// triggers.
+
+type Key = seq<int>
+type Value = seq<int>
+
+type Hashtable = map<Key, Value>
+function HashtableLookup(h: Hashtable, k: Key): Value
+
+lemma HashtableAgreement(h1:Hashtable, h2:Hashtable, k:Key)
+  requires forall k :: HashtableLookup(h1,k) == HashtableLookup(h2,k) {
+    assert true || (k in h1) == (k in h2);
+}
diff --git a/Test/triggers/auto-triggers-fix-an-issue-listed-in-the-ironclad-notebook.dfy.expect b/Test/triggers/auto-triggers-fix-an-issue-listed-in-the-ironclad-notebook.dfy.expect
new file mode 100644
index 00000000..46ec143e
--- /dev/null
+++ b/Test/triggers/auto-triggers-fix-an-issue-listed-in-the-ironclad-notebook.dfy.expect
@@ -0,0 +1,4 @@
+auto-triggers-fix-an-issue-listed-in-the-ironclad-notebook.dfy(21,11): Info: Selected triggers:
+   {HashtableLookup(h2, k)}, {HashtableLookup(h1, k)}
+
+Dafny program verifier finished with 3 verified, 0 errors
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 b/Test/triggers/function-applications-are-triggers.dfy
new file mode 100644
index 00000000..0aad9018
--- /dev/null
+++ b/Test/triggers/function-applications-are-triggers.dfy
@@ -0,0 +1,15 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// This file checks that function applications yield trigger candidates
+
+method M(P: (int -> int) -> bool, g: int -> int)
+  requires P.requires(g)
+  requires P(g) {
+  assume forall f: int -> int :: P.requires(f);
+  assume forall f: int -> int :: P(f) ==> f.requires(10) && f(10) == 0;
+  assert forall f: int -> int ::
+    (forall x :: f.requires(x) && g.requires(x) ==> f(x) == g(x)) ==>
+    f.requires(10) ==>
+    f(10) == 0;
+}
diff --git a/Test/triggers/function-applications-are-triggers.dfy.expect b/Test/triggers/function-applications-are-triggers.dfy.expect
new file mode 100644
index 00000000..1214536d
--- /dev/null
+++ b/Test/triggers/function-applications-are-triggers.dfy.expect
@@ -0,0 +1,13 @@
+function-applications-are-triggers.dfy(9,9): Info: Selected triggers: {P.requires(f)}
+function-applications-are-triggers.dfy(10,9): Info: For expression "P(f) ==> f.requires(10)":
+   Selected triggers:
+     {f(10)}, {f.requires(10)}, {P(f)}
+function-applications-are-triggers.dfy(10,9): Info: For expression "P(f) ==> f(10) == 0":
+   Selected triggers:
+     {f(10)}, {f.requires(10)}, {P(f)}
+function-applications-are-triggers.dfy(11,9): Info: Selected triggers:
+   {f(10)}, {f.requires(10)}
+function-applications-are-triggers.dfy(12,5): Info: Selected triggers:
+   {g(x)}, {f(x)}, {g.requires(x)}, {f.requires(x)}
+
+Dafny program verifier finished with 2 verified, 0 errors
diff --git a/Test/triggers/large-quantifiers-dont-break-dafny.dfy b/Test/triggers/large-quantifiers-dont-break-dafny.dfy
new file mode 100644
index 00000000..58eb56e1
--- /dev/null
+++ b/Test/triggers/large-quantifiers-dont-break-dafny.dfy
@@ -0,0 +1,61 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// This test ensures that the trigger  collector (the routine that picks trigger
+// candidates) does not  actually consider all subsets of terms;  if it did, the
+// following would take horribly long
+
+predicate P0(x: bool)
+predicate P1(x: bool)
+predicate P2(x: bool)
+predicate P3(x: bool)
+predicate P4(x: bool)
+predicate P5(x: bool)
+predicate P6(x: bool)
+predicate P7(x: bool)
+predicate P8(x: bool)
+predicate P9(x: bool)
+predicate P10(x: bool)
+predicate P11(x: bool)
+predicate P12(x: bool)
+predicate P13(x: bool)
+predicate P14(x: bool)
+predicate P15(x: bool)
+predicate P16(x: bool)
+predicate P17(x: bool)
+predicate P18(x: bool)
+predicate P19(x: bool)
+predicate P20(x: bool)
+predicate P21(x: bool)
+predicate P22(x: bool)
+predicate P23(x: bool)
+predicate P24(x: bool)
+predicate P25(x: bool)
+predicate P26(x: bool)
+predicate P27(x: bool)
+predicate P28(x: bool)
+predicate P29(x: bool)
+predicate P30(x: bool)
+predicate P31(x: bool)
+predicate P32(x: bool)
+predicate P33(x: bool)
+predicate P34(x: bool)
+predicate P35(x: bool)
+predicate P36(x: bool)
+predicate P37(x: bool)
+predicate P38(x: bool)
+predicate P39(x: bool)
+predicate P40(x: bool)
+predicate P41(x: bool)
+predicate P42(x: bool)
+predicate P43(x: bool)
+predicate P44(x: bool)
+predicate P45(x: bool)
+predicate P46(x: bool)
+predicate P47(x: bool)
+predicate P48(x: bool)
+predicate P49(x: bool)
+
+method M() {
+  assert forall x :: true || P0(x) || P1(x) || P2(x) || P3(x) || P4(x) || P5(x) || P6(x) || P7(x) || P8(x) || P9(x) || P10(x) || P11(x) || P12(x) || P13(x) || P14(x) || P15(x) || P16(x) || P17(x) || P18(x) || P19(x) || P20(x) || P21(x) || P22(x) || P23(x) || P24(x) || P25(x) || P26(x) || P27(x) || P28(x) || P29(x) || P30(x) || P31(x) || P32(x) || P33(x) || P34(x) || P35(x) || P36(x) || P37(x) || P38(x) || P39(x) || P40(x) || P41(x) || P42(x) || P43(x) || P44(x) || P45(x) || P46(x) || P47(x) || P48(x) || P49(x);
+}
diff --git a/Test/triggers/large-quantifiers-dont-break-dafny.dfy.expect b/Test/triggers/large-quantifiers-dont-break-dafny.dfy.expect
new file mode 100644
index 00000000..5e7c14b9
--- /dev/null
+++ b/Test/triggers/large-quantifiers-dont-break-dafny.dfy.expect
@@ -0,0 +1,4 @@
+large-quantifiers-dont-break-dafny.dfy(60,9): Info: Selected triggers:
+   {P49(x)}, {P48(x)}, {P47(x)}, {P46(x)}, {P45(x)}, {P44(x)}, {P43(x)}, {P42(x)}, {P41(x)}, {P40(x)}, {P39(x)}, {P38(x)}, {P37(x)}, {P36(x)}, {P35(x)}, {P34(x)}, {P33(x)}, {P32(x)}, {P31(x)}, {P30(x)}, {P29(x)}, {P28(x)}, {P27(x)}, {P26(x)}, {P25(x)}, {P24(x)}, {P23(x)}, {P22(x)}, {P21(x)}, {P20(x)}, {P19(x)}, {P18(x)}, {P17(x)}, {P16(x)}, {P15(x)}, {P14(x)}, {P13(x)}, {P12(x)}, {P11(x)}, {P10(x)}, {P9(x)}, {P8(x)}, {P7(x)}, {P6(x)}, {P5(x)}, {P4(x)}, {P3(x)}, {P2(x)}, {P1(x)}, {P0(x)}
+
+Dafny program verifier finished with 52 verified, 0 errors
diff --git a/Test/triggers/loop-detection-is-not-too-strict.dfy b/Test/triggers/loop-detection-is-not-too-strict.dfy
new file mode 100644
index 00000000..81f764ad
--- /dev/null
+++ b/Test/triggers/loop-detection-is-not-too-strict.dfy
@@ -0,0 +1,40 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// This test shows that the loop detection engine makes compromises when looking
+// for subexpressions matching a trigger; in particular, it allows a
+// subexpression to match a trigger without reporting a loop and without being
+// equal to that trigger, as long as the only differences are variable
+
+predicate P(x: int, y: int)
+predicate Q(x: int)
+
+method Test(z: int) {
+  // P(x, y) and P(y, x) might look like they would cause a loop. Since they
+  // only differ by their variables, though, they won't raise flags.
+  assume forall x: int, y: int :: P(x, y) == P(y, x);
+
+  // This works independent of extra parentheses:
+  assume forall x: int, y: int :: P(x, y) == (P(y, x));
+
+  // Contrast with the following:
+  assume forall x: int, y: int :: P(x, y) == P(x, y+1);
+
+  // The following examples were made legal after an exchange where Chris
+  // pointed examples in the IronClad sources where things like this were
+  // incorrectly flagged.
+  assert forall x :: true || Q(x) || Q(0);
+  assert forall x :: true || Q(x) || Q(z);
+  assert forall x :: true || P(x, 1) || P(x, z);
+
+  // Support for the following was added following a discussion with Rustan; in
+  // the second one the expression `if z > 1 then z else 3 * z + 1` is not
+  // directly a constant expression, but it does not involve x, so it's ok:
+  assert forall x :: true || Q(x) || Q(0+1);
+  assert forall x :: true || Q(x) || Q(if z > 1 then z else 3 * z + 1);
+  // Sanity check:
+  assert forall x :: true || Q(x) || Q(if z > 1 then x else 3 * z + 1);
+
+  // WISH: It might also be good to zeta-reduce before loop detection.
+  assert forall x :: true || Q(x) || (var xx := x+1; Q(xx));
+}
diff --git a/Test/triggers/loop-detection-is-not-too-strict.dfy.expect b/Test/triggers/loop-detection-is-not-too-strict.dfy.expect
new file mode 100644
index 00000000..65ea0d79
--- /dev/null
+++ b/Test/triggers/loop-detection-is-not-too-strict.dfy.expect
@@ -0,0 +1,17 @@
+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(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(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 b/Test/triggers/loop-detection-looks-at-ranges-too.dfy
new file mode 100644
index 00000000..7a99ea2d
--- /dev/null
+++ b/Test/triggers/loop-detection-looks-at-ranges-too.dfy
@@ -0,0 +1,14 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// This file checks that loops between the range and the term of a quantifier
+// are properly detected.
+
+predicate P(x: int)
+
+method M(x: int) {
+  // This will be flagged as a loop even without looking at the range
+  assert true || forall x: int | P(x) :: P(x+1);
+  // This requires checking the range for looping terms
+  assert true || forall x: int | P(x+1) :: P(x);
+}
diff --git a/Test/triggers/loop-detection-looks-at-ranges-too.dfy.expect b/Test/triggers/loop-detection-looks-at-ranges-too.dfy.expect
new file mode 100644
index 00000000..a32e4a60
--- /dev/null
+++ b/Test/triggers/loop-detection-looks-at-ranges-too.dfy.expect
@@ -0,0 +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.
+
+Dafny program verifier finished with 3 verified, 0 errors
diff --git a/Test/triggers/loop-detection-messages--unit-tests.dfy b/Test/triggers/loop-detection-messages--unit-tests.dfy
new file mode 100644
index 00000000..c1560317
--- /dev/null
+++ b/Test/triggers/loop-detection-messages--unit-tests.dfy
@@ -0,0 +1,29 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// This file is a series of basic tests for loop detection, focusing on the
+// warnings and information messages
+
+function f(i: int): int
+function g(i: int): int
+
+method M() {
+  assert forall i :: false ==> f(i) == f(f(i));
+  assert forall i :: false ==> f(i) == f(i+1);
+  assert forall i {:matchingloop} :: false ==> f(i) == f(i+1);
+
+  assert forall i :: false ==> f(i) == f(i+1) && f(i) == g(i);
+  assert forall i :: false ==> f(i) == f(i+1) && f(i) == f(i);
+  assert forall i {:matchingloop} :: false ==> f(i) == f(i+1) && f(i) == f(i);
+
+  assert forall i :: false ==> f(i) == 0;
+  assert forall i :: false ==> f(i+1) == 0;
+  assert forall i {:autotriggers false} :: false ==> f(i+1) == 0;
+
+  assert forall i, j: int :: false ==> f(i) == f(j);
+  assert forall i, j: int :: false ==> f(i) == f(i);
+  assert forall i, j: int :: false ==> f(i) == f(i) && g(j) == 0;
+  assert forall i, j: int :: false ==> f(i) == f(i) && g(j+1) == 0;
+  assert forall i, j: int {:autotriggers false} :: false ==> f(i) == f(i);
+  assert forall i, j: int {:trigger f(i), g(j)} :: false ==> f(i) == f(i);
+}
diff --git a/Test/triggers/loop-detection-messages--unit-tests.dfy.expect b/Test/triggers/loop-detection-messages--unit-tests.dfy.expect
new file mode 100644
index 00000000..eba8c179
--- /dev/null
+++ b/Test/triggers/loop-detection-messages--unit-tests.dfy.expect
@@ -0,0 +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)":
+   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)":
+   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)":
+   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)":
+   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". 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)":
+   Selected triggers: {g(j), f(i)}
+loop-detection-messages--unit-tests.dfy(25,9): Info: For expression "false ==> g(j) == 0":
+   Selected triggers: {g(j), f(i)}
+loop-detection-messages--unit-tests.dfy(26,9): Warning: For expression "false ==> f(i) == f(i)":
+   /!\ No trigger covering all quantified variables found.
+loop-detection-messages--unit-tests.dfy(26,9): Warning: For expression "false ==> g(j + 1) == 0":
+   /!\ No trigger covering all quantified variables found.
+loop-detection-messages--unit-tests.dfy(27,9): Info: Not generating triggers for "false ==> f(i) == f(i)". 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 b/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy
new file mode 100644
index 00000000..c54089f2
--- /dev/null
+++ b/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy
@@ -0,0 +1,32 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// This file shows cases where loops could hide behind equalities. In all three
+// cases we behave the same; that is, we don't warn for loops that would only
+// exist in the presence of an equality. The easiest way to understand the
+// issue, I (CPC) feel, is to look at the old case: f(x) could very well loop
+// with old(f(f(x))) if f(f(x)) did not change the heap at all.
+
+// This equality issue is generally undecidable. It could make sense to special
+// case `old`, but KRML and CPC decided against it on 2015-08-21. Future
+// experiences could cause a change of mind.
+
+class C { }
+function f(c: C): C
+function g(c: C): C
+function h(c: C, i: int): C
+
+// With explicit arguments
+method M0(i: int, j: int, sc: set<C>) {
+  assert forall c | c in sc :: true || h(c, i) == h(h(c, j), j);
+}
+
+// With implicit arguments (f and g respectively, to Apply)
+method M1(f: int -> int, g: int -> int) {
+  assert forall x :: true || f(x) == g(f(x));
+}
+
+// With implicit arguments (the heap, to old)
+method M2(sc: set<C>) {
+  assert forall c | c in sc :: true || f(c) == old(f(f(c)));
+}
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
new file mode 100644
index 00000000..e900c1f9
--- /dev/null
+++ b/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy.expect
@@ -0,0 +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)")
+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)))")
+
+Dafny program verifier finished with 9 verified, 0 errors
diff --git a/Test/triggers/matrix-accesses-are-triggers.dfy b/Test/triggers/matrix-accesses-are-triggers.dfy
new file mode 100644
index 00000000..630fab9d
--- /dev/null
+++ b/Test/triggers/matrix-accesses-are-triggers.dfy
@@ -0,0 +1,9 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// This file checks that multi-dimensional array accesses yield trigger candidates
+
+method M(m: array2<int>)
+  requires m != null
+  requires forall i, j | 0 <= i < m.Length0 && 0 <= j < m.Length1 :: m[i, j] == m[j, i+1] {
+}
diff --git a/Test/triggers/matrix-accesses-are-triggers.dfy.expect b/Test/triggers/matrix-accesses-are-triggers.dfy.expect
new file mode 100644
index 00000000..572fc41f
--- /dev/null
+++ b/Test/triggers/matrix-accesses-are-triggers.dfy.expect
@@ -0,0 +1,12 @@
+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
+    (0,0): anon4_Then
+matrix-accesses-are-triggers.dfy(8,86): Error: index 1 out of range
+Execution trace:
+    (0,0): anon0
+    (0,0): anon4_Then
+
+Dafny program verifier finished with 1 verified, 2 errors
diff --git a/Test/triggers/nested-quantifiers-all-get-triggers.dfy b/Test/triggers/nested-quantifiers-all-get-triggers.dfy
new file mode 100644
index 00000000..a55019db
--- /dev/null
+++ b/Test/triggers/nested-quantifiers-all-get-triggers.dfy
@@ -0,0 +1,9 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// This checks that nested quantifiers do get triggers, and that the parent
+// quantifier does not get annotated twice
+
+method M() {
+  ghost var x := forall s: set<int>, x: int :: (x in s ==> forall y :: y == x ==> y in s);
+}
diff --git a/Test/triggers/nested-quantifiers-all-get-triggers.dfy.expect b/Test/triggers/nested-quantifiers-all-get-triggers.dfy.expect
new file mode 100644
index 00000000..172f5607
--- /dev/null
+++ b/Test/triggers/nested-quantifiers-all-get-triggers.dfy.expect
@@ -0,0 +1,4 @@
+nested-quantifiers-all-get-triggers.dfy(8,17): Info: Selected triggers: {x in s}
+nested-quantifiers-all-get-triggers.dfy(8,59): Info: Selected triggers: {y in s}
+
+Dafny program verifier finished with 2 verified, 0 errors
diff --git a/Test/triggers/old-is-a-special-case-for-triggers.dfy b/Test/triggers/old-is-a-special-case-for-triggers.dfy
new file mode 100644
index 00000000..4424e8d3
--- /dev/null
+++ b/Test/triggers/old-is-a-special-case-for-triggers.dfy
@@ -0,0 +1,32 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// This file ensures that `old()` receives the special treatment that it
+// requires; that is, `old(f(x))` is not less liberal than `f(x)`, and
+// old(f(f(x))) does not loop with f(x) (doesn't it?)
+
+class C { }
+function f(c: C): C
+function g(c: C): C
+function h(c: C, i: int): C
+
+method M(sc: set<C>)
+  // Ensure that old(c) does not get picked as a trigger
+  ensures forall c | c in sc :: true || c == old(f(c))
+
+  // This checks whether loop detection handles `old` expressions properly.
+  // In the first one f(c)/old(f(f(c))) is not reported as a loop. See
+  // looping-is-hard-to-decide-modulo-equalities.dfy for an explanation.
+  ensures forall c | c in sc :: true || f(c) == old(f(f(c)))
+  ensures forall c | c in sc :: true || old(f(f(c))) == old(g(f(c))) || old(f(g(c))) == g(f(c)) || f(g(c)) == g(f(c))
+
+  // These check that the final trigger filtering step doesn't get confused
+  // between old expressions and regular expressions.
+  ensures forall c | c in sc :: true || f(c) == old(g(f(c)))
+  ensures forall c | c in sc :: true || f(c) == old(f(c)) || old(g(f(c))) == g(f(c))
+
+  // WISH: A Dafny rewriter could cleanup expressions so that adding the
+  //       expression forall c :: c == old(c) in a quantifier would cause a warning,
+  //       instead of a trigger generation error as it does now.
+{
+}
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
new file mode 100644
index 00000000..7388a911
--- /dev/null
+++ b/Test/triggers/old-is-a-special-case-for-triggers.dfy.expect
@@ -0,0 +1,22 @@
+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)))")
+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)))")
+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))})
+old-is-a-special-case-for-triggers.dfy(26,10): Info: Selected triggers:
+   {old(f(c))}, {f(c)}, {c in sc}
+ Rejected triggers:
+   {g(f(c))} (more specific than {f(c)})
+   {old(g(f(c)))} (more specific than {old(f(c))})
+
+Dafny program verifier finished with 5 verified, 0 errors
diff --git a/Test/triggers/redundancy-detection-is-bidirectional.dfy b/Test/triggers/redundancy-detection-is-bidirectional.dfy
new file mode 100644
index 00000000..06541b70
--- /dev/null
+++ b/Test/triggers/redundancy-detection-is-bidirectional.dfy
@@ -0,0 +1,29 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// This test checks for tricky cases of redundancy suppression when building
+// triggers.
+
+predicate P(x: int, y: int)
+predicate Q(x: int)
+predicate R(x: int)
+
+method M() {
+  // For this term, it is enough to order the terms by number of variables
+  assert forall x, y :: true || P(x, y) || Q(y) || R(x);
+  assert forall x, y :: true || Q(y) || P(x, y) || R(x);
+  assert forall x, y :: true || Q(y) || R(x) || P(x, y);
+}
+
+predicate PP(x: int, y: int, z: int)
+predicate QQ(x: int, y: int)
+predicate RR(x: int, y: int)
+predicate SS(x: int, y: int)
+
+method MM() {
+  // Not for this one, though
+  assert forall x, y, z, u, v, w :: true || PP(x, y, z) || QQ(x, u) || RR(y, v) || SS(z, w);
+  assert forall x, y, z, u, v, w :: true || QQ(x, u) || PP(x, y, z) || RR(y, v) || SS(z, w);
+  assert forall x, y, z, u, v, w :: true || QQ(x, u) || RR(y, v) || PP(x, y, z) || SS(z, w);
+  assert forall x, y, z, u, v, w :: true || QQ(x, u) || RR(y, v) || SS(z, w) || PP(x, y, z);
+}
diff --git a/Test/triggers/redundancy-detection-is-bidirectional.dfy.expect b/Test/triggers/redundancy-detection-is-bidirectional.dfy.expect
new file mode 100644
index 00000000..78c9e7ca
--- /dev/null
+++ b/Test/triggers/redundancy-detection-is-bidirectional.dfy.expect
@@ -0,0 +1,12 @@
+redundancy-detection-is-bidirectional.dfy(13,9): Info: Selected triggers:
+   {R(x), Q(y)}, {P(x, y)}
+redundancy-detection-is-bidirectional.dfy(14,9): Info: Selected triggers:
+   {R(x), Q(y)}, {P(x, y)}
+redundancy-detection-is-bidirectional.dfy(15,9): Info: Selected triggers:
+   {P(x, y)}, {R(x), Q(y)}
+redundancy-detection-is-bidirectional.dfy(25,9): Info: Selected triggers: {SS(z, w), RR(y, v), QQ(x, u)}
+redundancy-detection-is-bidirectional.dfy(26,9): Info: Selected triggers: {SS(z, w), RR(y, v), QQ(x, u)}
+redundancy-detection-is-bidirectional.dfy(27,9): Info: Selected triggers: {SS(z, w), RR(y, v), QQ(x, u)}
+redundancy-detection-is-bidirectional.dfy(28,9): Info: Selected triggers: {SS(z, w), RR(y, v), QQ(x, u)}
+
+Dafny program verifier finished with 11 verified, 0 errors
diff --git a/Test/triggers/regression-tests.dfy b/Test/triggers/regression-tests.dfy
new file mode 100644
index 00000000..263e424a
--- /dev/null
+++ b/Test/triggers/regression-tests.dfy
@@ -0,0 +1,20 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// This tests checks that quantifier splitting is resilient to the fact that
+// certain statements (like calc) can return duplicate subexpressions. This was
+// once a problem, because a quantifier that got returned twice would get split
+// on the first pass over it, and would have its nely created children re-split
+// on the second pass. This created a split quantifier whose children were split
+// quantifiers, which violated an invariant of spliit quantifiers.
+
+abstract module Base { }
+
+module Blah refines Base {
+  lemma A() {
+    calc {
+	    forall b :: b;
+   	}
+  }
+}
+
diff --git a/Test/triggers/regression-tests.dfy.expect b/Test/triggers/regression-tests.dfy.expect
new file mode 100644
index 00000000..e780e966
--- /dev/null
+++ b/Test/triggers/regression-tests.dfy.expect
@@ -0,0 +1,3 @@
+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/set-construction-is-a-good-trigger.dfy b/Test/triggers/set-construction-is-a-good-trigger.dfy
new file mode 100644
index 00000000..b3dee172
--- /dev/null
+++ b/Test/triggers/set-construction-is-a-good-trigger.dfy
@@ -0,0 +1,12 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// This file ensures that display expressions can be picked as triggers. This is
+// useful for code that checks if a set, sequence, or multiset is a singleton.
+
+method M(s: seq<int>, st: set<int>, mst: multiset<int>)
+  requires exists y :: s == [y]           // Seq#Build(Seq#Empty(): Seq Box, $Box(y#3))
+  requires exists y :: st == {y}          // Set#UnionOne(Set#Empty(): Set Box, $Box(y#4))
+  requires exists y :: mst == multiset{y} // MultiSet#UnionOne(MultiSet#Empty(): MultiSet Box, $Box(y#5))
+{
+}
diff --git a/Test/triggers/set-construction-is-a-good-trigger.dfy.expect b/Test/triggers/set-construction-is-a-good-trigger.dfy.expect
new file mode 100644
index 00000000..822b8498
--- /dev/null
+++ b/Test/triggers/set-construction-is-a-good-trigger.dfy.expect
@@ -0,0 +1,5 @@
+set-construction-is-a-good-trigger.dfy(8,11): Info: Selected triggers: {[y]}
+set-construction-is-a-good-trigger.dfy(9,11): Info: Selected triggers: {{y}}
+set-construction-is-a-good-trigger.dfy(10,11): Info: Selected triggers: {multiset{y}}
+
+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..bc2e0934
--- /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 use
+// /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 b/Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy
new file mode 100644
index 00000000..d7636ea2
--- /dev/null
+++ b/Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy
@@ -0,0 +1,16 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// This file shows how Dafny detects loops even for terms that are not literal
+// AST matches. This file also checks that triggers are reported exactly as
+// picked (that is, `x in s` yields `s[x]` for a multiset s), but matches as
+// they appear in the buffer text (that is, `x+1 in s` is not translated to
+// s[x+1] when highlited as a cause for a potential matching loop.
+
+method M() {
+  // This is an obvious loop
+  ghost var b := forall s: multiset<int>, x: int :: s[x] > 0 ==> s[x+1] > 0;
+
+  // x in s loops with s[x+1] due to the way [x in s] is translated
+  ghost var a := forall s: multiset<int>, x: int :: x in s ==> s[x+1] > 0 && x+2 !in s;
+}
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
new file mode 100644
index 00000000..1a143edb
--- /dev/null
+++ b/Test/triggers/some-terms-do-not-look-like-the-triggers-they-match.dfy.expect
@@ -0,0 +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.
+
+Dafny program verifier finished with 2 verified, 0 errors
diff --git a/Test/triggers/splitting-picks-the-right-tokens.dfy b/Test/triggers/splitting-picks-the-right-tokens.dfy
new file mode 100644
index 00000000..76065eca
--- /dev/null
+++ b/Test/triggers/splitting-picks-the-right-tokens.dfy
@@ -0,0 +1,24 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// This file ensures that trigger splitting picks the right tokens
+
+function Id(i: int): int { i }
+
+method MSuchThat()
+  requires forall x | x > 0 :: Id(x) > 1 && x > 2 && x > -1 { }
+
+method MImplies()
+  // The bodies of the two terms that are produced here are both
+  // BinaryExpressions(==>); the token they use, however, is that of the RHS
+  // terms of these implications; otherwise, error messages would get stacked on
+  // the ==> sign
+  requires forall x :: x > 0 ==> Id(x) > 1 && x > 2 && x > -1 { }
+
+method M() {
+  if * {
+    MImplies();
+  } else {
+    MSuchThat();
+  }
+}
diff --git a/Test/triggers/splitting-picks-the-right-tokens.dfy.expect b/Test/triggers/splitting-picks-the-right-tokens.dfy.expect
new file mode 100644
index 00000000..f01ed1a0
--- /dev/null
+++ b/Test/triggers/splitting-picks-the-right-tokens.dfy.expect
@@ -0,0 +1,38 @@
+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":
+   Selected triggers: {Id(x)}
+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":
+   Selected triggers: {Id(x)}
+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":
+   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.
+splitting-picks-the-right-tokens.dfy(16,48): Related location
+Execution trace:
+    (0,0): anon0
+    (0,0): anon3_Then
+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.
+splitting-picks-the-right-tokens.dfy(16,39): Related location
+Execution trace:
+    (0,0): anon0
+    (0,0): anon3_Then
+splitting-picks-the-right-tokens.dfy(22,13): Error BP5002: A precondition for this call might not hold.
+splitting-picks-the-right-tokens.dfy(9,11): Related location: This is the precondition that might not hold.
+splitting-picks-the-right-tokens.dfy(9,46): Related location
+Execution trace:
+    (0,0): anon0
+    (0,0): anon3_Else
+splitting-picks-the-right-tokens.dfy(22,13): Error BP5002: A precondition for this call might not hold.
+splitting-picks-the-right-tokens.dfy(9,11): Related location: This is the precondition that might not hold.
+splitting-picks-the-right-tokens.dfy(9,37): Related location
+Execution trace:
+    (0,0): anon0
+    (0,0): anon3_Else
+
+Dafny program verifier finished with 6 verified, 4 errors
diff --git a/Test/triggers/splitting-triggers-recovers-expressivity.dfy b/Test/triggers/splitting-triggers-recovers-expressivity.dfy
new file mode 100644
index 00000000..dd1bd81d
--- /dev/null
+++ b/Test/triggers/splitting-triggers-recovers-expressivity.dfy
@@ -0,0 +1,61 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+predicate P(i: int)
+predicate Q(i: int)
+
+/* This file demonstrates a case where automatic trigger splitting is useful to
+   prevent loop detection from reducing expressivity too much. */
+
+lemma exists_0()
+  requires P(0)
+  ensures exists i {:split false} :: P(i) || (Q(i) ==> P(i+1)) {
+    // Fails: P(i) is not a trigger
+}
+
+lemma forall_0(i: int)
+  requires forall j {:split false} :: j >= 0 ==> (P(j) && (Q(j) ==> P(j+1)))
+  requires i >= 0
+  ensures P(i) {
+    // Fails: P(i) is not a trigger
+}
+
+
+lemma exists_1()
+  requires P(0)
+  ensures exists i {:split false} :: P(i) || (Q(i) ==> P(i+1)) {
+    assert Q(0) || !Q(0);
+    // Works: the dummy assertion introduces a term that causes the quantifier
+    // to trigger, producing a witness.
+  }
+
+lemma forall_1(i: int)
+  requires forall j {:split false} :: j >= 0 ==> (P(j) && (Q(j) ==> P(j+1)))
+  requires i >= 0
+  ensures P(i) {
+    assert Q(i) || !Q(i);
+    // Works: the dummy assertion introduces a term that causes the quantifier
+    // to trigger, producing a witness.
+}
+
+
+lemma exists_2()
+  requires P(0)
+  ensures exists i :: P(i) || (Q(i) ==> P(i+1)) {
+    // Works: automatic trigger splitting allows P(i) to get its own triggers
+}
+
+lemma forall_2(i: int)
+  requires forall j :: j >= 0 ==> (P(j) && (Q(j) ==> P(j+1)))
+  requires i >= 0
+  ensures P(i) {
+    // Works: automatic trigger splitting allows P(i) to get its own triggers
+}
+
+
+lemma loop()
+  requires P(0)
+  requires forall i {:matchingloop} :: i >= 0 ==> Q(i) && (P(i) ==> P(i+1))
+  ensures P(100) {
+    // Works: the matching loop is explicitly allowed
+}
diff --git a/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect b/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect
new file mode 100644
index 00000000..a8bb2345
--- /dev/null
+++ b/Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect
@@ -0,0 +1,39 @@
+splitting-triggers-recovers-expressivity.dfy(12,10): Info: Selected triggers: {Q(i)}
+ 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)")
+splitting-triggers-recovers-expressivity.dfy(26,10): Info: Selected triggers: {Q(i)}
+ 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)":
+   Selected triggers:
+     {Q(i)}, {P(i)}
+splitting-triggers-recovers-expressivity.dfy(44,10): Info: For expression "!Q(i)":
+   Selected triggers:
+     {Q(i)}, {P(i)}
+splitting-triggers-recovers-expressivity.dfy(44,10): Info: For expression "P(i + 1)":
+   Selected triggers: {Q(i)}
+   Rejected triggers: {P(i)} (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)":
+   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)":
+   Selected triggers:
+     {P(i)}, {Q(i)}
+splitting-triggers-recovers-expressivity.dfy(58,11): Info: For expression "i >= 0 ==> P(i) ==> P(i + 1)":
+   Selected triggers:
+     {P(i)} (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:
+    (0,0): anon0
+splitting-triggers-recovers-expressivity.dfy(19,15): Error BP5003: A postcondition might not hold on this return path.
+splitting-triggers-recovers-expressivity.dfy(19,10): Related location: This is the postcondition that might not hold.
+Execution trace:
+    (0,0): anon0
+
+Dafny program verifier finished with 14 verified, 2 errors
diff --git a/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy b/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy
new file mode 100644
index 00000000..20e90843
--- /dev/null
+++ b/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.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 tests shows that, since quantifiers are split, it becomes possible to know more precisely what part of a precondition did not hold at the call site.
+
+method f()
+  requires forall y :: y > 0 && y < 0 {
+}
+
+method g(x: int) {
+  f();
+}
+
+function gf(): int
+  requires forall y :: y > 0 && y < 0 {
+    1
+}
+
+function gg(x: int): int {
+  gf()
+}
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..27548ac9
--- /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
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/triggers-prevent-some-inlining.dfy b/Test/triggers/triggers-prevent-some-inlining.dfy
new file mode 100644
index 00000000..90af62a3
--- /dev/null
+++ b/Test/triggers/triggers-prevent-some-inlining.dfy
@@ -0,0 +1,26 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// This  file looks  at the  interactions  between inlining  and triggers.   The
+// sum_is_sum predicate gets a {sum(a,  b)} trigger, which explicitly depends on
+// one of the  variables being passed in. Since triggers  are generated prior to
+// inlining  (inlining  happens  during  translation),  inlining  the  last  two
+// instances of that call below would cause  b+1 (a trigger killer) to pop up in
+// a trigger.   This would create  an invalid trigger,  so Dafny doesn't  let it
+// happen.
+
+function sum(a: int, b: int): int {
+  a + b
+}
+
+predicate sum_is_sum(b: int, c: int) {
+  forall a: int :: sum(a, b) + c == a + b + c
+}
+
+method can_we_inline(b: int, c: int)
+  ensures sum_is_sum(0, 0)     // OK  to inline
+  ensures sum_is_sum(b, c)     // OK  to inline
+  ensures sum_is_sum(b, c+1)   // OK  to inline
+  ensures sum_is_sum(b+1, c)   // NOK to inline
+  ensures sum_is_sum(b+1, c+1) // NOK to inline
+{ }
diff --git a/Test/triggers/triggers-prevent-some-inlining.dfy.expect b/Test/triggers/triggers-prevent-some-inlining.dfy.expect
new file mode 100644
index 00000000..0b6f3e30
--- /dev/null
+++ b/Test/triggers/triggers-prevent-some-inlining.dfy.expect
@@ -0,0 +1,9 @@
+triggers-prevent-some-inlining.dfy(17,2): Info: Selected triggers: {sum(a, b)}
+triggers-prevent-some-inlining.dfy(24,10): Info: Some instances of this call cannot safely be inlined.
+triggers-prevent-some-inlining.dfy(25,10): Info: Some instances of this call cannot safely be inlined.
+triggers-prevent-some-inlining.dfy(24,10): Info: Some instances of this call cannot safely be inlined.
+triggers-prevent-some-inlining.dfy(25,10): Info: Some instances of this call cannot safely be inlined.
+triggers-prevent-some-inlining.dfy(24,10): Info: Some instances of this call cannot safely be inlined.
+triggers-prevent-some-inlining.dfy(25,10): Info: Some instances of this call cannot safely be inlined.
+
+Dafny program verifier finished with 4 verified, 0 errors
diff --git a/Test/triggers/useless-triggers-are-removed.dfy b/Test/triggers/useless-triggers-are-removed.dfy
new file mode 100644
index 00000000..658890f2
--- /dev/null
+++ b/Test/triggers/useless-triggers-are-removed.dfy
@@ -0,0 +1,25 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// This file ensures that Dafny does get rid of redundant triggers before
+// annotating a quantifier, and that ths process does not interfere with cycle
+// detection.
+
+function f(x: int): int
+function g(x: int): int
+function h(x: int): int
+
+method M()
+  // In the following, only f(x) is kept. Note that the subset enumeration was
+  // already smart enough to not build any trigger with multiple terms (it only
+  // built 5 candidates)
+  requires forall x: int :: f(x) + g(f(x)) + h(f(x)) + g(h(f(x))) + h(g(f(x))) == 0
+
+  // Loop detection still works fine: in the following example, the trigger is
+  // f(f(x))
+  requires forall x: int :: f(x) == f(f(x))
+
+  // This works for multi-triggers, too:
+  requires forall x, y :: f(x) + g(f(y)) + g(y) + g(f(x)) == 0
+{
+}
diff --git a/Test/triggers/useless-triggers-are-removed.dfy.expect b/Test/triggers/useless-triggers-are-removed.dfy.expect
new file mode 100644
index 00000000..d6b49a9e
--- /dev/null
+++ b/Test/triggers/useless-triggers-are-removed.dfy.expect
@@ -0,0 +1,17 @@
+useless-triggers-are-removed.dfy(16,11): Info: Selected triggers: {f(x)}
+ Rejected triggers:
+   {h(g(f(x)))} (more specific than {g(f(x))}, {f(x)})
+   {g(h(f(x)))} (more specific than {h(f(x))}, {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))")
+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(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)})
+
+Dafny program verifier finished with 5 verified, 0 errors
diff --git a/Test/triggers/wf-checks-use-the-original-quantifier.dfy b/Test/triggers/wf-checks-use-the-original-quantifier.dfy
new file mode 100644
index 00000000..a1a2bd90
--- /dev/null
+++ b/Test/triggers/wf-checks-use-the-original-quantifier.dfy
@@ -0,0 +1,28 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// This test checks that typical expressions requiring WF checks do not suddenly
+// loose expressivity due to quantifier splitting. Without special care, the
+// expression (forall x :: x != null && x.a == 0) could fail to verify.
+
+// 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.
+
+// Of course, the assumption that WF checks produce for a quantifier is a
+// quantifier, so the assumption part that comes after the WF check does use the
+// split expression.
+
+// This test case is inspired by the example that Chris gave.
+
+predicate P(b: nat)
+function f(a: int): int
+class C { var x: int; }
+
+method M(s: set<C>)
+  requires forall n: nat :: 0 <= f(n) && P(f(n))
+  requires forall c, c' | c in s && c' in s :: c != null && c'!= null && c.x == c'.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
new file mode 100644
index 00000000..6c3e4853
--- /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