mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-05 14:56:11 +00:00
Code Activity

check for lease expiration before checking for m.inc()

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-06-15 16:00:26 -06:00
parent 48ae786c4c
commit fc5e4d7557
1 changed files with 3 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/solver/parallel_tactical2.cpp
View file

@ -1171,10 +1171,6 @@ class parallel_solver {
if (m_config.m_global_backbones) { if (m_config.m_global_backbones) {
bb_candidates local_candidates = find_backbone_candidates(cube); bb_candidates local_candidates = find_backbone_candidates(cube);
b.collect_backbone_candidates(m_l2g, local_candidates); b.collect_backbone_candidates(m_l2g, local_candidates);
if (!m.inc()) {
b.set_cancel();
return;
}
} }
lbool r = check_cube(cube); lbool r = check_cube(cube);
@ -1185,11 +1181,14 @@ class parallel_solver {
continue; continue;
} }
// NSB - at this point it shouldn't be possible to call inc_cancel.
// Is this ensured? I am not sure.
if (!m.inc()) { if (!m.inc()) {
b.set_cancel(); b.set_cancel();
return; return;
} }
switch (r) { switch (r) {
case l_undef: { case l_undef: {