From e45683de4bfa8f12fb58874ff2f9be0c84d145f9 Mon Sep 17 00:00:00 2001
From: Ilana Shapiro <ilanashapiro@Ilanas-MacBook-Pro.local>
Date: Sun, 21 Jun 2026 15:26:42 -0700
Subject: [PATCH] add the safe_run pattern from the tactic (which handles
 external cancel like Ctrl+C  safely) to smt_parallel

---
 src/smt/smt_parallel.cpp | 47 ++++++++++++++++++++++++++++++++++++----
 src/smt/smt_parallel.h   |  1 +
 2 files changed, 44 insertions(+), 4 deletions(-)

diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp
index 2fbf67975..f26fb52bb 100644
--- a/src/smt/smt_parallel.cpp
+++ b/src/smt/smt_parallel.cpp
@@ -1112,6 +1112,11 @@ namespace smt {
         cancel_background_threads();
     }
 
+    void parallel::batch_manager::set_canceled() {
+        std::scoped_lock lock(mux);
+        set_canceled_unlocked();
+    }
+
     void parallel::batch_manager::release_worker_lease_unlocked(unsigned worker_id, node_lease& lease) {
         if (worker_id >= m_worker_leases.size()) {
             lease = {};
@@ -1901,18 +1906,52 @@ namespace smt {
                                        << m_global_backbones_workers.size() << " global backbone threads.\n";);
 
         m_batch_manager.initialize(num_global_bb_threads);
+
+        auto safe_run = [&](auto&& run_fn, reslimit& lim) {
+            try {
+                run_fn();
+                if (lim.is_canceled())
+                    m_batch_manager.set_canceled();
+            } catch (z3_error &err) {
+                IF_VERBOSE(0, verbose_stream() << "Exception in parallel solver: " << err.what() << "\n");
+                if (!lim.is_canceled())
+                    m_batch_manager.set_exception(err.error_code());
+                else
+                    m_batch_manager.set_canceled();
+            } catch (z3_exception &ex) {
+                IF_VERBOSE(0, verbose_stream() << "Exception in parallel solver: " << ex.what() << "\n");
+                if (!lim.is_canceled() && !is_cancellation_exception(ex.what()))
+                    m_batch_manager.set_exception(ex.what());
+                else
+                    m_batch_manager.set_canceled();
+            } catch (...) {
+                IF_VERBOSE(0, verbose_stream() << "Unknown exception in parallel solver\n");
+                if (!lim.is_canceled())
+                    m_batch_manager.set_exception("unknown exception");
+                else
+                    m_batch_manager.set_canceled();
+            }
+        };
         
         // Launch threads
         vector<std::thread> threads(total_threads);
         unsigned thread_idx = 0;
         for (auto* w : m_workers) 
-            threads[thread_idx++] = std::thread([&, w]() { w->run(); });                
+            threads[thread_idx++] = std::thread([w, &safe_run]() {
+                safe_run([w]() { w->run(); }, w->limit());
+            });
         if (m_sls_worker)
-            threads[thread_idx++] = std::thread([&]() { m_sls_worker->run(); });
+            threads[thread_idx++] = std::thread([this, &safe_run]() {
+                safe_run([this]() { m_sls_worker->run(); }, m_sls_worker->limit());
+            });
         if (m_core_minimizer_worker)
-            threads[thread_idx++] = std::thread([&]() { m_core_minimizer_worker->run(); });
+            threads[thread_idx++] = std::thread([this, &safe_run]() {
+                safe_run([this]() { m_core_minimizer_worker->run(); }, m_core_minimizer_worker->limit());
+            });
         for (auto* w : m_global_backbones_workers) 
-            threads[thread_idx++] = std::thread([&, w]() { w->run(); });                   
+            threads[thread_idx++] = std::thread([w, &safe_run]() {
+                safe_run([w]() { w->run(); }, w->limit());
+            });
 
 
         // Wait for all threads to finish
diff --git a/src/smt/smt_parallel.h b/src/smt/smt_parallel.h
index 9c0b99e82..b5fdfc11a 100644
--- a/src/smt/smt_parallel.h
+++ b/src/smt/smt_parallel.h
@@ -196,6 +196,7 @@ namespace smt {
 
             void set_unsat(ast_translation& l2g, expr_ref_vector const& unsat_core);
             void set_sat(ast_translation& l2g, model& m);
+            void set_canceled();
             void set_exception(std::string const& msg);
             void set_exception(unsigned error_code);
             void collect_statistics(::statistics& st) const;