From ac80dfaa8b6780db35c33def0c0967a248462c35 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 10 Sep 2025 09:46:50 -0700
Subject: [PATCH] fix cancelation within nex.

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/lp/cross_nested.h  | 15 +++++++++++----
 src/math/lp/horner.cpp      |  4 +++-
 src/math/lp/nla_grobner.cpp |  4 +++-
 src/smt/smt_parallel2.cpp   |  2 +-
 4 files changed, 18 insertions(+), 7 deletions(-)

diff --git a/src/math/lp/cross_nested.h b/src/math/lp/cross_nested.h
index df0e25303..b232db604 100644
--- a/src/math/lp/cross_nested.h
+++ b/src/math/lp/cross_nested.h
@@ -19,6 +19,8 @@
   --*/
 #pragma once
 #include <functional>
+#include "util/util.h"
+#include "util/rlimit.h"
 #include "math/lp/nex.h"
 #include "math/lp/nex_creator.h"
 
@@ -26,10 +28,11 @@ namespace nla {
 class cross_nested {
     
     // fields
+    reslimit&                                         m_limit;
     nex *                                             m_e = nullptr;
     std::function<bool (const nex*)>                  m_call_on_result;
     std::function<bool (unsigned)>                    m_var_is_fixed;
-    std::function<unsigned ()>                        m_random;    
+    random_gen                                        m_random;
     bool                                              m_done = false;
     ptr_vector<nex>                                   m_b_split_vec;
     int                                               m_reported = 0;
@@ -45,11 +48,13 @@ public:
     
     cross_nested(std::function<bool (const nex*)> call_on_result,
                  std::function<bool (unsigned)> var_is_fixed,
-                 std::function<unsigned ()> random,
-                 nex_creator& nex_cr) :
+                 reslimit& limit,
+                 unsigned random_seed,
+                 nex_creator& nex_cr) : 
+        m_limit(limit),
         m_call_on_result(call_on_result),
         m_var_is_fixed(var_is_fixed),
-        m_random(random),
+        m_random(random_seed),
         m_done(false),
         m_reported(0),
         m_mk_scalar([this]{return m_nex_creator.mk_scalar(rational(1));}),
@@ -279,6 +284,8 @@ public:
         TRACE(nla_cn, tout << "m_e=" << *m_e << "\nc=" << **c << "\nj = " << nex_creator::ch(j) << "\nfront="; print_front(front, tout) << "\n";);
         if (!split_with_var(*c, j, front))
             return;
+        if (!m_limit.inc())
+            return;
         TRACE(nla_cn, tout << "after split c=" << **c << "\nfront="; print_front(front, tout) << "\n";);
         if (front.empty()) {
 #ifdef Z3DEBUG
diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp
index 2afad8980..89c528a9d 100644
--- a/src/math/lp/horner.cpp
+++ b/src/math/lp/horner.cpp
@@ -90,7 +90,9 @@ bool horner::lemmas_on_row(const T& row) {
     cross_nested cn(
         [this, dep](const nex* n) { return c().m_intervals.check_nex(n, dep); },
         [this](unsigned j)   { return c().var_is_fixed(j); },
-        [this]() { return c().random(); }, m_nex_creator);
+        c().reslim(),
+        c().random(),
+        m_nex_creator);
     bool ret = lemmas_on_expr(cn, to_sum(e));
     c().m_intervals.get_dep_intervals().reset(); // clean the memory allocated by the interval bound dependencies
     return ret;
diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp
index 09660a2a6..6203dd409 100644
--- a/src/math/lp/nla_grobner.cpp
+++ b/src/math/lp/nla_grobner.cpp
@@ -678,7 +678,9 @@ namespace nla {
         cross_nested cn(
             [this, dep](const nex* n) { return c().m_intervals.check_nex(n, dep);  },
             [this](unsigned j)   { return c().var_is_fixed(j); },
-            [this]() { return c().random(); }, nc);
+            c().reslim(), 
+            c().random(),
+            nc);
         cn.run(to_sum(e));
         bool ret = cn.done();
         return ret;
diff --git a/src/smt/smt_parallel2.cpp b/src/smt/smt_parallel2.cpp
index 234ed7b6c..7aafcc5e1 100644
--- a/src/smt/smt_parallel2.cpp
+++ b/src/smt/smt_parallel2.cpp
@@ -192,7 +192,7 @@ namespace smt {
         ctx = alloc(context, m, m_smt_params, p.ctx.get_params());
         context::copy(p.ctx, *ctx, true);
         ctx->set_random_seed(id + m_smt_params.m_random_seed);
-
+        
         smt_parallel_params pp(p.ctx.m_params);
         m_config.m_threads_max_conflicts = ctx->get_fparams().m_threads_max_conflicts;
         m_config.m_max_conflicts = ctx->get_fparams().m_max_conflicts;