CP-SAT certifies a wrong optimality proof on an all-linear model: adding one constraint lowers the certified optimum by 34% (9.15)

**What version of OR-Tools and what language are you using?**

- OR-Tools: **9.15.6755** (`Google.OrTools` NuGet package)
- Language: C# / .NET 10
- OS: Windows 11 x64 (10.0.26200)

**Which solver are you using?**

CP-SAT

**What did you do?**

Solved an exported `CpModelProto` (90'770 variables, 86'541 constraints — **every one of them linear**) three ways with the same library and **default parameters**:

| Run | Extra constraint | Status | Objective | Best bound | Wall |
|---|---|---|---|---|---|
| A | none | OPTIMAL | 9'086'429 | 9'086'429 | 19.8 s |
| B | `supply_dim_3_8 == 1` (one linear row) | OPTIMAL | **6'012'953** | 6'012'953 | 1.9 s |
| C | `supply_dim_3_8 == 0` | OPTIMAL | 9'086'429 | 9'086'429 | 17.4 s |

`supply_dim_3_8` is an ordinary Boolean (domain `[0,1]`, index 843). Runs B and C partition run A's feasible set, so A's optimum must be min(B, C) = 6'012'953 — yet A certifies 9'086'429 with a matching best bound (an optimality proof, not a gap-limit stop). **The three certificates are mutually inconsistent by case analysis on a single Boolean, so at least one is wrong regardless of any external checking.**

The contradiction also reproduces with `num_search_workers:1, random_seed:1` (deterministic, single-threaded: run A returns the same OPTIMAL 9'086'429 in 21.5 s) and with `num_search_workers:8`.

Self-contained repro (proto + ~60-line runner + the three solver logs): **https://github.com/jipjan/cpsat-915-wrong-optimal**

```bash
git clone https://github.com/jipjan/cpsat-915-wrong-optimal && cd cpsat-915-wrong-optimal
unzip model.pb.zip
dotnet run -c Release -- model.pb solve default # -> OPTIMAL 9086429
dotnet run -c Release -- model.pb solve default supply_dim_3_8 1 # -> OPTIMAL 6012953
dotnet run -c Release -- model.pb solve default supply_dim_3_8 0 # -> OPTIMAL 9086429
```

The pin is added to the proto as a plain linear row before model construction — no assumptions, no hints.

**Independent verification (no solver in the loop)**

After each solve the runner verifies the returned solution against the **original, unpinned** file by plain `Int128` arithmetic — every linear row evaluated directly (enforcement literals honoured, including negative literals; unenforced rows vacuously satisfied), every variable checked against its domain, the objective recomputed from `Objective.Vars`/`Coeffs`. Run B's solution passes: 45'475 enforced rows checked, **0 violations**, all domains respected, objective recomputed = 6'012'953 exactly. So the point run B returns is feasible in the file run A was solved on and is cheaper than run A's certified optimum — run A's OPTIMAL is a false certificate.

**Model characteristics**

- All 86'541 constraints are `linear`; 41'106 rows carry enforcement literals.
- Objective: a single term, `scaling_factor = 1`, no `domain`, no offset, no `floating_point_objective`.
- No `solution_hint`, no `search_strategy`, no `assumptions`, no `symmetry` in the proto.
- The model is accepted by CP-SAT's model validation (no MODEL_INVALID).
- max |linear coefficient| ≈ 1.8e15; max |variable bound| = 1e10; per-row activity within int64.

The model is machine-generated (an air-handling-unit configuration MILP; the integer coefficients are scaled decimal cost data, which is where the large-coefficient / fine-granularity mix comes from). A CBC solve of the same underlying model and an independent brute-force enumerator both agree the true optimum is the 6'012'953 point.

**What did you expect to see?**

Adding a constraint can never improve the optimum: run A ≤ min(run B, run C). Expected OPTIMAL 6'012'953 for run A.

**What did you see instead?**

OPTIMAL 9'086'429 with best bound 9'086'429 — a certified optimality proof 51% above a solution the same solver finds (in 1.9 s) as soon as one Boolean is fixed to the value it takes in the true optimum.

**Anything else we should know?**

- Full `log_search_progress:true` logs for all three runs are in the repro repository (default parameters plus logging only). Solution fingerprints: A `0xef05b681612e39ba`, B `0xf0ef5aa7e5a15806`, C `0x43ce7204306f86a7`.
- Possibly related past reports: #3639 (non-optimal solutions returned with status OPTIMAL), #3620 and #4839 (feasible models reported infeasible). We also observed the false-infeasible direction on a variant of this model (the same formulation with indicator slack rows closed).
- Happy to re-run against current `main` or any candidate fix.