From c96c37e8781fe63c5fe93a13108d907f8af94b16 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 19 Apr 2019 09:51:33 -0700 Subject: [PATCH] fix an assert Signed-off-by: Lev Nachmanson --- src/util/lp/lar_solver.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp index 93827e453..0b07dde5c 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(m_cube_rounded_columns.size() == 0 || ax_is_correct()); + lp_assert(m_cube_rounded_columns.size() != 0 || ax_is_correct()); set_status(lp_status::UNKNOWN); } @@ -911,7 +911,8 @@ void lar_solver::fix_Ax_b_on_rounded_rows() { } void lar_solver::solve_with_core_solver() { - fix_Ax_b_on_rounded_rows(); + if (m_cube_rounded_columns.size() != 0) + fix_Ax_b_on_rounded_rows(); if (!use_tableau()) add_last_rows_to_lu(m_mpq_lar_core_solver.m_r_solver); if (m_mpq_lar_core_solver.need_to_presolve_with_double_solver()) {