Cleanup boolbv quantifier instantiation #3926
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
tautschnig
requested review from
kroening,
martin-cs,
peterschrammel,
pkesseli and
smowton
as code owners
tautschnig
force-pushed
the
quantifier-fixes
branch
from
77f1e4c to
019f318
Compare
|
Some of this patchset seems to have been merged elsewhere. Shout when you want a review. |
tautschnig
force-pushed
the
quantifier-fixes
branch
from
019f318 to
5347b3c
Compare
tautschnig
changed the title
|
Rebased and ready for review. |
tautschnig
force-pushed
the
quantifier-fixes
branch
from
5347b3c to
12ab441
Compare
martin-cs
approved these changes
Jan 29, 2019
| @@ -1,4 +1,4 @@ | |||
| KNOWNBUG | |||
| CORE | |||
tautschnig
force-pushed
the
quantifier-fixes
branch
from
12ab441 to
b2d637d
Compare
martin-cs
approved these changes
Jan 30, 2019
tautschnig
force-pushed
the
quantifier-fixes
branch
from
b2d637d to
fdd8dbf
Compare
allredj
reviewed
Jan 30, 2019
There was a problem hiding this comment.
🚫
This PR failed Diffblue compatibility checks (cbmc commit: fdd8dbf).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99098932
Status will be re-evaluated on next push.
Please contact @peterschrammel, @thk123, or @allredj for support.
Common spurious failures:
- the cbmc commit has disappeared in the mean time (e.g. in a force-push)
- the author is not in the list of contributors (e.g. first-time contributors).
The incompatibility may have been introduced by an earlier PR. In that case merging this
PR should be avoided unless it fixes the current incompatibility.
1) Do not take references of temporaries. 2) Instead of post_processing, some expressions can be instantiated and converted immediately. 3) Use skip_typecast rather than local, partial typecast skipping. 4) No need for redundant precondition checks. 5) Mark file-local procedures static.
These can only be omitted when the instantiations trivially make them true. This surfaced further misinterpretations in the regression tests of the "==>" operator: bounded existential quantification should generally use &&.
tautschnig
force-pushed
the
quantifier-fixes
branch
from
fdd8dbf to
38fd81a
Compare
allredj
reviewed
Jan 30, 2019
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: 38fd81a).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/99112022
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This is work-in-progress.