From 897c4475af6c075697e4aa9bde3e3d31ac647232 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Tue, 16 Jun 2026 12:09:20 -0600 Subject: [PATCH] =?UTF-8?q?goal2sat:=20drop=20unsafe=20ref=5Fcount?= =?UTF-8?q?=E2=89=A41=20cache-skip=20optimization;=20keep=20bit=5Fblaster?= =?UTF-8?q?=20mk=5Feq=20improvement=20(#9882)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit PR #9872 caused timeouts in QF_UFBV, QF_BV, and QF_FP regressions (`t135`, `t136`, `nl53`, `3397`, `4841-1`, `fp-lt-gt`, `fp-rem-11`). ## Root cause The `goal2sat` change skipped caching AST nodes with `ref_count ≤ 1` under the assumption they're visited only once. This assumption is wrong: EUF, BV, and FP theory extensions all call `internalize()` from the theory solver side, outside the main DFS traversal. On the second `internalize(n)` call, the missing cache entry causes the entire subtree to be re-encoded with a fresh literal — inconsistent encoding and exponential blowup. ## Changes - **`goal2sat.cpp`**: revert the `ref_count ≤ 1` skip-caching optimization entirely; it is unsafe whenever any theory extension is active. - **`bit_blaster_tpl_def.h`**: retain the `mk_eq` micro-optimization from #9872 — pre-size with `resize(sz)` and use index assignment instead of `push_back`. This is correct: `resize` null-initializes slots and `element_ref::operator=` handles ref-counting via `inc_ref`/`dec_ref`. --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> --- src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h index 342ff5ed8..87785d8f8 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h +++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h @@ -768,9 +768,10 @@ void bit_blaster_tpl::mk_smod(unsigned sz, expr * const * a_bits, expr * co template void bit_blaster_tpl::mk_eq(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref & out) { expr_ref_vector out_bits(m()); + out_bits.resize(sz); for (unsigned i = 0; i < sz; ++i) { 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); }