BMC with iterative constraint strengthening #805
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
kroening
force-pushed
the
non-incremental-bmc
branch
4 times, most recently
from
5dd0152 to
2f79853
Compare
tautschnig
approved these changes
Nov 13, 2024
| ^EXIT=0$ | ||
| ^SIGNAL=0$ | ||
| ^UNSAT: No counterexample found within bound$ | ||
| ^UNSAT: .*$ |
Collaborator
There was a problem hiding this comment.
Can we use this (or any other) test to exercise bmc-with-assumptions?
| for(auto &h : property.timeframe_handles) | ||
| if(solver.get(h).is_false()) | ||
| return true; | ||
| return false; |
Collaborator
There was a problem hiding this comment.
How about return solver.get(h).is_false();
Collaborator
Author
There was a problem hiding this comment.
That won't work -- note the loop.
kroening
force-pushed
the
non-incremental-bmc
branch
from
2f79853 to
04aff5a
Compare
kroening
changed the title
kroening
force-pushed
the
non-incremental-bmc
branch
3 times, most recently
from
1424e6e to
22964f1
Compare
This implements "iterative constraint strengthening" in the word-level BMC engine (VMCAI 2009, Query-driven Program Testing), and makes it the default. The previous, assumption-based method remains available with --bmc-with-assumptions. When using MiniSat, the benefit on hwmcc08 is barely measurable. When using Cadical, the benefit is around 10%. MiniSat iterative 88.27s MiniSat asumptions 88.73s Cadical iterative 103.41s Cadical asumptions 117.74s
kroening
force-pushed
the
non-incremental-bmc
branch
from
22964f1 to
eab9d87
Compare
Romy15200
pushed a commit
to Romy15200/nws
that referenced
this pull request
Aug 19, 2025
BMC with iterative constraint strengthening
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 implements "iterative constraint strengthening" in the word-level BMC
engine (VMCAI 2009, Query-driven Program Testing), and makes it the default.
The previous, assumption-based method remains available with
--bmc-with-assumptions.When using MiniSat, the benefit on hwmcc08 is barely measurable. When using
Cadical, the benefit is around 10%.
MiniSat iterative 88.27s
MiniSat asumptions 88.73s
Cadical iterative 103.41s
Cadical asumptions 117.74s