From 96092b196c7350444365f85216f576aca077e6a8 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 14 Jun 2026 13:46:29 -0700
Subject: [PATCH] add exception handling in case run method throws

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_context.cpp           |  5 +----
 src/solver/parallel_tactical2.cpp | 28 +++++++++++++++++++++++-----
 2 files changed, 24 insertions(+), 9 deletions(-)

diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 6b6728e07..0e8062e88 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -120,9 +120,7 @@ namespace smt {
         }
         else {
             // selected parameters are safe to update after initialization
-            params_ref new_p;
-            new_p.set_uint("max_conflicts", p.get_uint("max_conflicts", UINT_MAX));
-            m_fparams.updt_params(new_p);
+            m_fparams.m_max_conflicts = p.get_uint("max_conflicts", m_fparams.m_max_conflicts);
         }
         for (auto th : m_theory_set)
             if (th)
@@ -4685,7 +4683,6 @@ namespace smt {
             theory_id th_id     = l->get_id();
 
             for (enode * parent : enode::parents(n)) {
-                auto p = parent->get_expr();
                 family_id fid = parent->get_family_id();
                 if (fid != th_id && fid != m.get_basic_family_id()) {
                     if (is_beta_redex(parent, n))
diff --git a/src/solver/parallel_tactical2.cpp b/src/solver/parallel_tactical2.cpp
index 13a5aa18d..2d73046bd 100644
--- a/src/solver/parallel_tactical2.cpp
+++ b/src/solver/parallel_tactical2.cpp
@@ -883,7 +883,7 @@ class parallel_solver {
             if (lim.is_canceled() || m_state != state::is_running)
                 return false;
 
-                if (m_bb_last_batch_processed[bb_thread_id] == m_bb_batch_id) {
+            if (m_bb_last_batch_processed[bb_thread_id] == m_bb_batch_id) {
                 unsigned n = std::min<unsigned>(m_bb_batch_size, m_bb_candidates.size());
                 m_bb_current_batch.reset();
                 for (unsigned i = 0; i < n; ++i) {
@@ -1912,14 +1912,32 @@ public:
 
         m_batch_manager.initialize(num_bb_threads);
 
+        auto safe_run = [&](std::function<void()> run_fn, reslimit& lim) {
+            try {
+                run_fn();
+            } catch (z3_error &err) {
+                if (!lim.is_canceled())
+                    m_batch_manager.set_exception(err.error_code());
+            } catch (z3_exception &ex) {
+                if (!lim.is_canceled() && !is_cancellation_exception(ex.what()))
+                    m_batch_manager.set_exception(ex.what());
+            }
+        };
         /* Launch threads. */
         vector<std::thread> threads;
-        for (auto* w : m_workers)
-            threads.push_back(std::thread([w]() { w->run(); }));
+        for (auto *w : m_workers)
+            threads.push_back(std::thread([&]() {
+                safe_run([w]() -> void { w->run(); }, w->limit());
+            }));
         if (m_core_minimizer_worker)
-            threads.push_back(std::thread([this]() { m_core_minimizer_worker->run(); }));
+            threads.push_back(std::thread([&]() {
+                safe_run([this]() -> void { m_core_minimizer_worker->run(); }, m_core_minimizer_worker->limit());
+            }));
         for (auto* w : m_global_backbones_workers)
-            threads.push_back(std::thread([w]() { w->run(); }));
+            threads.push_back(std::thread([&]() {
+                safe_run([w]() -> void {
+                    w->run(); }, w->limit());
+                    }));
 
         for (auto& t : threads)
             t.join();