Merge commit 'df5c5f5'

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;

+}