opt: fix timeout on real-valued optimization with open (strict) optima

Commit fdc32d0e6 ("Fix inconsistent optimization result with unvalidated
LP bound (#10028)") regressed lexicographic/single real optimization whose
optimum is an open infimum/supremum (a strict inequality that no model
attains). Such objectives now time out instead of reporting the correct
optimum.

Root cause: the #10028 fix deferred committing the LP optimization hint in
opt_solver::maximize_objective until validated by check_bound(), and added a
`!bound_valid` term to optsmt::geometric_lex's blocker-tightening condition.
For a real objective with an open optimum, mk_ge() drops the negative
infinitesimal, so check_bound() legitimately fails (the strict optimum is not
attained), leaving bound_valid == false. geometric_lex then falls back to
coarse model-derived +1 stepping (delta_per_step is pinned to 1 for reals)
across a potentially huge range, which does not converge.

The #10028 problem is integer (a Golomb-ruler encoding with a large
`distinct`). Both changed behaviors only make sense for integer objectives,
so gate them on `is_int`:

- opt_solver::maximize_objective: commit the hint eagerly for real
  objectives (pre-#10028 behavior); keep the deferred, validated commit for
  integer objectives.
- optsmt::geometric_lex: only take the model-derived tightening branch on an
  invalid bound when the objective is integer (`!bound_valid && is_int`).

This restores the exact pre-#10028 code path for reals while leaving the
integer path unchanged.

Validated by rebuilding z3 and re-running inputs/issues/iss-1851/bug-1.smt2
(byte-exact match with the recorded oracle) and confirming the #10028
integer reproducer still returns a consistent true optimum.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

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

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));