Adjust WF checks to use unsplit quantifiers.

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. The issue boiled down to
being able to verify (forall x :: x != null && x.a == 0).

Of course, the assumption that WF checks produce for a quantifier is a
quantifier, so it uses the split expression.

1 files changed, 17 insertions, 0 deletions

diff --git a/Test/triggers/wf-checks-use-the-original-quantifier.dfy.expect b/Test/triggers/wf-checks-use-the-original-quantifier.dfy.expect
new file mode 100644
index 00000000..6b152262
--- /dev/null
+++ b/Test/triggers/wf-checks-use-the-original-quantifier.dfy.expect
@@ -0,0 +1,17 @@
+wf-checks-use-the-original-quantifier.dfy(26,11): Info: For expression {0 <= f(n)}:

+   Selected triggers: {f(n)}

+   Rejected triggers: {P(f(n))} (more specific than {f(n)})

+wf-checks-use-the-original-quantifier.dfy(26,11): Info: For expression {P(f(n))}:

+   Selected triggers: {f(n)}

+   Rejected triggers: {P(f(n))} (more specific than {f(n)})

+wf-checks-use-the-original-quantifier.dfy(27,11): Info: For expression {c != null}:

+   Selected triggers:

+     {c'.x, c.x}, {c'.x, c in s}, {c.x, c' in s}, {c' in s, c in s}

+wf-checks-use-the-original-quantifier.dfy(27,11): Info: For expression {c' != null}:

+   Selected triggers:

+     {c'.x, c.x}, {c'.x, c in s}, {c.x, c' in s}, {c' in s, c in s}

+wf-checks-use-the-original-quantifier.dfy(27,11): Info: For expression {c.x == c'.x}:

+   Selected triggers:

+     {c'.x, c.x}, {c'.x, c in s}, {c.x, c' in s}, {c' in s, c in s}

+

+Dafny program verifier finished with 4 verified, 0 errors