mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
fix #4948
This commit is contained in:
parent
0aac7e54a9
commit
fc3a642876
|
@ -252,11 +252,10 @@ namespace opt {
|
|||
|
||||
auto decrement = [&]() {
|
||||
SASSERT(has_shared);
|
||||
if (l_true != decrement_value(i, val)) {
|
||||
if (l_true != m_context.check(0, nullptr))
|
||||
throw default_exception("maximization suspended");
|
||||
m_context.get_model(m_last_model);
|
||||
}
|
||||
decrement_value(i, val);
|
||||
if (l_true != m_context.check(0, nullptr))
|
||||
throw default_exception("maximization suspended");
|
||||
m_context.get_model(m_last_model);
|
||||
};
|
||||
|
||||
if (!val.is_finite()) {
|
||||
|
|
|
@ -3459,7 +3459,11 @@ public:
|
|||
st = lp::lp_status::UNBOUNDED;
|
||||
}
|
||||
else {
|
||||
if (lp().get_status() != lp::lp_status::OPTIMAL || lp().has_changed_columns())
|
||||
make_feasible();
|
||||
|
||||
vi = get_lpvar(v);
|
||||
|
||||
st = lp().maximize_term(vi, term_max);
|
||||
if (has_int() && lp().has_inf_int()) {
|
||||
st = lp::lp_status::FEASIBLE;
|
||||
|
@ -3483,6 +3487,7 @@ public:
|
|||
return inf_eps(rational::zero(), val);
|
||||
}
|
||||
default:
|
||||
std::cout << st << "\n";
|
||||
SASSERT(st == lp::lp_status::UNBOUNDED);
|
||||
TRACE("arith", display(tout << st << " v" << v << " vi: " << vi << "\n"););
|
||||
has_shared = false;
|
||||
|
|
Loading…
Reference in a new issue