diff --git a/src/util/lp/lp_core_solver_base.h b/src/util/lp/lp_core_solver_base.h
index 925206680..7313a46de 100644
--- a/src/util/lp/lp_core_solver_base.h
+++ b/src/util/lp/lp_core_solver_base.h
@@ -479,6 +479,7 @@ public:
     
     void change_basis(unsigned entering, unsigned leaving) {
         lean_assert(m_basis_heading[entering] < 0);
+		lean_assert(m_basis_heading[leaving] >= 0);
         
         int place_in_basis =  m_basis_heading[leaving];
         int place_in_non_basis = - m_basis_heading[entering] - 1;
diff --git a/src/util/lp/lp_core_solver_base.hpp b/src/util/lp/lp_core_solver_base.hpp
index d551daf27..03ae4e184 100644
--- a/src/util/lp/lp_core_solver_base.hpp
+++ b/src/util/lp/lp_core_solver_base.hpp
@@ -925,7 +925,9 @@ template <typename T, typename X>  void lp_core_solver_base<T, X>::transpose_row
 }
 // 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)  {
-    unsigned row_index = m_basis_heading[j_basic];
+	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()) {
@@ -940,15 +942,16 @@ template <typename T, typename X> bool lp_core_solver_base<T, X>::pivot_column_g
             return false;
         }
     } else { // the tableau case
-        pivot_column_tableau(j, row_index);
+       return pivot_column_tableau(j, row_index);
     }
-    return true;
 }
+
 template <typename T, typename X>  void lp_core_solver_base<T, X>::pivot_fixed_vars_from_basis() {
     // run over basis and non-basis at the same time
     indexed_vector<T> w(m_basis.size()); // the buffer
     unsigned i = 0; // points to basis
     unsigned j = 0; // points to nonbasis
+	
     for (; i < m_basis.size() && j < m_nbasis.size(); i++) {
         unsigned ii = m_basis[i];
         unsigned jj;
@@ -963,8 +966,9 @@ 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))
-                break;
+			if (!pivot_column_general(jj, ii, w))
+				return; // total failure
+			break;
         } 
     }
 }