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