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