diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp
index cc30537eff..1416ac53dd 100644
--- a/src/math/lp/horner.cpp
+++ b/src/math/lp/horner.cpp
@@ -109,7 +109,7 @@ bool horner::horner_lemmas() {
     // exclude zero and expose conflicts. Done here (instead of core::propagate)
     // so the LP maximization only runs when horner is actually scheduled.
     // optimize_nl_bounds() checks arith.nl.optimize_bounds internally.
-    c().optimize_nl_bounds();
+    c().m_monomial_bounds.optimize_nl_bounds();
     // optimize_nl_bounds re-calibrated m_to_refine against the model it produced.
     // If nothing remains to refine, every monomial is consistent under a feasible
     // LP model: the nonlinear goal is satisfied. Declare it and stop.
@@ -145,4 +145,3 @@ bool horner::horner_lemmas() {
     return conflict;
 }
 }
-
diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp
index 0b8f2bbbb9..23260bbf65 100644
--- a/src/math/lp/monomial_bounds.cpp
+++ b/src/math/lp/monomial_bounds.cpp
@@ -1123,4 +1123,97 @@ namespace nla {
         return dep;
     }
 
+    /**
+       \brief Tighten the bounds of variables occurring in nonlinear monomials by
+       maximizing/minimizing them over the LP tableau (analogous to theory_arith's
+       max_min_nl_vars). The tighter implied bounds, each carrying an LP explanation,
+       let the subsequent horner/cross-nested interval evaluation exclude zero and
+       detect a conflict that would otherwise be missed with only the propagated
+       bounds.
+    */
+    bool monomial_bounds::optimize_nl_bounds() {
+        if (!c().params().arith_nl_optimize_bounds() || !m_bounds_optimization_enabled)
+            return false;
+
+        c().trail().push(value_trail(m_bounds_optimization_enabled));
+        m_bounds_optimization_enabled = false;
+
+        auto& lra = c().lra;
+        if (!lra.is_feasible())
+            return false;
+        if (lra.find_feasible_solution() == lp::lp_status::INFEASIBLE) {
+            // find_feasible_solution moved the model; keep m_to_refine in sync.
+            c().init_to_refine();
+            return false;
+        }
+
+        // Gather the candidate columns: every non-fixed leaf variable that
+        // participates in a monomial (mirrors solver=2's max_min_nl_vars).
+        svector<lpvar> cands;
+        auto add = [&](lpvar j) {
+            if (c().active_var_set_contains(j))
+                return;
+            c().insert_to_active_var_set(j);
+            if (lra.column_is_fixed(j))
+                return;
+            cands.push_back(j);
+        };
+        c().clear_active_var_set();
+        for (auto const& m : c().emons()) {
+            add(m.var());
+            for (lpvar k : m.vars())
+                add(k);
+        }
+
+        // Throttle: the LP maximize/minimize cost scales with the number of
+        // candidate variables (two LP optimizations each). On large nonlinear
+        // problems this pass is expensive and rarely productive, so skip it when the
+        // candidate set exceeds the threshold (0 = unlimited).
+        unsigned const max_vars = c().params().arith_nl_optimize_bounds_lp_max_vars();
+        if (max_vars != 0 && cands.size() > max_vars) {
+            // find_feasible_solution() above already moved the model, so m_to_refine
+            // is stale on this path too and has to be re-calibrated before returning.
+            c().init_to_refine();
+            return false;
+        }
+
+        // Collect improved bounds first (each improve_bound maximizes a term
+        // over the *unchanged* constraint set, so all improvements are valid implied
+        // bounds), then apply them together and re-establish feasibility once.
+        // Interleaving update_column_type_and_bound between the maximize calls
+        // corrupts the core solver's x/inf_heap (maximize_term_on_tableau issues a
+        // raw solve() that does not reconcile pending bound changes).
+        struct improved_bound { lpvar j; lp::lconstraint_kind kind; rational bound; u_dependency* dep; };
+        vector<improved_bound> improvements;
+        for (lpvar j : cands) {
+            if (!lra.is_feasible())
+                break;
+            for (bool is_lower : { true, false }) {
+                rational bound;
+                u_dependency* dep = improve_bound(j, is_lower, bound);
+                if (!dep)
+                    continue;
+                auto kind = is_lower ? lp::lconstraint_kind::GE : lp::lconstraint_kind::LE;
+                improvements.push_back({ j, kind, bound, dep });
+            }
+        }
+
+        if (improvements.empty()) {
+            // The exploratory simplex walk in improve_bound/mm_optimize mutated the
+            // LP model even though no bound was tightened.  Restore a clean feasible
+            // model and re-calibrate m_to_refine so downstream lemma passes (grobner,
+            // basic_lemma) never see a stale monomial that is now consistent.
+            lra.find_feasible_solution();
+            c().init_to_refine();
+            return false;
+        }
+
+        for (auto const& ib : improvements)
+            lra.update_column_type_and_bound(ib.j, ib.kind, ib.bound, ib.dep);
+        lra.find_feasible_solution();
+        // The model changed: re-calibrate m_to_refine against the new assignment.
+        c().init_to_refine();
+        return true;
+    }
+
 }
diff --git a/src/math/lp/monomial_bounds.h b/src/math/lp/monomial_bounds.h
index fcc206efe4..a433073df8 100644
--- a/src/math/lp/monomial_bounds.h
+++ b/src/math/lp/monomial_bounds.h
@@ -16,6 +16,7 @@ namespace nla {
     class core;
     class monomial_bounds : common {
         dep_intervals& dep;
+        bool m_bounds_optimization_enabled = true;
 
         bool tighten_lp_bound(dep_interval const &range, lpvar v, unsigned p);
         bool tighten_lp_upper_bound(dep_interval const& range, lpvar v, unsigned p);
@@ -91,6 +92,7 @@ namespace nla {
         bool propagate_linear_bounds();
         bool propagate_changed_bounds();
         bool propagate_fixed_rows();
+        bool optimize_nl_bounds();
 
         // Maximize (is_lower == false) or minimize (is_lower == true) column j
         // over the LP tableau and, if the resulting bound improves j's current
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 66224d24ba..855fa65d52 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1564,99 +1564,6 @@ bool core::incremental_propagate() {
     return propagated;    
 }
 
-/**
-   \brief Tighten the bounds of variables occurring in nonlinear monomials by
-   maximizing/minimizing them over the LP tableau (analogous to theory_arith's
-   max_min_nl_vars). The tighter implied bounds, each carrying an LP explanation,
-   let the subsequent horner/cross-nested interval evaluation exclude zero and
-   detect a conflict that would otherwise be missed with only the propagated
-   bounds.
-*/
-bool core::optimize_nl_bounds() {
-    if (!params().arith_nl_optimize_bounds() || !m_bounds_optimization_enabled)
-        return false;
-
-    trail().push(value_trail(m_bounds_optimization_enabled));
-    m_bounds_optimization_enabled = false;
-
-    if (!lra.is_feasible())
-        return false;
-    if (lra.find_feasible_solution() == lp::lp_status::INFEASIBLE) {
-        // find_feasible_solution moved the model; keep m_to_refine in sync.
-        init_to_refine();
-        return false;
-    }
-
-    // Gather the candidate columns: every non-fixed leaf variable that
-    // participates in a monomial (mirrors solver=2's max_min_nl_vars).
-    svector<lpvar> cands;
-    auto add = [&](lpvar j) {
-        if (active_var_set_contains(j))
-            return;
-        insert_to_active_var_set(j);
-        if (lra.column_is_fixed(j))
-            return;
-        cands.push_back(j);
-    };
-    clear_active_var_set();
-    for (auto const& m : m_emons) {
-        add(m.var());
-        for (lpvar k : m.vars())
-            add(k);
-    }
-
-    // Throttle: the LP maximize/minimize cost scales with the number of
-    // candidate variables (two LP optimizations each). On large nonlinear
-    // problems this pass is expensive and rarely productive, so skip it when the
-    // candidate set exceeds the threshold (0 = unlimited).
-    unsigned const max_vars = params().arith_nl_optimize_bounds_lp_max_vars();
-    if (max_vars != 0 && cands.size() > max_vars) {
-        // find_feasible_solution() above already moved the model, so m_to_refine
-        // is stale on this path too and has to be re-calibrated before returning.
-        init_to_refine();
-        return false;
-    }
-
-    // Collect improved bounds first (each find_improved_bound maximizes a term
-    // over the *unchanged* constraint set, so all improvements are valid implied
-    // bounds), then apply them together and re-establish feasibility once.
-    // Interleaving update_column_type_and_bound between the maximize calls
-    // corrupts the core solver's x/inf_heap (maximize_term_on_tableau issues a
-    // raw solve() that does not reconcile pending bound changes).
-    struct improved_bound { lpvar j; lp::lconstraint_kind kind; rational bound; u_dependency* dep; };
-    vector<improved_bound> improvements;
-    for (lpvar j : cands) {
-        if (!lra.is_feasible())
-            break;
-        for (bool is_lower : { true, false }) {
-            rational bound;
-            u_dependency* dep = m_monomial_bounds.improve_bound(j, is_lower, bound);
-            if (!dep)
-                continue;
-            auto kind = is_lower ? lp::lconstraint_kind::GE : lp::lconstraint_kind::LE;
-            improvements.push_back({ j, kind, bound, dep });
-        }
-    }
-
-    if (improvements.empty()) {
-        // The exploratory simplex walk in improve_bound/mm_optimize mutated the
-        // LP model even though no bound was tightened.  Restore a clean feasible
-        // model and re-calibrate m_to_refine so downstream lemma passes (grobner,
-        // basic_lemma) never see a stale monomial that is now consistent.
-        lra.find_feasible_solution();
-        init_to_refine();
-        return false;
-    }
-
-    for (auto const& ib : improvements)
-        lra.update_column_type_and_bound(ib.j, ib.kind, ib.bound, ib.dep);
-    lra.find_feasible_solution();
-    // The model changed: re-calibrate m_to_refine against the new assignment.
-    init_to_refine();
-    return true;
-}
-
-
 void core::simplify() {
     // in-processing simplifiation can go here, such as bounds improvements.
 }
diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
index 81976f07a5..2debf32e1d 100644
--- a/src/math/lp/nla_core.h
+++ b/src/math/lp/nla_core.h
@@ -111,7 +111,6 @@ class core {
 
     nla_throttle             m_throttle;
     bool                     m_throttle_enabled = true;
-    bool                     m_bounds_optimization_enabled = true;
 
 
 
@@ -122,8 +121,6 @@ class core {
     bool is_pseudo_linear(monic const& m) const;    
     void refine_pseudo_linear(monic const& m);
 
-    bool optimize_nl_bounds();
-
     std::ostream& display_constraint_smt(std::ostream& out, unsigned id, lp::lar_base_constraint const& c) const;
     std::ostream& display_declarations_smt(std::ostream& out) const;