From c557743be4e09aebda5a18b4ffbc0426ff882d92 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 18 Apr 2019 23:16:19 -0700 Subject: [PATCH] fix in rounding rows Signed-off-by: Lev Nachmanson --- src/util/lp/lar_solver.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp index ac2b36e0b..93827e453 100644 --- a/src/util/lp/lar_solver.cpp +++ b/src/util/lp/lar_solver.cpp @@ -397,7 +397,7 @@ void lar_solver::pop(unsigned k) { m_settings.simplex_strategy() = m_simplex_strategy; lp_assert(sizes_are_correct()); lp_assert((!m_settings.use_tableau()) || m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau()); - lp_assert(ax_is_correct()); + lp_assert(m_cube_rounded_columns.size() == 0 || ax_is_correct()); set_status(lp_status::UNKNOWN); }