diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index c7a29e9a7..1c8d2e832 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1327,12 +1327,18 @@ lbool core::check(unsigned level) {
 
         if (lp_settings().get_cancel_flag())
             return l_undef;
+
+        if (params().arith_nl_nra_before_lemma_return() && should_run_bounded_nlsat()) {
+            ret = bounded_nlsat();
+            if (ret == l_true)
+                return l_true;
+        }
+
         if (!m_lemmas.empty() || !m_literals.empty() || m_check_feasible)
             return l_false;
     }
 
-    
-    if (no_effect() && should_run_bounded_nlsat()) 
+    if (!params().arith_nl_nra_before_lemma_return() && no_effect() && should_run_bounded_nlsat()) 
         ret = bounded_nlsat();
                 
     if (no_effect()) 
diff --git a/src/params/smt_params_helper.pyg b/src/params/smt_params_helper.pyg
index 451a07964..0f8a7675c 100644
--- a/src/params/smt_params_helper.pyg
+++ b/src/params/smt_params_helper.pyg
@@ -86,6 +86,7 @@ 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'),