Fix array refinement: use actual SAT model values in get()#8842
Fix array refinement: use actual SAT model values in get()#8842tautschnig wants to merge 2 commits intodiffblue:developfrom
Conversation
tautschnig
requested review from
kroening,
martin-cs and
peterschrammel
as code owners
There was a problem hiding this comment.
Pull request overview
This PR fixes two bugs in the array refinement mechanism that prevented detection of spurious counterexamples. The first bug caused boolbvt::get() to symbolically evaluate sub-expressions instead of returning actual SAT model values for expressions in the bitvector cache. The second bug caused MiniSat crashes during refinement because freeze_lazy_constraints() didn't freeze intermediate variables created by convert().
Changes:
- Modified
boolbvt::get()to return actual model values viabv_get()when expressions are in the bitvector cache - Updated
freeze_lazy_constraints()to pre-convert and freeze the full constraint literal along with intermediate variables - Changed Array_UF4 and Array_UF8 test statuses from KNOWNBUG to CORE
Reviewed changes
Copilot reviewed 4 out of 4 changed files in this pull request and generated no comments.
| File | Description |
|---|---|
| src/solvers/flattening/boolbv_get.cpp | Added logic to return actual SAT model values for cached bitvector expressions instead of symbolic evaluation |
| src/solvers/refinement/refine_arrays.cpp | Added constraint literal conversion and freezing to prevent variable elimination during refinement |
| regression/cbmc/Array_UF4/test.desc | Changed test status from KNOWNBUG to CORE |
| regression/cbmc/Array_UF8/test.desc | Changed test status from KNOWNBUG to CORE |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## develop #8842 +/- ##
========================================
Coverage 80.00% 80.00%
========================================
Files 1700 1700
Lines 188252 188271 +19
Branches 73 73
========================================
+ Hits 150613 150630 +17
- Misses 37639 37641 +2 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
|
What bugs me a bit about item 1. is that the behaviour of |
I don't know whether I'd use the term "caching decisions" here - we, after all, "cache" everything that we convert, which, in absence of refinement, is everything. With refinement, it's more of a "refinement" decision rather than a "caching" decision I'd say? |
Indeed we do now -- however, we may not wish to do so in the future, and hence, I would rather not promise this feature to users of |
Two bugs prevented the array refinement loop from detecting spurious counterexamples: 1. boolbvt::get() for non-symbol expressions (e.g., array index expressions like a[i]) fell through to prop_conv_solvert::get() which symbolically evaluated sub-expressions. For with-expressions, this symbolic evaluation produced the 'correct' value, masking inconsistencies in the actual SAT model. Fix: when an expression is in the bitvector cache (i.e., it was converted to SAT variables), return the actual model value via bv_get(). 2. freeze_lazy_constraints() only froze the symbols appearing in lazy constraints, but not the intermediate variables created by convert(). When the refinement loop later called convert() on a violated constraint, MiniSat crashed because some variables had been eliminated. Fix: pre-convert and freeze the full constraint literal during freeze_lazy_constraints(). These fixes resolve Array_UF4 and Array_UF8 which were marked as KNOWNBUG. Co-authored-by: Kiro
get() should not have its behaviour depend on whether an expression was previously converted (cached in bv_cache). Instead, add a dedicated get_value() method to boolbvt that checks the bitvector cache before falling back to recursive evaluation. Use get_value() in arrays_overapproximated() so that the refinement loop reads actual SAT model values for converted expressions (e.g., array index expressions) rather than symbolically evaluating with-expressions, which can mask inconsistencies in the SAT model. Co-authored-by: Kiro
tautschnig
force-pushed
the
arrays/refine-get
branch
from
468b7fa to
6ff2ce4
Compare
Added a second commit to implement this. (And revert the prior use of |
3 participants
Two bugs prevented the array refinement loop from detecting spurious counterexamples:
boolbvt::get() for non-symbol expressions (e.g., array index expressions like a[i]) fell through to prop_conv_solvert::get() which symbolically evaluated sub-expressions. For with-expressions, this symbolic evaluation produced the 'correct' value, masking inconsistencies in the actual SAT model. Fix: when an expression is in the bitvector cache (i.e., it was converted to SAT variables), return the actual model value via bv_get().
freeze_lazy_constraints() only froze the symbols appearing in lazy constraints, but not the intermediate variables created by convert(). When the refinement loop later called convert() on a violated constraint, MiniSat crashed because some variables had been eliminated. Fix: pre-convert and freeze the full constraint literal during freeze_lazy_constraints().
These fixes resolve Array_UF4 and Array_UF8 which were marked as KNOWNBUG.
Co-authored-by: Kiro