1 files changed, 24 insertions, 0 deletions
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();
+  }
+}