Fix inconsistent optimization result with unvalidated LP bound (#10028) (#10040)

Fixes #10028.

## Problem

Minimizing an integer variable over a problem containing a large
`distinct` constraint returned an **inconsistent** result: the reported
optimum did not match the returned model, and it was not the true
optimum.

Reproducer from the issue (a Golomb-ruler problem, true optimum = 55):

```python
import z3
n, U = 10, 500
x = [z3.Int(f"x{i}") for i in range(n)]
o = z3.Optimize()
for xi in x: o.add(xi >= 0, xi <= U)
o.add(x[0] == 0)
for i in range(n - 1): o.add(x[i] < x[i + 1])
o.add(z3.Distinct([x[j] - x[i] for i in range(n) for j in range(i + 1, n)]))
h = o.minimize(x[n - 1])
print(o.check(), o.lower(h), o.upper(h), o.model()[x[n - 1]])
# sat 20 20 500   <-- objective 20, but model has x9 = 500 (and 20 is unsat)
```

## Root cause

A `distinct` with more than 32 arguments is encoded with a fresh
uninterpreted sort and function (`smt_internalizer.cpp`), so the
objective variable becomes a *shared symbol* whose feasible values
depend on EUF as well as arithmetic. The arithmetic relaxation therefore
only produces a **hint** for the optimum, which may over-estimate it and
be unachievable.

Two combined defects:

- `opt_solver::maximize_objective` committed the hint into
`m_objective_values` **before** validating it with `check_bound`, and
never rolled it back when validation failed. `update_objective` only
ever *raises* the stored value, so the real (achievable) model value was
discarded.
- `optsmt::geometric_lex` **ignored** the boolean return value and
asserted the blocker derived from the unachievable hint, so the very
next `check_sat` was UNSAT and the search terminated prematurely,
reporting the bogus bound together with a non-matching model.

## Fix

- `opt_solver.cpp`: do not commit the hint before it is validated. On
validation failure, `update_objective` now records the actual achievable
model value. The no-model early-return keeps its previous behavior.
- `optsmt.cpp`: `geometric_lex` now honors the validation result. When
the hint could not be validated, it discards the poisoned blocker and
tightens from the real model value, so the search keeps converging
toward the true optimum. When the hint is valid, the condition reduces
to the original expression and behavior is unchanged.

After the fix the same reproducer produces consistent,
monotonically-improving bounds (325 → 85 → … → 58 → … → 55), and the
reported objective always matches the returned model.

## Testing

Exact-optimum, fast-terminating checks (all correct): EUF-forced minimum
(= 5), `distinct(x, 0..32)` minimize (= 33), Golomb n=8 (= 34), plus
basic min/max, real objective, box, lex, pareto, and weighted
soft/maxsat.

Regression suites, rebuilt in **both Release and Debug**:

| Suite | Release | Debug |
|-------|---------|-------|
| `test-z3 /a` | 92 passed, 0 failed | 92 passed, 0 failed |
| z3test `regressions/smt2` (908 files, `model_validate=true`) | 0
failures | 0 failures |

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

src/opt/optsmt.cpp

@@ -233,7 +233,7 @@ namespace opt {
                   if (is_sat == l_true) m_s->display(tout);
                   );
             if (is_sat == l_true) {                
-                m_s->maximize_objective(obj_index, bound);
+                bool bound_valid = m_s->maximize_objective(obj_index, bound);
                 m_s->get_model(m_model);
                 SASSERT(m_model);
                 inf_eps obj = m_s->saved_objective_value(obj_index);
@@ -250,7 +250,14 @@ namespace opt {
                 else {
                     ++steps;
                 }
-                if (delta_per_step > rational::one() || (obj == last_objective && is_int)) {
+                // When maximize_objective could not validate its arithmetic
+                // hint (bound_valid == false), the blocker it produced refers to
+                // that unachievable hint and must not be used.  'obj' now holds
+                // 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)) {
                     m_s->push();
                     ++num_scopes;
                     bound = m_s->mk_ge(obj_index, obj + inf_eps(delta_per_step));