diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp
index b6116b20fd..5096d23144 100644
--- a/src/smt/smt_parallel.cpp
+++ b/src/smt/smt_parallel.cpp
@@ -784,8 +784,21 @@ namespace smt {
 
             switch (r) {
             case l_undef: {
-                update_max_thread_conflicts();
                 LOG_WORKER(1, " found undef cube\n");
+                // Escalating the per-thread conflict budget and re-splitting the
+                // cube only helps when the cube was abandoned because the per-cube
+                // conflict limit was reached. For any other source of incompleteness
+                // (an incomplete theory, quantifiers, lambdas, resource limits, ...)
+                // the verdict cannot change, so re-checking the same cube would spin
+                // forever and the run hangs to a wall-clock timeout. Record a sound
+                // 'unknown' verdict and stop working this branch instead.
+                std::string reason = ctx->last_failure_as_string();
+                if (reason != "max-conflicts-reached") {
+                    LOG_WORKER(1, " undef cube not conflict-limited (" << reason << "); reporting unknown\n");
+                    b.set_unknown(reason);
+                    return;
+                }
+                update_max_thread_conflicts();
                 if (m_config.m_max_cube_depth <= cube.size())
                     goto check_cube_start;
 
@@ -1727,7 +1740,7 @@ namespace smt {
     void parallel::batch_manager::set_sat(ast_translation &l2g, model &m) {
         std::scoped_lock lock(mux);
         IF_VERBOSE(1, verbose_stream() << "Batch manager setting SAT.\n");
-        if (m_state != state::is_running)
+        if (m_state != state::is_running && m_state != state::is_unknown)
             return;
         m_state = state::is_sat;
         p.ctx.set_model(m.translate(l2g));
@@ -1737,7 +1750,7 @@ namespace smt {
     void parallel::batch_manager::set_unsat(ast_translation &l2g, expr_ref_vector const &unsat_core) {
         std::scoped_lock lock(mux);
         IF_VERBOSE(1, verbose_stream() << "Batch manager setting UNSAT.\n");
-        if (m_state != state::is_running)
+        if (m_state != state::is_running && m_state != state::is_unknown)
             return;
         m_state = state::is_unsat;
 
@@ -1748,6 +1761,16 @@ namespace smt {
         cancel_background_threads();
     }
 
+    void parallel::batch_manager::set_unknown(std::string const &reason) {
+        std::scoped_lock lock(mux);
+        IF_VERBOSE(1, verbose_stream() << "Batch manager setting UNKNOWN: " << reason << ".\n");
+        if (m_state != state::is_running)
+            return;  // a definitive sat/unsat verdict or exception already won.
+        m_state = state::is_unknown;
+        m_reason_unknown = reason;
+        cancel_background_threads();
+    }
+
     void parallel::batch_manager::set_exception(unsigned error_code) {
         std::scoped_lock lock(mux);
         IF_VERBOSE(1, verbose_stream() << "Batch manager setting exception code: " << error_code << ".\n");
@@ -1779,6 +1802,8 @@ namespace smt {
             return l_false;
         case state::is_sat:
             return l_true;
+        case state::is_unknown:
+            return l_undef;
         case state::is_exception_msg:
             throw default_exception(m_exception_msg.c_str());
         case state::is_exception_code:
@@ -1989,7 +2014,10 @@ namespace smt {
         for (auto* bb_w : m_global_backbones_workers)
             bb_w->collect_statistics(ctx.m_aux_stats);
 
-        return m_batch_manager.get_result();
+        lbool result = m_batch_manager.get_result();
+        if (result == l_undef && !m_batch_manager.get_reason_unknown().empty())
+            ctx.set_reason_unknown(m_batch_manager.get_reason_unknown().c_str());
+        return result;
     }
 
 }  // namespace smt
diff --git a/src/smt/smt_parallel.h b/src/smt/smt_parallel.h
index f8acfe8ff8..4af58efbc9 100644
--- a/src/smt/smt_parallel.h
+++ b/src/smt/smt_parallel.h
@@ -81,6 +81,7 @@ namespace smt {
                 is_running,
                 is_sat,
                 is_unsat,
+                is_unknown,
                 is_exception_msg,
                 is_exception_code
             };
@@ -109,6 +110,7 @@ namespace smt {
             
             unsigned m_exception_code = 0;
             std::string m_exception_msg;
+            std::string m_reason_unknown;
             vector<shared_clause> shared_clause_trail; // store all shared clauses with worker IDs
             obj_hashtable<expr> shared_clause_set; // for duplicate filtering on per-thread clause expressions
 
@@ -200,6 +202,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_unknown(std::string const& reason);
             void set_canceled();
             void set_exception(std::string const& msg);
             void set_exception(unsigned error_code);
@@ -238,6 +241,7 @@ namespace smt {
             expr_ref_vector return_shared_clauses(ast_translation& g2l, unsigned& worker_limit, unsigned worker_id);
 
             lbool get_result() const;
+            std::string const& get_reason_unknown() const { return m_reason_unknown; }
 
             bool is_global_backbone_or_negation(ast_translation& l2g, expr* bb_cand) {
                 std::scoped_lock lock(mux);