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

[levnach]

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

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