CP-SAT: `sufficient_assumptions_for_infeasibility()` returns a literal that is not in the assumption list (presolve only)

**What version of OR-Tools and what language are you using?**
Version: `main` @ commit `79e340fd50e1cae499bd6c9035486cf06c8261a5` (built from source). Also reproduces on stable `v9.15.6755` (PyPI) and `v9.14.6206` (PyPI).
Language: Python

**Which solver are you using (e.g. CP-SAT, Routing Solver, GLOP, BOP, Gurobi)**
CP-SAT

**What operating system (Linux, Windows, ...) and version?**
Linux. Reproduced on Ubuntu 24.04 with the stable PyPI wheel, and inside `python:3.13-bookworm` Docker for the master build.

**What did you do?**

`CpSolver.sufficient_assumptions_for_infeasibility()` is documented to return "a subset of the model assumptions that are sufficient to ensure infeasibility" (an MUS). With the default `cp_model_presolve=True`, it returns a literal index that was never passed to `CpModel.add_assumptions(...)`. Disabling presolve returns a correct subset.

Minimal repro — run this script:

```python
"""Minimal reproducer for an OR-Tools CP-SAT bug:

CpSolver.sufficient_assumptions_for_infeasibility() is documented to return
a subset of the model assumptions. With the default cp_model_presolve=True,
the returned list contains a literal that is NOT in the assumption list.
Disabling presolve returns the correct subset.
"""
from ortools.sat.python import cp_model

def build_model():
"""Tiny model with:
- assumption literal `y` (the only assumption)
- a constraint `y == 0` that makes `y=1` infeasible
- a circuit constraint whose only arc into an otherwise isolated node is
a self-loop gated on NOT(v), which forces v = 0
- v is NEVER added to the assumption list
The correct MUS is [y]; the bug returns [v] when presolve is enabled.
"""
m = cp_model.CpModel()

# v — forced to 0 by the circuit, never assumed.
v = m.new_bool_var("v")
# y — the assumption; `y == 0` makes `y=1` infeasible.
y = m.new_bool_var("y")
m.add(y == 0)

# Two further bools used as circuit-node self-loop literals.
a = m.new_bool_var("a")
b = m.new_bool_var("b")

# Tour over {0, 1, 2} plus an isolated node 99 whose only arc is a
# self-loop gated on NOT(v). The circuit must pick that self-loop, so
# v is forced to 0.
arcs = [
(0, 1, m.new_bool_var("arc_0_1")),
(1, 0, m.new_bool_var("arc_1_0")),
(0, 2, m.new_bool_var("arc_0_2")),
(2, 0, m.new_bool_var("arc_2_0")),
(1, 1, a.Not()), # node 1 self-loop (optional)
(2, 2, b.Not()), # node 2 self-loop (optional)
(99, 99, v.Not()), # forces v = 0
]
m.add_circuit(arcs)
return m, v, y

def solve(model, presolve):
s = cp_model.CpSolver()
s.parameters.cp_model_presolve = presolve
s.parameters.num_workers = 1
status = s.solve(model)
return s.status_name(status), list(s.sufficient_assumptions_for_infeasibility())

model, v, y = build_model()
model.add_assumptions([y])
assumptions = [y.index]

print(f"v.index = {v.index} (NOT in assumptions)")
print(f"y.index = {y.index} (the only assumption)")
print(f"assumptions = {assumptions}")
print()
for presolve in (True, False):
m, v2, y2 = build_model()
m.add_assumptions([y2])
status, core = solve(m, presolve=presolve)
bad = [c for c in core if c != y2.index]
tag = "BUG" if bad else "OK"
print(f"presolve={presolve!s:5} status={status} core={core} "
f"literals_not_in_assumptions={bad} [{tag}]")
```

**What did you expect to see**

Both runs should return `[y.index]` (= `[1]`). The documented contract is that the returned list is a subset of the literals passed to `add_assumptions(...)`.

**What did you see instead?**

```
v.index = 0 (NOT in assumptions)
y.index = 1 (the only assumption)
assumptions = [1]

presolve=True status=INFEASIBLE core=[0] literals_not_in_assumptions=[0] [BUG]
presolve=False status=INFEASIBLE core=[1] literals_not_in_assumptions=[] [OK]
```

With presolve enabled, the core is `[0]` — that is `v`'s literal index, which was never added via `add_assumptions`. With presolve disabled, the core is `[1]` = `y.index`, the correct result.