mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-05 14:56:11 +00:00
Code Activity

fix: keep only bit_blaster mk_eq optimization from PR #9872

Browse source 
The goal2sat caching optimization (skip caching ref_count<=1 nodes) is
unsafe in general: theory extensions for BV and FP call internalize()
independently from the theory solver side, breaking the assumption that
a singly-referenced node is visited only once.

Keep only the bit_blaster_tpl::mk_eq micro-optimization (reserve+index
instead of push_back), which is semantically correct and safe.

Fixes regressions: t135.smt2, t136.smt2, nl53.smt2, 3397.smt2,
4841-1.smt2, fp-lt-gt.smt2, fp-rem-11.smt2
This commit is contained in:
copilot-swe-agent[bot] 2026-06-16 18:02:42 +00:00 • committed by GitHub
parent b6c7ef2f68
commit b6f7a70a39
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h
View file

@ -768,9 +768,10 @@ void bit_blaster_tpl<Cfg>::mk_smod(unsigned sz, expr * const * a_bits, expr * co
template<typename Cfg> template<typename Cfg>
void bit_blaster_tpl<Cfg>::mk_eq(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref & out) { void bit_blaster_tpl<Cfg>::mk_eq(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref & out) {
expr_ref_vector out_bits(m()); expr_ref_vector out_bits(m());
out_bits.reserve(sz);
for (unsigned i = 0; i < sz; ++i) { for (unsigned i = 0; i < sz; ++i) {
mk_iff(a_bits[i], b_bits[i], out); mk_iff(a_bits[i], b_bits[i], out);
out_bits.push_back(out); out_bits[i] = out;
} }
mk_and(out_bits.size(), out_bits.data(), out); mk_and(out_bits.size(), out_bits.data(), out);
} }