diff --git a/src/util/lp/int_solver.cpp b/src/util/lp/int_solver.cpp
index 1a6d6ddae..938a13fac 100644
--- a/src/util/lp/int_solver.cpp
+++ b/src/util/lp/int_solver.cpp
@@ -281,9 +281,18 @@ bool int_solver::mk_gomory_cut(unsigned row_index, explanation & ex) {
     */
 
 }
+
+void int_solver::init_check_data() {
+	init_inf_int_set();
+	unsigned n = m_lar_solver->A_r().column_count();
+	m_old_values_set.resize(n);
+	m_old_values_data.resize(n);
+}
+
 lia_move int_solver::check(lar_term& t, mpq& k, explanation& ex) {
-    lean_assert(is_feasible());
-    init_inf_int_set();
+	lean_assert(m_lar_solver->m_mpq_lar_core_solver.r_basis_is_OK());
+	lean_assert(is_feasible());
+	init_check_data();
     lean_assert(inf_int_set_is_correct());
     // currently it is a reimplementation of
     // final_check_status theory_arith<Ext>::check_int_feasibility()
@@ -298,9 +307,12 @@ lia_move int_solver::check(lar_term& t, mpq& k, explanation& ex) {
         
     */
     m_lar_solver->pivot_fixed_vars_from_basis();
+	lean_assert(m_lar_solver->m_mpq_lar_core_solver.r_basis_is_OK());
     patch_int_infeasible_columns();
-    fix_non_base_columns();
-    lean_assert(is_feasible());
+	lean_assert(m_lar_solver->m_mpq_lar_core_solver.r_basis_is_OK());
+	fix_non_base_columns();
+	lean_assert(m_lar_solver->m_mpq_lar_core_solver.r_basis_is_OK());
+	lean_assert(is_feasible());
     TRACE("arith_int_rows", trace_inf_rows(););
     
     if (find_inf_int_base_column() == -1)
@@ -339,7 +351,8 @@ lia_move int_solver::check(lar_term& t, mpq& k, explanation& ex) {
             return lia_move::branch;
         }
     }
-    //    return true;
+	lean_assert(m_lar_solver->m_mpq_lar_core_solver.r_basis_is_OK());
+	//    return true;
     return lia_move::give_up;
 }
 
diff --git a/src/util/lp/int_solver.h b/src/util/lp/int_solver.h
index edfba5e5b..8259ae128 100644
--- a/src/util/lp/int_solver.h
+++ b/src/util/lp/int_solver.h
@@ -98,5 +98,6 @@ private:
     void move_non_base_vars_to_bounds();
     void branch_infeasible_int_var(unsigned);
     bool mk_gomory_cut(unsigned row_index, explanation & ex);
+	void init_check_data();
 };
 }
diff --git a/src/util/lp/lp_core_solver_base.hpp b/src/util/lp/lp_core_solver_base.hpp
index d251c9ebf..d870b0c33 100644
--- a/src/util/lp/lp_core_solver_base.hpp
+++ b/src/util/lp/lp_core_solver_base.hpp
@@ -939,26 +939,32 @@ template <typename T, typename X>  void lp_core_solver_base<T, X>::transpose_row
     m_A.transpose_rows(i, j);
 }
 // j is the new basic column, j_basic - the leaving column
-template <typename T, typename X> bool lp_core_solver_base<T, X>::pivot_column_general(unsigned j, unsigned j_basic, indexed_vector<T> & w)  {
-    lean_assert(m_basis_heading[j] < 0);
-    lean_assert(m_basis_heading[j_basic] >= 0);
-    unsigned row_index = m_basis_heading[j_basic];
-    change_basis(j, j_basic);
-    if (m_settings.m_simplex_strategy == simplex_strategy_enum::lu) {
-        if (m_factorization->need_to_refactor()) {
-            init_lu();
-        } else {
-            m_factorization->prepare_entering(j, w); // to init vector w
-            m_factorization->replace_column(zero_of_type<T>(), w, row_index);
-        }
-        if (m_factorization->get_status() != LU_status::OK) {
-            change_basis(j_basic, j);
-            init_lu();
-            return false;
-        }
-    } else { // the tableau case
-       return pivot_column_tableau(j, row_index);
-    }
+template <typename T, typename X> bool lp_core_solver_base<T, X>::pivot_column_general(unsigned j, unsigned j_basic, indexed_vector<T> & w) {
+	lean_assert(m_basis_heading[j] < 0);
+	lean_assert(m_basis_heading[j_basic] >= 0);
+	unsigned row_index = m_basis_heading[j_basic];
+	if (m_settings.m_simplex_strategy == simplex_strategy_enum::lu) {
+		if (m_factorization->need_to_refactor()) {
+			init_lu();
+		}
+		else {
+			m_factorization->prepare_entering(j, w); // to init vector w
+			m_factorization->replace_column(zero_of_type<T>(), w, row_index);
+		}
+		if (m_factorization->get_status() != LU_status::OK) {
+			init_lu();
+			return false;
+		}
+		else {
+			change_basis(j, j_basic);
+		}
+	}
+	else { // the tableau case
+		if (pivot_column_tableau(j, row_index))
+			change_basis(j, j_basic);
+		else return false;
+	}
+	return true;
 }
 
 template <typename T, typename X>  void lp_core_solver_base<T, X>::pivot_fixed_vars_from_basis() {
@@ -981,10 +987,10 @@ template <typename T, typename X>  void lp_core_solver_base<T, X>::pivot_fixed_v
             if (j >= m_nbasis.size())
                 break;
             j++;
-            if (!pivot_column_general(jj, ii, w))
-                return; // total failure
-            break;
-        }
+            if (pivot_column_general(jj, ii, w))
+                break;
+        } 
+    }
 }
 
 template <typename T, typename X> bool