diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp
index b16d14021..236b85d4f 100644
--- a/src/math/lp/nla_solver.cpp
+++ b/src/math/lp/nla_solver.cpp
@@ -108,4 +108,10 @@ namespace nla {
         return m_core->lemmas();
     }
 
+    void solver::propagate_bounds_for_touched_monomials() {
+        init_bound_propagation();
+        for (unsigned v : monics_with_changed_bounds()) 
+            calculate_implied_bounds_for_monic(v);        
+        reset_monics_with_changed_bounds();
+    }
 }
diff --git a/src/math/lp/nla_solver.h b/src/math/lp/nla_solver.h
index b4fba1f86..0448d840f 100644
--- a/src/math/lp/nla_solver.h
+++ b/src/math/lp/nla_solver.h
@@ -51,6 +51,6 @@ namespace nla {
         void calculate_implied_bounds_for_monic(lp::lpvar v);
         void init_bound_propagation();
         vector<nla::lemma> const& lemmas() const;        
-
+        void propagate_bounds_for_touched_monomials();
     };
 }
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index ce53b8f25..3b6a71b3d 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -2199,12 +2199,8 @@ public:
             finish_bound_propagation();
     }
     
-    void propagate_bounds_for_touched_monomials() {
-        m_nla->init_bound_propagation();
-        for (unsigned v : m_nla->monics_with_changed_bounds()) 
-            m_nla->calculate_implied_bounds_for_monic(v);
-        
-        m_nla->reset_monics_with_changed_bounds();
+    void propagate_bounds_for_monomials() {
+        m_nla->propagate_bounds_for_touched_monomials();
         for (const auto & l : m_nla->lemmas()) 
             false_case_of_check_nla(l);
     }
@@ -2215,8 +2211,7 @@ public:
         if (is_infeasible() || !should_propagate())
             return;
 
-        m_bp.init();
-        propagate_bounds_for_touched_monomials();
+        propagate_bounds_for_monomials();
 
         if (m.inc())
             finish_bound_propagation();