mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix an assert

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-04-19 09:51:33 -07:00
parent c557743be4
commit c96c37e878
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/util/lp/lar_solver.cpp
View file

@ -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()) {