From 99339798ee98c6317995a4ed10a26bd39e5a8433 Mon Sep 17 00:00:00 2001 From: Lev Date: Thu, 4 Oct 2018 16:42:32 -0700 Subject: [PATCH] fix the value oflar_solver.m_status during pop() Signed-off-by: Lev --- src/util/lp/lar_solver.cpp | 2 +- src/util/lp/lar_solver.h | 1 - 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp index 5b3028a98..31e9d2654 100644 --- a/src/util/lp/lar_solver.cpp +++ b/src/util/lp/lar_solver.cpp @@ -377,7 +377,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()); - m_status = m_mpq_lar_core_solver.m_r_solver.current_x_is_feasible()? lp_status::OPTIMAL: lp_status::UNKNOWN; + set_status(lp_status::UNKNOWN); } vector lar_solver::get_all_constraint_indices() const { diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h index 8541a9b86..7af9cfacb 100644 --- a/src/util/lp/lar_solver.h +++ b/src/util/lp/lar_solver.h @@ -94,7 +94,6 @@ class lar_solver : public column_namer { var_register m_var_register; stacked_vector m_columns_to_ul_pairs; vector m_constraints; -private: stacked_value m_constraint_count; // the set of column indices j such that bounds have changed for j int_set m_columns_with_changed_bound;