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.

2 files changed, 45 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 {

+}

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