diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index eb8b4dd6cb..e22127d048 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -320,19 +320,31 @@ namespace opt { TRACE(opt, tout << "maximize " << i << " " << val << " " << m_objective_values[i] << " " << blocker << "\n";); // - // Do NOT commit 'val' to m_objective_values yet: 'val' is only an - // optimization hint from the arithmetic relaxation. When the - // objective shares symbols with other theories (e.g. it occurs inside - // an uninterpreted function such as the auxiliary function used to - // encode large 'distinct' constraints) the hint can over-estimate the - // true optimum and may not be achievable by any model. Committing it - // prematurely and then failing validation (check_bound below) would + // Do NOT commit 'val' to m_objective_values yet for INTEGER objectives: + // 'val' is only an optimization hint from the arithmetic relaxation. + // When the objective shares symbols with other theories (e.g. it occurs + // inside an uninterpreted function such as the auxiliary function used + // to encode large 'distinct' constraints) the hint can over-estimate + // the true optimum and may not be achievable by any model. Committing + // it prematurely and then failing validation (check_bound below) would // leave m_objective_values holding an unachievable bound that callers // such as optsmt::geometric_lex report as the optimum, together with a // model that does not attain it (issue #10028). The value is only // committed after it has been validated, or replaced by the value of // an actual model in update_objective(). // + // Real-valued objectives are different: their optimum can be an open + // infimum/supremum (a strict inequality) that no model attains, so the + // validation below legitimately fails even though 'val' is the correct + // optimum. Deferring the commit there would make saved_objective_value() + // report a suboptimal model value and make geometric_lex fall back to + // coarse +1 stepping over a possibly huge range (timeout). Restore the + // pre-#10028 behavior for reals by committing the hint eagerly; only + // integer objectives use the deferred, validated commit. + // + bool is_int_obj = arith_util(m).is_int(m_objective_terms.get(i)); + if (!is_int_obj && val > m_objective_values[i]) + m_objective_values[i] = val; if (!m_model) { // Without a model there is nothing to validate 'val' against; keep diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp index 5a2b4457b0..713696a094 100644 --- a/src/opt/optsmt.cpp +++ b/src/opt/optsmt.cpp @@ -256,8 +256,13 @@ namespace opt { // the value of an actual model, so replace the blocker with a // model-derived tightening so the search keeps making progress // toward the true optimum instead of terminating prematurely - // (issue #10028). - if (!bound_valid || delta_per_step > rational::one() || (obj == last_objective && is_int)) { + // (issue #10028). This only applies to integer objectives: for + // real objectives the optimum may be an open infimum/supremum + // that no model attains, so 'bound' correctly holds the LP + // blocker for that strict optimum and switching to coarse +1 + // stepping (delta_per_step is pinned to 1 for reals) would fail + // to converge over a large range. + if ((!bound_valid && is_int) || 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));