Fix psmt deadlock when formula is theory-incomplete (#9986)

`batch_manager::set_unknown()` in the parallel SMT tactic changed
`m_state` to `is_unknown` but never notified backbone workers or the
core-minimizer worker waiting on `m_bb_cv` / `m_core_min_cv`. Those
threads blocked indefinitely, deadlocking `solve()` at `t.join()`.

### Root cause

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

Every CDCL worker returns `l_undef` with reason `(incomplete (theory
array))`. The first worker calls `set_unknown()` (a soft verdict — other
workers may still find sat/unsat) and exits. Other CDCL workers exit
when `get_cube()` checks `m_state != is_running`. Meanwhile, backbone
workers and the core minimizer are already blocked in
`wait_for_backbone_job()` / `wait_for_core_min_job()`, both of which
condition-wait on CVs that `set_unknown()` never signals. Their
predicates check `m_state != is_running`, but a CV predicate only
re-evaluates on notification or spurious wakeup.

### Fix

- **`src/solver/parallel_tactical.cpp`** — `set_unknown()` now calls
`m_bb_cv.notify_all()` and `m_core_min_cv.notify_all()` after setting
the terminal state, so waiting helper threads observe the change and
exit via the existing `m_state != is_running` guard in their wait
predicates.

### Test

- **`src/test/psmt.cpp`** — new regression covering SAT, UNSAT, and the
theory-incomplete (deadlock) path using `(as-array f)` terms to
reproduce the exact array-theory incompleteness that triggers
`set_unknown()`.

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

src/solver/parallel_tactical.cpp

@@ -522,12 +522,18 @@ class parallel_solver {
         // Record a sound 'unknown' verdict. This is a soft result: it does not
         // cancel the remaining workers, so a definitive sat/unsat verdict from
         // another branch may still arrive and override it.
+        // Backbone workers and the core minimizer block on their own condition
+        // variables waiting for work that will never arrive once the state
+        // transitions away from is_running, so we must notify them here to
+        // prevent a deadlock.
         void 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;
             m_state = state::is_unknown;
             m_reason_unknown = reason;
+            m_bb_cv.notify_all();
+            m_core_min_cv.notify_all();
         }
 
         void set_exception(std::string const& msg) {

src/test/CMakeLists.txt

@@ -115,6 +115,7 @@ add_executable(test-z3
   polynomial_factorization.cpp
   polynorm.cpp
   prime_generator.cpp
+  psmt.cpp
   seq_regex_bisim.cpp
   proof_checker.cpp
   qe_arith.cpp

src/test/main.cpp

@@ -199,7 +199,8 @@
     X(fpa) \
     X(seq_regex_bisim) \
     X(term_enumeration) \
-    X(lcube)
+    X(lcube) \
+    X(psmt)
 
 #define FOR_EACH_TEST(X, X_ARGV) \
     FOR_EACH_ALL_TEST(X, X_ARGV) \

src/test/psmt.cpp

@@ -0,0 +1,153 @@
+/*++
+Copyright (c) 2026 Microsoft Corporation
+
+Module Name:
+
+    psmt.cpp
+
+Abstract:
+
+    Tests for the parallel SMT tactic (psmt).
+    Regression test for GitHub issue #9985 (deadlock on psmt).
+
+--*/
+#ifndef SINGLE_THREAD
+
+#include "ast/reg_decl_plugins.h"
+#include "ast/array_decl_plugin.h"
+#include "ast/arith_decl_plugin.h"
+#include "smt/smt_solver.h"
+#include "smt/tactic/smt_tactic_core.h"
+#include "tactic/goal.h"
+#include "tactic/tactic.h"
+#include <iostream>
+
+// Regression test for GitHub issue #9985:
+//
+// psmt used to deadlock when every CDCL worker returned l_undef with a
+// reason other than "max-conflicts-reached" (e.g., theory incompleteness).
+// batch_manager::set_unknown() changed the terminal state but did not
+// notify backbone workers or the core-minimizer worker that were blocked on
+// their condition variables.  Those workers blocked forever.
+//
+// Fix: set_unknown() now calls m_bb_cv.notify_all() and
+// m_core_min_cv.notify_all() so all waiting helper threads observe the
+// state change and exit cleanly.
+//
+// We exercise three cases:
+//   1. SAT  – trivially satisfiable boolean formula.
+//   2. UNSAT – trivially unsatisfiable boolean formula.
+//   3. UNKNOWN (no deadlock) – formula whose root cube is theory-incomplete.
+//      The formula uses (as-array f) terms for a function f : Int -> Bool.
+//      The array theory marks itself incomplete for as-array, so every
+//      CDCL worker returns l_undef with "(incomplete (theory array))",
+//      triggering the set_unknown path that used to deadlock.
+static void tst_psmt_worker() {
+    ast_manager m;
+    reg_decl_plugins(m);
+    params_ref p;
+
+    // ------------------------------------------------------------------
+    // 1. SAT test: assert (or x (not x)) – always true
+    // ------------------------------------------------------------------
+    {
+        tactic_ref t = mk_parallel_smt_tactic(m, p);
+        goal_ref   g = alloc(goal, m, false, true, false);
+        expr_ref   x(m.mk_const(symbol("x"), m.mk_bool_sort()), m);
+        g->assert_expr(m.mk_or(x, m.mk_not(x)));
+
+        model_ref           md;
+        labels_vec          labels;
+        proof_ref           pr(m);
+        expr_dependency_ref core(m);
+        std::string         reason_unknown;
+        lbool r = check_sat(*t, g, md, labels, pr, core, reason_unknown);
+        SASSERT(r == l_true);
+        (void)r;
+        std::cout << "psmt SAT: " << r << "\n";
+    }
+
+    // ------------------------------------------------------------------
+    // 2. UNSAT test: assert (and x (not x))
+    // ------------------------------------------------------------------
+    {
+        tactic_ref t = mk_parallel_smt_tactic(m, p);
+        goal_ref   g = alloc(goal, m, false, true, false);
+        expr_ref   x(m.mk_const(symbol("x"), m.mk_bool_sort()), m);
+        g->assert_expr(m.mk_and(x, m.mk_not(x)));
+
+        model_ref           md;
+        labels_vec          labels;
+        proof_ref           pr(m);
+        expr_dependency_ref core(m);
+        std::string         reason_unknown;
+        lbool r = check_sat(*t, g, md, labels, pr, core, reason_unknown);
+        SASSERT(r == l_false);
+        (void)r;
+        std::cout << "psmt UNSAT: " << r << "\n";
+    }
+
+    // ------------------------------------------------------------------
+    // 3. UNKNOWN (deadlock regression) test.
+    //
+    // Reproduce: (declare-fun f (Int) Bool)
+    //            (declare-fun g (Int) Bool)
+    //            (assert (distinct f g))
+    //            (check-sat-using psmt)
+    //
+    // In SMT-LIB2, the function symbols f and g are lifted to array terms
+    // via (as-array f) and (as-array g).  The array theory is explicitly
+    // incomplete for as-array, so check_sat returns l_undef with reason
+    // "(incomplete (theory array))".  Previously set_unknown() forgot to
+    // notify backbone and core-minimizer workers' condition variables,
+    // causing a deadlock; now it does.
+    // ------------------------------------------------------------------
+    {
+        tactic_ref t = mk_parallel_smt_tactic(m, p);
+        goal_ref   g = alloc(goal, m, false, true, false);
+
+        // Build func_decls: f : Int -> Bool, g : Int -> Bool
+        arith_util arith(m);
+        sort* int_s     = arith.mk_int();
+        sort* domain[1] = { int_s };
+        func_decl* f_decl = m.mk_func_decl(symbol("f_fn"), 1, domain, m.mk_bool_sort());
+        func_decl* g_decl = m.mk_func_decl(symbol("g_fn"), 1, domain, m.mk_bool_sort());
+
+        // (as-array f) and (as-array g): array representations of f and g
+        array_util autil(m);
+        expr_ref f_arr(autil.mk_as_array(f_decl), m);
+        expr_ref g_arr(autil.mk_as_array(g_decl), m);
+
+        // (distinct (as-array f) (as-array g))
+        expr* dist_args[2] = { f_arr, g_arr };
+        expr_ref distinct_fg(m.mk_distinct(2, dist_args), m);
+        g->assert_expr(distinct_fg);
+
+        model_ref           md;
+        labels_vec          labels;
+        proof_ref           pr(m);
+        expr_dependency_ref core(m);
+        std::string         reason_unknown;
+        lbool r = check_sat(*t, g, md, labels, pr, core, reason_unknown);
+        // The result must be l_undef (theory-incomplete).
+        // If the fix is absent, this call deadlocks instead of returning.
+        SASSERT(r == l_undef);
+        (void)r;
+        std::cout << "psmt UNKNOWN (no deadlock): " << r << "\n";
+    }
+
+    std::cout << "psmt tests passed\n";
+}
+
+void tst_psmt() {
+    tst_psmt_worker();
+}
+
+#else
+
+void tst_psmt() {
+    // Single-threaded build: parallel tactic degrades to sequential.
+    // No deadlock is possible; nothing to test.
+}
+
+#endif