[snapshot-regression-fix] Fix psmt infinite loop on theory-incomplete cubes (#3044)

[levnach]

Summary

Fixes a psmt (parallel SMT tactic) regression where the solver hangs to a wall-clock timeout instead of returning unknown on formulas whose root cube is genuinely undetermined by an incomplete theory.

• Originating discussion: https://github.com/Z3Prover/bench/discussions/2735
• Benchmark: iss-3044/bug-1.smt2 (from Z3 issue #3044)

(declare-fun a (Int) Bool)
(declare-fun b (Int) Bool)
(assert (distinct a b))
(check-sat-using psmt)

Divergence

The recorded oracle (expected) vs. current z3 (combined stdout+stderr, -T:20):

-(incomplete (theory array))
-unknown
+timeout

Root cause

The rewritten parallel tactic (src/solver/parallel_tactical.cpp, introduced in #9824/#9825) hangs on this input.

In the worker run() loop, every l_undef cube result was treated as if the per-cube conflict limit had been reached: the worker escalated the per-thread conflict budget (update_max_thread_conflicts) and re-checked / re-split the same cube. When the l_undef actually comes from theory incompleteness (here, the array theory cannot decide (distinct a b) over Int -> Bool) rather than the conflict limit, the verdict never changes, so the worker re-checks the same cube forever.

Compounding this, the batch_manager state machine had no terminal unknown state — the only way to finish was for some worker to prove sat/unsat, which is impossible for a root-level theory-incomplete formula. The combination produced an infinite loop and a wall-clock timeout.

The pre-rewrite parallel tactic avoided this: its giveup() detected reasons starting with (incomplete / (sat.giveup, reported a soft undef, and echoed the reason to verbose_stream().

Fix

All changes are confined to src/solver/parallel_tactical.cpp (47 insertions, 4 deletions):

1. Distinguish genuine incompleteness from conflict-limit exhaustion. In the worker l_undef case, only reason_unknown() == "max-conflicts-reached" benefits from escalating the budget / splitting. For any other reason (incomplete theory, quantifiers, lambdas, resource limits, ...) re-checking is futile, so the worker records a sound unknown and stops working the branch.
2. Add a terminal is_unknown batch-manager state (set_unknown, get_result() -> l_undef, reason storage). It is a soft result: it does not cancel the other workers, and a definitive sat/unsat verdict from another branch may still override it (the set_sat/set_unsat guards now permit overriding is_unknown). All set_unsat call sites are global formula-unsat (core ⊆ assumptions, or independent of the tested backbone literal), so the override is sound; tree-closure unsat remains guarded by is_running and cannot fire because the undef leaf stays open.
3. Restore the reason output. The captured reason_unknown is propagated to the result goal and echoed to verbose_stream(), reproducing the (incomplete (theory array)) line that the sequential path / old parallel tactic emitted.

Validation

Rebuilt the ./z3 checkout (./configure && make -C build -j16) and re-ran the benchmark with the freshly built binary using the same options the snapshot capture uses (-T:20, combined stdout+stderr):

$ z3 inputs/issues/iss-3044/bug-1.smt2 -T:20
(incomplete (theory array))
unknown

This matches the recorded bug-1.expected.out oracle byte-for-byte, and the benchmark now completes in ~0.5s (was: timeout). Verified stable across 8 consecutive runs. Basic psmt sat/unsat checks continue to produce correct results.

Opened as a draft for human review.

Co-authored-by: Copilot 223556219+Copilot@users.noreply.github.com

Generated by Fix a Z3 snapshot-regression divergence · 5.7K AIC · ⌖ 85.8 AIC · ⊞ 41.2K · ◷