diff options
author | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-21 19:09:37 -0700 |
---|---|---|
committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-21 19:09:37 -0700 |
commit | 84b52a48efda3e9658b772dbc02d34a6f6c9d16b (patch) | |
tree | c5ebcbf04525051ee046197cd46b5d6111d45245 /Test/wishlist/tooltips-on-inductive-lemmas.dfy.expect | |
parent | b41056b45861f6ddb41e2a5e4d7c6d816684f095 (diff) |
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.
Diffstat (limited to 'Test/wishlist/tooltips-on-inductive-lemmas.dfy.expect')
0 files changed, 0 insertions, 0 deletions