From b6f7a70a3972787f3ebe20e644bfd5f21907386f Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 16 Jun 2026 18:02:42 +0000 Subject: [PATCH] fix: keep only bit_blaster mk_eq optimization from PR #9872 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 --- 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..a4b5410f6 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.reserve(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); }