diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp
index e7c842a5d..5ddd4d8e6 100644
--- a/src/util/lp/lar_solver.cpp
+++ b/src/util/lp/lar_solver.cpp
@@ -1709,8 +1709,19 @@ void lar_solver::push_and_register_term(lar_term* t) {
     m_terms.push_back(t);
 }
 
+
 // terms
+bool lar_solver::all_vars_are_registered(const vector<std::pair<mpq, var_index>> & coeffs) {
+    for (const auto & p : coeffs) {
+        if (p.second >= m_var_register.size()) {
+            return false;
+        }
+    }
+    return true;
+}
+
 var_index lar_solver::add_term(const vector<std::pair<mpq, var_index>> & coeffs) {
+    lp_assert(all_vars_are_registered(coeffs));
     if (strategy_is_undecided())
         return add_term_undecided(coeffs);
 
diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h
index 2b2438f56..6000d414c 100644
--- a/src/util/lp/lar_solver.h
+++ b/src/util/lp/lar_solver.h
@@ -176,6 +176,8 @@ public:
 
 
     // terms
+    bool all_vars_are_registered(const vector<std::pair<mpq, var_index>> & coeffs);
+
     var_index add_term(const vector<std::pair<mpq, var_index>> & coeffs);
 
     var_index add_term_undecided(const vector<std::pair<mpq, var_index>> & coeffs);