[BUG] Fail closed when Z3 returns unknown during satisfiability evidence construction

[doublewhy]

Gap claim

The satisfiability solver can return unknown from a bounded check. The current solver path treats that non-answer like a decisive result while reducing an unsatisfiable core or selecting a canonical witness, so published evidence can claim minimality or canonicality that was not established.

Existing surface audit

The service boundary already has a typed operational-error path, but the shared solver-check seam does not classify unknown. Evidence replay detects the divergence only after invalid evidence has already been emitted.

Reproduction

1. Force one solver.check() call to return unknown during core reduction or witness selection.
2. Run scenario satisfiability analysis.
3. Observe that analysis continues instead of reporting an operational failure.

Duplicate clause identifiers also reach Z3 with an opaque exception, and an empty allowed-value intersection relies on implicit zero-argument behavior.

Expected behavior

• Every unknown result fails closed through the typed operational-error boundary.
• No evidence claiming minimality or canonicality is emitted after an incomplete check.
• Duplicate clause identifiers are rejected before solver construction.
• Empty membership is represented explicitly as false.

Verification

Regression tests must cover incomplete core reduction, incomplete witness selection, duplicate identifiers, and empty membership without changing the governed Z3 version or published schemas.

Related implementation

Proposed in #1083.

[doublewhy]

Implementation remediation brief supplement:

1. Gap claim. The issue reproduction is confirmed at the shared solver-check seam: unknown is neither SAT nor UNSAT and cannot support canonical-witness or subset-minimal-core evidence.
2. Existing surface audit. The normalized model, solver adapter, service operational-error boundary, evidence/replay contract, ADR-086, ASR-530, scenario-satisfiability specification, parser/translation boundary, and closed Governed whole-scenario constraint satisfiability and solver evidence #826 lineage were reviewed. The established solver family is sufficient; no new SDL, schema, parser alias, or backend surface is warranted.
3. Lineage and precedent. The correction remains inside closed Governed whole-scenario constraint satisfiability and solver evidence #826's governed QF_LIA profile and preserves its theory, package pin, ordering rules, evidence schema, and replay semantics.
4. Literature and practice. Z3's official API keeps unknown distinct from SAT/UNSAT and supports temporary check assumptions: https://z3prover.github.io/api/html/classz3py_1_1_solver.html
5. Alternatives. Rejected: silently continue; map unknown to unsupported; retry without a governed bound; rely on replay to catch bad evidence; or change the v1 wire contract. Chosen: central fail-closed classification plus defensive identity and empty-set handling.
6. Chosen architecture. The single check path rejects unknown with bounded reason and phase/check context; the service translates it to the typed operational boundary and emits no evidence. Clause IDs are checked before solver construction, and empty membership is encoded as BoolVal(False).
7. Documentation defense. The implementation adds docs/decisions/issue-1114-solver-operational-safety-remediation.md, updates the normative solver semantics, and traces [BUG] Fail closed when Z3 returns unknown during satisfiability evidence construction #1114 through ASR-530. Closed Governed whole-scenario constraint satisfiability and solver evidence #826 remains related lineage only.
8. Verification plan. Tests force unknown during initial decision, core reduction, and witness selection; exercise duplicate IDs and empty membership; verify safe service propagation; and retain the governed Z3 version and unchanged published schemas. The successor draft will close [BUG] Fail closed when Z3 returns unknown during satisfiability evidence construction #1114 together with the operation-bound issue fix(processor): bound the complete satisfiability solver operation #1108.