CP-SAT: SIGSEGV in CompiledCircuitConstraint::UpdateGraph when a circuit's enforcement_literal is false

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

Reproduced on three builds, all Linux x86_64 / CPython 3.13, `num_search_workers=32`:

| build | SIGSEGV |
|---|---|
| **`main` @ `98c165af62df62b3056c2ee0fca66b24e79097cb`**, built from source today | **23 / 24** |
| self-built from `271bbaebb9962ad2608a512c2690af7494a8aad6` (2026-08-07) | 24 / 24 |
| **released `9.15.6755` from PyPI** | 7 / 36 |

So it is live on current `main`, and it is in a version you ship. The three functions in the stack
below are byte-identical between `271bbaeb` and `main` — I extracted each function body from
`ortools/sat/constraint_violation.cc` at both refs and compared sha256.

Language: Python.

**Which solver are you using**

CP-SAT.

**What operating system (Linux, Windows, ...) and version?**

Linux x86_64, Ubuntu 22.04 userspace on kernel `5.15.153.1-microsoft-standard-WSL2`, 32 cores,
CPython 3.13.

**What did you do?**

Ran the script at the bottom of this issue, which builds a model containing `circuit` constraints
whose `enforcement_literal` is **false** in the local-search solution:

```
python3 repro.py 24 32
```

Each attempt is a fresh child process, because the fault kills the interpreter rather than raising.
The model is ~40 lines of `CpModel` API calls:

* one plain `circuit` over 8 nodes, which exists only to give the FeasibilityJump general phase
something to iterate on;
* 40 four-node `circuit` constraints, each with its own enforcement literal `e_k`;
* `x_k <= 5 * e_k` for each, plus a shared cap `sum(x_k) <= 5`. The cap is what keeps the `e_k`
alive through presolve: with it, whether any one `e_k` pays for itself depends on the others, so
none is dominated in either direction. Each `e_k` has a positive objective coefficient, which is
what makes `ResetCurrentSolution()` start it at `Min()`, i.e. 0;
* one linear constraint coupling the 40 circuits' arc literals to the plain circuit's, so an arc
literal of an unenforced circuit is moved 0 → 1 during the **general** phase —
`DoSomeGeneralIterations()` only runs once `DoSomeLinearIterations()` returns true.

All default parameters other than `num_search_workers`. Presolve is on.

**What did you expect to see**

`solve()` returning a status.

**What did you see instead?**

SIGSEGV in one of CP-SAT's own worker threads:

```
CompiledCircuitConstraint::UpdateGraph(int, long) <- SIGSEGV
CompiledCircuitConstraint::PerformMove(int, long, Span)
LsEvaluator::UpdateNonLinearViolations(int, long, Span)
FeasibilityJumpSolver::DoSomeGeneralIterations()
operations_research::ThreadPool::RunWorker()
```

`si_code = SEGV_MAPERR`, `si_addr = 0x4`, identical in all 21 dumps we captured on our own model.
The kernel record gives the faulting instruction and registers:

```
segfault at 4 ip 00007f08fa8bd80c sp 00007f08737fd900 error 4
Code: … 45 84 e4 75 11 48 8b 8d f0 00 00 00 <8b> 3c 91 39 3c 81 41 0f 95 c4 …
RAX: 0000000000000000 RCX: 0000000000000000 RDX: 0000000000000001
```

`8b 3c 91` is `mov edi,[rcx+rdx*4]` with `rcx = 0`, `rdx = 1`; the instruction before it
(`48 8b 8d f0 00 00 00`) loads that `rcx` from a member at offset `0xf0`, and `45 84 e4 / 75 11`
(`test r12b,r12b; jne`) ahead of it is the `needs_update ||` short-circuit. So the read is
`committed_sccs_.root[1]` on a `std::vector` whose `data()` is still null, and the `39 3c 81`
that follows is the `root[head]` half of the same comparison with `head = 0`.

The `main` build and released 9.15 fault at the identical instruction — same `45 84 e4 / 75 11`
short-circuit, same `mov rcx,[rbp+0xf8]` (the member offset shifts by 8 between builds), same
faulting load with `rcx = 0` — at `si_addr = 0x8` rather than `0x4`, i.e. `root[2]` instead of
`root[1]`. Same site, different `tail`.

**Mechanism** (`ortools/sat/constraint_violation.cc`)

1. `CompiledCircuitConstraint::committed_sccs_.root` is sized only by `SccOutput::reset()`, which
runs inside `ViolationForCurrentGraph()`.
2. `CompiledConstraintWithProto::ComputeViolation()` returns 0 *without* calling
`ComputeViolationWhenEnforced()` when an enforcement literal is false. So after
`LsEvaluator::ComputeAllNonLinearViolations()`, a circuit whose enforcement literal is false
still has an empty `committed_sccs_.root`.
3. `CompiledCircuitConstraint::PerformMove()` overrides the base class and calls `UpdateGraph()`
unconditionally. It never consults `enforcement_literal()` — unlike
`CompiledConstraintWithProto::ViolationDelta()`, which returns 0 early with the comment *"If an
enforcement literal stays false, the violation stays 0."*
4. `LsEvaluator::UpdateNonLinearViolations()` calls `PerformMove()` for every general constraint
containing the moved variable, enforced or not. So the first general-phase move that **enables**
an arc literal of an unenforced circuit reaches `UpdateGraph()`'s second loop and evaluates
`committed_sccs_.root[tail] != committed_sccs_.root[head]` on that empty vector.

Because of the `needs_update ||` short-circuit, the crash also needs the *disabled* arc list for
that literal to be empty or all self-arcs, which is the ordinary case when arcs carry positive
literals.

There is a second consequence of the same missing check with no crash attached: `PerformMove()`
assigns `violation_ = ViolationForCurrentGraph()` for a constraint that is **not** enforced — whose
violation should be 0 — and computes it over a `graph_` that `InitGraph()` never filled.

**Anything else we should know about your project / environment**

_(Body edited after filing: the worker-count table now shows all three outcomes, and the script
is refreshed — it now exits nonzero on `MODEL_INVALID` and bounds each child, so an incompatible
build cannot look like a clean no-crash run. The model itself is unchanged. The comments below
are the record of what changed and why.)_

Frequency rises with the worker count, which is what decides how many local-search subsolvers run.
On the script below, worker count varied and nothing else:

| `num_search_workers` | SIGSEGV | SIGABRT (the `next_[node]` CHECK below) | clean |
|---|---|---|---|
| 32 | 24 | 0 | 0 |
| 16 | 0 | 8 | 4 |
| 8 | 0 | 4 | 6 |

Read those as three outcomes, not two. An earlier version of this table gave only the SIGSEGV
column, which makes the lower rows look like "ran sixteen times, did not crash" — in fact most of
those processes died on the second fault below, having never reached the local-search code. A worker
count where that abort dominates is not one where this fault is absent, and nothing here separates
them.

Both local-search families reach it, since `DoSomeGeneralIterations()` backs the `fj` first-solution
subsolvers and the `ls` interleaved ones alike, so one knob is not enough on this model:

| parameters (32 workers) | SIGSEGV |
|---|---|
| default | 24 / 24 |
| `num_violation_ls = 0` | 8 / 8 |
| `use_feasibility_jump = false` | 4 / 8 |
| `use_feasibility_jump = false` **and** `num_violation_ls = 0` | 0 / 8 |

We first hit this on a real 607-variable / 906-constraint scheduling model, where the rate at
`num_search_workers = 16` was 8/52 and at 32 was 21/24, and where `use_feasibility_jump = false`
alone *was* enough (0/16 at 16 workers, 0/12 at 32) — a property of that model rather than of the
knob. I can supply that model as a `CpModelProto` if it is useful, though the script above should
make it unnecessary.

Two fixes suggest themselves, neither tried against a build: give `SccOutput` a constructor-time
`reset(graph_.size())` so the read is in bounds whatever the enforcement state, or make
`CompiledCircuitConstraint::PerformMove()` honour `enforcement_literal` the way `ViolationDelta()`
already does. The second also fixes the wrong-`violation_` half.

**A second, probably unrelated fault on the same model.** With both local-search families off, 4 of
16 runs abort instead:

```
Check failed: next_[node] == -1 (1 vs. -1)
```

That is `CHECK_EQ(next_[node], -1)` in `CircuitPropagator::Propagate`, `ortools/sat/circuit.cc:378`,
whose own comment says *"This shouldn't happen because `ExactlyOnePerRowAndPerColumn()` should have
executed first"*. Different subsystem, different signal; reproduce it by adding `--no-ls` to the
script. Say the word and I will split it into its own issue.

**The script**

```python
#!/usr/bin/env python3
"""CP-SAT: SIGSEGV in CompiledCircuitConstraint::UpdateGraph on a local-search
worker, when a `circuit` constraint's enforcement literal is false.

python3 repro.py 24 32 # attempts, num_search_workers
python3 repro.py 8 32 --no-ls # control: both LS families off
"""
from __future__ import annotations

import subprocess
import sys

from ortools.sat.python import cp_model

BUSY_NODES = 8 # nodes of the plain circuit that keeps the general phase busy
NUM_VICTIMS = 40 # enforced circuits whose enforcement literal is false
VICTIM_NODES = 4 # nodes per victim circuit
CAP = 5 # shared cap on the rewards the enforcement literals unlock
# The solve below is capped at 10s and a crash arrives in a few seconds, so this
# only bites if a child wedges.
CHILD_TIMEOUT_S = 90

def build_model() -> cp_model.CpModel:
model = cp_model.CpModel()

# A plain circuit, purely to keep the FeasibilityJump general phase busy.
busy_arcs, busy_lits = [], []
for i in range(BUSY_NODES):
for j in range(BUSY_NODES):
if i == j:
continue
lit = model.new_bool_var(f"a_{i}_{j}")
busy_arcs.append((i, j, lit))
busy_lits.append(lit)
model.add_circuit(busy_arcs)

victim_lits, rewards, enforcements = [], [], []
for k in range(NUM_VICTIMS):
enforce = model.new_bool_var(f"e{k}")
arcs, lits = [], []
for i in range(VICTIM_NODES):
# The diagonal is DELIBERATE and load-bearing: unlike the busy
# circuit above, these loops keep the (i, i) self-arcs. Dropping
# them to match that loop removes BOTH crashes -- 0 SIGSEGV and 0
# SIGABRT in 16 runs -- so a tidy-up here silently deletes the
# reproduction rather than simplifying it.
for j in range(VICTIM_NODES):
lit = model.new_bool_var(f"b{k}_{i}_{j}")
arcs.append((i, j, lit))
lits.append(lit)
model.add_circuit(arcs).only_enforce_if(enforce)

reward = model.new_int_var(0, CAP, f"x{k}")
model.add(reward <= CAP * enforce)
victim_lits += lits
rewards.append(reward)
enforcements.append(enforce)

# The shared cap: a second enforced victim buys nothing, so no single
# enforcement literal is dominated either way and presolve fixes none.
model.add(sum(rewards) <= CAP)

# Couple the victims' arc literals to the busy circuit's, so that they are
# moved 0 -> 1 in the general phase rather than the linear one.
model.add(sum(victim_lits) >= sum(busy_lits) - (BUSY_NODES - 2))

model.minimize(900 * sum(enforcements) - 200 * sum(rewards)
+ sum(busy_lits) + sum(victim_lits))
return model

def solve_once(workers: int, *, disable_local_search: bool = False) -> None:
solver = cp_model.CpSolver()
solver.parameters.num_search_workers = workers
solver.parameters.max_time_in_seconds = 10.0
if disable_local_search:
# Both families, because both run DoSomeGeneralIterations().
solver.parameters.use_feasibility_jump = False
solver.parameters.num_violation_ls = 0
status = solver.solve(build_model())
print(solver.status_name(status))
if status == cp_model.MODEL_INVALID:
# A wheel that cannot express this model returns MODEL_INVALID WITHOUT
# raising, so without this the child exits 0 and the harness counts it
# as a completed no-crash sample -- 30 of them then report that
# google/or-tools#5357 may be fixed, when in fact the model was never
# solved once. Demonstrated on the 9.14 wheel, which rejects circuit
# enforcement literals. Raised by aitkn-code-review-bot (Codex, Grok).
#
# ONLY MODEL_INVALID. Requiring a SOLUTION status would be wrong: the
# 10s cap can legitimately end a no-crash run at UNKNOWN on a slower or
# busier host, and rejecting that would make the control arm fail, and
# make the "N full samples, retire this harness" verdict unreachable on
# exactly the hosts where it matters.
raise SystemExit(f"solver rejected the model: {solver.status_name(status)}")

def main(argv: list[str]) -> int:
# `--no-ls` is the control arm: same model, same worker count, with BOTH
# violation-local-search families off. It says the model itself is solvable
# and the harness works. Turning off only use_feasibility_jump does NOT
# make this model safe -- see the table in the module docstring.
no_ls = "--no-ls" in argv
argv = [a for a in argv if a != "--no-ls"]

if argv[1:2] == ["--child"]:
solve_once(int(argv[2]), disable_local_search=no_ls)
return 0

attempts = int(argv[1]) if len(argv) > 1 else 24
workers = int(argv[2]) if len(argv) > 2 else 32
child = [sys.executable, __file__, "--child", str(workers)]
if no_ls:
child.append("--no-ls")
segv = timeouts = 0
for i in range(1, attempts + 1):
try:
# Bounded because a crashing CP-SAT worker can wedge rather than
# exit: without this the script hangs with no diagnostic, which is
# the worst outcome for someone reproducing the upstream issue.
proc = subprocess.run(child, capture_output=True, text=True,
timeout=CHILD_TIMEOUT_S)
except subprocess.TimeoutExpired:
timeouts += 1
print(f" attempt {i}: TIMED OUT after {CHILD_TIMEOUT_S}s "
f"(wedged child, neither crash nor solve)")
continue
if proc.returncode in (-11, 139): # killed by SIGSEGV
segv += 1
print(f" attempt {i}: SIGSEGV")
else:
tail = (proc.stdout.strip() or proc.stderr.strip()[-200:])
print(f" attempt {i}: exit {proc.returncode} {tail}")
print(f"\n{segv}/{attempts} attempts died with SIGSEGV "
f"at num_search_workers={workers}")
if timeouts:
# Said separately because a wedged child is not a measurement: a run
# that is all timeouts would otherwise read as "0/N SIGSEGV", i.e. as
# evidence of no crash.
print(f"{timeouts}/{attempts} wedged and were killed at "
f"{CHILD_TIMEOUT_S}s -- those attempts measured nothing")
return 0

if __name__ == "__main__":
raise SystemExit(main(sys.argv))
```