From 9bab5ce7b71c65ad264365d9ff9a683260c4df10 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 9 Sep 2025 16:02:01 -0700
Subject: [PATCH] timeout backoff

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_parallel.cpp  | 2 +-
 src/smt/smt_parallel2.cpp | 3 ++-
 src/smt/smt_parallel2.h   | 5 +++++
 3 files changed, 8 insertions(+), 2 deletions(-)

diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp
index 8e29270dc..591bb8a65 100644
--- a/src/smt/smt_parallel.cpp
+++ b/src/smt/smt_parallel.cpp
@@ -501,7 +501,7 @@ namespace smt {
             auto& cube = m_cubes.back();
             // print out the cubes in m_cubes
             for (auto& e : m_cubes) {
-                IF_VERBOSE(1, verbose_stream() << "Cube: " << e << "\n");
+                IF_VERBOSE(4, verbose_stream() << "Cube: " << e << "\n");
             }
 
             expr_ref_vector l_cube(g2l.to());
diff --git a/src/smt/smt_parallel2.cpp b/src/smt/smt_parallel2.cpp
index 85a561be0..209988785 100644
--- a/src/smt/smt_parallel2.cpp
+++ b/src/smt/smt_parallel2.cpp
@@ -89,6 +89,7 @@ namespace smt {
             
             switch (r) {
                 case l_undef: {
+                    update_max_thread_conflicts();
                     LOG_WORKER(1, " found undef cube\n");
                     // return unprocessed cubes to the batch manager
                     // add a split literal to the batch manager.
@@ -283,7 +284,7 @@ namespace smt {
             asms.push_back(atom);                
         lbool r = l_undef;
 
-        ctx->get_fparams().m_max_conflicts = std::min(cube.size() * 0 + m_config.m_threads_max_conflicts, m_config.m_max_conflicts);
+        ctx->get_fparams().m_max_conflicts = std::min(m_config.m_threads_max_conflicts, m_config.m_max_conflicts);
         IF_VERBOSE(1, verbose_stream() << " Checking cube\n" << bounded_pp_exprs(cube) << "with max_conflicts: " << ctx->get_fparams().m_max_conflicts << "\n";);
         try {
             r = ctx->check(asms.size(), asms.data());
diff --git a/src/smt/smt_parallel2.h b/src/smt/smt_parallel2.h
index 56f229e47..b1983d192 100644
--- a/src/smt/smt_parallel2.h
+++ b/src/smt/smt_parallel2.h
@@ -155,6 +155,11 @@ namespace smt {
             lbool check_cube(expr_ref_vector const& cube);
             void share_units(ast_translation& l2g);
 
+            void update_max_thread_conflicts() {
+                m_config.m_threads_max_conflicts = (unsigned)(m_config.m_max_conflict_mul * m_config.m_threads_max_conflicts);
+            } // allow for backoff scheme of conflicts within the thread for cube timeouts.
+
+
         public:
             worker(unsigned id, parallel2& p, expr_ref_vector const& _asms);
             void run();