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

src/opt/opt_solver.cpp

@@ -319,12 +319,28 @@ namespace opt {
             m_models.set(i, m_last_model.get());
 
         TRACE(opt, tout << "maximize " << i << " " << val << " " << m_objective_values[i] << " " << blocker << "\n";);
-        if (val > m_objective_values[i]) {
-            m_objective_values[i] = val;
-        }
+        //
+        // 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
+        // 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().
+        //
 
-        if (!m_last_model)
+        if (!m_last_model) {
+            // Without a model there is nothing to validate 'val' against; keep
+            // the previous behavior of adopting the (possibly infinite) hint.
+            if (val > m_objective_values[i])
+                m_objective_values[i] = val;
             return true;
+        }
 
         //
         // retrieve value of objective from current model and update 

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