diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index a306c024a..a883de0a8 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1328,10 +1328,7 @@ lbool core::check(unsigned level) {
         if (lp_settings().get_cancel_flag())
             return l_undef;
 
-        if (params().arith_nl_nra_before_lemma_return()
-            && lp_settings().stats().m_nla_calls > 0
-            && lp_settings().stats().m_nla_calls % params().arith_nl_delay() == 0
-            && should_run_bounded_nlsat()) {
+        if (has_real_monomial() && should_run_bounded_nlsat()) {
             ret = bounded_nlsat();
             if (ret == l_true)
                 return l_true;
@@ -1341,7 +1338,7 @@ lbool core::check(unsigned level) {
             return l_false;
     }
 
-    if (!params().arith_nl_nra_before_lemma_return() && no_effect() && should_run_bounded_nlsat()) 
+    if (no_effect() && should_run_bounded_nlsat()) 
         ret = bounded_nlsat();
                 
     if (no_effect()) 
@@ -1404,6 +1401,13 @@ bool core::should_run_bounded_nlsat() {
     return m_nlsat_delay < 2;
 }
 
+bool core::has_real_monomial() const {
+    for (lpvar j : m_to_refine)
+        if (!var_is_int(j))
+            return true;
+    return false;
+}
+
 lbool core::bounded_nlsat() {
     params_ref p;
     lbool ret;
diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
index 5ccbc17e0..1916847b0 100644
--- a/src/math/lp/nla_core.h
+++ b/src/math/lp/nla_core.h
@@ -65,6 +65,7 @@ class core {
     unsigned m_nlsat_delay_bound = 0;
 
     bool should_run_bounded_nlsat();
+    bool has_real_monomial() const;
     lbool bounded_nlsat();
 
     var_eqs<emonics>         m_evars;
diff --git a/src/params/smt_params_helper.pyg b/src/params/smt_params_helper.pyg
index 0f8a7675c..451a07964 100644
--- a/src/params/smt_params_helper.pyg
+++ b/src/params/smt_params_helper.pyg
@@ -86,7 +86,6 @@ def_module_params(module_name='smt',
                           ('arith.nl.grobner_expand_terms', BOOL, True, 'expand terms before computing grobner basis'),
                           ('arith.nl.reduce_pseudo_linear', BOOL, True, 'create incremental linearization axioms for pseudo-linear monomials'),
                           ('arith.nl.delay', UINT, 10, 'number of calls to final check before invoking bounded nlsat check'),
-                          ('arith.nl.nra_before_lemma_return', BOOL, True, 'try bounded nlsat before returning lemmas from monomial bounds propagation'),
                           ('arith.nl.propagate_linear_monomials', BOOL, True, 'propagate linear monomials'),
                           ('arith.nl.optimize_bounds', BOOL, True, 'enable bounds optimization'),
                           ('arith.nl.cross_nested', BOOL, True, 'enable cross-nested consistency checking'),