diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index ff5b72159..9c054830c 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1118,7 +1118,7 @@ public:
             (v != null_theory_var) &&
             (v < static_cast<theory_var>(m_theory_var2var_index.size())) && 
             (UINT_MAX != m_theory_var2var_index[v]) &&
-            !m_variable_values.empty();
+            (!m_variable_values.empty() || m_solver->is_term(m_theory_var2var_index[v]));
     }
 
     bool can_get_bound(theory_var v) const {
@@ -1163,13 +1163,19 @@ public:
     }
         
     rational get_value(theory_var v) const {
-        if (!can_get_value(v)) return rational::zero();
+
+        if (v == null_theory_var || 
+            v >= static_cast<theory_var>(m_theory_var2var_index.size())) 
+            return rational::zero();
+            
         lp::var_index vi = m_theory_var2var_index[v];
         if (m_variable_values.count(vi) > 0)
             return m_variable_values[vi];
         
-        if(!m_solver->is_term(vi))
+        if (!m_solver->is_term(vi)) {
+            TRACE("arith", tout << "not a term v" << v << "\n";);
             return rational::zero();
+        }
         
         m_todo_terms.push_back(std::make_pair(vi, rational::one()));
         rational result(0);