mirror of
https://github.com/Z3Prover/z3
synced 2026-07-16 03:55:42 +00:00
897c4475af
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> |
||
|---|---|---|
| .. | ||
| bit_blaster.cpp | ||
| bit_blaster.h | ||
| bit_blaster_rewriter.cpp | ||
| bit_blaster_rewriter.h | ||
| bit_blaster_tpl.h | ||
| bit_blaster_tpl_def.h | ||
| CMakeLists.txt | ||