mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
fix the value oflar_solver.m_status during pop()
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
parent
2097983db3
commit
99339798ee
|
@ -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<constraint_index> lar_solver::get_all_constraint_indices() const {
|
||||
|
|
|
@ -94,7 +94,6 @@ class lar_solver : public column_namer {
|
|||
var_register m_var_register;
|
||||
stacked_vector<ul_pair> m_columns_to_ul_pairs;
|
||||
vector<lar_base_constraint*> m_constraints;
|
||||
private:
|
||||
stacked_value<unsigned> m_constraint_count;
|
||||
// the set of column indices j such that bounds have changed for j
|
||||
int_set m_columns_with_changed_bound;
|
||||
|
|
Loading…
Reference in a new issue