1 files changed, 21 insertions, 0 deletions
diff --git a/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy b/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy
new file mode 100644
index 00000000..20e90843
--- /dev/null
+++ b/Test/triggers/splitting-triggers-yields-better-precondition-related-errors.dfy
@@ -0,0 +1,21 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// This tests shows that, since quantifiers are split, it becomes possible to know more precisely what part of a precondition did not hold at the call site.
+
+method f()
+  requires forall y :: y > 0 && y < 0 {
+}
+
+method g(x: int) {
+  f();
+}
+
+function gf(): int
+  requires forall y :: y > 0 && y < 0 {
+    1
+}
+
+function gg(x: int): int {
+  gf()
+}