Work around Z3 not producing models for some quantified expressions#8703
Work around Z3 not producing models for some quantified expressions#8703tautschnig wants to merge 1 commit intodiffblue:developfrom
Conversation
tautschnig
force-pushed
the
trying-to-fix-z3-with-quantifiers
branch
from
b77cf1c to
e92bda3
Compare
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## develop #8703 +/- ##
===========================================
- Coverage 80.41% 80.41% -0.01%
===========================================
Files 1703 1703
Lines 188398 188403 +5
Branches 73 73
===========================================
- Hits 151502 151500 -2
- Misses 36896 36903 +7 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
Z3's solve_eqs preprocessor eliminates symbols defined via (assert (= symbol <quantified-expr>)) by substituting the quantified expression everywhere. This causes get-value to return quantified expressions instead of simple boolean values, which CBMC cannot parse. Using bidirectional implication (assert (=> symbol <expr>)) and (assert (=> <expr> symbol)) instead of equality prevents solve_eqs from recognising this as an elimination opportunity, while preserving the logical equivalence. See Z3Prover/z3#7743 for the upstream bug report. Fixes: diffblue#8679 Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
force-pushed
the
trying-to-fix-z3-with-quantifiers
branch
from
e92bda3 to
bfa6d2d
Compare
tautschnig
requested review from
TGWDB,
kroening,
martin-cs and
peterschrammel
as code owners
There was a problem hiding this comment.
Pull request overview
Works around a Z3 issue where preprocessing can eliminate Boolean symbols whose definitions contain quantifiers, leading to problematic get-value/model extraction behavior (e.g., quantified expressions appearing in counterexamples).
Changes:
- Switch quantifier-containing Boolean “definitions” from a single equality assertion to two implication assertions (bidirectional implication) to avoid Z3’s
solve_eqssubstitution eliminating the symbol. - Add explanatory comments documenting why equality assertions are insufficient in this scenario.
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| out << "(assert (=> "; | ||
| convert_literal(l); | ||
| out << ' '; | ||
| convert_expr(prepared_expr); | ||
| out << "))\n"; | ||
| out << "(assert (=> "; | ||
| convert_expr(prepared_expr); | ||
| out << ' '; | ||
| convert_literal(l); | ||
| out << "))\n"; |
There was a problem hiding this comment.
The quantified expression is emitted twice (once in each implication), which can significantly increase SMT2 output size and slow down both writing and solving for large quantified terms. Consider using a single assert that binds the quantified term once (e.g., via an SMT-LIB let) and then asserts both implications against that binding to avoid duplicating prepared_expr.
| // Z3 refuses get-value when a defined symbol contains a quantifier. | ||
| // Using (assert (= ...)) doesn't help because Z3's solve_eqs | ||
| // preprocessor eliminates the symbol by substituting the quantified | ||
| // expression. Using bidirectional implication instead prevents this. | ||
| if(has_quantifier(prepared_expr)) |
There was a problem hiding this comment.
This change is intended to address a Z3 model/get-value regression involving quantified terms, but the PR description indicates no regression test is included. Please add or update a regression test (e.g., in regression/cbmc/z3/) that reproduces #8679 on affected Z3 versions and demonstrates the workaround prevents quantified terms from appearing in get-value responses / keeps traces readable.
Until the Z3 bug-fix (see Z3Prover/z3#7743) is available widely work around the problem that Z3's preprocessing introduces by adding extra symbols. This may cause solving to take longer, to be determined empirically.
Fixes: #8679