[zayenz]

Problem

photo -restart constant -restart-scale 5 -nogoods true -seed 4 -time 5000 1 segfaults (exit 139) in Space::_clone, which BAB calls from inside RBS::next. It reproduces on 6.5.0 and on the Gecode 7 line. On Linux, unfixed main crashed in 19 of 32 runs across seeds 1–8, restart scales 1, 5 and 8, and -threads 2. Without -nogoods it does not crash.

Root cause

gecode/search/relax.hh is shared by the Int, Bool, Set and Float relax functions. When posting a kept solution value fails, it called home.failed(), which only asks whether the space has failed. It should call home.fail(), so the space stayed unfailed.

IntVarImp::eq_full assigns the variable before it detects that the value lies in a hole. It then returns fail(home) without notifying any propagators, relying on the caller to fail the space. The variable was therefore left assigned while its propagators were never told. Search then continued on that inconsistent space. With no-goods, the no-goods propagator cancelled subscriptions against it, and VarImp::remove ran past the end of the subscription array, which is not bounds-checked outside audit builds. The corrupted memory crashed later in Space::_clone.

No-goods make the crash common: they prune the persistent space, so the LNS relaxation often tries to keep a value that is no longer in the domain.

Fix

Call home.fail(). Every caller of relax already handles a failed space; in RBS, a failed spoke leads to the next restart. The fix changes no API and prunes nothing extra.

Test

Search::Relax::Failed relaxes two variables with domain {0,2} against the solution value 1, with probability 0 so that one value is kept, and checks that the space ends up failed. It fails without the fix and passes with it.

Validation

Configuration	Result
macOS Release, -tag standard -test Search::	796/796
macOS Release, -tag standard -test NoGoods::	160/160
Linux GCC Release, check	536/536
Linux GCC Release, -tag standard -test Search:: / NoGoods::	796/796, 160/160
Linux Clang ASan+UBSan, Search::Relax, Search::RBS, -tag check NoGoods::	37/37, 96/96
photo sweep with -nogoods true, unfixed main (GCC)	19/32 segfaults
photo sweep with -nogoods true, fixed (GCC, and ASan+UBSan)	0/32, 0/32

uv run misc/tidy.py --check passes.

Related, not fixed here

• Space::master posts restart no-goods even when slave() returned false. No-goods recorded in a restricted (LNS) spoke are then posted into the master, which can turn a non-optimal solution into a false optimality proof.
• DFS and BAB check the stop object before exhaustion, so RBS with no-goods on an unsatisfiable model does not terminate for some cutoffs.