diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 0eb65e197..62712914c 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -1034,14 +1034,10 @@ namespace lp {
             r += p.coeff() * get_value(p.column());
         return r;
     }
-
-    impq lar_solver::get_tv_ivalue(tv const& t) const {
-        if (t.is_var())
-            return get_column_value(t.column());
-        impq r;
-        for (lar_term::ival p : get_term(t)) 
-            r += p.coeff() * get_column_value(p.column());
-        return r;
+    //fetches the cached value of the term or the variable by the given index
+    const impq& lar_solver::get_tv_ivalue(tv const& t) const {
+        unsigned j = t.is_var()? (unsigned)t.column(): this->map_term_index_to_column_index(t.index());
+        return this->get_column_value(j);
     }
 
     void lar_solver::get_rid_of_inf_eps() {
diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h
index 182ef0be3..5b421d70d 100644
--- a/src/math/lp/lar_solver.h
+++ b/src/math/lp/lar_solver.h
@@ -506,7 +506,7 @@ public:
     bool init_model() const;
     mpq get_value(column_index const& j) const;
     mpq get_tv_value(tv const& t) const;
-    impq get_tv_ivalue(tv const& t) const;
+    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;