diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index f1ffbf60c..b0ba51129 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1465,10 +1465,12 @@ public:
         if (!m_has_int) {
             return true;
         }
-        unsigned nv = th.get_num_vars();
+        unsigned nv = std::min(th.get_num_vars(), m_theory_var2var_index.size());
         bool all_bounded = true;
         for (unsigned v = 0; v < nv; ++v) {
             lp::var_index vi = m_theory_var2var_index[v];
+			if (vi == UINT_MAX)
+				continue;
             if (!m_solver->is_term(vi) && !var_has_bound(vi, true) && !var_has_bound(vi, false)) {
                 lp::lar_term term;
                 term.add_monomial(rational::one(), vi);
diff --git a/src/util/lp/lp_settings.h b/src/util/lp/lp_settings.h
index dd19df23a..71be7258a 100644
--- a/src/util/lp/lp_settings.h
+++ b/src/util/lp/lp_settings.h
@@ -357,7 +357,7 @@ public:
     }
     
 #ifdef Z3DEBUG
-    static unsigned ddd; // used for debugging    
+static unsigned ddd; // used for debugging    
 #endif
 }; // end of lp_settings class