fix(processor): bound the complete satisfiability solver operation

[doublewhy]

Problem

The finite-domain satisfiability adapter can perform up to 32,769 checks. Each check currently rebuilds the entire Z3 variable/constraint graph, and the governed 5-second timeout starts only inside solver.check(). Python-side expression construction and the total multi-check operation are therefore outside the claimed runtime bound.

Decision

Build one deterministic incremental QF_LIA solver session per normalized model. Encode each clause once behind a Boolean assumption, use assumptions for selected clauses and fixed witness indices, and preserve the incumbent initial-decision, lexicographic witness, and sorted-deletion core semantics. Add one monotonic 5-second operation deadline covering model construction, every check, and result selection. Each Z3 call receives only its remaining deadline (capped at 5000 ms); a result returned after the operation deadline is rejected. No partial SAT/UNSAT evidence is emitted.

Acceptance

• one solver and one expression graph are built per analysis;
• deterministic SAT witnesses and subset-minimal UNSAT cores remain byte-identical to the incumbent algorithm on generated bounded models;
• timeout includes Python model construction and all repeated checks;
• timeout/exhaustion/unknown remain typed operational failures with safe phase, check count/budget, and bounded reason;
• performance regression covers the published maximum check-count shape without rebuilding solvers;
• replay and solver-configuration evidence remain compatible.

Requirement: ASR-530. Related: #826, PR #1083.

[doublewhy]

Implementation remediation brief:

1. Gap claim. The current finite-domain adapter can perform up to 32,769 solver checks while rebuilding the full Z3 graph for each probe. Its configured 5,000 ms timeout begins only inside each native check(), so RAES cannot claim that the complete analysis—including Python expression construction and deterministic witness/core selection—is bounded. An unknown result inside those selection loops can also invalidate the stronger canonical-evidence claim unless it fails closed.
2. Existing surface audit. The audit covered the normalized finite-domain model, _solver.py, _service.py, parser/translation entry points, SolverConfigurationModel, the published satisfiability evidence schema and replay path, CLI exposure, ADR-086, the scenario-satisfiability specification, ASR-530 traceability, fixtures, and Governed whole-scenario constraint satisfiability and solver evidence #826/fix(processor): fail loudly on z3 unknown in the satisfiability solver #1083. These already own the semantic family; no new SDL, parser alias, evidence schema, or backend/runtime surface is needed.
3. Lineage and precedent. This is a bounded operational correction within ADR-086 and closed issue Governed whole-scenario constraint satisfiability and solver evidence #826's governed QF_LIA profile. It preserves the existing theory, solver pin, witness ordering, core-reduction ordering, replay digest, and evidence meaning while making the declared timeout honest.
4. Literature and practice. Z3's official API defines checks over temporary assumptions and preserves unknown as distinct from SAT/UNSAT (https://z3prover.github.io/api/html/classz3py_1_1_solver.html). Python's monotonic clock is explicitly non-decreasing and unaffected by system-clock updates, making elapsed-time deltas appropriate for the operation deadline (https://docs.python.org/3/library/time.html#time.monotonic).
5. Alternatives. Rejected: keep rebuilding and document the timeout as per-check; return partial evidence when the deadline expires; retry unknown; add a new caller-controlled wire timeout; or move only the native check into a deadline. Chosen: one incremental assumption-gated solver plus one monotonic operation deadline and the existing independent check-count budget.
6. Chosen architecture. Encode variables, domains, and each clause once. Select clauses and fixed witness indices through Boolean assumptions. Start the 5,000 ms deadline before construction, pass only the rounded-up remaining milliseconds (capped at 5,000) to each check, and reject expiry before or after any native result. Timeout, exhaustion, and unknown remain typed operational failures and emit no partial SAT/UNSAT evidence.
7. Documentation defense. The implementation must carry a dedicated fix(processor): bound the complete satisfiability solver operation #1108 decision record, update the normative solver semantics and ASR-530 traceability, state compatibility and nonclaims, and retain Governed whole-scenario constraint satisfiability and solver evidence #826 only as related lineage. No published schema should change because the completed evidence contract remains identical.
8. Verification plan. Differential property tests compare SAT witnesses and UNSAT cores with the incumbent rebuilding oracle; unit tests cover construction, every deadline boundary, unknown, budget exhaustion, duplicate ids, empty membership, safe service propagation, and a maximum-check-shape construction-count regression. Run solver/parser/processor regressions, Ruff, policy, changed line and branch coverage, and the stable Python 3.12 suite.