diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 03bd61ff1..e1648c66b 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -2344,11 +2344,14 @@ void lar_solver::deregister_normalized_term(const lar_term& t) {
 }
 
 void lar_solver::register_existing_terms() {
-    TRACE("nla_solver", tout << "registering " << m_terms.size() << " terms\n";);
-    for (unsigned k = 0; k < m_terms.size(); k++) {
-        lpvar j = m_var_register.external_to_local(k + m_terms_start_index);
-        register_normalized_term(*m_terms[k], j);
+    if (!m_need_register_terms) {
+        TRACE("nla_solver", tout << "registering " << m_terms.size() << " terms\n";);
+        for (unsigned k = 0; k < m_terms.size(); k++) {
+            lpvar j = m_var_register.external_to_local(k + m_terms_start_index);
+            register_normalized_term(*m_terms[k], j);
+        }
     }
+    m_need_register_terms = true;
 }
 // a_j.first gives the normalised coefficient,
 // a_j.second givis the column
diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h
index dce1ebe0f..b142f3082 100644
--- a/src/math/lp/lar_solver.h
+++ b/src/math/lp/lar_solver.h
@@ -87,6 +87,7 @@ public:
     lar_core_solver                                     m_mpq_lar_core_solver;
 private:
     int_solver *                                        m_int_solver;
+    bool                                                m_need_register_terms;
 public:
     const var_index                                     m_terms_start_index;
     var_register                                        m_var_register;
@@ -104,7 +105,6 @@ public:
     stacked_value<unsigned>                             m_term_count;
     vector<lar_term*>                                   m_terms;
     indexed_vector<mpq>                                 m_column_buffer;
-    bool                                                m_need_register_terms;
     std::unordered_map<lar_term, std::pair<mpq, unsigned>, term_hasher, term_comparer>
                                                         m_normalized_terms_to_columns;
     // end of fields
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 85289f81b..8b5739cb1 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -690,10 +690,7 @@ class theory_lra::imp {
 
         TRACE("arith", tout << "v" << v << " := " << mk_pp(t, m) << "\n";);
         if (!_has_var) {
-            if (m_solver->m_need_register_terms == false) {
-                m_solver->m_need_register_terms = true;
-                m_solver->register_existing_terms();
-            }
+            m_solver->register_existing_terms();            
             m_switcher.add_monic(register_theory_var_in_lar_solver(v), vars.size(), vars.c_ptr());
         }
     }