diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp
index 5096d23144..d1df20a508 100644
--- a/src/smt/smt_parallel.cpp
+++ b/src/smt/smt_parallel.cpp
@@ -879,6 +879,8 @@ namespace smt {
         if (m_config.m_ablate_backtracking) {
             m_config.m_core_minimize = false;
         }
+
+        m_config.m_threads_max_conflicts = m_smt_params.m_threads_max_conflicts;
     }
 
     parallel::sls_worker::sls_worker(parallel& p)
diff --git a/src/smt/smt_parallel.h b/src/smt/smt_parallel.h
index 4af58efbc9..8e5ebcf8f8 100644
--- a/src/smt/smt_parallel.h
+++ b/src/smt/smt_parallel.h
@@ -304,7 +304,9 @@ namespace smt {
 
             void update_max_thread_conflicts() {
                 // allow for backoff scheme of conflicts within the thread for cube timeouts.
-                m_config.m_threads_max_conflicts = (unsigned)(m_config.m_max_conflict_mul * m_config.m_threads_max_conflicts);
+                // Use saturating arithmetic to avoid unsigned overflow / undefined behaviour.
+                double next = m_config.m_max_conflict_mul * m_config.m_threads_max_conflicts;
+                m_config.m_threads_max_conflicts = (next >= (double)UINT_MAX) ? UINT_MAX : (unsigned)next;
             }
 
             void simplify();
diff --git a/src/solver/parallel_tactical.cpp b/src/solver/parallel_tactical.cpp
index 972379ea7c..803f54eb74 100644
--- a/src/solver/parallel_tactical.cpp
+++ b/src/solver/parallel_tactical.cpp
@@ -1025,8 +1025,9 @@ class parallel_solver {
         unsigned         m_num_initial_atoms = 0;
 
         void update_max_thread_conflicts() {
-            m_config.m_threads_max_conflicts = static_cast<unsigned>(
-                m_config.m_max_conflict_mul * m_config.m_threads_max_conflicts);
+            // Use saturating arithmetic to avoid unsigned overflow / undefined behaviour.
+            double next = m_config.m_max_conflict_mul * m_config.m_threads_max_conflicts;
+            m_config.m_threads_max_conflicts = (next >= (double)UINT_MAX) ? UINT_MAX : static_cast<unsigned>(next);
         }
 
         lbool check_cube(expr_ref_vector const& cube) {