diff --git a/src/util/lp/antecedents.h b/src/util/lp/antecedents.h
deleted file mode 100644
index e96c92614..000000000
--- a/src/util/lp/antecedents.h
+++ /dev/null
@@ -1,10 +0,0 @@
-/*
-  Copyright (c) 2017 Microsoft Corporation
-  Author: Lev Nachmanson
-*/
-#pragma once
-
-namespace lp {
-class antecedents {
-};
-}
diff --git a/src/util/lp/int_solver.cpp b/src/util/lp/int_solver.cpp
index 56037c841..a6eea6021 100644
--- a/src/util/lp/int_solver.cpp
+++ b/src/util/lp/int_solver.cpp
@@ -5,7 +5,6 @@
 
 #include "util/lp/int_solver.h"
 #include "util/lp/lar_solver.h"
-#include "util/lp/antecedents.h"
 namespace lp {
 
 void int_solver::fix_non_base_columns() {
@@ -114,7 +113,9 @@ int int_solver::find_inf_int_boxed_base_column_with_smallest_range() {
 bool int_solver::is_gomory_cut_target() {
     m_iter_on_gomory_row->reset();
     unsigned j;
-    TRACE("gomory_cut", m_lar_solver->print_linear_iterator(m_iter_on_gomory_row, tout););
+    TRACE("gomory_cut", m_lar_solver->print_linear_iterator(m_iter_on_gomory_row, tout);
+          m_iter_on_gomory_row->reset();
+          );
 
     while (m_iter_on_gomory_row->next(j)) {
         // All non base variables must be at their bounds and assigned to rationals (that is, infinitesimals are not allowed).
@@ -126,23 +127,25 @@ bool int_solver::is_gomory_cut_target() {
             return false;
         }
     }
+    m_iter_on_gomory_row->reset();
     return true;
 }
 
 
-void int_solver::is_real_case_in_gomory_cut(const mpq & a, unsigned x_j, mpq & k, buffer<row_entry> & pol) {
+void int_solver::real_case_in_gomory_cut(const mpq & a, unsigned x_j, mpq & k, lar_term& pol, explanation & expl) {
     mpq f_0  = fractional_part(get_value(m_gomory_cut_inf_column));
     mpq new_a;
     if (at_lower(x_j)) {
         if (a.is_pos()) {
-            new_a  =  a / (mpq(1) - f_0);
+            new_a  =  a / (1 - f_0);
         }
         else {
             new_a  =  a / f_0;
             new_a.neg();
         }
         k += lower_bound(x_j).x * k;  // k.addmul(new_a, lower_bound(x_j).x); // is it a faster operation
-        //        lower(x_j)->push_justification(ante, new_a, coeffs_enabled());*/
+        
+        expl.push_justification(column_low_bound_constraint(x_j), new_a);
     }
     else {
         lp_assert(at_upper(x_j));
@@ -154,33 +157,43 @@ void int_solver::is_real_case_in_gomory_cut(const mpq & a, unsigned x_j, mpq & k
             new_a =   a / (mpq(1) - f_0); 
         }
         k += upper_bound(x_j).x * k; // k.addmul(new_a, upper_bound(x_j).get_rational());
-        //        upper(x_j)->push_justification(ante, new_a, coeffs_enabled());*/
+        expl.push_justification(column_upper_bound_constraint(x_j), new_a);
     }
     TRACE("gomory_cut_detail", tout << a << "*v" << x_j << " k: " << k << "\n";);
-    pol.push_back(row_entry(new_a, x_j));
+    pol.add_monoid(new_a, x_j);
 }
-void int_solver::int_case_in_gomory_cut(const mpq & a, unsigned x_j, mpq & k, buffer<row_entry> & pol) {
-    /*
-    ++num_ints;
-    SASSERT(is_int(x_j));
-    mpq f_j = Ext::fractional_part(a);
+
+constraint_index int_solver::column_upper_bound_constraint(unsigned j) const {
+    return m_lar_solver->get_column_upper_bound_witness(j);
+}
+
+constraint_index int_solver::column_low_bound_constraint(unsigned j) const {
+    return m_lar_solver->get_column_low_bound_witness(j);
+}
+
+
+void int_solver::int_case_in_gomory_cut(const mpq & a, unsigned x_j, mpq & k, lar_term & pol, explanation& expl, mpq & lcm_den) {
+    mpq f_0  = fractional_part(get_value(m_gomory_cut_inf_column));
+    lp_assert(is_int(x_j));
+    mpq f_j =  fractional_part(a);
     TRACE("gomory_cut_detail", 
           tout << a << "*v" << x_j << "\n";
-          tout << "fractional_part: " << Ext::fractional_part(a) << "\n";
+          tout << "fractional_part: " << fractional_part(a) << "\n";
           tout << "f_j: " << f_j << "\n";
           tout << "f_0: " << f_0 << "\n";
-          tout << "one_minus_f_0: " << one_minus_f_0 << "\n";);
+          tout << "one_minus_f_0: " << 1 - f_0 << "\n";);
     if (!f_j.is_zero()) {
         mpq new_a;
         if (at_lower(x_j)) {
+            auto one_minus_f_0 = 1 - f_0;
             if (f_j <= one_minus_f_0) {
                 new_a = f_j / one_minus_f_0;
             }
             else {
-                new_a = (mpq(1) - f_j) / f_0;
+                new_a = (1 - f_j) / f_0;
             }
-            k.addmul(new_a, lower_bound(x_j).get_rational());
-            lower(x_j)->push_justification(ante, new_a, coeffs_enabled());
+            k.addmul(new_a, lower_bound(x_j).x);
+            expl.push_justification(column_low_bound_constraint(x_j), new_a);
         }
         else {
             SASSERT(at_upper(x_j));
@@ -188,111 +201,96 @@ void int_solver::int_case_in_gomory_cut(const mpq & a, unsigned x_j, mpq & k, bu
                 new_a = f_j / f_0;
             }
             else {
-                new_a = (mpq(1) - f_j) / one_minus_f_0;
+                new_a = (mpq(1) - f_j) / 1 - f_0;
             }
             new_a.neg(); // the upper terms are inverted
-            k.addmul(new_a, upper_bound(x_j).get_rational());
-            upper(x_j)->push_justification(ante, new_a, coeffs_enabled());
+            k.addmul(new_a, upper_bound(x_j).x);
+            expl.push_justification(column_upper_bound_constraint(x_j), new_a);
         }
         TRACE("gomory_cut_detail", tout << "new_a: " << new_a << " k: " << k << "\n";);
-        pol.push_back(row_entry(new_a, x_j));
+        pol.add_monoid(new_a, x_j);
         lcm_den = lcm(lcm_den, denominator(new_a));
-        }*/
+    }
 }
 
-lia_move int_solver::mk_gomory_cut(explanation & ex) {
+lia_move int_solver::mk_gomory_cut(lar_term& t, mpq& k, explanation & expl ) {
 
     lp_assert(column_is_int_inf(m_gomory_cut_inf_column));
 
-    TRACE("gomory_cut", tout << "applying cut at:\n"; m_lar_solver->print_linear_iterator(m_iter_on_gomory_row, tout); tout << "\n";);
+    TRACE("gomory_cut", tout << "applying cut at:\n"; m_lar_solver->print_linear_iterator(m_iter_on_gomory_row, tout); tout << std::endl; m_iter_on_gomory_row->reset(););
         
-    antecedents ante();
-    // gomory will be   pol >= k
-    mpq k(1);
-    buffer<row_entry> pol;
-       
-    mpq f_0  = fractional_part(get_value(m_gomory_cut_inf_column));
-    mpq one_minus_f_0 = mpq(1) - f_0;
-    lp_assert(!is_zero(f_0) && !is_zero(one_minus_f_0));
+    // gomory will be   t >= k
+    k = 1;
     mpq lcm_den(1);
     unsigned num_ints = 0;
     unsigned x_j;
     mpq a;
-
     while (m_iter_on_gomory_row->next(a, x_j)) {
         if (x_j == m_gomory_cut_inf_column)
             continue;
         // make the format compatible with the format used in: Integrating Simplex with DPLL(T)
         a.neg();  
         if (is_real(x_j)) 
-            is_real_case_in_gomory_cut(a, x_j, k, pol);
-        else
-            int_case_in_gomory_cut(a, x_j, k, pol);
+            real_case_in_gomory_cut(a, x_j, k, t, expl);
+        else {
+            num_ints++;
+            int_case_in_gomory_cut(a, x_j, k, t, expl, lcm_den);
+        }
     }
-    /*
-    CTRACE("empty_pol", pol.empty(), display_row_info(tout, r););
 
-    expr_ref bound(get_manager());
-    if (pol.empty()) {
-        SASSERT(k.is_pos());
+    if (t.is_empty()) {
+        TRACE("empty_pol",
+              display_row_info(tout,
+                               m_lar_solver->m_mpq_lar_core_solver.m_r_heading[m_gomory_cut_inf_column]););
+        lp_assert(k.is_pos());
         // conflict 0 >= k where k is positive
-        set_conflict(ante, ante, "gomory-cut");
-        return true;
+        k.neg(); // returning 0 <= -k
+        return lia_move::conflict;
     }
-    else if (pol.size() == 1) {
-        theory_var v = pol[0].m_var;
-        k /= pol[0].m_coeff;
-        bool is_lower = pol[0].m_coeff.is_pos();
-        if (is_int(v) && !k.is_int()) {
+
+    auto pol = t.coeffs_as_vector();
+    if (pol.size() == 1) {
+        unsigned j = pol[0].second;
+        k /= pol[0].first;
+        bool is_lower = pol[0].first.is_pos();
+        if (is_int(j) && !k.is_int()) {
             k = is_lower?ceil(k):floor(k);
         }
-        rational _k = k.to_rational();
-        if (is_lower)
-            bound = m_util.mk_ge(get_enode(v)->get_owner(), m_util.mk_numeral(_k, is_int(v)));
-        else
-            bound = m_util.mk_le(get_enode(v)->get_owner(), m_util.mk_numeral(_k, is_int(v)));
-    }
-    else { 
+        if (is_lower) { // returning -t <= -k which is equivalent to t >= k
+            k.neg();
+            t.negate();
+        }
+    } else { 
         if (num_ints > 0) {
             lcm_den = lcm(lcm_den, denominator(k));
             TRACE("gomory_cut_detail", tout << "k: " << k << " lcm_den: " << lcm_den << "\n";
-                  for (unsigned i = 0; i < pol.size(); i++) {
-                      tout << pol[i].m_coeff << " " << pol[i].m_var << "\n";
-                  }
-                  tout << "k: " << k << "\n";);
+                  linear_combination_iterator_on_vector<mpq> pi(pol);
+                  m_lar_solver->print_linear_iterator(&pi, tout);
+                  tout << "\nk: " << k << "\n";);
             SASSERT(lcm_den.is_pos());
             if (!lcm_den.is_one()) {
                 // normalize coefficients of integer parameters to be integers.
-                unsigned n = pol.size();
-                for (unsigned i = 0; i < n; i++) {
-                    pol[i].m_coeff *= lcm_den;
-                    SASSERT(!is_int(pol[i].m_var) || pol[i].m_coeff.is_int());
+                for (auto & pi: pol) {
+                    pi.first *= lcm_den;
+                    SASSERT(!is_int(pi.second) || pi.first.is_int());
                 }
                 k *= lcm_den;
             }
             TRACE("gomory_cut_detail", tout << "after *lcm\n";
                   for (unsigned i = 0; i < pol.size(); i++) {
-                      tout << pol[i].m_coeff << " * v" << pol[i].m_var << "\n";
+                      tout << pol[i].first << " * v" << pol[i].second << "\n";
                   }
                   tout << "k: " << k << "\n";);
+            t.clear();
+            // negate everything to return -pol <= -k
+            for (const auto & pi: pol)
+                t.add_monoid(-pi.first, pi.second);
+            k.neg();
+        } else {
+            lp_assert(false); // not sure what happens here
         }
-        mk_polynomial_ge(pol.size(), pol.c_ptr(), k.to_rational(), bound);            */
-    /*
-    TRACE("gomory_cut", tout << "new cut:\n" << bound << "\n"; ante.display(tout););
-    literal l     = null_literal;
-    context & ctx = get_context();
-    ctx.internalize(bound, true);
-    l = ctx.get_literal(bound);
-    ctx.mark_as_relevant(l);
-    dump_lemmas(l, ante);
-    ctx.assign(l, ctx.mk_justification(
-                                       gomory_cut_justification(
-                                                                get_id(), ctx.get_region(), 
-                                                                ante.lits().size(), ante.lits().c_ptr(), 
-                                                                ante.eqs().size(), ante.eqs().c_ptr(), ante, l)));
-    return true;
-    */
-   return lia_move::give_up;
+    }
+    return lia_move::cut;
 }
 
 void int_solver::init_check_data() {
@@ -317,7 +315,7 @@ lia_move int_solver::proceed_with_gomory_cut(lar_term& t, mpq& k, explanation& e
     if (j != -1) {
         m_found_free_var_in_gomory_row = true;
         lp_assert(t.is_empty());
-        t.add_to_map(j, mpq(1));
+        t.add_monoid(mpq(1), j);
         k = zero_of_type<mpq>();
         return lia_move::branch; // branch on a free column
     }
@@ -328,7 +326,7 @@ lia_move int_solver::proceed_with_gomory_cut(lar_term& t, mpq& k, explanation& e
         return lia_move::continue_with_check;
     }
 
-    lia_move ret = mk_gomory_cut(ex);
+    lia_move ret = mk_gomory_cut(t, k, ex);
     delete m_iter_on_gomory_row;
     m_iter_on_gomory_row = nullptr;
     return ret;
@@ -387,7 +385,7 @@ lia_move int_solver::check(lar_term& t, mpq& k, explanation& ex) {
             TRACE("arith_int", tout << "j" << j << " does not have an integer assignment: " << get_value(j) << "\n";);
 
             lp_assert(t.is_empty());
-            t.add_to_map(j, mpq(1));
+            t.add_monoid(1, j);
             k = floor(get_value(j));
             TRACE("arith_int", tout << "branching v" << j << " = " << get_value(j) << "\n";
               display_column(tout, j);
@@ -906,4 +904,22 @@ lp_settings& int_solver::settings() {
     return m_lar_solver->settings();
 }
 
+void int_solver::display_row_info(std::ostream & out, unsigned row_index) const  {
+    auto & rslv = m_lar_solver->m_mpq_lar_core_solver.m_r_solver;
+    auto it = m_lar_solver->get_iterator_on_row(row_index);
+    mpq a;
+    unsigned j;
+    while (it->next(a, j)) {
+        if (numeric_traits<mpq>::is_pos(a))
+            out << "+";
+        out << a << rslv.column_name(j) << " ";
+    }
+
+    it->reset();
+    while(it->next(j)) {
+        rslv.print_column_bound_info(j, out);
+    }
+    rslv.print_column_bound_info(rslv.m_basis[row_index], out);
+    delete it;
+}
 }
diff --git a/src/util/lp/int_solver.h b/src/util/lp/int_solver.h
index 22d37d9a6..18b44dccb 100644
--- a/src/util/lp/int_solver.h
+++ b/src/util/lp/int_solver.h
@@ -8,7 +8,6 @@
 #include "util/lp/iterator_on_row.h"
 #include "util/lp/int_set.h"
 #include "util/lp/lar_term.h"
-
 namespace lp {
 class lar_solver;
 template <typename T, typename X>
@@ -24,14 +23,12 @@ enum class lia_move {
 
 struct explanation {
     vector<std::pair<mpq, constraint_index>> m_explanation;
+    void push_justification(constraint_index j, const mpq& v) {
+        m_explanation.push_back(std::make_pair(v, j));
+    }
 };
 
 class int_solver {
-    struct row_entry {
-        mpq m_coeff;
-        unsigned m_var;
-        row_entry(const mpq & coeff, unsigned var) : m_coeff(coeff), m_var(var) {}
-    };
 public:
     // fields
     lar_solver *m_lar_solver;
@@ -108,7 +105,7 @@ private:
     lp_settings& settings();
     void move_non_base_vars_to_bounds();
     void branch_infeasible_int_var(unsigned);
-    lia_move mk_gomory_cut(explanation & ex);
+    lia_move mk_gomory_cut(lar_term& t, mpq& k,explanation & ex);
 	void init_check_data();
     bool constrain_free_vars(linear_combination_iterator<mpq> *  r);
     lia_move proceed_with_gomory_cut(lar_term& t, mpq& k, explanation& ex);
@@ -127,7 +124,10 @@ private:
         lp_assert(is_rational);
         return n.x - floor(n.x);
     }
-    void is_real_case_in_gomory_cut(const mpq & a, unsigned x_j, mpq & k, buffer<row_entry> & pol);
-    void int_case_in_gomory_cut(const mpq & a, unsigned x_j, mpq & k, buffer<row_entry> & pol);
+    void real_case_in_gomory_cut(const mpq & a, unsigned x_j, mpq & k, lar_term& t, explanation & ex);
+    void int_case_in_gomory_cut(const mpq & a, unsigned x_j, mpq & k, lar_term& t, explanation& ex, mpq & lcm_den);
+    constraint_index column_upper_bound_constraint(unsigned j) const;
+    constraint_index column_low_bound_constraint(unsigned j) const;
+    void display_row_info(std::ostream & out, unsigned row_index) const;
 };
 }
diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp
index 3cef85ce2..451be98fe 100644
--- a/src/util/lp/lar_solver.cpp
+++ b/src/util/lp/lar_solver.cpp
@@ -237,7 +237,7 @@ void lar_solver::explain_implied_bound(implied_bound & ib, bound_propagator & bp
         } 
         int a_sign = is_pos(a)? 1: -1;
         int sign = j_sign * a_sign;
-        const ul_pair & ul =  m_vars_to_ul_pairs[j];
+        const ul_pair & ul =  m_columns_to_ul_pairs[j];
         auto witness = sign > 0? ul.upper_bound_witness(): ul.low_bound_witness();
         lp_assert(is_valid(witness));
         bp.consume(a, witness);
@@ -309,7 +309,7 @@ lp_status lar_solver::solve() {
 void lar_solver::fill_explanation_from_infeasible_column(vector<std::pair<mpq, constraint_index>> & evidence) const{
 
     // this is the case when the lower bound is in conflict with the upper one
-    const ul_pair & ul =  m_vars_to_ul_pairs[m_infeasible_column_index];
+    const ul_pair & ul =  m_columns_to_ul_pairs[m_infeasible_column_index];
     evidence.push_back(std::make_pair(numeric_traits<mpq>::one(), ul.upper_bound_witness()));
     evidence.push_back(std::make_pair(-numeric_traits<mpq>::one(), ul.low_bound_witness()));
 }
@@ -325,7 +325,7 @@ vector<unsigned> lar_solver::get_list_of_all_var_indices() const {
 void lar_solver::push() {
     m_simplex_strategy = m_settings.simplex_strategy();
     m_simplex_strategy.push();
-    m_vars_to_ul_pairs.push();
+    m_columns_to_ul_pairs.push();
     m_infeasible_column_index.push();
     m_mpq_lar_core_solver.push();
     m_term_count = m_terms.size();
@@ -354,14 +354,14 @@ void lar_solver::pop(unsigned k) {
 
     int n_was = static_cast<int>(m_ext_vars_to_columns.size());
     m_infeasible_column_index.pop(k);
-    unsigned n = m_vars_to_ul_pairs.peek_size(k);
+    unsigned n = m_columns_to_ul_pairs.peek_size(k);
     for (unsigned j = n_was; j-- > n;)
         m_ext_vars_to_columns.erase(m_columns_to_ext_vars_or_term_indices[j]);
     m_columns_to_ext_vars_or_term_indices.resize(n);
     if (m_settings.use_tableau()) {
         pop_tableau();
     }
-    m_vars_to_ul_pairs.pop(k);
+    m_columns_to_ul_pairs.pop(k);
 
     m_mpq_lar_core_solver.pop(k);
     clean_popped_elements(n, m_columns_with_changed_bound);
@@ -531,15 +531,15 @@ void lar_solver::pop_core_solver_params(unsigned k) {
 
 
 void lar_solver::set_upper_bound_witness(var_index j, constraint_index ci) {
-    ul_pair ul = m_vars_to_ul_pairs[j];
+    ul_pair ul = m_columns_to_ul_pairs[j];
     ul.upper_bound_witness() = ci;
-    m_vars_to_ul_pairs[j] = ul;
+    m_columns_to_ul_pairs[j] = ul;
 }
 
 void lar_solver::set_low_bound_witness(var_index j, constraint_index ci) {
-    ul_pair ul = m_vars_to_ul_pairs[j];
+    ul_pair ul = m_columns_to_ul_pairs[j];
     ul.low_bound_witness() = ci;
-    m_vars_to_ul_pairs[j] = ul;
+    m_columns_to_ul_pairs[j] = ul;
 }
 
 void lar_solver::register_one_coeff_in_map(std::unordered_map<var_index, mpq> & coeffs, const mpq & a, unsigned j) {
@@ -1041,11 +1041,11 @@ mpq lar_solver::sum_of_right_sides_of_explanation(const vector<std::pair<mpq, un
 
 bool lar_solver::has_lower_bound(var_index var, constraint_index& ci, mpq& value, bool& is_strict) {
 
-    if (var >= m_vars_to_ul_pairs.size()) {
+    if (var >= m_columns_to_ul_pairs.size()) {
         // TBD: bounds on terms could also be used, caller may have to track these.
         return false;
     }
-    const ul_pair & ul = m_vars_to_ul_pairs[var];
+    const ul_pair & ul = m_columns_to_ul_pairs[var];
     ci = ul.low_bound_witness();
     if (ci != static_cast<constraint_index>(-1)) {
         auto& p = m_mpq_lar_core_solver.m_r_low_bounds()[var];
@@ -1060,11 +1060,11 @@ bool lar_solver::has_lower_bound(var_index var, constraint_index& ci, mpq& value
     
 bool lar_solver::has_upper_bound(var_index var, constraint_index& ci, mpq& value, bool& is_strict) {
 
-    if (var >= m_vars_to_ul_pairs.size()) {
+    if (var >= m_columns_to_ul_pairs.size()) {
         // TBD: bounds on terms could also be used, caller may have to track these.
         return false;
     }
-    const ul_pair & ul = m_vars_to_ul_pairs[var];
+    const ul_pair & ul = m_columns_to_ul_pairs[var];
     ci = ul.upper_bound_witness();
     if (ci != static_cast<constraint_index>(-1)) {
         auto& p = m_mpq_lar_core_solver.m_r_upper_bounds()[var];
@@ -1105,7 +1105,7 @@ void lar_solver::get_infeasibility_explanation_for_inf_sign(
         unsigned j = it.second;
 
         int adj_sign = coeff.is_pos() ? inf_sign : -inf_sign;
-        const ul_pair & ul = m_vars_to_ul_pairs[j];
+        const ul_pair & ul = m_columns_to_ul_pairs[j];
 
         constraint_index bound_constr_i = adj_sign < 0 ? ul.upper_bound_witness() : ul.low_bound_witness();
         lp_assert(bound_constr_i < m_constraints.size());
@@ -1238,7 +1238,7 @@ void lar_solver::pop() {
 }
 
 bool lar_solver::column_represents_row_in_tableau(unsigned j) {
-    return m_vars_to_ul_pairs()[j].m_i != static_cast<row_index>(-1);
+    return m_columns_to_ul_pairs()[j].m_i != static_cast<row_index>(-1);
 }
 
 void lar_solver::make_sure_that_the_bottom_right_elem_not_zero_in_tableau(unsigned i, unsigned j) {
@@ -1462,9 +1462,9 @@ var_index lar_solver::add_var(unsigned ext_j, bool is_int) {
 	if (it != m_ext_vars_to_columns.end()) {
 		return it->second.ext_j();
 	}
-	lp_assert(m_vars_to_ul_pairs.size() == A_r().column_count());
+	lp_assert(m_columns_to_ul_pairs.size() == A_r().column_count());
 	i = A_r().column_count();
-	m_vars_to_ul_pairs.push_back(ul_pair(static_cast<unsigned>(-1)));
+	m_columns_to_ul_pairs.push_back(ul_pair(static_cast<unsigned>(-1)));
 	add_non_basic_var_to_core_fields(ext_j, is_int);
 	lp_assert(sizes_are_correct());
 	return i;
@@ -1568,7 +1568,7 @@ void lar_solver::add_row_from_term_no_constraint(const lar_term * term, unsigned
 	// j will be a new variable
 	unsigned j = A_r().column_count();
 	ul_pair ul(j);
-	m_vars_to_ul_pairs.push_back(ul);
+	m_columns_to_ul_pairs.push_back(ul);
 	add_basic_var_to_core_fields();
 	if (use_tableau()) {
 		auto it = iterator_on_term_with_basis_var(*term, j);
@@ -1677,7 +1677,7 @@ void lar_solver::add_constraint_from_term_and_create_new_column_row(unsigned ter
 
 void lar_solver::decide_on_strategy_and_adjust_initial_state() {
 	lp_assert(strategy_is_undecided());
-	if (m_vars_to_ul_pairs.size() > m_settings.column_number_threshold_for_using_lu_in_lar_solver) {
+	if (m_columns_to_ul_pairs.size() > m_settings.column_number_threshold_for_using_lu_in_lar_solver) {
 		m_settings.simplex_strategy() = simplex_strategy_enum::lu;
 	}
 	else {
diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h
index 491bc0167..9afb4180b 100644
--- a/src/util/lp/lar_solver.h
+++ b/src/util/lp/lar_solver.h
@@ -52,7 +52,7 @@ class lar_solver : public column_namer {
     stacked_value<simplex_strategy_enum> m_simplex_strategy;
     std::unordered_map<unsigned, ext_var_info> m_ext_vars_to_columns;
     vector<unsigned> m_columns_to_ext_vars_or_term_indices;
-    stacked_vector<ul_pair> m_vars_to_ul_pairs;
+    stacked_vector<ul_pair> m_columns_to_ul_pairs;
     vector<lar_base_constraint*> m_constraints;
     stacked_value<unsigned> m_constraint_count;
     // the set of column indices j such that bounds have changed for j
@@ -433,7 +433,7 @@ public:
     }
 
     void get_bound_constraint_witnesses_for_column(unsigned j, constraint_index & lc, constraint_index & uc) const {
-        const ul_pair & ul = m_vars_to_ul_pairs[j];
+        const ul_pair & ul = m_columns_to_ul_pairs[j];
         lc = ul.low_bound_witness();
         uc = ul.upper_bound_witness();
     }
@@ -453,6 +453,13 @@ public:
         return m_mpq_lar_core_solver.m_r_solver.get_base_column_in_row(row_index);
     }
 
-    
+    constraint_index get_column_upper_bound_witness(unsigned j) const {
+        return m_columns_to_ul_pairs()[j].upper_bound_witness();
+    }
+
+    constraint_index get_column_low_bound_witness(unsigned j) const {
+        return m_columns_to_ul_pairs()[j].low_bound_witness();
+    }
+
 };
 }
diff --git a/src/util/lp/lar_term.h b/src/util/lp/lar_term.h
index 71320b7c3..dc3921767 100644
--- a/src/util/lp/lar_term.h
+++ b/src/util/lp/lar_term.h
@@ -10,7 +10,7 @@ struct lar_term {
     std::unordered_map<unsigned, mpq> m_coeffs;
     mpq m_v;
     lar_term() {}
-    void add_to_map(unsigned j, const mpq& c) {
+    void add_monoid(const mpq& c, unsigned j) {
         auto it = m_coeffs.find(j);
         if (it == m_coeffs.end()) {
             m_coeffs.emplace(j, c);
@@ -34,7 +34,7 @@ struct lar_term {
     lar_term(const vector<std::pair<mpq, unsigned>>& coeffs,
              const mpq & v) : m_v(v) {
         for (const auto & p : coeffs) {
-            add_to_map(p.second, p.first);
+            add_monoid(p.first, p.second);
         }
     }
     bool operator==(const lar_term & a) const {  return false; } // take care not to create identical terms
@@ -56,7 +56,7 @@ struct lar_term {
         if (it == m_coeffs.end()) return;
         const mpq & b = it->second;
         for (unsigned it_j :li.m_index) {
-            add_to_map(it_j, - b * li.m_data[it_j]);
+            add_monoid(- b * li.m_data[it_j], it_j);
         }
         m_coeffs.erase(it);
     }
@@ -64,5 +64,16 @@ struct lar_term {
     bool contains(unsigned j) const {
         return m_coeffs.find(j) != m_coeffs.end();
     }
+
+    void negate() {
+        for (auto & t : m_coeffs)
+            t.second.neg();
+    }
+
+    void clear() {
+        m_coeffs.clear();
+        m_v = zero_of_type<mpq>();
+    }
+    
 };
 }