mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
fix #4810
This commit is contained in:
parent
065e0652a3
commit
6d0b89a989
|
@ -1552,11 +1552,9 @@ public:
|
|||
IF_VERBOSE(12, verbose_stream() << "final-check " << lp().get_status() << "\n");
|
||||
lbool is_sat = l_true;
|
||||
SASSERT(lp().ax_is_correct());
|
||||
if (lp().get_status() != lp::lp_status::OPTIMAL) { // || lp().has_changed_columns()) {
|
||||
if (lp().get_status() != lp::lp_status::OPTIMAL || lp().has_changed_columns()) {
|
||||
is_sat = make_feasible();
|
||||
}
|
||||
else
|
||||
SASSERT(!lp().has_changed_columns());
|
||||
final_check_status st = FC_DONE;
|
||||
|
||||
switch (is_sat) {
|
||||
|
@ -2088,6 +2086,7 @@ public:
|
|||
}
|
||||
|
||||
void propagate() {
|
||||
m_model_is_initialized = false;
|
||||
flush_bound_axioms();
|
||||
if (!can_propagate()) {
|
||||
return;
|
||||
|
|
Loading…
Reference in a new issue