diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index e20621f0b25..351d7608e64 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -1176,16 +1176,21 @@ namespace lp {
         return rp.x + m_delta * rp.y;        
     }
 
-    mpq lar_solver::get_value(tv const& t) const {
+    mpq lar_solver::get_tv_value(tv const& t) const {
         if (t.is_var())
             return get_value(t.column());
+#if 0
+        unsigned term_j = 0;
+        if (m_var_register.term_is_used(t.id(), term_j))
+            return get_value(column_index(term_j));
+#endif
         mpq r(0);
         for (const auto& p : get_term(t)) 
             r += p.coeff() * get_value(p.column());
         return r;
     }
 
-    impq lar_solver::get_ivalue(tv const& t) const {
+    impq lar_solver::get_tv_ivalue(tv const& t) const {
         if (t.is_var())
             return get_ivalue(t.column());
         impq r;
diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h
index 706ed682ad2..a5df070e176 100644
--- a/src/math/lp/lar_solver.h
+++ b/src/math/lp/lar_solver.h
@@ -524,8 +524,8 @@ class lar_solver : public column_namer {
     std::ostream& print_values(std::ostream& out) const;
     bool init_model() const;
     mpq get_value(column_index const& j) const;
-    mpq get_value(tv const& t) const;
-    impq get_ivalue(tv const& t) const;
+    mpq get_tv_value(tv const& t) const;
+    impq get_tv_ivalue(tv const& t) const;
     void get_model(std::unordered_map<var_index, mpq> & variable_values) const;
     void get_rid_of_inf_eps();
     void get_model_do_not_care_about_diff_vars(std::unordered_map<var_index, mpq> & variable_values) const;
diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index 46801131e04..57d929c2199 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -794,11 +794,11 @@ namespace arith {
 
     lp::impq solver::get_ivalue(theory_var v) const {
         SASSERT(is_registered_var(v));
-        return m_solver->get_ivalue(get_tv(v));
+        return m_solver->get_tv_ivalue(get_tv(v));
     }
 
     rational solver::get_value(theory_var v) const {
-        return is_registered_var(v) ? m_solver->get_value(get_tv(v)) : rational::zero();      
+        return is_registered_var(v) ? m_solver->get_tv_value(get_tv(v)) : rational::zero();      
     }
 
     void solver::random_update() {
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index b06001de73d..bf10cda82d7 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1409,11 +1409,11 @@ class theory_lra::imp {
  
     lp::impq get_ivalue(theory_var v) const {
         SASSERT(is_registered_var(v));       
-        return lp().get_ivalue(get_tv(v));
+        return lp().get_tv_ivalue(get_tv(v));
     }
         
     rational get_value(theory_var v) const {
-        return is_registered_var(v) ? lp().get_value(get_tv(v)) : rational::zero();        
+        return is_registered_var(v) ? lp().get_tv_value(get_tv(v)) : rational::zero();        
     }    
 
     bool m_model_is_initialized{ false };