From 6daebef4e43f3d56d23505f90c36c23a0e4cdf9c Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Sun, 28 Jun 2026 13:27:58 -0600 Subject: [PATCH] Fix psmt deadlock when formula is theory-incomplete (#9986) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `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 | 6 ++ src/test/CMakeLists.txt | 1 + src/test/main.cpp | 3 +- src/test/psmt.cpp | 153 +++++++++++++++++++++++++++++++ 4 files changed, 162 insertions(+), 1 deletion(-) create mode 100644 src/test/psmt.cpp diff --git a/src/solver/parallel_tactical.cpp b/src/solver/parallel_tactical.cpp index 7191197767..eab95aa586 100644 --- a/src/solver/parallel_tactical.cpp +++ b/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) { diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt index e26f17cf44..b41175deda 100644 --- a/src/test/CMakeLists.txt +++ b/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 diff --git a/src/test/main.cpp b/src/test/main.cpp index dc5854da7c..453bf5eb55 100644 --- a/src/test/main.cpp +++ b/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) \ diff --git a/src/test/psmt.cpp b/src/test/psmt.cpp new file mode 100644 index 0000000000..c8cf2da541 --- /dev/null +++ b/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 + +// 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