diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 605498e53..babafe129 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -3329,7 +3329,8 @@ public:
             st = lp::lp_status::UNBOUNDED;
         }
         else {
-            st = m_solver->maximize_term(v, term_max);
+            vi = m_theory_var2var_index[v];
+            st = m_solver->maximize_term(vi, term_max);
         }
         switch (st) {
         case lp::lp_status::OPTIMAL: {
diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp
index 2daedc045..879dfd32f 100644
--- a/src/util/lp/lar_solver.cpp
+++ b/src/util/lp/lar_solver.cpp
@@ -505,24 +505,23 @@ bool lar_solver::remove_from_basis(unsigned j) {
     return m_mpq_lar_core_solver.m_r_solver.remove_from_basis(j);
 }
 
-lar_term lar_solver::get_term_to_maximize(unsigned ext_j) const {
-    unsigned local_j;
-    if (m_var_register.external_is_used(ext_j, local_j)) {
+lar_term lar_solver::get_term_to_maximize(unsigned j_or_term) const {
+    if (is_term(j_or_term))
+        return get_term(j_or_term);
+    if (j_or_term < m_mpq_lar_core_solver.m_r_x.size()) {
         lar_term r;
-        r. add_monomial(one_of_type<mpq>(), local_j);
+        r.add_monomial(one_of_type<mpq>(), j_or_term);
         return r;
-    }
-    if (!is_term(ext_j) || adjust_term_index(ext_j) >= m_terms.size())
-        return lar_term(); // return an empty term
-    return get_term(ext_j);
+    } 
+    return lar_term(); // return an empty term
 }
 
-lp_status lar_solver::maximize_term(unsigned ext_j,
+lp_status lar_solver::maximize_term(unsigned j_or_term,
                                impq &term_max) {
     TRACE("lar_solver", print_values(tout););
     bool was_feasible = m_mpq_lar_core_solver.m_r_solver.calc_current_x_is_feasible_include_non_basis();
     impq prev_value;
-    lar_term term = get_term_to_maximize(ext_j);
+    lar_term term = get_term_to_maximize(j_or_term);
     if (term.is_empty()) {
         return lp_status::UNBOUNDED;
     }
diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h
index 1dce8524e..39adbd86f 100644
--- a/src/util/lp/lar_solver.h
+++ b/src/util/lp/lar_solver.h
@@ -310,7 +310,7 @@ public:
                                              impq &term_max);    
     // starting from a given feasible state look for the maximum of the term
     // return true if found and false if unbounded
-    lp_status maximize_term(unsigned ext_j ,
+    lp_status maximize_term(unsigned j_or_term,
                             impq &term_max);