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