mirror of
https://github.com/Z3Prover/z3
synced 2025-04-15 13:28:47 +00:00
update to retain original behavior
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
eeb79e1c3c
commit
cc7a176c89
|
@ -406,7 +406,7 @@ namespace opt {
|
||||||
if (r == l_true && !get_lower_as_num(i).is_finite()) {
|
if (r == l_true && !get_lower_as_num(i).is_finite()) {
|
||||||
return r;
|
return r;
|
||||||
}
|
}
|
||||||
if (r == l_true && i + 1 < m_objectives.size() && get_lower_as_num(i).is_finite()) {
|
if (r == l_true && i + 1 < m_objectives.size()) {
|
||||||
update_lower();
|
update_lower();
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
Loading…
Reference in a new issue