From c3ed06915c7a0a5070129ba229732f6207be8829 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 31 Dec 2019 14:03:48 -0800 Subject: [PATCH] avoid the state change in an assert statement Signed-off-by: Lev Nachmanson --- src/util/lp/lar_solver.cpp | 2 +- src/util/lp/lp_settings.h | 7 +++++++ 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp index 7a416741e..8feb018bc 100644 --- a/src/util/lp/lar_solver.cpp +++ b/src/util/lp/lar_solver.cpp @@ -857,7 +857,7 @@ void lar_solver::solve_with_core_solver() { update_x_and_inf_costs_for_columns_with_changed_bounds(); m_mpq_lar_core_solver.solve(); set_status(m_mpq_lar_core_solver.m_r_solver.get_status()); - lp_assert((m_settings.random_next() % 100) != 0 || m_status != lp_status::OPTIMAL || all_constraints_hold()); + lp_assert((((m_settings.m_counter_for_debug++) % 100) != 0) || m_status != lp_status::OPTIMAL || all_constraints_hold()); } diff --git a/src/util/lp/lp_settings.h b/src/util/lp/lp_settings.h index d0bdc284d..3ae29649f 100644 --- a/src/util/lp/lp_settings.h +++ b/src/util/lp/lp_settings.h @@ -198,6 +198,9 @@ public: unsigned limit_on_rows_for_hnf_cutter; unsigned limit_on_columns_for_hnf_cutter; bool m_enable_hnf; +#ifdef Z3DEBUG + unsigned m_counter_for_debug; +#endif unsigned hnf_cut_period() const { return m_hnf_cut_period; } @@ -266,6 +269,10 @@ public: limit_on_rows_for_hnf_cutter(75), limit_on_columns_for_hnf_cutter(150), m_enable_hnf(true) + #ifdef Z3DEBUG + , m_counter_for_debug(0) + #endif + {} void set_resource_limit(lp_resource_limit& lim) { m_resource_limit = &lim; }