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