1 files changed, 28 insertions, 0 deletions
diff --git a/Test/triggers/wf-checks-use-the-original-quantifier.dfy b/Test/triggers/wf-checks-use-the-original-quantifier.dfy
new file mode 100644
index 00000000..a1a2bd90
--- /dev/null
+++ b/Test/triggers/wf-checks-use-the-original-quantifier.dfy
@@ -0,0 +1,28 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// This test checks that typical expressions requiring WF checks do not suddenly
+// loose expressivity due to quantifier splitting. Without special care, the
+// expression (forall x :: x != null && x.a == 0) could fail to verify.
+
+// The logic about split quantifiers is that Boogie (and z3) should never realize
+// that there was an unsplit quantifier. The WF check code does not produce a
+// quantifier, at least in it's checking part; thus, it should use original
+// quantifier. This fixes a problem in VerifyThis2015/Problem2.dfy with a null
+// check, and a problem spotted by Chris, made into a test case saved in
+// triggers/wf-checks-use-the-original-quantifier.dfy.
+
+// Of course, the assumption that WF checks produce for a quantifier is a
+// quantifier, so the assumption part that comes after the WF check does use the
+// split expression.
+
+// This test case is inspired by the example that Chris gave.
+
+predicate P(b: nat)
+function f(a: int): int
+class C { var x: int; }
+
+method M(s: set<C>)
+  requires forall n: nat :: 0 <= f(n) && P(f(n))
+  requires forall c, c' | c in s && c' in s :: c != null && c'!= null && c.x == c'.x {
+}