From 0ee68220e1ff210e663434cc3559b9486135188a Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Mon, 30 Jul 2018 14:34:03 -0700
Subject: [PATCH] use CASSERT instead of lp_assert for static_matrix

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/util/lp/lar_solver.cpp            | 2 +-
 src/util/lp/lp_core_solver_base.h     | 2 +-
 src/util/lp/lp_core_solver_base_def.h | 6 +++---
 src/util/lp/static_matrix.h           | 8 ++++----
 src/util/lp/static_matrix_def.h       | 2 --
 5 files changed, 9 insertions(+), 11 deletions(-)

diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp
index 5408bd922..0d8e7f70a 100644
--- a/src/util/lp/lar_solver.cpp
+++ b/src/util/lp/lar_solver.cpp
@@ -1373,7 +1373,7 @@ void lar_solver::remove_last_row_and_column_from_tableau(unsigned j) {
     lp_assert(A_r().m_columns[j].live_size() == 0);
     A_r().m_rows.pop_back();
     A_r().m_columns.pop_back();
-	lp_assert(A_r().is_correct());
+	CASSERT("check_static_matrix", A_r().is_correct());
     slv.m_b.pop_back();
 }
 
diff --git a/src/util/lp/lp_core_solver_base.h b/src/util/lp/lp_core_solver_base.h
index fbb08edfe..00ba437d1 100644
--- a/src/util/lp/lp_core_solver_base.h
+++ b/src/util/lp/lp_core_solver_base.h
@@ -230,7 +230,7 @@ public:
     bool reduced_costs_are_correct_tableau() const {
         if (m_settings.simplex_strategy() == simplex_strategy_enum::tableau_rows)
             return true;
-        lp_assert(m_A.is_correct());
+        CASSERT("check_static_matrix", m_A.is_correct());
         if (m_using_infeas_costs) {
             if (infeasibility_costs_are_correct() == false) {
                 return false;
diff --git a/src/util/lp/lp_core_solver_base_def.h b/src/util/lp/lp_core_solver_base_def.h
index 8cfc39170..6a9af8a26 100644
--- a/src/util/lp/lp_core_solver_base_def.h
+++ b/src/util/lp/lp_core_solver_base_def.h
@@ -616,7 +616,7 @@ divide_row_by_pivot(unsigned pivot_row, unsigned pivot_col) {
         }
     }
     coeff = one_of_type<T>();
-    lp_assert(m_A.is_correct());
+    CASSERT("check_static_matrix", m_A.is_correct());
     return true;
 }
 template <typename T, typename X> bool lp_core_solver_base<T, X>::
@@ -639,7 +639,7 @@ pivot_column_tableau(unsigned j, unsigned piv_row_index) {
     if (pivot_col_cell_index != 0)
         m_A.swap_with_head_cell(j, pivot_col_cell_index);
 
-    lp_assert(m_A.is_correct());
+    CASSERT("check_static_matrix", m_A.is_correct());
     while (column.live_size() > 1) {
         auto & c = column.back();
         if (c.dead()) {
@@ -655,7 +655,7 @@ pivot_column_tableau(unsigned j, unsigned piv_row_index) {
     }
     m_A.compress_column_if_needed(j);
     lp_assert(column.live_size() == 1);
-    lp_assert(m_A.is_correct());
+    CASSERT("check_static_matrix", m_A.is_correct());
 
     if (m_settings.simplex_strategy() == simplex_strategy_enum::tableau_costs)
         pivot_to_reduced_costs_tableau(piv_row_index, j);
diff --git a/src/util/lp/static_matrix.h b/src/util/lp/static_matrix.h
index e3ea3c1b0..cb6af1379 100644
--- a/src/util/lp/static_matrix.h
+++ b/src/util/lp/static_matrix.h
@@ -184,7 +184,7 @@ public:
             c.next_dead_index() = m_first_dead;
             m_first_dead = j;
         }
-        lp_assert(is_correct());
+        CASSERT("check_static_matrix", is_correct());
     }
 
     bool is_correct() const {
@@ -264,7 +264,7 @@ public:
             c.next_dead_index() = m_first_dead;
             m_first_dead = j;
         }
-        lp_assert(is_correct());
+        CASSERT("check_static_matrix", is_correct());
     }
     
     const column_cell& operator[] (unsigned i) const { return m_cells[i];}
@@ -330,7 +330,7 @@ public:
         }
         m_cells[0] = m_cells[i];
         m_cells[i] = head_copy;
-        lp_assert(is_correct());
+        CASSERT("check_static_matrix", is_correct());
     }
 
     column_cell & add_cell(unsigned i, unsigned & index) {
@@ -580,7 +580,7 @@ public:
                 m_columns.pop_back(); // delete the last column
             m_stack.pop();
         }
-        lp_assert(is_correct());
+        CASSERT("check_static_matrix", is_correct());
     }
 
     void multiply_row(unsigned row, T const & alpha) {
diff --git a/src/util/lp/static_matrix_def.h b/src/util/lp/static_matrix_def.h
index ae0e22540..43c91cefa 100644
--- a/src/util/lp/static_matrix_def.h
+++ b/src/util/lp/static_matrix_def.h
@@ -293,8 +293,6 @@ template <typename T, typename X>    T static_matrix<T, X>::get_row_balance(unsi
 }
 
 template <typename T, typename X> bool static_matrix<T, X>::is_correct() const {
-    if (m_rows.size() > 100 || m_columns.size() > 100)
-        return true;
     for (unsigned i = 0; i < m_rows.size(); i++) {
         auto &r = m_rows[i];
         std::unordered_set<unsigned> s;