opt: don't stop the search on a stalled delta-rational objective (#10412)

## Problem

`optsmt::geometric_lex` terminates the search when `maximize_objective`
returns the same blocker twice:

```cpp
if (bound == last_bound)
    break;
```

That fixed-point test is unreliable for a **delta-rational optimum** `r
+ k*delta` with `k > 0`. `theory_lra::mk_ge` builds the blocker from the
*rational part and a strictness flag only*:

```cpp
rational r = val.get_rational();
bool is_strict = val.get_infinitesimal().is_pos();
...
b = a.mk_le(mk_obj(v), a.mk_numeral(r, is_int));   // k is discarded
```

So two consecutive stalled rounds at `r + k1*delta` and `r + k2*delta`
produce the *identical* literal, the loop breaks, and the stalled value
is reported as the optimum.

Such a value is not a proven optimum — it only records that the
arithmetic solver could not move off the bound it was just given.

## Symptom

```smt2
(declare-const a Real)
(declare-const b Real)
(assert (xor (= 0.0 b) (> (mod (to_int (- a)) 50) 3)))
(minimize a)
(check-sat)
(get-objectives)
```

`a` is unbounded below — `b = 0` with `a = -50k` satisfies the
constraint for every `k`. But master reports a finite value whenever the
integer cut/cube heuristics run less often than the default period:

```
$ z3 lp.int_hammer_period=64 small.smt2
sat
(objectives
 (a (+ (/ 1.0 4.0) (* (- 1.0) epsilon))))    ; wrong, should be -oo
```

## Change

When the blocker has collapsed and the objective carries a *positive*
infinitesimal, force a strictly larger rational step instead of giving
up. If that step is infeasible the loop still terminates normally
through the `l_false` branch with the best proven bound, so the change
cannot weaken a genuine optimum.

## Validation

- **Unit tests**: 94/94 pass.
- **New regression coverage**: `tst_scaled_min` now also runs at
`lp.int_hammer_period` 16/32/64/128. It **fails on master** (`infinity
coeff: 0` — a finite value for an unbounded objective) and **passes with
this change**.
- **Differential testing** against master on randomly generated
optimization benchmarks (`-T:10`, no crashes anywhere):

  | corpus | files | diffs | crashes |
  |---|---|---|---|
  | linear, `int_hammer_period=4` | 3000 | 0 | 0 |
  | linear, `int_hammer_period=64` | 3000 | 0 | 0 |
  | nonlinear / `mod` / `to_int` / box+lex+pareto | 490 | 5 | 0 |

All 5 differences were checked against an independent satisfiability
oracle, and **master is wrong in every one**:

  | case | master | this PR | oracle |
  |---|---|---|---|
| `maximize (* -5.0 x0)` | `5 + 5ε` | `25` | `= 25` sat, `> 25` unsat →
**25 is optimal** |
| `minimize (+ (* -3.0 x0) (* 3.0 x1))` | `237/5 - ε` | `-oo` | `<
-1000000` sat → **unbounded** |
| `minimize (+ (* -5.0 x2) ...)`, box | `290 - 5ε` | `321/2` | `< 170`
sat → master's value unreachable |
| `minimize (* 5.0 x1)` | `495/4 - 5ε` | `487/4 - 5ε` | `<= 487/4` sat →
strictly better |
| `minimize (+ (* -1.0 x3) (* 4.0 x3) (* 4.0 x2))` | `-4ε` | `-36` | `=
-36` sat, `< -36` unsat → **-36 is optimal** |

Three become exactly optimal and two strictly closer to the true
optimum; no case regressed.

## Note

This addresses the `optsmt` side of the fixed-point test. The underlying
cause — `theory_lra::mk_ge` dropping the infinitesimal coefficient `k`
when building a blocker — is the same root issue that #10269 addresses
in the LRA path, and a complete fix there would make this guard
redundant rather than conflict with it.

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

src/opt/optsmt.cpp

@@ -270,6 +270,22 @@ namespace opt {
                     // to_int, prevent the LP from seeing the full feasible region.
                     if (m_lower[obj_index].is_finite() && m_lower[obj_index] > obj)
                         bound = m_s->mk_ge(obj_index, m_lower[obj_index]);
+                    if (bound == last_bound && obj.get_infinitesimal().is_pos()) {
+                        // The objective sits infinitesimally above the strict
+                        // bound asserted in the previous round: r + k*delta with
+                        // k > 0.  Such a value is not a proven optimum, it only
+                        // says the arithmetic solver could not move off the
+                        // bound it was just given.  Its blocker is built from
+                        // the rational part alone, so it collapses onto the
+                        // previous blocker and the search would stop here and
+                        // report the stalled value as the optimum.  Force a
+                        // strictly larger rational step instead; if the step is
+                        // infeasible the loop terminates through the l_false
+                        // branch below with the best proven bound.
+                        m_s->push();
+                        ++num_scopes;
+                        bound = m_s->mk_ge(obj_index, obj + inf_eps(delta_per_step));
+                    }
                     if (bound == last_bound)
                         break;
                 }

src/test/api.cpp

@@ -10,6 +10,7 @@ Copyright (c) 2015 Microsoft Corporation
 #include "util/util.h"
 #include "util/trace.h"
 #include <map>
+#include <string>
 #include "util/trace.h"
 
 void test_apps() {
@@ -423,8 +424,39 @@ void test_scaled_minimize_unbounded() {
     std::cout << "scaled minimize unbounded test done" << std::endl;
 }
 
+// Sets a global parameter for the duration of the scope and restores the
+// previous value on exit.
+class scoped_global_param {
+    std::string m_id;
+    std::string m_old;
+    bool m_had = false;
+public:
+    scoped_global_param(char const* id, char const* value) : m_id(id) {
+        Z3_string v = nullptr;
+        m_had = Z3_global_param_get(id, &v);
+        if (m_had && v)
+            m_old = v;
+        Z3_global_param_set(id, value);
+    }
+    ~scoped_global_param() {
+        if (m_had)
+            Z3_global_param_set(m_id.c_str(), m_old.c_str());
+    }
+};
+
 void tst_scaled_min() {
     test_scaled_minimize_unbounded();
+
+    // The same objectives must stay unbounded when the integer cut/cube
+    // heuristics run less often.  At these periods the LRA optimizer stalls at
+    // a delta-rational value r + k*delta, whose blocker degenerates to the same
+    // 'objective > r' literal in consecutive rounds; the search used to stop
+    // there and report a finite value for an unbounded objective.
+    for (unsigned period : {16u, 32u, 64u, 128u}) {
+        std::cout << "lp.int_hammer_period=" << period << std::endl;
+        scoped_global_param _period("lp.int_hammer_period", std::to_string(period).c_str());
+        test_scaled_minimize_unbounded();
+    }
 }
 
 void tst_max_rev() {