fix(processor): fail loudly on z3 unknown in the satisfiability solver

[doublewhy]

Related issues

Closes #1114

Related to #826 and #1108.

---

What breaks

The satisfiability analyzer could publish a result that claims more than it actually established, and the overclaim only surfaced later as an unexplained replay failure.

Each solver call has a 5-second timeout, so z3 can answer "I don't know" (unknown) rather than yes or no. The code treated that non-answer as a definite answer.

Concretely

Analyzing a scenario emits a ScenarioSatisfiabilityEvidence record. That record is labelled with the profile it was produced under:

• core_reduction: "sorted-deletion-subset-minimal/v1" — asserts the unsatisfiable core is subset-minimal
• witness_selection: "canonical-lexicographic/v1" — asserts the witness is the canonical first choice

Under load, a single probe times out. Because unknown is not unsat, the core-reduction loop keeps a clause it would otherwise have removed; because unknown is not sat, the witness loop skips a value it would otherwise have chosen. The emitted record is structurally valid and still carries both labels — but neither property was checked. Nobody sees an error.

The failure shows up much later, somewhere else: replay_satisfiability_evidence re-derives the result, gets the correct core or witness, compares digests, and disagrees. The published evidence looks corrupt for no visible reason.

For a project whose premise is that a specification plus its evidence is the reproducible unit of exchange, silently emitting evidence that overstates what was proven is the worst available outcome.

Why it happens

In raes_processor/satisfiability/_solver.py, _check returns z3's raw result, and both callers compare against one outcome only:

• _reduce_unsat_core keeps any clause whose removal is != z3.unsat
• _select_witness skips any value that is != z3.sat

unknown falls into the same branch as a decisive answer in both.

The fix

_check now raises SolverOperationalError on unknown, carrying z3's own reason_unknown(). This is the single seam every caller shares, so no path can forge minimality or canonicality. The service boundary already converts that into the typed SatisfiabilityOperationalError("the pinned solver did not complete"), so no new error style is introduced — a timeout becomes a diagnosable operational failure instead of quiet bad evidence.

Two smaller issues in the same file:

• A clause whose allowed values do not intersect its symbol domain produced a zero-argument z3.Or(). In the pinned z3 that happens to assert as unsatisfiable, but it is undocumented edge behaviour; the empty case is now stated explicitly as BoolVal(False).
• Duplicate clause ids were silently collapsed by an id-to-clause dict while z3 rejected the repeated tracked assumption with an opaque Z3Exception. They are now refused at the model boundary with a clear message.

The governed z3-solver==4.16.0.0 pin is untouched, and nothing under contracts/schemas/ or specs/ changes.

How I know

4 new tests. A helper forces the Nth solver call to return unknown and leaves the rest real:

• timeout during core reduction → operational error, and no evidence claiming minimality is emitted
• timeout during witness selection → operational error
• duplicate clause ids → refused at the boundary (previously leaked a raw Z3Exception)
• empty allowed-value set → unsatisfiable, locking the semantics the explicit guard now states

The first three fail against the current code. The fourth passes before and after by design — it pins existing behaviour rather than demonstrating the bug, and is called out as such.

Full nox -s verify green on Ubuntu 22.04 / Python 3.12, all six lanes, 91% total coverage.

🤖 Generated with Claude Code

[Brad-Edwards]

Please note in the comments or body which issue this PR closes. If no issue exists, please create one and link it.

Thank you!

[doublewhy]

Linked the focused bug issue in the PR body: this PR closes #1114. I also noted the related governed solver work in #826 and #1108. Thank you.

[doublewhy]

Superseded by #1127, which closes #1108 and #1114 and includes the operation-wide deadline, fail-closed evidence handling, and expanded regression coverage discovered during integration. Closing this duplicate so review stays on the current-dev successor.