goal2sat: drop unsafe ref_count≤1 cache-skip optimization; keep bit_blaster mk_eq improvement (#9882)

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

@@ -768,9 +768,10 @@ void bit_blaster_tpl<Cfg>::mk_smod(unsigned sz, expr * const * a_bits, expr * co
 template<typename Cfg>
 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());
+    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);
 }