From fc5e4d7557d4dda0e31e06689551e27f36d1ec8f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 15 Jun 2026 16:00:26 -0600 Subject: [PATCH] check for lease expiration before checking for m.inc() Signed-off-by: Nikolaj Bjorner --- src/solver/parallel_tactical2.cpp | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/solver/parallel_tactical2.cpp b/src/solver/parallel_tactical2.cpp index ab69b713c..ec27f176f 100644 --- a/src/solver/parallel_tactical2.cpp +++ b/src/solver/parallel_tactical2.cpp @@ -1171,10 +1171,6 @@ class parallel_solver { if (m_config.m_global_backbones) { bb_candidates local_candidates = find_backbone_candidates(cube); b.collect_backbone_candidates(m_l2g, local_candidates); - if (!m.inc()) { - b.set_cancel(); - return; - } } lbool r = check_cube(cube); @@ -1185,11 +1181,14 @@ class parallel_solver { continue; } + // NSB - at this point it shouldn't be possible to call inc_cancel. + // Is this ensured? I am not sure. if (!m.inc()) { b.set_cancel(); return; } + switch (r) { case l_undef: {