diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index bf38a9269..08ff3b0d4 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -789,6 +789,8 @@ namespace lp {
     void lar_solver::detect_rows_with_changed_bounds() {
         for (auto j : m_columns_with_changed_bounds)
             detect_rows_with_changed_bounds_for_column(j);
+        if (m_find_monics_with_changed_bounds_func)
+            m_find_monics_with_changed_bounds_func(m_columns_with_changed_bounds);
     }
 
     void lar_solver::update_x_and_inf_costs_for_columns_with_changed_bounds_tableau() {
diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h
index 4b8cd0c1b..acab137b5 100644
--- a/src/math/lp/lar_solver.h
+++ b/src/math/lp/lar_solver.h
@@ -670,6 +670,7 @@ class lar_solver : public column_namer {
             return 0;
         return m_usage_in_terms[j];
     }
+    std::function<void (const indexed_uint_set& columns_with_changed_bound)> m_find_monics_with_changed_bounds_func = nullptr;
     friend int_solver;
     friend int_branch;
 };
diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp
index e21891ee4..77e01c2db 100644
--- a/src/math/lp/monomial_bounds.cpp
+++ b/src/math/lp/monomial_bounds.cpp
@@ -259,8 +259,8 @@ namespace nla {
     }
 
     void monomial_bounds::unit_propagate() {        
-        for (auto const& m : c().m_emons) 
-            unit_propagate(m);
+        for (lpvar v : c().m_monics_with_changed_bounds) 
+            unit_propagate(c().emons()[v]);
     }
 
     void monomial_bounds::unit_propagate(monic const& m) {
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 4d4fa6cbe..cc2f0f1b5 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -21,28 +21,40 @@ namespace nla {
 
 typedef lp::lar_term term;
 
-core::core(lp::lar_solver& s, params_ref const& p, reslimit & lim) :
-    m_evars(),
-    lra(s),
-    m_reslim(lim),
-    m_params(p),
-    m_tangents(this),
-    m_basics(this),
-    m_order(this),
-    m_monotone(this),
-    m_powers(*this),
-    m_divisions(*this),
-    m_intervals(this, lim),
-    m_monomial_bounds(this),
-    m_horner(this),
-    m_grobner(this),
-    m_emons(m_evars),
-    m_use_nra_model(false),
-    m_nra(s, m_nra_lim, *this) 
-{
+core::core(lp::lar_solver& s, params_ref const& p, reslimit& lim) : m_evars(),
+                                                                    lra(s),
+                                                                    m_reslim(lim),
+                                                                    m_params(p),
+                                                                    m_tangents(this),
+                                                                    m_basics(this),
+                                                                    m_order(this),
+                                                                    m_monotone(this),
+                                                                    m_powers(*this),
+                                                                    m_divisions(*this),
+                                                                    m_intervals(this, lim),
+                                                                    m_monomial_bounds(this),
+                                                                    m_horner(this),
+                                                                    m_grobner(this),
+                                                                    m_emons(m_evars),
+                                                                    m_use_nra_model(false),
+                                                                    m_nra(s, m_nra_lim, *this) {
     m_nlsat_delay = lp_settings().nlsat_delay();
+    lra.m_find_monics_with_changed_bounds_func = [&](const indexed_uint_set& columns_with_changed_bounds) {
+    m_monics_with_changed_bounds.clear();
+    for (const auto& m : m_emons) {
+        if (columns_with_changed_bounds.contains(m.var())) {
+            m_monics_with_changed_bounds.push_back(m.var());
+            continue;
+        }
+        for (lpvar j : m.vars()) {
+            if (columns_with_changed_bounds.contains(j)) {
+                m_monics_with_changed_bounds.push_back(m.var());
+                break;
+            }
+        }
+    } };
 }
-    
+
 bool core::compare_holds(const rational& ls, llc cmp, const rational& rs) const {
     switch(cmp) {
     case llc::LE: return ls <= rs;
diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
index 9c96f2fbf..8dee571ae 100644
--- a/src/math/lp/nla_core.h
+++ b/src/math/lp/nla_core.h
@@ -87,7 +87,8 @@ class core {
     std::function<bool(lpvar)> m_relevant;
     vector<lemma> *          m_lemma_vec;
     vector<ineq> *           m_literal_vec = nullptr;
-    indexed_uint_set                m_to_refine;
+    indexed_uint_set         m_to_refine;
+    vector<lpvar>            m_monics_with_changed_bounds;
     tangents                 m_tangents;
     basics                   m_basics;
     order                    m_order;
diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h
index ae224e3ec..dd9ba2dfe 100644
--- a/src/smt/theory_arith_aux.h
+++ b/src/smt/theory_arith_aux.h
@@ -1532,8 +1532,6 @@ namespace smt {
         bool max, 
         bool maintain_integrality, 
         bool& has_shared) {
-        return UNBOUNDED;    
-
         m_stats.m_max_min++;
         unsigned best_efforts = 0;
         bool inc = false;