diff --git a/src/util/lp/lp_core_solver_base.hpp b/src/util/lp/lp_core_solver_base.hpp
index 2039ad62b..d251c9ebf 100644
--- a/src/util/lp/lp_core_solver_base.hpp
+++ b/src/util/lp/lp_core_solver_base.hpp
@@ -940,9 +940,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)  {
-	lean_assert(m_basis_heading[j] < 0);
-	lean_assert(m_basis_heading[j_basic] >= 0);
-	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()) {
@@ -966,7 +966,7 @@ template <typename T, typename X>  void lp_core_solver_base<T, X>::pivot_fixed_v
     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;
@@ -981,19 +981,10 @@ template <typename T, typename X>  void lp_core_solver_base<T, X>::pivot_fixed_v
             if (j >= m_nbasis.size())
                 break;
             j++;
-<<<<<<< a4275bb735828a40f94571cae4765f8be8225423
             if (!pivot_column_general(jj, ii, w))
-                break;
-            }
+                return; // total failure
+            break;
         }
-        SASSERT(m_factorization->get_status()== LU_status::OK);
-=======
-			if (!pivot_column_general(jj, ii, w))
-				return; // total failure
-			break;
-        } 
-    }
->>>>>>> fix a bug in pivot_fixed_vars_from_basis
 }
 
 template <typename T, typename X> bool