diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp
index eb8b4dd6cb..c41c563ee7 100644
--- a/src/opt/opt_solver.cpp
+++ b/src/opt/opt_solver.cpp
@@ -312,6 +312,16 @@ namespace opt {
         inf_eps val = get_optimizer().maximize(v, blocker, has_shared);
         m_context.get_model(m_model);
         inf_eps val2;
+        //
+        // 'has_shared' as returned by maximize() is false only when the
+        // arithmetic solver proved an *exact* optimum: a pure-LP optimum with
+        // no shared-symbol or integrality relaxation (theory_lra returns an
+        // exact optimum only for lp_status::OPTIMAL; theory_arith only when no
+        // shared symbols or nonlinear monomials are involved).  Capture it
+        // before it is overwritten below; it tells us whether a strict
+        // supremum hint is trustworthy enough to adopt without validation.
+        //
+        bool exact_optimum = !has_shared;
         has_shared = true;
         TRACE(opt, tout << (has_shared?"has shared":"non-shared") << " " << val << " " << blocker << "\n";
               if (m_model) tout << *m_model << "\n";);
@@ -342,6 +352,28 @@ namespace opt {
             return true;
         }
 
+        //
+        // The arithmetic solver proved an exact optimum (exact_optimum) whose
+        // value is a strict supremum: a finite value carrying a non-zero
+        // infinitesimal, e.g. 'maximize a' subject to 'a < 0' yields -epsilon.
+        // Such a bound is genuinely achievable in the limit but cannot be
+        // re-validated by check_bound() below: mk_ge() has to drop the negative
+        // infinitesimal (the strict real bound 'a >= q - epsilon' is not
+        // expressible), so the subsequent assert+check is UNSAT and the hint
+        // would otherwise be discarded, leaving m_objective_values holding the
+        // strictly smaller current model value (regression from #10028;
+        // discussion Z3Prover/bench#3059).  Adopt it here.  This is restricted
+        // to proved-exact optima: for shared-symbol or relaxed hints
+        // (has_shared) the value may over-estimate the true optimum and is
+        // still deferred to validation below, so the soundness fix of #10028
+        // (and the revert of #10052) is preserved.  update_objective() only
+        // ever raises the stored value, so a genuine larger model value still
+        // wins.
+        //
+        if (exact_optimum && val.is_finite() && !val.get_infinitesimal().is_zero() &&
+            val > m_objective_values[i])
+            m_objective_values[i] = val;
+
         //
         // retrieve value of objective from current model and update 
         // current optimal.
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index d3ac4840ad..b092cd4850 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -4089,6 +4089,11 @@ public:
             return value(v);
         case lp::lp_status::FEASIBLE:
             TRACE(arith, display(tout << st << " v" << v << " vi: " << vi << "\n"););
+            // FEASIBLE (as opposed to OPTIMAL) means the returned value is only
+            // a hint: the exact optimum could not be proved, e.g. integrality
+            // forced a fallback to a feasible assignment.  Flag it as shared so
+            // the optimizer validates the bound instead of adopting it eagerly.
+            has_shared = true;
             blocker = mk_gt(v);
             return value(v);
         default:
@@ -4118,8 +4123,12 @@ public:
         else {
             st = max_with_lp(v, vi, term_max);
             inf_eps nl_result;
-            if (max_with_nl(v, st, level, blocker, nl_result))
+            if (max_with_nl(v, st, level, blocker, nl_result)) {
+                // NLA returned a feasible hint rather than a proved optimum;
+                // mark it as shared so the optimizer validates it.
+                has_shared = true;
                 return nl_result;
+            }
         }
         return max_result(v, vi, st, blocker, has_shared);
     }