Correctly handle SMT solver errors in loop acceleration code #5948
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
SaswatPadhi
requested review from
allredj,
chrisr-diffblue,
hannes-steffenhagen-diffblue,
kroening,
martin-cs,
peterschrammel,
romainbrenguier,
smowton and
tautschnig
as code owners
SaswatPadhi
changed the title
kroening
reviewed
Mar 17, 2021
kroening
reviewed
Mar 17, 2021
SaswatPadhi
force-pushed
the
acceleration_smt_fix
branch
from
72c0f7d to
7f7806b
Compare
|
Build failures would be resolved after fa657ac is merged. |
SaswatPadhi
force-pushed
the
acceleration_smt_fix
branch
from
7f7806b to
1c941a8
Compare
Codecov Report
@@ Coverage Diff @@
## develop #5948 +/- ##
===========================================
+ Coverage 74.24% 75.01% +0.77%
===========================================
Files 1431 1431
Lines 155290 155281 -9
===========================================
+ Hits 115290 116485 +1195
+ Misses 40000 38796 -1204
Continue to review full report at Codecov.
|
SaswatPadhi
force-pushed
the
acceleration_smt_fix
branch
from
1c941a8 to
760bfc1
Compare
|
@kroening @thomasspriggs I have addressed your comments now. Could you please take another look? Thanks. |
kroening
approved these changes
Mar 22, 2021
SaswatPadhi
force-pushed
the
acceleration_smt_fix
branch
from
760bfc1 to
c0b731c
Compare
`check_sat` in scratch_programt was treating UNSAT and ERROR as the same. This was causing SMT solver errors to be silently ignored, and be treated as UNSAT results instead.
SaswatPadhi
force-pushed
the
acceleration_smt_fix
branch
from
c0b731c to
449cab0
Compare
| switch((*checker)()) | ||
| { | ||
| case decision_proceduret::resultt::D_ERROR: | ||
| throw "error running the SMT solver"; |
There was a problem hiding this comment.
Is there a structure exception you could throw instead of a raw string?
chrisr-diffblue
approved these changes
Mar 22, 2021
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.
Related to #5944 and #5947.
This PR correctly handles SMT solver failures in loop acceleration routines. Earlier these errors were silently ignored, and were being treated as UNSAT.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/My commit message includes data points confirming performance improvements (if claimed).White-space or formatting changes outside the feature-related changed lines are in commits of their own.