fix(solver): preserve incremental queries, theory lemmas and bit widths

[sjkim1127]

Scope

Split the Solver work from mixed PR #562 so its unresolved normalization finding does not block independent Solver correctness fixes. No normalization, loader, script, signature, CLI/schema or production dependency changes are included.

Closes #532. Closes #427. Closes #428. Closes #545. Closes #561.
Closes #337. Closes #393. Closes #365. Closes #382.

Changes

• Treat AIG constants as explicit true/false assumptions; prohibit free CNF variables for AIG index zero.
• Include unsigned maximum endpoints and reset stale decisions before permanent clause insertion.
• Zero-extend the subtrahend before complementing mixed-width subtraction.
• Share assertion catch-up and eager loading through one cursor, including append-only public compatibility assertions.
• Require satisfiable, supported contexts for constant eval/min/max queries.
• Install global theory lemmas through the root clause path and restore every assumption. Preserve root conflicts, correct watches and fresh-variable bounds.
• Retain every glue clause and capture learned LBD on the conflict trail.
• Bound whole-array scalar placeholders, abstain on nested array sorts and avoid extracting array-valued model entries as u64 scalars.
• Guard invalid/overflowing/zero-width SMT-LIB extracts.

Existing contracts retained

Scalar widths remain 1..=64. Wider/invalid scalar operations produce Unknown and no scalar model; this PR does not implement arbitrary-precision values. Signed operand width mismatches already abstained on main; they continue to return Unknown rather than guessing sign extension. Some AIG extract/constant/array guards were already present on main and are verified by the new issue regressions. LBD was previously computed after backtracking, but current backtracking retains level metadata; the reproduced #382 defect was glue eviction, not a demonstrated LBD numeric mismatch.

Array read/store axioms and memory CEGAR issue #295 remain separate; this PR does not claim complete array theory support or close that issue.

Evidence

New regressions failed before their fixes: mixed-width subtraction (even 0:2 - 0:1), assertion cursor, constant queries, nested array lowering/model extraction, assumptions lost by theory units, missed theory propagation, fresh multi-literal theory variables, sticky empty/root theory conflicts, and glue retention. Retained logs are under Fission benchmark/artifacts/pr-issue-triage/2026-10-19/.

• Solver nextest: 105 passed / 1 skipped.
• Emulator + DIR nextest: 280 passed / 3 skipped.
• Solver/emulator/CLI checks, workspace fmt and whitespace checks passed.
• All 900 mixed-width unsigned pairs at widths 1..4 checked with equality and disequality probes.
• 2,000 delayed theory-lemma problems with assumptions checked against enumeration, including every returned SAT model.
• Prior 20,000-CNF, 2,000 incremental-sequence and unsigned interval/endpoint regressions remain enabled.

The optional external SMT process oracle remains skipped. No decompiler-quality, execution-parity, speed or ranking claim is made. Remote CI must pass on the submitted HEAD before merging; #562 and its normalization issues remain open.