From 55daa2424c192dcf19d05c955db1abc9ab6431fa Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 22 Jun 2021 12:26:27 -0700
Subject: [PATCH] fix #5362

---
 src/math/lp/nla_core.cpp | 11 ++++++++---
 src/math/lp/nla_core.h   |  1 +
 2 files changed, 9 insertions(+), 3 deletions(-)

diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 55a42c2f8..eedf46967 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -36,7 +36,7 @@ core::core(lp::lar_solver& s, reslimit & lim) :
     m_emons(m_evars),
     m_reslim(lim),
     m_use_nra_model(false),
-    m_nra(s, lim, *this)
+    m_nra(s, m_nra_lim, *this)
 {
     m_nlsat_delay = lp_settings().nlsat_delay();
 }
@@ -1563,10 +1563,15 @@ bool core::should_run_bounded_nlsat() {
 
 lbool core::bounded_nlsat() {
     params_ref p;
+    lbool ret;
     p.set_uint("max_conflicts", 100);
-    scoped_rlimit sr(m_reslim, 100000);
     m_nra.updt_params(p);
-    lbool ret = m_nra.check(); 
+    {
+        scoped_limits sl(m_reslim);
+        sl.push_child(&m_nra_lim);
+        scoped_rlimit sr(m_nra_lim, 100000);
+        ret = m_nra.check();
+    }
     p.set_uint("max_conflicts", UINT_MAX);           
     m_nra.updt_params(p);
     m_stats.m_nra_calls++;
diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
index 18baa0847..d0dc8d77d 100644
--- a/src/math/lp/nla_core.h
+++ b/src/math/lp/nla_core.h
@@ -175,6 +175,7 @@ private:
     svector<lpvar>           m_add_buffer;
     mutable lp::u_set        m_active_var_set;
     lp::u_set                m_rows;
+    reslimit                 m_nra_lim;
 public:
     reslimit&                m_reslim;
     bool                     m_use_nra_model;