smt_solver: correct models on six hard files crash the validator and score the whole submission 0 #42

Task

smt_solver

Claim

On the current smt_solver judge with an 8 MiB stack, correct sat answers on at least six hard QF_UFLRA files crash the witness validator, and the judge reports a valid 0 for the whole submission.

evaluate.py raises the recursion limit to 20000 and validates in a pool worker on the default stack. On these files the recursion overflows the C stack before reaching the limit. The worker dies with SIGSEGV, the pool raises BrokenProcessPool, evaluate.py exits 1 without writing a score, and parse_result.py turns the missing file into valid: true, score 0.

Impact

A solver that returns a model on any of these files (7cf7d9bc1df9f7f0, 85b67deb9ba8a2ab, 8e72757e0b560007, bc8b317ecdcf7301, e4bf0f1de993c180, 3e0629390fbba04a). The sixth crashed when we ran the solver on it alone (14.0 s, n=1); in a full grade at 7 GiB the solver didn't return a model for it, so the tables below cover the first five. The one we hold scores 0.00, correct=0/0, and 47.34 (correct=336/774, same worker) once validation can finish. It answers these files in 0.63-9.56 s, well inside the 60 s limit.

That solver is a C++ program Claude Opus 5.5 wrote in one of our agent runs, unchanged (archive sha256 3c131e4eb2f54e2433e8a1de5ca96beb2ac74c7328cb8df8bea4656de1cb100e, at https://github.com/findalexli/EdgeBench/tree/7f9709bfb8767156ca0ef8990a490ca587c97604). It was submitted three times in that run and none of those grades finished: the logs stop at "Running eval script...", and we did not establish why, so this crash has no report from the original run. The 49 finished reports from those runs, all correct=0/774, are earlier submissions whose solve only prints unknown.

A solver that times out on these files, or answers unknown, isn't affected. Upstream's historical scores on this judge are nonzero, so those solvers don't reach the crash. We can't say how many leaderboard entries do; you hold the archives.

Evidence and how to reproduce

A small submission reproduces it without a real solver. solve answers unknown on every file except 8e72757e0b560007, recognised by the hash of its perturbed input, where it prints the correct model our solver gave. It is a test fixture, not a solver, and it discloses one model for one hidden file.

mkdir -p repro/src && cd repro
printf '#!/bin/sh\nexit 0\n' > build.sh
cat > solve <<'REPRO_EOF'
#!/bin/sh
if [ "$(sha256sum "$1" | cut -d' ' -f1)" = 188810ef857f4784df60497fbb5fdf6138294a6f00a4809c81b041fba1769020 ]; then cat "$(dirname "$0")/src/model.txt"; else echo unknown; fi
REPRO_EOF
cat > src/model.txt <<'REPRO_EOF'
sat
{"values":{"|calculate_output3::__retval__@2|":"(- (/ 7 6))","|calculate_output3::__retval__@1|":"(- (/ 7 6))","a12@1":"4","|calculate_output7::input@3|":"3","a15@1":"1","|calculate_output4::input@1|":"(/ 31 6)","a12@2":"2","|calculate_output6::input@1|":"(/ 5 6)","|calculate_output6::input@2|":"(/ 5 6)","|calculate_output8::__retval__@2|":"(- (/ 13 6))","|calculate_output4::input@2|":"(/ 31 6)","|calculate_output5::__retval__@2|":"(- (/ 7 6))","|calculate_output5::input@2|":"(/ 37 6)","a16@1":"1","|main::input@7|":"3","a25@1":"(/ 7 6)","|calculate_output::__tool_marker_TMP_0@1|":"0","|calculate_output7::input@2|":"0","|main::input@4|":"6","|calculate_output5::input@1|":"(/ 37 6)","|__ADDRESS_OF_main::input|":"0","|calculate_output8::input@1|":"(- (/ 1 6))","|calculate_output2::input@3|":"3","|main::input@3|":"(/ 37 6)","|calculate_output3::__tool_marker_TMP_0@1|":"(- (/ 4 3))","|calculate_output7::input@1|":"0","|calculate_output4::__retval__@1|":"(- (/ 7 6))","|calculate_output3::input@3|":"3","|calculate_output6::__tool_marker_TMP_0@1|":"0","|calculate_output8::input@3|":"3","a20@1":"6","|calculate_output4::__tool_marker_TMP_0@1|":"(- (/ 4 3))","|calculate_output5::__tool_marker_TMP_0@1|":"(- (/ 4 3))","|calculate_output3::input@2|":"(/ 16 3)","|calculate_output2::__retval__@2|":"(- (/ 7 6))","|calculate_output3::input@1|":"(/ 16 3)","|calculate_output2::input@1|":"(/ 37 6)","|calculate_output8::input@2|":"(- (/ 1 6))","|calculate_output5::__retval__@1|":"(- (/ 7 6))","a20@2":"5","|calculate_output8::__retval__@1|":"(- (/ 13 6))","|calculate_output4::input@3|":"3","a27@1":"1","|calculate_output2::input@2|":"(/ 37 6)","|calculate_output4::__retval__@2|":"(- (/ 7 6))","|calculate_output::__retval__@2|":"(- 1)","a9@2":"16","|calculate_output7::__retval__@1|":"(- (/ 7 6))","a15@2":"1","a2@2":"9","|calculate_output6::__retval__@1|":"(- (/ 7 6))","|calculate_output7::__retval__@2|":"(- (/ 7 6))","a2@1":"11","|calculate_output6::input@3|":"3","|calculate_output::input@3|":"3","|calculate_output5::input@3|":"3","a9@1":"16","|calculate_output2::__retval__@1|":"(- (/ 7 6))","|main::input@6|":"3","|calculate_output6::__retval__@2|":"(- (/ 7 6))","|calculate_output::input@2|":"6","|calculate_output2::__tool_marker_TMP_0@1|":"0","|calculate_output7::__tool_marker_TMP_0@1|":"(- (/ 4 3))","a25@2":"1","__sebench_8119ec9bb4d5_b0":"false","__sebench_8119ec9bb4d5_b1":"false","__sebench_8119ec9bb4d5_b2":"false","__sebench_8119ec9bb4d5_b3":"false","__sebench_8119ec9bb4d5_b4":"false","__sebench_8119ec9bb4d5_x0":"0","(__BASE_ADDRESS_OF__ _68)":"0"}}
REPRO_EOF
chmod +x build.sh solve
tar czf ../stub.tar.gz build.sh solve src
cd ..
python -m sforge build --task smt_solver
python -m sforge eval --task smt_solver --archive stub.tar.gz --judge-cpu-limit 8 --judge-mem-limit 7g --json

Expected, grading in about 10 s (n=2 per judge, reversing order, and once more with these exact commands, 6-7 s): community at f92857a gives valid: true, score_0_100: 0, correct=0/0, with BrokenProcessPool in the run's judge_output.txt. The branch in the PR gives valid: true, 0.11, correct=1/774. Check ulimit -s inside the judge container first, see below.

The answers are correct, not just harmless. We captured the solver's perturbed input and witness on each file once and replayed the identical pairs:

z3 agrees independently: each input plus its witness's values is sat, 5 of 5. Validating one of these files takes 3-321 s and up to 1427 MiB peak RSS.

The crash depends on the stack limit. Every crash above is at ulimit -s 8192, and sforge and tools/judge_local.py set no stack limit, so a judge container inherits the Docker daemon's. Running the current judge's run.sh on the fixture with ulimit -s 1048576 or unlimited doesn't crash: it gives correct=0/774 (n=1 each), because the model is then rejected with RecursionError. So on such a host the run isn't lost, but the correct answers still lose credit. We didn't run the real solver that way; with a separate diagnostic, the old validator in a 1 GiB thread at limit 20000, it scored 47.04 and 46.17, with 4-5 invalid models in QF_UFLRA. CPUs and memory made no difference to the crash in what we tested.

Proposed fix

Validate in a thread with a 2 GiB stack and a recursion limit of 1,000,000 (#43), and report an evaluator crash as invalid instead of a valid 0 (#45).

Limits

Measured on 8-vCPU, 8 GiB workers at 8 CPUs and 7 GiB, because the official 16 CPUs and 16 GiB don't fit, so the score on a full run may differ at official resources; many cases sit near the 60 s limit. We hold one such solver.