Merge commit 'df5c5f5'

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 {

+}