[findalexli]

Task finding: #42.

What and why

Correct sat models on at least six hard QF_UFLRA files crash the recursive validator at an 8 MiB stack. The pool breaks, no score file is written, and the judge reports a valid 0 for the whole submission. validate_sat_witness now runs in a thread with a 2 GiB stack and a recursion limit of 1,000,000. A thread that can't start, or a validator out of memory, ends the evaluation as a crash does today, because that says nothing about the model. The two evaluate.py changes are identical. Validator logic, cases, formula and scale don't change.

A larger stack alone isn't enough: at the old limit the crash becomes RecursionError, which counts as an invalid model, so correct answers still lose credit (4-5 in QF_UFLRA on a real solver; 0 with the raised limit).

Reporting an evaluator crash as invalid, not a valid 0, is a separate PR, #45.

Limits

• Deeper than the new limit. A correct model past 1,000,000 frames still scores as an invalid model. An iterative validator would remove that; we kept the smaller change, and that choice is yours. A heuristic simulation estimates 1.29-3.82 million frames on five sat files if a model visits every definition; real models on three of them passed, and the solver gave none on the other two. Of 40 synthetic deep formulas across 15 shapes, 34 finished without a crash, mostly rejected at the limit, and six timed out with no verdict, so they don't show that deep correct models pass.
• Memory. A host that can't reserve 2 GiB of address space per validation ends the evaluation even on a shallow file (ulimit -v table at https://github.com/findalexli/EdgeBench/tree/8a4d1576af560cbd4074da3524d8df098dd97752). A deep validation reached 1427 MiB peak RSS on captured witnesses.
• Resources. 8 CPUs and 7 GiB on 8 GiB workers; the official 16 and 16g don't fit, so expect a different full-run number there. We hold one solver that reaches this crash.

How old scores map. For identical solver outputs and a host with the memory above, verdicts are preserved unless the old validator crashed, rejected a model at its recursion limit, or ran out of memory. All 774 inputs, 354 models of the real solver, validated by both on identical witnesses: 322 accepted by both, 28 rejected by both with the same exception types and recorded message prefixes, 4 crash on old and pass on new. Regrade a valid 0 with correct=0/0 from a submission that built and ran. Timed reruns can vary.

Old vs new judge

Old key cd3a5bf1f538, new e70c10c6fb4b, sforge eval, ulimit -s 8192. Failure-path rows: one worker, order swapped, n=2 per judge.

Submission	Old	New
Real solver, full 774 files	0.00, valid, correct=0/0, 1473 s	46.15, correct=328/774, 1861 s
The issue's reproducer	0, valid, correct=0/0	0.11, correct=1/774
Fails to build, or no solve, or rejected by preflight	0, valid, correct=0/0	Same
Always unknown, or wrong models	0, valid, correct=0/774	Same
Replay fixture, correct models on 42 files	6.28, correct=42/774	Same

The real-solver row isn't one same-host pair: a worker's budget fits one pair at best, and these two grades are on different workers. The complete same-host pairs include #45: 0.00 to 47.34 old first has the same validator (its evaluator differs in one exit status), and 0.00 to 46.58 and 46.45 new first are earlier revisions without the MemoryError re-raise. Attempts that didn't finish, all pairs and scripts: https://github.com/findalexli/EdgeBench/tree/8a4d1576af560cbd4074da3524d8df098dd97752. Your archives can settle this if any reach the crash.

Checklist for task changes

• version in task.toml is bumped (any change that can move scores).
• NOTES.md: the change and its score effect are under Changes. No Known issue covered this crash.
• Old vs new judge on the same submissions, with the same-host limit stated above.
• New blobs: none.