mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

#6421

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-10-28 14:12:28 -07:00
parent 91cdc082c4
commit 0e651eee04
1 changed files with 6 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/opt/opt_solver.cpp
View file

@ -287,7 +287,9 @@ namespace opt {
bool ok = bound_value(i, val); bool ok = bound_value(i, val);
if (l_true != m_context.check(0, nullptr)) if (l_true != m_context.check(0, nullptr))
return false; return false;
m_context.get_model(m_last_model); m_context.get_model(m_last_model);
if (!m_last_model)
return false;
update_objective(); update_objective();
return ok; return ok;
}; };
@ -299,7 +301,9 @@ namespace opt {
TRACE("opt", tout << "updated\n";); TRACE("opt", tout << "updated\n";);
m_last_model = nullptr; m_last_model = nullptr;
m_context.get_model(m_last_model); m_context.get_model(m_last_model);
if (!has_shared || val == current_objective_value(i)) if (!m_last_model)
return false;
else if (!has_shared || val == current_objective_value(i))
m_models.set(i, m_last_model.get()); m_models.set(i, m_last_model.get());
else if (!check_bound()) else if (!check_bound())
return false; return false;