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
+{ }