[zayenz]

The float model in MiniZinc/MiniZincIDE#220 finds its optimum at once and then never proves it. This makes the float improvement cuts in FlatZinc and in MiniModel's FloatMinimizeSpace/FloatMaximizeSpace strict in the objective bound, so the incumbent value is pruned as soon as the cut is posted.

Root cause

The cut obj < best - step was posted as obj <= best - step plus a disequality. NqFloat only fails once the objective is assigned, so the incumbent value stayed inside the objective bounds. Proving optimality then had to split the other float variables down to single ulps before the objective became assigned.

Change

• FlatZinc (FlatZincSpace::constrain): post obj <= pred(lo(best - step)) when minimizing and obj >= succ(hi(best + step)) when maximizing. If that bound is at or beyond the float limits, the space fails. On assigned objectives this admits exactly the solutions the old cut admitted, so step 0 stays exact. The step is also initialized in the default constructor and read before the Gist branch, which used it uninitialized.
• MiniModel (FloatMinimizeSpace::constrain, FloatMaximizeSpace::constrain): the same strict cut on the bound that compare ranks. The difference with the step is now rounded outward, so a positive step no longer admits an improvement slightly smaller than the step. With step 0, assigned costs are accepted exactly as before.
• Changelog entries for both, under 7.0.0.

Testing

• New tests FlatZinc::Float::CutExcludesIncumbent and Float::Basic::OptimizeCut constrain by an incumbent with objective 0.5 in both directions and require the unassigned objective's bound to exclude 0.5. Each fails without its fix.
• The two Review cleanups for main branch #220 models now prove optimality, in 93 and 358 nodes, instead of running indefinitely.
• The float examples that optimize (archimedean-spiral, golden-spiral, descartes-folium) find the same solutions in 3 to 4 percent fewer nodes.
• check passed 536/536, all FlatZinc tests passed (149), and the Float::Rel and Float::Basic selections passed, in a macOS Release build. The changelog tidy check passed.

Not in this PR

Coarse-first float step schedules (optimize with a large relative step, then shrink it) are planned separately, together with portfolio search.