diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp
index f0d6085de6..3f5bcec5fc 100644
--- a/src/math/lp/monomial_bounds.cpp
+++ b/src/math/lp/monomial_bounds.cpp
@@ -293,6 +293,8 @@ namespace nla {
        the pass to violated monomials keeps the wins without that regression.
     */
     bool monomial_bounds::propagate_violated_linear_monomials() {
+        if (!c().params().arith_nl_linearize_violated_monomials())
+            return false;
         if (!c().lra.is_feasible())
             return false;
         bool propagated = false;
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 606155e24a..5b5068ecae 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1547,8 +1547,7 @@ bool core::propagate() {
 		propagated = true;
     if (m_monomial_bounds.propagate_changed_bounds())
         propagated = true;
-    if (params().arith_nl_linearize_violated_monomials() &&
-        m_monomial_bounds.propagate_violated_linear_monomials())
+    if (m_monomial_bounds.propagate_violated_linear_monomials())
         propagated = true;
     m_monics_with_changed_bounds.reset();
     if (propagated)