diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp
index fc9897ed3..dbf3aa35e 100644
--- a/src/util/lp/nla_solver.cpp
+++ b/src/util/lp/nla_solver.cpp
@@ -1330,7 +1330,6 @@ struct solver::imp {
     }
 
     void clear() {
-        m_to_refine.clear();
         m_var_to_its_monomial.clear();
         m_vars_equivalence.clear();
         m_rm_table.clear();
@@ -1344,10 +1343,10 @@ struct solver::imp {
         map_vars_to_monomials();
         init_vars_equivalence();
         register_monomials_in_tables();
-        init_to_refine();
     }
 
     void init_to_refine() {
+        m_to_refine.clear();
         for (unsigned i = 0; i < m_monomials.size(); i++) {
             if (!check_monomial(m_monomials[i]))
                 m_to_refine.push_back(i);
@@ -1917,11 +1916,11 @@ struct solver::imp {
             return l_undef;
         }
 
-        init_search();
+        init_to_refine();
         if (m_to_refine.empty()) {
             return l_true;
         }
-
+        init_search();
         lbool ret = l_undef;
         for (int search_level = 0; search_level < 3 && ret == l_undef; search_level++) {
             TRACE("nla_solver", tout << "search_level = " << search_level << "\n";);