summaryrefslogtreecommitdiff
path: root/Test/triggers/wf-checks-use-the-original-quantifier.dfy.expect
Commit message (Collapse)AuthorAge
* Implement {:nowarn}, clarify some messages, and add a few testsGravatar Clément Pit--Claudel2015-08-28
|
* Adjust WF checks to use unsplit quantifiers.Gravatar Clément Pit--Claudel2015-08-21
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.