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
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
/*++
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 "cmd_context/cmd_context.h"
#include "parsers/smt2/smt2parser.h"
#include "smt/smt_solver.h"
#include "smt/tactic/smt_tactic_core.h"
#include "tactic/goal.h"
#include "tactic/tactic.h"
#include "tactic/smtlogics/qfbv_tactic.h"
#include "util/cancel_eh.h"
#include "util/scoped_timer.h"
#include <iostream>
#include <sstream>
// 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";
}
// Exercise native smt.threads, which uses smt_parallel rather than the psmt tactic.
{
cmd_context cmd(false, &m);
std::istringstream input(R"(
(declare-fun g (Real) Real)
(declare-fun f ((_ FloatingPoint 8 24)) (_ FloatingPoint 8 24))
(declare-fun y () (_ FloatingPoint 8 24))
(declare-fun x () (_ FloatingPoint 8 24))
(assert (forall ((q Real)) (! (> (g q) 0.0) :pattern ((g q)))))
(assert (forall ((q Real)) (! (>= (g q) (+ 1.0 q)) :pattern ((g q)))))
(assert (=> (not (fp.isNaN (fp.sub roundNearestTiesToEven x y)))
(fp.geq (f (fp.sub roundNearestTiesToEven x y)) (_ +zero 8 24))))
(assert (not (fp.geq (f (fp.sub roundNearestTiesToEven x y)) (_ +zero 8 24))))
)");
VERIFY(parse_smt2_commands(cmd, input));
params_ref parallel_params;
parallel_params.set_uint("threads", 2);
parallel_params.set_uint("random_seed", 66);
ref<solver> s = mk_smt_solver(m, parallel_params, symbol::null);
for (expr* a : cmd.assertions())
s->assert_expr(a);
cancel_eh<reslimit> eh(m.limit());
scoped_timer timer(10000, &eh);
s->check_sat(0, nullptr);
statistics st;
s->collect_statistics(st);
bool split = false;
for (unsigned i = 0; i < st.size(); ++i) {
if (std::string(st.get_key(i)) == "parallel-max-cube-size") {
split = st.get_uint_value(i) > 0;
break;
}
}
ENSURE(split);
}
std::cout << "psmt tests passed\n";
}
// Regression test for GitHub issue #11158:
//
// (check-sat-using qfbv) on a quantified array formula does not match the
// QF_BV probes, so qfbv falls back to the smt tactic, which with
// parallel.enable=true becomes the parallel (cube-and-conquer) solver. That
// configuration spawns CDCL workers, a core-minimizer worker and backbone
// workers, and used to crash intermittently.
//
// The formula below is the one from the issue. It is UNSAT; the test mainly
// guards against crashes, hangs, and unsoundness in that fallback path, so a
// resource-limited l_undef is tolerated but l_true is not.
static void tst_parallel_qfbv() {
ast_manager m;
reg_decl_plugins(m);
cmd_context cmd(false, &m);
std::istringstream input(R"(
(declare-fun a (Int Int) Int)
(declare-fun b ((Array Int (Array Int Int))) (Array Int (Array Int Int)))
(declare-fun c (Int Int Int) (Array Int (Array Int Int)))
(assert (forall ((d Int) (e Int))
(= (<= d e) (= (select (select (c 0 (a e e) e) d) e) e))))
(assert (forall ((f Int) (g Int) (h (Array Int (Array Int Int))) (i Int))
(let ((j (b h)))
(= (or (<= f i) (<= g i)) (= 0 (select (j g) f))))))
)");
VERIFY(parse_smt2_commands(cmd, input));
for (unsigned seed = 0; seed < 6; ++seed) {
params_ref p;
p.set_bool("enable", true);
p.set_uint("random_seed", seed);
p.set_uint("num_bb_threads", seed % 3);
tactic_ref t = mk_qfbv_tactic(m, p);
goal_ref g = alloc(goal, m, false, true, false);
for (expr* a : cmd.assertions())
g->assert_expr(a);
model_ref md;
labels_vec labels;
proof_ref pr(m);
expr_dependency_ref core(m);
std::string reason_unknown;
cancel_eh<reslimit> eh(m.limit());
scoped_timer timer(60000, &eh);
lbool r = check_sat(*t, g, md, labels, pr, core, reason_unknown);
m.limit().reset_cancel();
ENSURE(r != l_true);
std::cout << "psmt qfbv fallback (seed=" << seed << "): " << r << "\n";
}
}
void tst_psmt() {
tst_psmt_worker();
tst_parallel_qfbv();
}
#else
void tst_psmt() {
// Single-threaded build: parallel tactic degrades to sequential.
// No deadlock is possible; nothing to test.
}
#endif