diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index e3cc00816..02f90e5a1 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1469,13 +1469,12 @@ lbool core::check(vector& l_vec) { init_to_refine(); patch_monomials(); + set_use_nra_model(false); if (m_to_refine.is_empty()) { return l_true; } init_search(); lbool ret = l_undef; - set_use_nra_model(false); - if (l_vec.empty() && !done()) m_monomial_bounds();