mirror of
https://github.com/Z3Prover/z3
synced 2025-04-16 22:05:36 +00:00
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
30974968af
commit
0490056e7a
|
@ -235,7 +235,7 @@ namespace opt {
|
|||
else {
|
||||
++steps;
|
||||
}
|
||||
if (delta_per_step > rational::one() || obj == last_objective) {
|
||||
if (delta_per_step > rational::one() || (obj == last_objective && is_int)) {
|
||||
m_s->push();
|
||||
++num_scopes;
|
||||
bound = m_s->mk_ge(obj_index, obj + inf_eps(delta_per_step));
|
||||
|
|
Loading…
Reference in a new issue