Add tests for quantifier splitting and trigger generation

1 files changed, 26 insertions, 0 deletions

diff --git a/Test/triggers/triggers-prevent-some-inlining.dfy b/Test/triggers/triggers-prevent-some-inlining.dfy
new file mode 100644
index 00000000..04b8051c
--- /dev/null
+++ b/Test/triggers/triggers-prevent-some-inlining.dfy
@@ -0,0 +1,26 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"

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

+

+// This  file looks  at the  interactions  between inlining  and triggers.   The

+// sum_is_sum predicate gets a {sum(a,  b)} trigger, which explicitly depends on

+// one of the  variables being passed in. Since triggers  are generated prior to

+// inlining  (inlining  happens  during  translation),  inlining  the  last  two

+// instances of that call below would cause  b+1 (a trigger killer) to pop up in

+// a trigger.   This would create  an invalid trigger,  so Dafny doesn't  let it

+// happen.

+

+function sum(a: int, b: int): int {

+  a + b

+}

+

+predicate sum_is_sum(b: int, c: int) {

+  forall a: int :: sum(a, b) + c == a + b + c

+}

+

+method can_we_inline(b: int, c: int)

+  ensures sum_is_sum(0, 0)     // OK  to inline

+  ensures sum_is_sum(b, c)     // OK  to inline

+  ensures sum_is_sum(b, c+1)   // OK  to inline

+  ensures sum_is_sum(b+1, c)   // NOK to inline

+  ensures sum_is_sum(b+1, c+1) // NOK to inline

+{ }