diff --git a/src/math/lp/gomory.cpp b/src/math/lp/gomory.cpp
index fbba6fa9f..d8d8b48c1 100644
--- a/src/math/lp/gomory.cpp
+++ b/src/math/lp/gomory.cpp
@@ -50,7 +50,7 @@ class create_cut {
     const impq & upper_bound(unsigned j) const  { return m_int_solver.upper_bound(j); }
     constraint_index column_lower_bound_constraint(unsigned j) const { return m_int_solver.column_lower_bound_constraint(j); }
     constraint_index column_upper_bound_constraint(unsigned j) const { return m_int_solver.column_upper_bound_constraint(j); }
-    bool column_is_fixed(unsigned j) const { return m_int_solver.m_lar_solver->column_is_fixed(j); }
+    bool column_is_fixed(unsigned j) const { return m_int_solver.lra.column_is_fixed(j); }
 
     void int_case_in_gomory_cut(unsigned j) {
         lp_assert(m_int_solver.column_is_int(j) && m_fj.is_pos());
@@ -217,7 +217,7 @@ class create_cut {
         }
         for (const auto& p : m_t) {
             unsigned v = p.var();
-            if (m_int_solver.m_lar_solver->is_term(v)) {
+            if (m_int_solver.lra.is_term(v)) {
                 dump_declaration(out, v);
             }
         }
@@ -276,7 +276,7 @@ public:
     void dump(std::ostream& out) {
         out << "applying cut at:\n"; print_linear_combination_indices_only<row_strip<mpq>, mpq>(m_row, out); out << std::endl;
         for (auto & p : m_row) {
-            m_int_solver.m_lar_solver->m_mpq_lar_core_solver.m_r_solver.print_column_info(p.var(), out);
+            m_int_solver.lra.m_mpq_lar_core_solver.m_r_solver.print_column_info(p.var(), out);
         }
         out << "inf_col = " << m_inf_col << std::endl;
     }
@@ -336,7 +336,7 @@ public:
             adjust_term_and_k_for_some_ints_case_gomory();
         lp_assert(m_int_solver.current_solution_is_inf_on_cut());
         TRACE("gomory_cut_detail", dump_cut_and_constraints_as_smt_lemma(tout););
-        m_int_solver.m_lar_solver->subs_term_columns(m_t);
+        m_int_solver.lra.subs_term_columns(m_t);
         TRACE("gomory_cut", print_linear_combination_of_column_indices_only(m_t.coeffs_as_vector(), tout << "gomory cut:"); tout << " <= " << m_k << std::endl;);
         return lia_move::cut;
     }
@@ -386,16 +386,16 @@ int gomory::find_basic_var() {
     // Prefer boxed to non-boxed
     // Prefer smaller ranges
 
-    for (unsigned j : s.m_lar_solver->r_basis()) {
+    for (unsigned j : s.lra.r_basis()) {
         if (!s.column_is_int_inf(j))
             continue;
-        const row_strip<mpq>& row = s.m_lar_solver->get_row(s.row_of_basic_column(j));
+        const row_strip<mpq>& row = s.lra.get_row(s.row_of_basic_column(j));
         if (!is_gomory_cut_target(row)) 
             continue;
 
 #if 0
         if (is_boxed(j) && (min_row_size == UINT_MAX || 4*row.size() < 5*min_row_size)) {
-            lar_core_solver & lcs = m_lar_solver->m_mpq_lar_core_solver;
+            lar_core_solver & lcs = lra.m_mpq_lar_core_solver;
             auto new_range = lcs.m_r_upper_bounds()[j].x - lcs.m_r_lower_bounds()[j].x;
             if (!boxed) {
                 result = j;
@@ -427,8 +427,8 @@ int gomory::find_basic_var() {
 }
     
 lia_move gomory::operator()(lar_term & t, mpq & k, explanation* ex, bool& upper) {
-    if (s.m_lar_solver->move_non_basic_columns_to_bounds()) {
-        lp_status st = s.m_lar_solver->find_feasible_solution();
+    if (s.lra.move_non_basic_columns_to_bounds()) {
+        lp_status st = s.lra.find_feasible_solution();
         (void)st;
         lp_assert(st == lp_status::FEASIBLE || st == lp_status::OPTIMAL);
     }
@@ -436,8 +436,8 @@ lia_move gomory::operator()(lar_term & t, mpq & k, explanation* ex, bool& upper)
     int j = find_basic_var();
     if (j == -1) return lia_move::undef;
     unsigned r = s.row_of_basic_column(j);
-    const row_strip<mpq>& row = s.m_lar_solver->get_row(r);
-    SASSERT(s.m_lar_solver->row_is_correct(r));
+    const row_strip<mpq>& row = s.lra.get_row(r);
+    SASSERT(s.lra.row_is_correct(r));
     SASSERT(is_gomory_cut_target(row));
     upper = true;
     return cut(t, k, ex, j, row);
diff --git a/src/math/lp/int_cube.cpp b/src/math/lp/int_cube.cpp
index b3aba8cd5..3b5a87f65 100644
--- a/src/math/lp/int_cube.cpp
+++ b/src/math/lp/int_cube.cpp
@@ -1,5 +1,5 @@
 /*++
-Copyright (c) 2017 Microsoft Corporation
+Copyright (c) 2020 Microsoft Corporation
 
 Module Name:
 
@@ -15,8 +15,6 @@ Author:
 
 Revision History:
 --*/
-#pragma once
-
 
 #include "math/lp/int_solver.h"
 #include "math/lp/lar_solver.h"
@@ -24,7 +22,7 @@ Revision History:
 
 namespace lp {
 
-    int_cube::int_cube(int_solver& lia):lia(lia), lra(*lia.m_lar_solver) {}
+    int_cube::int_cube(int_solver& lia):lia(lia), lra(lia.lra) {}
 
     lia_move int_cube::operator()() {
         lia.settings().stats().m_cube_calls++;
diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp
index 44a45b86b..b976a830a 100644
--- a/src/math/lp/int_solver.cpp
+++ b/src/math/lp/int_solver.cpp
@@ -14,7 +14,7 @@ namespace lp {
 
 
 std::ostream& int_solver::display_inf_rows(std::ostream& out) const {
-    unsigned num = m_lar_solver->A_r().column_count();
+    unsigned num = lra.A_r().column_count();
     for (unsigned v = 0; v < num; v++) {
         if (column_is_int(v) && !get_value(v).is_int()) {
             display_column(out, v);
@@ -22,11 +22,11 @@ std::ostream& int_solver::display_inf_rows(std::ostream& out) const {
     }
     
     num = 0;
-    for (unsigned i = 0; i < m_lar_solver->A_r().row_count(); i++) {
-        unsigned j = m_lar_solver->m_mpq_lar_core_solver.m_r_basis[i];
+    for (unsigned i = 0; i < lra.A_r().row_count(); i++) {
+        unsigned j = lra.m_mpq_lar_core_solver.m_r_basis[i];
         if (column_is_int_inf(j)) {
             num++;
-            m_lar_solver->print_row(m_lar_solver->A_r().m_rows[i], out);
+            lra.print_row(lra.A_r().m_rows[i], out);
             out << "\n";
         }
     }
@@ -34,10 +34,6 @@ std::ostream& int_solver::display_inf_rows(std::ostream& out) const {
     return out;
 }
 
-bool int_solver::has_inf_int() const {
-    return m_lar_solver->has_inf_int();
-}
-
 int int_solver::find_inf_int_base_column() {
     unsigned inf_int_count = 0;
     int j = find_inf_int_boxed_base_column_with_smallest_range(inf_int_count);
@@ -51,7 +47,7 @@ int int_solver::find_inf_int_base_column() {
 }
 
 int int_solver::get_kth_inf_int(unsigned k) const {
-    for (unsigned j : m_lar_solver->r_basis()) 
+    for (unsigned j : lra.r_basis()) 
         if (column_is_int_inf(j) && k-- == 0)
             return j;
     lp_assert(false);
@@ -59,7 +55,7 @@ int int_solver::get_kth_inf_int(unsigned k) const {
 }
 
 int int_solver::find_inf_int_nbasis_column() const {
-    for (unsigned j : m_lar_solver->r_nbasis())
+    for (unsigned j : lra.r_nbasis())
         if (!column_is_int_inf(j)) {
             return j;    
         }
@@ -73,9 +69,9 @@ int int_solver::find_inf_int_boxed_base_column_with_smallest_range(unsigned & in
     mpq new_range;
     mpq small_range_thresold(1024);
     unsigned n = 0;
-    lar_core_solver & lcs = m_lar_solver->m_mpq_lar_core_solver;
+    lar_core_solver & lcs = lra.m_mpq_lar_core_solver;
 
-    for (unsigned j : m_lar_solver->r_basis()) {
+    for (unsigned j : lra.r_basis()) {
         if (!column_is_int_inf(j))
             continue;
         inf_int_count++;
@@ -99,7 +95,7 @@ int int_solver::find_inf_int_boxed_base_column_with_smallest_range(unsigned & in
 }
 
 bool int_solver::current_solution_is_inf_on_cut() const {
-    const auto & x = m_lar_solver->m_mpq_lar_core_solver.m_r_x;
+    const auto & x = lra.m_mpq_lar_core_solver.m_r_x;
     impq v = m_t.apply(x);
     mpq sign = m_upper ? one_of_type<mpq>()  : -one_of_type<mpq>();
     CTRACE("current_solution_is_inf_on_cut", v * sign <= impq(m_k) * sign,
@@ -109,28 +105,32 @@ bool int_solver::current_solution_is_inf_on_cut() const {
     return v * sign > impq(m_k) * sign;
 }
 
+bool int_solver::has_inf_int() const {
+    return lra.has_inf_int();
+}
+
 constraint_index int_solver::column_upper_bound_constraint(unsigned j) const {
-    return m_lar_solver->get_column_upper_bound_witness(j);
+    return lra.get_column_upper_bound_witness(j);
 }
 
 constraint_index int_solver::column_lower_bound_constraint(unsigned j) const {
-    return m_lar_solver->get_column_lower_bound_witness(j);
+    return lra.get_column_lower_bound_witness(j);
 }
 
 unsigned int_solver::row_of_basic_column(unsigned j) const {
-    return m_lar_solver->row_of_basic_column(j);
+    return lra.row_of_basic_column(j);
 }
 
 lp_settings& int_solver::settings() {  
-    return m_lar_solver->settings(); 
+    return lra.settings(); 
 }
 
 const lp_settings& int_solver::settings() const { 
-    return m_lar_solver->settings(); 
+    return lra.settings(); 
 }
 
 bool int_solver::column_is_int(unsigned j) const {
-    return m_lar_solver->column_is_int(j);
+    return lra.column_is_int(j);
 }
 
 bool int_solver::is_real(unsigned j) const {
@@ -138,24 +138,39 @@ bool int_solver::is_real(unsigned j) const {
 }
 
 bool int_solver::value_is_int(unsigned j) const {
-    return m_lar_solver->column_value_is_int(j);
+    return lra.column_value_is_int(j);
 }    
 
+unsigned int_solver::random() {
+    return lra.get_core_solver().settings().random_next();
+}
+
+const impq& int_solver::upper_bound(unsigned j) const {
+    return lra.column_upper_bound(j);
+}
+
+bool int_solver::is_term(unsigned j) const {
+    return lra.column_corresponds_to_term(j);
+}
+
+unsigned int_solver::column_count() const  { 
+    return lra.column_count(); 
+}
 
 // this will allow to enable and disable tracking of the pivot rows
 struct check_return_helper {
-    lar_solver *     m_lar_solver;
+    lar_solver&      lra;
     bool             m_track_pivoted_rows;
-    check_return_helper(lar_solver* ls) :
-        m_lar_solver(ls),
-        m_track_pivoted_rows(ls->get_track_pivoted_rows())
+    check_return_helper(lar_solver& ls) :
+        lra(ls),
+        m_track_pivoted_rows(lra.get_track_pivoted_rows())
     {
-        TRACE("pivoted_rows", tout << "pivoted rows = " << ls->m_mpq_lar_core_solver.m_r_solver.m_pivoted_rows->size() << std::endl;);
-        m_lar_solver->set_track_pivoted_rows(false);
+        TRACE("pivoted_rows", tout << "pivoted rows = " << lra.m_mpq_lar_core_solver.m_r_solver.m_pivoted_rows->size() << std::endl;);
+        lra.set_track_pivoted_rows(false);
     }
     ~check_return_helper() {
-        TRACE("pivoted_rows", tout << "pivoted rows = " << m_lar_solver->m_mpq_lar_core_solver.m_r_solver.m_pivoted_rows->size() << std::endl;);
-        m_lar_solver->set_track_pivoted_rows(m_track_pivoted_rows);
+        TRACE("pivoted_rows", tout << "pivoted rows = " << lra.m_mpq_lar_core_solver.m_r_solver.m_pivoted_rows->size() << std::endl;);
+        lra.set_track_pivoted_rows(m_track_pivoted_rows);
     }
 };
 
@@ -173,7 +188,6 @@ lia_move int_solver::find_cube() {
     }
 }
 
-
 bool int_solver::should_run_gcd_test() {
     return settings().m_int_run_gcd_test;    
 }
@@ -208,10 +222,10 @@ lia_move int_solver::gomory_cut() {
 
 void int_solver::try_add_term_to_A_for_hnf(unsigned i) {
     mpq rs;
-    const lar_term* t = m_lar_solver->terms()[i];
+    const lar_term* t = lra.terms()[i];
     constraint_index ci;
     bool upper_bound;
-    if (!hnf_cutter_is_full() && m_lar_solver->get_equality_and_right_side_for_term_on_current_x(i, rs, ci, upper_bound)) {
+    if (!hnf_cutter_is_full() && lra.get_equality_and_right_side_for_term_on_current_x(i, rs, ci, upper_bound)) {
         m_hnf_cutter.add_term(t, rs, ci, upper_bound);
     }
 }
@@ -232,7 +246,7 @@ bool int_solver::hnf_has_var_with_non_integral_value() const {
 
 bool int_solver::init_terms_for_hnf_cut() {
     m_hnf_cutter.clear();
-    for (unsigned i = 0; i < m_lar_solver->terms().size() && !hnf_cutter_is_full(); i++) {
+    for (unsigned i = 0; i < lra.terms().size() && !hnf_cutter_is_full(); i++) {
         try_add_term_to_A_for_hnf(i);
     }
     return hnf_has_var_with_non_integral_value();
@@ -245,12 +259,12 @@ lia_move int_solver::make_hnf_cut() {
     settings().stats().m_hnf_cutter_calls++;
     TRACE("hnf_cut", tout << "settings().stats().m_hnf_cutter_calls = " << settings().stats().m_hnf_cutter_calls << "\n";
           for (unsigned i : m_hnf_cutter.constraints_for_explanation()) {
-              m_lar_solver->constraints().display(tout, i);
+              lra.constraints().display(tout, i);
           }              
-          tout << m_lar_solver->constraints();
+          tout << lra.constraints();
           );
 #ifdef Z3DEBUG
-    vector<mpq> x0 = m_hnf_cutter.transform_to_local_columns(m_lar_solver->m_mpq_lar_core_solver.m_r_x);
+    vector<mpq> x0 = m_hnf_cutter.transform_to_local_columns(lra.m_mpq_lar_core_solver.m_r_x);
 #else
     vector<mpq> x0;
 #endif
@@ -258,10 +272,10 @@ lia_move int_solver::make_hnf_cut() {
 
     if (r == lia_move::cut) {      
         TRACE("hnf_cut",
-              m_lar_solver->print_term(m_t, tout << "cut:"); 
+              lra.print_term(m_t, tout << "cut:"); 
               tout << " <= " << m_k << std::endl;
               for (unsigned i : m_hnf_cutter.constraints_for_explanation()) {
-                  m_lar_solver->constraints().display(tout, i);
+                  lra.constraints().display(tout, i);
               }              
               );
         lp_assert(current_solution_is_inf_on_cut());
@@ -293,7 +307,7 @@ lia_move int_solver::hnf_cut() {
 }
 
 lia_move int_solver::check(lp::explanation * e) {
-    SASSERT(m_lar_solver->ax_is_correct());
+    SASSERT(lra.ax_is_correct());
     if (!has_inf_int()) return lia_move::sat;
 
 #define CHECK_RET(fn)                                                   \
@@ -309,10 +323,10 @@ lia_move int_solver::check(lp::explanation * e) {
 
     CHECK_RET(run_gcd_test());
 
-    check_return_helper pc(m_lar_solver);
+    check_return_helper pc(lra);
 
     if (settings().m_int_pivot_fixed_vars_from_basis)
-        m_lar_solver->pivot_fixed_vars_from_basis();
+        lra.pivot_fixed_vars_from_basis();
 
     CHECK_RET(patch_nbasic_columns());
     ++m_number_of_calls;
@@ -335,15 +349,15 @@ int int_solver::find_any_inf_int_column_basis_first() {
 
 void int_solver::set_value_for_nbasic_column_ignore_old_values(unsigned j, const impq & new_val) {
     lp_assert(!is_base(j));
-    auto & x = m_lar_solver->m_mpq_lar_core_solver.m_r_x[j];
+    auto & x = lra.m_mpq_lar_core_solver.m_r_x[j];
     auto delta = new_val - x;
     x = new_val;
     TRACE("int_solver", tout << "x[" << j << "] = " << x << "\n";);
-    m_lar_solver->change_basic_columns_dependend_on_a_given_nb_column(j, delta);
+    lra.change_basic_columns_dependend_on_a_given_nb_column(j, delta);
 }
 
 void int_solver::patch_nbasic_column(unsigned j) {
-    auto & lcs = m_lar_solver->m_mpq_lar_core_solver; 
+    auto & lcs = lra.m_mpq_lar_core_solver; 
     impq & val = lcs.m_r_x[j];
     bool inf_l, inf_u;
     impq l, u;
@@ -364,12 +378,12 @@ void int_solver::patch_nbasic_column(unsigned j) {
           tout << ", ";
           if (inf_u) tout << "oo"; else tout << u;
           tout << "]";
-          tout << ", m: " << m << ", val: " << val << ", is_int: " << m_lar_solver->column_is_int(j) << "\n";);
+          tout << ", m: " << m << ", val: " << val << ", is_int: " << lra.column_is_int(j) << "\n";);
     if (!inf_l) {
         l = impq(m_is_one ? ceil(l) : m * ceil(l / m));
         if (inf_u || l <= u) {
             TRACE("patch_int",    tout << "patching with l: " << l << '\n';);
-            m_lar_solver->set_value_for_nbasic_column(j, l);
+            lra.set_value_for_nbasic_column(j, l);
         }
         else {
             TRACE("patch_int", tout << "not patching " << l << "\n";);
@@ -377,11 +391,11 @@ void int_solver::patch_nbasic_column(unsigned j) {
     }
     else if (!inf_u) {
         u = impq(m_is_one ? floor(u) : m * floor(u / m));
-        m_lar_solver->set_value_for_nbasic_column(j, u);
+        lra.set_value_for_nbasic_column(j, u);
         TRACE("patch_int", tout << "patching with u: " << u << '\n';);
     }
     else {
-        m_lar_solver->set_value_for_nbasic_column(j, impq(0));
+        lra.set_value_for_nbasic_column(j, impq(0));
         TRACE("patch_int", tout << "patching with 0\n";);
     }
 }
@@ -389,7 +403,7 @@ void int_solver::patch_nbasic_column(unsigned j) {
 lia_move int_solver::patch_nbasic_columns() {
     settings().stats().m_patches++;
     lp_assert(is_feasible());
-    for (unsigned j : m_lar_solver->m_mpq_lar_core_solver.m_r_nbasis) {
+    for (unsigned j : lra.m_mpq_lar_core_solver.m_r_nbasis) {
         patch_nbasic_column(j);
     }
     lp_assert(is_feasible());
@@ -410,7 +424,7 @@ mpq get_denominators_lcm(const row_strip<mpq> & row) {
     
 bool int_solver::gcd_test_for_row(static_matrix<mpq, numeric_pair<mpq>> & A, unsigned i) {
     auto const& row = A.m_rows[i];
-    auto & lcs = m_lar_solver->m_mpq_lar_core_solver;
+    auto & lcs = lra.m_mpq_lar_core_solver;
     unsigned basic_var = lcs.m_r_basis[i];
 
     if (!column_is_int(basic_var) || get_value(basic_var).is_int())
@@ -424,27 +438,27 @@ bool int_solver::gcd_test_for_row(static_matrix<mpq, numeric_pair<mpq>> & A, uns
     for (auto &c : A.m_rows[i]) {
         j = c.var();
         const mpq& a = c.coeff();
-        if (m_lar_solver->column_is_fixed(j)) {
+        if (lra.column_is_fixed(j)) {
             mpq aux = lcm_den * a;
-            consts += aux * m_lar_solver->column_lower_bound(j).x;
+            consts += aux * lra.column_lower_bound(j).x;
         }
-        else if (m_lar_solver->column_is_real(j)) {
+        else if (lra.column_is_real(j)) {
             return true;
         }
         else if (gcds.is_zero()) {
             gcds = abs(lcm_den * a);
             least_coeff = gcds;
-            least_coeff_is_bounded = m_lar_solver->column_is_bounded(j);
+            least_coeff_is_bounded = lra.column_is_bounded(j);
         }
         else {
             mpq aux = abs(lcm_den * a);
             gcds = gcd(gcds, aux);
             if (aux < least_coeff) {
                 least_coeff = aux;
-                least_coeff_is_bounded = m_lar_solver->column_is_bounded(j);
+                least_coeff_is_bounded = lra.column_is_bounded(j);
             }
             else if (least_coeff_is_bounded && aux == least_coeff) {
-                least_coeff_is_bounded = m_lar_solver->column_is_bounded(j);
+                least_coeff_is_bounded = lra.column_is_bounded(j);
             }
         }
         SASSERT(gcds.is_int());
@@ -481,20 +495,20 @@ bool int_solver::gcd_test_for_row(static_matrix<mpq, numeric_pair<mpq>> & A, uns
 
 void int_solver::add_to_explanation_from_fixed_or_boxed_column(unsigned j) {
     constraint_index lc, uc;
-    m_lar_solver->get_bound_constraint_witnesses_for_column(j, lc, uc);
+    lra.get_bound_constraint_witnesses_for_column(j, lc, uc);
     m_ex->push_justification(lc);
     m_ex->push_justification(uc);
 }
 void int_solver::fill_explanation_from_fixed_columns(const row_strip<mpq> & row) {
     for (const auto & c : row) {
-        if (!m_lar_solver->column_is_fixed(c.var()))
+        if (!lra.column_is_fixed(c.var()))
             continue;
         add_to_explanation_from_fixed_or_boxed_column(c.var());
     }
 }
     
 bool int_solver::gcd_test() {
-    auto & A = m_lar_solver->A_r(); // getting the matrix
+    auto & A = lra.A_r(); // getting the matrix
     for (unsigned i = 0; i < A.row_count(); i++)
         if (!gcd_test_for_row(A, i)) 
             return false;        
@@ -505,7 +519,7 @@ bool int_solver::ext_gcd_test(const row_strip<mpq> & row,
                               mpq const & least_coeff, 
                               mpq const & lcm_den,
                               mpq const & consts) {
-    TRACE("ext_gcd_test", tout << "row = "; m_lar_solver->print_row(row, tout););
+    TRACE("ext_gcd_test", tout << "row = "; lra.print_row(row, tout););
     mpq gcds(0);
     mpq l(consts);
     mpq u(consts);
@@ -514,27 +528,27 @@ bool int_solver::ext_gcd_test(const row_strip<mpq> & row,
     unsigned j;
     for (const auto & c : row) {
         j = c.var();
-        TRACE("ext_gcd_test", tout << "col = "; m_lar_solver->m_mpq_lar_core_solver.m_r_solver.print_column_bound_info(j, tout););
+        TRACE("ext_gcd_test", tout << "col = "; lra.m_mpq_lar_core_solver.m_r_solver.print_column_bound_info(j, tout););
         const mpq & a = c.coeff();
-        if (m_lar_solver->column_is_fixed(j))
+        if (lra.column_is_fixed(j))
             continue;
-        SASSERT(!m_lar_solver->column_is_real(j));
+        SASSERT(!lra.column_is_real(j));
         mpq ncoeff = lcm_den * a;
         SASSERT(ncoeff.is_int());
         mpq abs_ncoeff = abs(ncoeff);
         if (abs_ncoeff == least_coeff) {
-            SASSERT(m_lar_solver->column_is_bounded(j));
+            SASSERT(lra.column_is_bounded(j));
             if (ncoeff.is_pos()) {
-                // l += ncoeff * m_lar_solver->column_lower_bound(j).x;
-                l.addmul(ncoeff, m_lar_solver->column_lower_bound(j).x);
-                // u += ncoeff * m_lar_solver->column_upper_bound(j).x;
-                u.addmul(ncoeff, m_lar_solver->column_upper_bound(j).x);
+                // l += ncoeff * lra.column_lower_bound(j).x;
+                l.addmul(ncoeff, lra.column_lower_bound(j).x);
+                // u += ncoeff * lra.column_upper_bound(j).x;
+                u.addmul(ncoeff, lra.column_upper_bound(j).x);
             }
             else {
                 // l += ncoeff * upper_bound(j).get_rational();
-                l.addmul(ncoeff, m_lar_solver->column_upper_bound(j).x);
+                l.addmul(ncoeff, lra.column_upper_bound(j).x);
                 // u += ncoeff * lower_bound(j).get_rational();
-                u.addmul(ncoeff, m_lar_solver->column_lower_bound(j).x);
+                u.addmul(ncoeff, lra.column_lower_bound(j).x);
             }
             add_to_explanation_from_fixed_or_boxed_column(j);
         }
@@ -557,23 +571,21 @@ bool int_solver::ext_gcd_test(const row_strip<mpq> & row,
     if (u1 < l1) {
         fill_explanation_from_fixed_columns(row);
         return false;
-    }
-        
+    }        
     return true;
-
 }
 
-int_solver::int_solver(lar_solver* lar_slv) :
-    m_lar_solver(lar_slv),
+int_solver::int_solver(lar_solver& lar_slv) :
+    lra(lar_slv),
     m_number_of_calls(0),
     m_hnf_cutter(settings()),
     m_hnf_cut_period(settings().hnf_cut_period()) {
-    m_lar_solver->set_int_solver(this);
+    lra.set_int_solver(this);
 }
 
 
 bool int_solver::has_lower(unsigned j) const {
-    switch (m_lar_solver->m_mpq_lar_core_solver.m_column_types()[j]) {
+    switch (lra.m_mpq_lar_core_solver.m_column_types()[j]) {
     case column_type::fixed:
     case column_type::boxed:
     case column_type::lower_bound:
@@ -584,7 +596,7 @@ bool int_solver::has_lower(unsigned j) const {
 }
 
 bool int_solver::has_upper(unsigned j) const {
-    switch (m_lar_solver->m_mpq_lar_core_solver.m_column_types()[j]) {
+    switch (lra.m_mpq_lar_core_solver.m_column_types()[j]) {
     case column_type::fixed:
     case column_type::boxed:
     case column_type::upper_bound:
@@ -609,7 +621,7 @@ static void set_upper(impq & u, bool & inf_u, impq const & v) {
 }
 
 bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq & l, bool & inf_u, impq & u, mpq & m) {
-    auto & lcs = m_lar_solver->m_mpq_lar_core_solver;
+    auto & lcs = lra.m_mpq_lar_core_solver;
     if (lcs.m_r_heading[j] >= 0) // the basic var 
         return false;
 
@@ -630,7 +642,7 @@ bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq
 
     unsigned row_index;
     lp_assert(settings().use_tableau());
-    const auto & A = m_lar_solver->A_r();
+    const auto & A = lra.A_r();
     unsigned rounds = 0;
     for (const auto &c : A.column(j)) {
         row_index = c.var();
@@ -684,7 +696,7 @@ bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq
 
     TRACE("freedom_interval",
           tout << "freedom variable for:\n";
-          tout << m_lar_solver->get_variable_name(j);
+          tout << lra.get_variable_name(j);
           tout << "[";
           if (inf_l) tout << "-oo"; else tout << l;
           tout << "; ";
@@ -698,18 +710,18 @@ bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq
 
 
 bool int_solver::is_feasible() const {
-    auto & lcs = m_lar_solver->m_mpq_lar_core_solver;
+    auto & lcs = lra.m_mpq_lar_core_solver;
     lp_assert(
         lcs.m_r_solver.calc_current_x_is_feasible_include_non_basis() ==
         lcs.m_r_solver.current_x_is_feasible());
     return lcs.m_r_solver.current_x_is_feasible();
 }
 const impq & int_solver::get_value(unsigned j) const {
-    return m_lar_solver->m_mpq_lar_core_solver.m_r_x[j];
+    return lra.m_mpq_lar_core_solver.m_r_x[j];
 }
 
 std::ostream& int_solver::display_column(std::ostream & out, unsigned j) const {
-    return m_lar_solver->m_mpq_lar_core_solver.m_r_solver.print_column_info(j, out);
+    return lra.m_mpq_lar_core_solver.m_r_solver.print_column_info(j, out);
     return out;
 }
 
@@ -718,23 +730,23 @@ bool int_solver::column_is_int_inf(unsigned j) const {
 }
 
 bool int_solver::is_base(unsigned j) const {
-    return m_lar_solver->m_mpq_lar_core_solver.m_r_heading[j] >= 0;
+    return lra.m_mpq_lar_core_solver.m_r_heading[j] >= 0;
 }
 
 bool int_solver::is_boxed(unsigned j) const {
-    return m_lar_solver->m_mpq_lar_core_solver.m_column_types[j] == column_type::boxed;
+    return lra.m_mpq_lar_core_solver.m_column_types[j] == column_type::boxed;
 }
 
 bool int_solver::is_fixed(unsigned j) const {
-    return m_lar_solver->m_mpq_lar_core_solver.m_column_types[j] == column_type::fixed;
+    return lra.m_mpq_lar_core_solver.m_column_types[j] == column_type::fixed;
 }
 
 bool int_solver::is_free(unsigned j) const {
-    return m_lar_solver->m_mpq_lar_core_solver.m_column_types[j] == column_type::free_column;
+    return lra.m_mpq_lar_core_solver.m_column_types[j] == column_type::free_column;
 }
 
 bool int_solver::at_bound(unsigned j) const {
-    auto & mpq_solver = m_lar_solver->m_mpq_lar_core_solver.m_r_solver;
+    auto & mpq_solver = lra.m_mpq_lar_core_solver.m_r_solver;
     switch (mpq_solver.m_column_types[j] ) {
     case column_type::fixed:
     case column_type::boxed:
@@ -751,7 +763,7 @@ bool int_solver::at_bound(unsigned j) const {
 }
 
 bool int_solver::at_lower(unsigned j) const {
-    auto & mpq_solver = m_lar_solver->m_mpq_lar_core_solver.m_r_solver;
+    auto & mpq_solver = lra.m_mpq_lar_core_solver.m_r_solver;
     switch (mpq_solver.m_column_types[j] ) {
     case column_type::fixed:
     case column_type::boxed:
@@ -763,7 +775,7 @@ bool int_solver::at_lower(unsigned j) const {
 }
 
 bool int_solver::at_upper(unsigned j) const {
-    auto & mpq_solver = m_lar_solver->m_mpq_lar_core_solver.m_r_solver;
+    auto & mpq_solver = lra.m_mpq_lar_core_solver.m_r_solver;
     switch (mpq_solver.m_column_types[j] ) {
     case column_type::fixed:
     case column_type::boxed:
@@ -775,7 +787,7 @@ bool int_solver::at_upper(unsigned j) const {
 }
 
 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 & rslv = lra.m_mpq_lar_core_solver.m_r_solver;
     for (const auto &c: rslv.m_A.m_rows[row_index]) {
         if (numeric_traits<mpq>::is_pos(c.coeff()))
             out << "+";
@@ -788,12 +800,6 @@ void int_solver::display_row_info(std::ostream & out, unsigned row_index) const
     rslv.print_column_bound_info(rslv.m_basis[row_index], out);
 }
 
-unsigned int_solver::random() {
-    return m_lar_solver->get_core_solver().settings().random_next();
-}
-
-
-// at this point the 
 bool int_solver::shift_var(unsigned j, unsigned range) {
     if (is_fixed(j) || is_base(j))
         return false;
@@ -847,7 +853,7 @@ bool int_solver::shift_var(unsigned j, unsigned range) {
 }
 
 bool int_solver::non_basic_columns_are_at_bounds() const {
-    auto & lcs = m_lar_solver->m_mpq_lar_core_solver;
+    auto & lcs = lra.m_mpq_lar_core_solver;
     for (unsigned j :lcs.m_r_nbasis) {
         auto & val = lcs.m_r_x[j];
         switch (lcs.m_column_types()[j]) {
@@ -873,14 +879,14 @@ bool int_solver::non_basic_columns_are_at_bounds() const {
 }
 
 const impq& int_solver::lower_bound(unsigned j) const {
-    return m_lar_solver->column_lower_bound(j);
+    return lra.column_lower_bound(j);
 }
 
 lia_move int_solver::create_branch_on_column(int j) {
     TRACE("check_main_int", tout << "branching" << std::endl;);
     lp_assert(m_t.is_empty());
     lp_assert(j != -1);
-    m_t.add_monomial(mpq(1), m_lar_solver->adjust_column_index_to_term_index(j));
+    m_t.add_monomial(mpq(1), lra.adjust_column_index_to_term_index(j));
     if (is_free(j)) {
         m_upper = random() % 2;
         m_k = mpq(0);
@@ -898,7 +904,7 @@ lia_move int_solver::create_branch_on_column(int j) {
 }
 
 bool int_solver::left_branch_is_more_narrow_than_right(unsigned j) {
-    switch (m_lar_solver->m_mpq_lar_core_solver.m_r_solver.m_column_types[j] ) {
+    switch (lra.m_mpq_lar_core_solver.m_r_solver.m_column_types[j] ) {
     case column_type::fixed:
         return false;
     case column_type::boxed:
@@ -915,14 +921,5 @@ bool int_solver::left_branch_is_more_narrow_than_right(unsigned j) {
     }       
 }
     
-const impq& int_solver::upper_bound(unsigned j) const {
-    return m_lar_solver->column_upper_bound(j);
-}
-
-bool int_solver::is_term(unsigned j) const {
-    return m_lar_solver->column_corresponds_to_term(j);
-}
-
-unsigned int_solver::column_count() const  { return m_lar_solver->column_count(); }
 
 }
diff --git a/src/math/lp/int_solver.h b/src/math/lp/int_solver.h
index a437d4c19..a3b821ef3 100644
--- a/src/math/lp/int_solver.h
+++ b/src/math/lp/int_solver.h
@@ -39,7 +39,7 @@ class int_solver {
     friend class int_cube;
 public:
     // fields
-    lar_solver          *m_lar_solver;
+    lar_solver&         lra;
     unsigned            m_number_of_calls;
     lar_term            m_t; // the term to return in the cut
     mpq                 m_k; // the right side of the cut
@@ -48,7 +48,7 @@ public:
     hnf_cutter          m_hnf_cutter;
     unsigned            m_hnf_cut_period;
     // methods
-    int_solver(lar_solver* lp);
+    int_solver(lar_solver& lp);
 
     // main function to check that the solution provided by lar_solver is valid for integral values,
     // or provide a way of how it can be adjusted.
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 02d64c3b3..245111818 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -407,7 +407,7 @@ class theory_lra::imp {
         lp().settings().m_int_run_gcd_test = ctx().get_fparams().m_arith_gcd_test;
         lp().settings().set_random_seed(ctx().get_fparams().m_random_seed);
         m_switcher.m_use_nla = m_use_nla = lpar.nla();
-        m_lia = alloc(lp::int_solver, m_solver.get());
+        m_lia = alloc(lp::int_solver, *m_solver.get());
         get_one(true);
         get_zero(true);
         get_one(false);