mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
fix #7245
This commit is contained in:
parent
a6b502779b
commit
01e47bfe26
|
@ -259,8 +259,9 @@ namespace opt {
|
|||
if (!m_models[i])
|
||||
m_models.set(i, m_last_model.get());
|
||||
|
||||
if (val > m_objective_values[i])
|
||||
m_objective_values[i] = val;
|
||||
if (val > m_objective_values[i]) {
|
||||
m_objective_values[i] = val;
|
||||
}
|
||||
|
||||
if (!m_last_model)
|
||||
return true;
|
||||
|
@ -284,14 +285,7 @@ namespace opt {
|
|||
//
|
||||
auto check_bound = [&]() {
|
||||
SASSERT(has_shared);
|
||||
bool ok = bound_value(i, val);
|
||||
if (l_true != m_context.check(0, nullptr))
|
||||
return false;
|
||||
m_context.get_model(m_last_model);
|
||||
if (!m_last_model)
|
||||
return false;
|
||||
update_objective();
|
||||
return ok;
|
||||
return bound_value(i, val) && l_true == m_context.check(0, nullptr);
|
||||
};
|
||||
|
||||
if (!val.is_finite()) {
|
||||
|
|
|
@ -258,7 +258,7 @@ namespace smt {
|
|||
expr_ref_vector get_trail(unsigned max_level);
|
||||
|
||||
/**
|
||||
\brief (For debubbing purposes) Prints the state of the kernel
|
||||
\brief (For debugging purposes) Prints the state of the kernel
|
||||
*/
|
||||
std::ostream& display(std::ostream & out) const;
|
||||
|
||||
|
|
Loading…
Reference in a new issue