[snapshot-regression-fix] smt_parallel: report unknown on theory-incomplete cubes instead of hanging (#9999)

## Summary

Fixes a hang (wall-clock timeout) in the native parallel SMT solver when
a cube is incomplete for a reason that cannot change. Originating
discussion: https://github.com/Z3Prover/bench/discussions/2746

Benchmark: `iss-3707/bug-1.smt2` (`QF_NRA`, runs with
`parallel.enable=true`).

## Divergence

The recorded oracle vs. current z3 (`z3 -T:20`):

```diff
-(incomplete (theory difference-logic))
-unknown
+timeout
```

z3 should terminate with `unknown` (incomplete theory) but instead spins
until the 20s timeout.

## Root cause

In `src/smt/smt_parallel.cpp` the per-cube worker handled an `l_undef`
cube by unconditionally calling `update_max_thread_conflicts()` and
re-splitting/re-checking. That only helps when the cube was abandoned at
the per-cube conflict limit (`max-conflicts-reached`). When the cube is
incomplete for a permanent reason (incomplete theory, quantifiers,
resource limits), the verdict never changes, so the worker re-checks the
same cube forever. The `batch_manager` had no `unknown` terminal state,
so `get_result()` could only end as sat/unsat/exception — there was no
way to settle on `unknown`, hence the hang. This is the `smt_parallel`
analogue of the `parallel_tactical.cpp` regression fixed earlier.

## Fix

Minimal, mirroring the tactic-side fix:
- add an `is_unknown` batch-manager state + `m_reason_unknown`;
- a worker reporting `l_undef` whose `last_failure` is not
`max-conflicts-reached` calls `set_unknown(reason)` and stops
re-splitting;
- `set_sat`/`set_unsat` may still override `is_unknown` so a definitive
answer wins;
- `get_result()` maps `is_unknown -> l_undef` and the reason propagates
to the parent context.

## Validation

Rebuilt z3 (`make -C build -j16`) and re-ran the benchmark 5× with
`-T:20`. Every run finished in well under the timeout with output
matching the oracle byte-for-byte:

```
(incomplete (theory difference-logic))
unknown
```

Created as a **draft** for human review.




> Generated by [Fix a Z3 snapshot-regression
divergence](https://github.com/Z3Prover/bench/actions/runs/28358375255)
· 553.9 AIC · ⌖ 27.2 AIC · ⊞ 9K ·
[◷](https://github.com/search?q=repo%3AZ3Prover%2Fz3+%22gh-aw-workflow-id%3A+snapshot-regression-fixer%22&type=pullrequests)

<!-- gh-aw-agentic-workflow: Fix a Z3 snapshot-regression divergence,
engine: copilot, version: 1.0.63, model: claude-opus-4.8, id:
28358375255, workflow_id: snapshot-regression-fixer, run:
https://github.com/Z3Prover/bench/actions/runs/28358375255 -->

<!-- gh-aw-workflow-id: snapshot-regression-fixer -->
<!-- gh-aw-workflow-call-id: Z3Prover/bench/snapshot-regression-fixer
-->

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

src/smt/smt_parallel.cpp

@@ -784,8 +784,21 @@ namespace smt {
 
             switch (r) {
             case l_undef: {
-                update_max_thread_conflicts();
                 LOG_WORKER(1, " found undef cube\n");
+                // Escalating the per-thread conflict budget and re-splitting the
+                // cube only helps when the cube was abandoned because the per-cube
+                // conflict limit was reached. For any other source of incompleteness
+                // (an incomplete theory, quantifiers, lambdas, resource limits, ...)
+                // the verdict cannot change, so re-checking the same cube would spin
+                // forever and the run hangs to a wall-clock timeout. Record a sound
+                // 'unknown' verdict and stop working this branch instead.
+                std::string reason = ctx->last_failure_as_string();
+                if (reason != "max-conflicts-reached") {
+                    LOG_WORKER(1, " undef cube not conflict-limited (" << reason << "); reporting unknown\n");
+                    b.set_unknown(reason);
+                    return;
+                }
+                update_max_thread_conflicts();
                 if (m_config.m_max_cube_depth <= cube.size())
                     goto check_cube_start;
 
@@ -1727,7 +1740,7 @@ namespace smt {
     void parallel::batch_manager::set_sat(ast_translation &l2g, model &m) {
         std::scoped_lock lock(mux);
         IF_VERBOSE(1, verbose_stream() << "Batch manager setting SAT.\n");
-        if (m_state != state::is_running)
+        if (m_state != state::is_running && m_state != state::is_unknown)
             return;
         m_state = state::is_sat;
         p.ctx.set_model(m.translate(l2g));
@@ -1737,7 +1750,7 @@ namespace smt {
     void parallel::batch_manager::set_unsat(ast_translation &l2g, expr_ref_vector const &unsat_core) {
         std::scoped_lock lock(mux);
         IF_VERBOSE(1, verbose_stream() << "Batch manager setting UNSAT.\n");
-        if (m_state != state::is_running)
+        if (m_state != state::is_running && m_state != state::is_unknown)
             return;
         m_state = state::is_unsat;
 
@@ -1748,6 +1761,16 @@ namespace smt {
         cancel_background_threads();
     }
 
+    void parallel::batch_manager::set_unknown(std::string const &reason) {
+        std::scoped_lock lock(mux);
+        IF_VERBOSE(1, verbose_stream() << "Batch manager setting UNKNOWN: " << reason << ".\n");
+        if (m_state != state::is_running)
+            return;  // a definitive sat/unsat verdict or exception already won.
+        m_state = state::is_unknown;
+        m_reason_unknown = reason;
+        cancel_background_threads();
+    }
+
     void parallel::batch_manager::set_exception(unsigned error_code) {
         std::scoped_lock lock(mux);
         IF_VERBOSE(1, verbose_stream() << "Batch manager setting exception code: " << error_code << ".\n");
@@ -1779,6 +1802,8 @@ namespace smt {
             return l_false;
         case state::is_sat:
             return l_true;
+        case state::is_unknown:
+            return l_undef;
         case state::is_exception_msg:
             throw default_exception(m_exception_msg.c_str());
         case state::is_exception_code:
@@ -1989,7 +2014,10 @@ namespace smt {
         for (auto* bb_w : m_global_backbones_workers)
             bb_w->collect_statistics(ctx.m_aux_stats);
 
-        return m_batch_manager.get_result();
+        lbool result = m_batch_manager.get_result();
+        if (result == l_undef && !m_batch_manager.get_reason_unknown().empty())
+            ctx.set_reason_unknown(m_batch_manager.get_reason_unknown().c_str());
+        return result;
     }
 
 }  // namespace smt

src/smt/smt_parallel.h

@@ -81,6 +81,7 @@ namespace smt {
                 is_running,
                 is_sat,
                 is_unsat,
+                is_unknown,
                 is_exception_msg,
                 is_exception_code
             };
@@ -109,6 +110,7 @@ namespace smt {
             
             unsigned m_exception_code = 0;
             std::string m_exception_msg;
+            std::string m_reason_unknown;
             vector<shared_clause> shared_clause_trail; // store all shared clauses with worker IDs
             obj_hashtable<expr> shared_clause_set; // for duplicate filtering on per-thread clause expressions
 
@@ -200,6 +202,7 @@ namespace smt {
 
             void set_unsat(ast_translation& l2g, expr_ref_vector const& unsat_core);
             void set_sat(ast_translation& l2g, model& m);
+            void set_unknown(std::string const& reason);
             void set_canceled();
             void set_exception(std::string const& msg);
             void set_exception(unsigned error_code);
@@ -238,6 +241,7 @@ namespace smt {
             expr_ref_vector return_shared_clauses(ast_translation& g2l, unsigned& worker_limit, unsigned worker_id);
 
             lbool get_result() const;
+            std::string const& get_reason_unknown() const { return m_reason_unknown; }
 
             bool is_global_backbone_or_negation(ast_translation& l2g, expr* bb_cand) {
                 std::scoped_lock lock(mux);