From 38a8644ae3f6354022cff4f86b82c8d2bf320085 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 14 Jun 2026 22:24:02 -0700 Subject: [PATCH 1/4] avoid double cancel Signed-off-by: Nikolaj Bjorner --- src/solver/parallel_tactical2.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/solver/parallel_tactical2.cpp b/src/solver/parallel_tactical2.cpp index 8f1045c5e..921e6dcf6 100644 --- a/src/solver/parallel_tactical2.cpp +++ b/src/solver/parallel_tactical2.cpp @@ -482,6 +482,8 @@ class parallel_solver { void set_cancel() { std::scoped_lock lock(mux); + if (m_state != state::is_running) + return; cancel_workers_unlocked(); } From 26f7ce23b6d97dde43214ce6b682b9d61b8264a2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 14 Jun 2026 22:29:33 -0700 Subject: [PATCH 2/4] lipstick Signed-off-by: Nikolaj Bjorner --- src/solver/parallel_tactical2.cpp | 30 +++++++++++++++--------------- 1 file changed, 15 insertions(+), 15 deletions(-) diff --git a/src/solver/parallel_tactical2.cpp b/src/solver/parallel_tactical2.cpp index 921e6dcf6..3966732e6 100644 --- a/src/solver/parallel_tactical2.cpp +++ b/src/solver/parallel_tactical2.cpp @@ -928,9 +928,9 @@ class parallel_solver { expr_ref_vector const& get_unsat_core() const { return m_unsat_core; } void collect_statistics(statistics& st) const { - st.update("parallel-num_cubes", m_stats.m_num_cubes); + st.update("parallel-num-cubes", m_stats.m_num_cubes); st.update("parallel-max-cube-size", m_stats.m_max_cube_depth); - st.update("bb-backbones-found", m_stats.m_backbones_found); + st.update("parallel-backbones-found", m_stats.m_backbones_found); st.update("parallel-core-min-jobs-enqueued", m_stats.m_core_min_jobs_enqueued); st.update("parallel-core-min-jobs-published", m_stats.m_core_min_jobs_published); st.update("parallel-core-min-jobs-skipped", m_stats.m_core_min_jobs_skipped); @@ -1638,19 +1638,19 @@ class parallel_solver { } void collect_statistics(statistics& st) const { - st.update("bb-batches-total", m_stats.m_batches_total); - st.update("bb-candidates-total", m_stats.m_candidates_total); - st.update("bb-backbones-detected", m_stats.m_backbones_detected); - st.update("bb-internal-backbones-found", m_stats.m_internal_backbones_found); - st.update("bb-retry-backbones-found", m_stats.m_retry_backbones_found); - st.update("bb-retries", m_stats.m_bb_retries); - st.update("bb-core-refinement-rounds", m_stats.m_core_refinement_rounds); - st.update("bb-singleton-backbones", m_stats.m_singleton_backbones); - st.update("bb-fallback-singleton-checks", m_stats.m_fallback_singleton_checks); - st.update("bb-fallback-chunk-exhausted", m_stats.m_fallback_reason_chunk_exhausted); - st.update("bb-fallback-undef", m_stats.m_fallback_reason_undef); - st.update("bb-literals-removed-by-core", m_stats.m_lits_removed_by_core); - st.update("bb-num-chunk-increases", m_stats.m_num_chunk_increases); + st.update("parallel-bb-batches-total", m_stats.m_batches_total); + st.update("parallel-bb-candidates-total", m_stats.m_candidates_total); + st.update("parallel-bb-backbones-detected", m_stats.m_backbones_detected); + st.update("parallel-bb-internal-backbones-found", m_stats.m_internal_backbones_found); + st.update("parallel-bb-retry-backbones-found", m_stats.m_retry_backbones_found); + st.update("parallel-bb-retries", m_stats.m_bb_retries); + st.update("parallel-bb-core-refinement-rounds", m_stats.m_core_refinement_rounds); + st.update("parallel-bb-singleton-backbones", m_stats.m_singleton_backbones); + st.update("parallel-bb-fallback-singleton-checks", m_stats.m_fallback_singleton_checks); + st.update("parallel-bb-fallback-chunk-exhausted", m_stats.m_fallback_reason_chunk_exhausted); + st.update("parallel-bb-fallback-undef", m_stats.m_fallback_reason_undef); + st.update("parallel-bb-literals-removed-by-core", m_stats.m_lits_removed_by_core); + st.update("parallel-bb-num-chunk-increases", m_stats.m_num_chunk_increases); auto safe_ratio = [](double num, double den) -> double { return den > 0 ? num / den : 0.0; From e95f9757c92185e5c8a9cd2795ee7a8ec7b3d95b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 14 Jun 2026 22:38:40 -0700 Subject: [PATCH 3/4] lipstick Signed-off-by: Nikolaj Bjorner --- src/solver/parallel_tactical2.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/solver/parallel_tactical2.cpp b/src/solver/parallel_tactical2.cpp index 3966732e6..5b0902751 100644 --- a/src/solver/parallel_tactical2.cpp +++ b/src/solver/parallel_tactical2.cpp @@ -1656,13 +1656,13 @@ class parallel_solver { return den > 0 ? num / den : 0.0; }; - st.update("bb-backbone-yield-pct", + st.update("parallel-bb-backbone-yield-pct", 100.0 * safe_ratio(m_stats.m_internal_backbones_found, m_stats.m_candidates_total)); - st.update("bb-avg-backbones-per-batch", + st.update("parallel-bb-avg-backbones-per-batch", safe_ratio(m_stats.m_internal_backbones_found, m_stats.m_batches_total)); - st.update("bb-core-refinement-rounds-per-batch", + st.update("parallel-bb-core-refinement-rounds-per-batch", safe_ratio(m_stats.m_core_refinement_rounds, m_stats.m_batches_total)); - st.update("bb-core-effectiveness-lit-removed-per-round", + st.update("parallel-bb-core-effectiveness-lit-removed-per-round", safe_ratio(m_stats.m_lits_removed_by_core, m_stats.m_core_refinement_rounds)); } From dba826039d457d5b29ef418179d7f42a68ec10b8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 14 Jun 2026 23:31:37 -0700 Subject: [PATCH 4/4] avoid spurious cancel Signed-off-by: Nikolaj Bjorner --- src/smt/smt_parallel.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index 2e893360b..ac0193169 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -1694,6 +1694,8 @@ namespace smt { void parallel::batch_manager::set_canceled() { std::scoped_lock lock(mux); + if (m_state != state::is_running) + return; cancel_background_threads(); }