diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp
index 5058bfaf3..0b3c5166a 100644
--- a/src/math/lp/dioph_eq.cpp
+++ b/src/math/lp/dioph_eq.cpp
@@ -709,8 +709,8 @@ namespace lp {
             while (column.size() > 1) {
                 auto& c = column.back();
                 SASSERT(c.var() != last_row_index);
-                m_l_matrix.pivot_row_to_row_given_cell(last_row_index, c, j);
                 m_changed_rows.insert(c.var());
+                m_l_matrix.pivot_row_to_row_given_cell(last_row_index, c, j);
             }
         }
 
diff --git a/src/math/lp/lp_core_solver_base_def.h b/src/math/lp/lp_core_solver_base_def.h
index c4c41c26e..21bd48a22 100644
--- a/src/math/lp/lp_core_solver_base_def.h
+++ b/src/math/lp/lp_core_solver_base_def.h
@@ -277,13 +277,11 @@ pivot_column_tableau(unsigned j, unsigned piv_row_index) {
         m_A.m_rows[c.var()][c.offset()].offset() = pivot_col_cell_index;
     }
     while (column.size() > 1) {
-        auto & c = column.back();
+        auto& c = column.back();
         SASSERT(c.var() != piv_row_index);
-        if(! m_A.pivot_row_to_row_given_cell(piv_row_index, c, j)) {
-            return false;
-        }
-        if (m_touched_rows!= nullptr)
+        if (m_touched_rows != nullptr)
             m_touched_rows->insert(c.var());
+        m_A.pivot_row_to_row_given_cell(piv_row_index, c, j);
     }
 
     if (m_settings.simplex_strategy() == simplex_strategy_enum::tableau_costs)
diff --git a/src/math/lp/static_matrix.cpp b/src/math/lp/static_matrix.cpp
index 26ce218de..4abf0d88a 100644
--- a/src/math/lp/static_matrix.cpp
+++ b/src/math/lp/static_matrix.cpp
@@ -51,8 +51,8 @@ namespace lp {
     template void static_matrix<mpq, numeric_pair<mpq> >::set(unsigned int, unsigned int, mpq const&);
 
 
-    template bool static_matrix<mpq, mpq>::pivot_row_to_row_given_cell(unsigned int, column_cell& , unsigned int);
-    template bool static_matrix<mpq, numeric_pair<mpq> >::pivot_row_to_row_given_cell(unsigned int, column_cell&, unsigned int);
+    template void static_matrix<mpq, mpq>::pivot_row_to_row_given_cell(unsigned int, column_cell& , unsigned int);
+    template void static_matrix<mpq, numeric_pair<mpq> >::pivot_row_to_row_given_cell(unsigned int, column_cell&, unsigned int);
     template void static_matrix<mpq, numeric_pair<mpq> >::pivot_row_to_row_given_cell_with_sign(unsigned int, column_cell&, unsigned int, int);
     template void static_matrix<mpq, mpq>::pivot_row_to_row_given_cell_with_sign(unsigned int, row_cell<empty_struct>&, unsigned int, int);
     template void static_matrix<mpq, numeric_pair<mpq> >::add_rows(mpq const&, unsigned int, unsigned int);
diff --git a/src/math/lp/static_matrix.h b/src/math/lp/static_matrix.h
index 415d3f1a2..08db2245d 100644
--- a/src/math/lp/static_matrix.h
+++ b/src/math/lp/static_matrix.h
@@ -293,7 +293,7 @@ public:
 
 
 // pivot row i to row ii
-    bool pivot_row_to_row_given_cell(unsigned i, column_cell& c, unsigned j);
+    void pivot_row_to_row_given_cell(unsigned i, column_cell& c, unsigned j);
     void pivot_row_to_row_given_cell_with_sign(unsigned piv_row_index, column_cell& c, unsigned j, int j_sign);
     void transpose_rows(unsigned i, unsigned ii) {
         auto t = m_rows[i];
diff --git a/src/math/lp/static_matrix_def.h b/src/math/lp/static_matrix_def.h
index b28d67740..af07c4482 100644
--- a/src/math/lp/static_matrix_def.h
+++ b/src/math/lp/static_matrix_def.h
@@ -48,7 +48,7 @@ namespace lp {
     }
 
 
-    template <typename T, typename X> bool static_matrix<T, X>::pivot_row_to_row_given_cell(unsigned i, 
+    template <typename T, typename X> void static_matrix<T, X>::pivot_row_to_row_given_cell(unsigned i, 
                                                                                             column_cell & c, unsigned pivot_col) {
         unsigned ii = c.var();
         SASSERT(i < row_count() && ii < column_count() && i != ii);
@@ -82,7 +82,7 @@ namespace lp {
             if (is_zero(rowii[k].coeff()))
                 remove_element(rowii, rowii[k]);
         }
-        return !rowii.empty();
+        SASSERT(!rowii.empty());
     }