Add tests for quantifier splitting and trigger generation

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..0fae8c0e
--- /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 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// This files 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;

+}