diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 9a1284b37..2a7ad9ed2 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -2302,7 +2302,7 @@ public:
         int new_num_of_p = m_solver->settings().st().m_num_of_implied_bounds;
         (void)new_num_of_p;
         CTRACE("arith", new_num_of_p > num_of_p, tout << "found " << new_num_of_p << " implied bounds\n";);
-        if (m_solver->get_status() == lp::lp_status::INFEASIBLE) {
+        if (is_infeasible()) {
             set_conflict();
         }
         else {
@@ -2960,7 +2960,7 @@ public:
     }
 
     void assert_bound(bool_var bv, bool is_true, lp_api::bound& b) {
-        if (m_solver->get_status() == lp::lp_status::INFEASIBLE) {
+        if (is_infeasible()) {
             return;
         }
         scoped_internalize_state st(*this);
@@ -2993,8 +2993,8 @@ public:
         else {
             ci = m_solver->add_var_bound(vi, k, b.get_value(), m_explanation);
         }
-        if (m_solver->get_status() == lp::lp_status::INFEASIBLE) {
-            NOT_IMPLEMENTED_YET();
+        if (is_infeasible()) {
+            set_conflict1();
             return;
         }
         TRACE("arith", tout << "v" << b.get_var() << "\n";);
diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp
index 97e582504..030217bb5 100644
--- a/src/util/lp/lar_solver.cpp
+++ b/src/util/lp/lar_solver.cpp
@@ -1925,180 +1925,6 @@ void lar_solver::fill_last_row_of_A_d(static_matrix<double, double> & A, const l
     lp_assert(A.is_correct());
 }
 
-void lar_solver::update_free_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_ind) {
-    mpq y_of_bound(0);
-    switch (kind) {
-    case LT:
-        y_of_bound = -1;
-    case LE:
-        m_mpq_lar_core_solver.m_column_types[j] = column_type::upper_bound;
-        lp_assert(m_mpq_lar_core_solver.m_column_types()[j] == column_type::upper_bound);
-        lp_assert(m_mpq_lar_core_solver.m_r_upper_bounds.size() > j);
-        {
-            auto up = numeric_pair<mpq>(right_side, y_of_bound);
-            m_mpq_lar_core_solver.m_r_upper_bounds[j] = up;
-        }
-        set_upper_bound_witness(j, constr_ind);
-        break;
-    case GT:
-        y_of_bound = 1;
-    case GE:
-        m_mpq_lar_core_solver.m_column_types[j] = column_type::lower_bound;
-        lp_assert(m_mpq_lar_core_solver.m_r_upper_bounds.size() > j);
-        {
-            auto low = numeric_pair<mpq>(right_side, y_of_bound);
-            m_mpq_lar_core_solver.m_r_lower_bounds[j] = low;
-        }
-        set_lower_bound_witness(j, constr_ind);
-        break;
-    case EQ:
-        m_mpq_lar_core_solver.m_column_types[j] = column_type::fixed;
-        m_mpq_lar_core_solver.m_r_lower_bounds[j] = m_mpq_lar_core_solver.m_r_upper_bounds[j] = numeric_pair<mpq>(right_side, zero_of_type<mpq>());
-        set_upper_bound_witness(j, constr_ind);
-        set_lower_bound_witness(j, constr_ind);
-        break;
-
-    default:
-        lp_unreachable();
-
-    }
-    m_columns_with_changed_bound.insert(j);
-}
-
-void lar_solver::update_upper_bound_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci,
-                                                          explanation& e) {
-    lp_assert(m_mpq_lar_core_solver.m_column_types()[j] == column_type::upper_bound);
-    mpq y_of_bound(0);
-    switch (kind) {
-    case LT:
-        y_of_bound = -1;
-    case LE:
-	{
-            auto up = numeric_pair<mpq>(right_side, y_of_bound);
-            if (up < m_mpq_lar_core_solver.m_r_upper_bounds()[j]) {
-                m_mpq_lar_core_solver.m_r_upper_bounds[j] = up;
-                set_upper_bound_witness(j, ci);
-                m_columns_with_changed_bound.insert(j);
-            }
-	}
-	break;
-    case GT:
-        y_of_bound = 1;
-    case GE:
-        m_mpq_lar_core_solver.m_column_types[j] = column_type::boxed;
-        {
-            auto low = numeric_pair<mpq>(right_side, y_of_bound);
-            m_mpq_lar_core_solver.m_r_lower_bounds[j] = low;
-            set_lower_bound_witness(j, ci);
-            m_columns_with_changed_bound.insert(j);
-            if (low > m_mpq_lar_core_solver.m_r_upper_bounds[j]) {
-                m_status = lp_status::INFEASIBLE;
-                e.push_justification(ci);
-                e.push_justification(get_column_lower_bound_witness(j));
-            }
-            else {
-                m_mpq_lar_core_solver.m_column_types[j] = m_mpq_lar_core_solver.m_r_lower_bounds()[j] < m_mpq_lar_core_solver.m_r_upper_bounds()[j] ? column_type::boxed : column_type::fixed;
-            }
-        }
-        break;
-    case EQ:
-	{
-            auto v = numeric_pair<mpq>(right_side, zero_of_type<mpq>());
-            if (v > m_mpq_lar_core_solver.m_r_upper_bounds[j]) {
-                m_status = lp_status::INFEASIBLE;
-                set_lower_bound_witness(j, ci);
-                //                m_infeasible_column_index = j;
-            }
-            else {
-                m_mpq_lar_core_solver.m_r_lower_bounds[j] = m_mpq_lar_core_solver.m_r_upper_bounds[j] = v;
-                m_columns_with_changed_bound.insert(j);
-                set_lower_bound_witness(j, ci);
-                set_upper_bound_witness(j, ci);
-                m_mpq_lar_core_solver.m_column_types[j] = column_type::fixed;
-            }
-            break;
-	}
-	break;
-
-    default:
-        lp_unreachable();
-
-    }
-}
-
-void lar_solver::update_boxed_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) {
-    lp_assert(m_status == lp_status::INFEASIBLE || (m_mpq_lar_core_solver.m_column_types()[j] == column_type::boxed && m_mpq_lar_core_solver.m_r_lower_bounds()[j] < m_mpq_lar_core_solver.m_r_upper_bounds()[j]));
-    mpq y_of_bound(0);
-    switch (kind) {
-    case LT:
-        y_of_bound = -1;
-    case LE:
-	{
-            auto up = numeric_pair<mpq>(right_side, y_of_bound);
-            if (up < m_mpq_lar_core_solver.m_r_upper_bounds[j]) {
-                m_mpq_lar_core_solver.m_r_upper_bounds[j] = up;
-                set_upper_bound_witness(j, ci);
-                m_columns_with_changed_bound.insert(j);
-            }
-
-            if (up < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
-                m_status = lp_status::INFEASIBLE;
-                //                m_infeasible_column_index = j;
-            }
-            else {
-                if (m_mpq_lar_core_solver.m_r_lower_bounds()[j] == m_mpq_lar_core_solver.m_r_upper_bounds()[j])
-                    m_mpq_lar_core_solver.m_column_types[j] = column_type::fixed;
-            }
-	}
-	break;
-    case GT:
-        y_of_bound = 1;
-    case GE:
-	{
-            auto low = numeric_pair<mpq>(right_side, y_of_bound);
-            if (low > m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
-                m_mpq_lar_core_solver.m_r_lower_bounds[j] = low;
-                m_columns_with_changed_bound.insert(j);
-                set_lower_bound_witness(j, ci);
-            }
-            if (low > m_mpq_lar_core_solver.m_r_upper_bounds[j]) {
-                m_status = lp_status::INFEASIBLE;
-                // m_infeasible_column_index = j;
-            }
-            else if (low == m_mpq_lar_core_solver.m_r_upper_bounds[j]) {
-                m_mpq_lar_core_solver.m_column_types[j] = column_type::fixed;
-            }
-	}
-	break;
-    case EQ:
-	{
-            auto v = numeric_pair<mpq>(right_side, zero_of_type<mpq>());
-            if (v < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
-                m_status = lp_status::INFEASIBLE;
-                // m_infeasible_column_index = j;
-                set_upper_bound_witness(j, ci);
-            }
-            else if (v > m_mpq_lar_core_solver.m_r_upper_bounds[j]) {
-                m_status = lp_status::INFEASIBLE;
-                // m_infeasible_column_index = j;
-                set_lower_bound_witness(j, ci);
-            }
-            else {
-                m_mpq_lar_core_solver.m_r_lower_bounds[j] = m_mpq_lar_core_solver.m_r_upper_bounds[j] = v;
-                set_lower_bound_witness(j, ci);
-                set_upper_bound_witness(j, ci);
-                m_mpq_lar_core_solver.m_column_types[j] = column_type::fixed;
-                m_columns_with_changed_bound.insert(j);
-            }
-
-            break;
-	}
-
-    default:
-        lp_unreachable();
-
-    }
-}
 void lar_solver::update_column_type_and_bound_with_ub(unsigned j, lp::lconstraint_kind kind, const mpq & right_side, unsigned constraint_index, lp::explanation& e) {
     SASSERT(column_has_upper_bound(j));
     if (column_has_lower_bound(j)) {
@@ -2332,127 +2158,6 @@ void lar_solver::update_bound_with_no_ub_no_lb(var_index j, lconstraint_kind kin
     }
 }
 
-
-void lar_solver::update_lower_bound_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) {
-    lp_assert(m_mpq_lar_core_solver.m_column_types()[j] == column_type::lower_bound);
-    mpq y_of_bound(0);
-    switch (kind) {
-    case LT:
-        y_of_bound = -1;
-    case LE:
-	{
-            auto up = numeric_pair<mpq>(right_side, y_of_bound);
-            m_mpq_lar_core_solver.m_r_upper_bounds[j] = up;
-            set_upper_bound_witness(j, ci);
-            m_columns_with_changed_bound.insert(j);
-
-            if (up < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
-                m_status = lp_status::INFEASIBLE;
-                // m_infeasible_column_index = j;
-            }
-            else {
-                m_mpq_lar_core_solver.m_column_types[j] = m_mpq_lar_core_solver.m_r_lower_bounds()[j] < m_mpq_lar_core_solver.m_r_upper_bounds()[j] ? column_type::boxed : column_type::fixed;
-            }
-	}
-	break;
-    case GT:
-        y_of_bound = 1;
-    case GE:
-	{
-            auto low = numeric_pair<mpq>(right_side, y_of_bound);
-            if (low > m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
-                m_mpq_lar_core_solver.m_r_lower_bounds[j] = low;
-                m_columns_with_changed_bound.insert(j);
-                set_lower_bound_witness(j, ci);
-            }
-	}
-	break;
-    case EQ:
-	{
-            auto v = numeric_pair<mpq>(right_side, zero_of_type<mpq>());
-            if (v < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
-                m_status = lp_status::INFEASIBLE;
-                // m_infeasible_column_index = j;
-                set_upper_bound_witness(j, ci);
-            }
-            else {
-                m_mpq_lar_core_solver.m_r_lower_bounds[j] = m_mpq_lar_core_solver.m_r_upper_bounds[j] = v;
-                set_lower_bound_witness(j, ci);
-                set_upper_bound_witness(j, ci);
-                m_mpq_lar_core_solver.m_column_types[j] = column_type::fixed;
-            }
-            m_columns_with_changed_bound.insert(j);
-            break;
-	}
-
-    default:
-        lp_unreachable();
-
-    }
-}
-
-void lar_solver::update_fixed_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci) {
-    lp_assert(m_status == lp_status::INFEASIBLE || (m_mpq_lar_core_solver.m_column_types()[j] == column_type::fixed && m_mpq_lar_core_solver.m_r_lower_bounds()[j] == m_mpq_lar_core_solver.m_r_upper_bounds()[j]));
-    lp_assert(m_status == lp_status::INFEASIBLE || (m_mpq_lar_core_solver.m_r_lower_bounds()[j].y.is_zero() && m_mpq_lar_core_solver.m_r_upper_bounds()[j].y.is_zero()));
-    auto v = numeric_pair<mpq>(right_side, mpq(0));
-
-    mpq y_of_bound(0);
-    switch (kind) {
-    case LT:
-        if (v <= m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
-            m_status = lp_status::INFEASIBLE;
-            // m_infeasible_column_index = j;
-            set_upper_bound_witness(j, ci);
-        }
-        break;
-    case LE:
-	{
-            if (v < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
-                m_status = lp_status::INFEASIBLE;
-                // m_infeasible_column_index = j;
-                set_upper_bound_witness(j, ci);
-            }
-	}
-	break;
-    case GT:
-	{
-            if (v >= m_mpq_lar_core_solver.m_r_upper_bounds[j]) {
-                m_status = lp_status::INFEASIBLE;
-                // m_infeasible_column_index = j;
-                set_lower_bound_witness(j, ci);
-            }
-	}
-	break;
-    case GE:
-	{
-            if (v > m_mpq_lar_core_solver.m_r_upper_bounds[j]) {
-                m_status = lp_status::INFEASIBLE;
-                // m_infeasible_column_index = j;
-                set_lower_bound_witness(j, ci);
-            }
-	}
-	break;
-    case EQ:
-	{
-            if (v < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
-                m_status = lp_status::INFEASIBLE;
-                // m_infeasible_column_index = j;
-                set_upper_bound_witness(j, ci);
-            }
-            else if (v > m_mpq_lar_core_solver.m_r_upper_bounds[j]) {
-                m_status = lp_status::INFEASIBLE;
-                // m_infeasible_column_index = j;
-                set_lower_bound_witness(j, ci);
-            }
-            break;
-	}
-
-    default:
-        lp_unreachable();
-
-    }
-}
-
 bool lar_solver::column_corresponds_to_term(unsigned j) const {
     return m_var_register.local_to_external(j) >= m_terms_start_index;
 }
diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h
index c50c28ff6..5322a801d 100644
--- a/src/util/lp/lar_solver.h
+++ b/src/util/lp/lar_solver.h
@@ -226,15 +226,6 @@ public:
     // this fills the last row of A_d and sets the basis column: -1 in the last column of the row
     void fill_last_row_of_A_d(static_matrix<double, double> & A, const lar_term* ls);
 
-    void update_free_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index constr_ind);
-
-    void update_upper_bound_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci, explanation &);
-    
-    void update_boxed_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci);
-    void update_lower_bound_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci);
-
-    void update_fixed_column_type_and_bound(var_index j, lconstraint_kind kind, const mpq & right_side, constraint_index ci);
-
     //end of init region