diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 120ce1517..513248d4b 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -2613,10 +2613,13 @@ public:
 
     bool get_lower(enode* n, expr_ref& r) {
         theory_var v = n->get_th_var(get_id());
+        if (!can_get_value(v))
+            return false;
+        lp::var_index vi = m_theory_var2var_index[v];
         lp::constraint_index ci;
         rational val;
         bool is_strict;
-        if (m_solver->has_lower_bound(v, ci, val, is_strict)) {
+        if (m_solver->has_lower_bound(vi, ci, val, is_strict)) {
             r = a.mk_numeral(val, is_int(n));
             return true;
         }
@@ -2625,10 +2628,13 @@ public:
 
     bool get_upper(enode* n, expr_ref& r) {
         theory_var v = n->get_th_var(get_id());
+        if (!can_get_value(v))
+            return false;
+        lp::var_index vi = m_theory_var2var_index[v];
         lp::constraint_index ci;
         rational val;
         bool is_strict;
-        if (m_solver->has_upper_bound(v, ci, val, is_strict)) {
+        if (m_solver->has_upper_bound(vi, ci, val, is_strict)) {
             r = a.mk_numeral(val, is_int(n));
             return true;
         }