From f486617f81e2b826845a82a442c13abd310a00da Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 17 Aug 2025 13:58:31 -0700
Subject: [PATCH] ensure that max-conflicts is propagated to nra-solver

---
 src/math/lp/nla_core.cpp | 5 ++++-
 src/smt/theory_lra.cpp   | 2 ++
 2 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 585d605c3..9a28363d7 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -38,7 +38,7 @@ core::core(lp::lar_solver& s, params_ref const& p, reslimit & lim) :
     m_grobner(this),
     m_emons(m_evars),
     m_use_nra_model(false),
-    m_nra(s, m_nra_lim, *this),
+    m_nra(s, m_nra_lim, *this, p),
     m_throttle(lra.trail(), 
 	lra.settings().stats()) {
      m_nlsat_delay_bound = lp_settings().nlsat_delay();
@@ -1561,6 +1561,9 @@ lbool core::check() {
     if (no_effect() && params().arith_nl_nra()) {
         scoped_limits sl(m_reslim);
         sl.push_child(&m_nra_lim);
+        params_ref p;
+        p.set_uint("max_conflicts", lp_settings().m_max_conflicts);
+        m_nra.updt_params(p);
         ret = m_nra.check();
         lp_settings().stats().m_nra_calls++;
     }
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index f3d9a5169..4b544fc20 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1427,6 +1427,8 @@ public:
     void init_search_eh() {
         m_arith_eq_adapter.init_search_eh();
         m_num_conflicts = 0;
+        if (m_solver)   
+           lp().settings().m_max_conflicts = ctx().get_fparams().m_max_conflicts;
     }
 
     bool can_get_value(theory_var v) const {