1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
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);
ENSURE(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);
ENSURE(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.
ENSURE(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