From 7709664052d09b6625397cd3aab143781ec056b1 Mon Sep 17 00:00:00 2001
From: findalexli <shengzhi@berkeley.edu>
Date: Tue, 3 Nov 2026 09:05:06 -0800
Subject: [PATCH 1/9] smt_solver: validate deep models on a large stack and
 report evaluator crashes as invalid

---
 edgebench/tasks/smt_solver/NOTES.md           | 18 +++++++++++++
 .../environment/workspace/scripts/evaluate.py | 26 +++++++++++++++++--
 .../tasks/smt_solver/judge/parse_result.py    | 11 ++++++--
 edgebench/tasks/smt_solver/judge/run.sh       |  2 +-
 .../judge/smt_judge/scripts/evaluate.py       | 26 +++++++++++++++++--
 edgebench/tasks/smt_solver/task.toml          |  2 +-
 6 files changed, 77 insertions(+), 8 deletions(-)

diff --git a/edgebench/tasks/smt_solver/NOTES.md b/edgebench/tasks/smt_solver/NOTES.md
index 6de487e4..e3de4565 100644
--- a/edgebench/tasks/smt_solver/NOTES.md
+++ b/edgebench/tasks/smt_solver/NOTES.md
@@ -53,6 +53,24 @@ shared host, two runs each. Raw score; 0..100 in brackets.
 Deterministic rows match exactly, including per-logic counts. The timed rows differ by a few cases
 near the 60 s limit; the old-new difference of means is smaller than either side's own spread.
 
+## Changes
+
+### 1.1.0
+
+`validate_sat_witness` walks the formula recursively with a recursion limit of 20000, more than the
+default 8 MiB stack can hold. On deep files a correct `sat` model segfaulted the evaluator's worker,
+the pool broke, no score file was written, and the outer judge reported a valid 0 for the whole
+submission (`correct=0/0`). Validation now runs in a thread with a 2 GiB reserved stack and a
+recursion limit of 1,000,000. A file deeper than that gives a clean rejection of that case. And if
+the evaluator exits with anything but 0 or 2 and no score file, the result is now invalid rather than
+a valid 0. A build failure, a missing `solve` and a preflight rejection stay a valid 0 (the missing
+`solve` exit changes from 1 to 2 to keep that).
+
+The score formula and scale are unchanged. Regrade crashed evaluations (a valid 0 with `correct=0/0`
+from a submission that built and ran) and models rejected because of the old recursion limit. Other
+validation verdicts are unchanged, while timed reruns can vary. A real solver goes from 0.00 to 47.36-48.14 (n=2 per judge) at 8 CPUs and 7 GiB; failure-path controls and a low-scoring
+solver are unchanged. Source, Deviations and Regression summary describe 1.0.0. Issue: https://github.com/ByteDance-Seed/EdgeBench/issues/42
+
 ## Known issues
 
 Kept as in v1, so scores stay comparable. Fixing any of them changes scores and bumps `version`.
diff --git a/edgebench/tasks/smt_solver/environment/workspace/scripts/evaluate.py b/edgebench/tasks/smt_solver/environment/workspace/scripts/evaluate.py
index a43158c8..8d6ab996 100644
--- a/edgebench/tasks/smt_solver/environment/workspace/scripts/evaluate.py
+++ b/edgebench/tasks/smt_solver/environment/workspace/scripts/evaluate.py
@@ -26,11 +26,14 @@
 import subprocess
 import sys
 import tempfile
+import threading
 import time
 from concurrent.futures import ProcessPoolExecutor, as_completed
 from pathlib import Path
 
 sys.setrecursionlimit(max(sys.getrecursionlimit(), 20000))
+VALIDATOR_RECURSION_LIMIT = 1_000_000
+VALIDATOR_STACK_BYTES = 2 * 1024**3  # reserved, not used, until a file nests this deep
 
 LOGICS = ["QF_UF", "QF_LRA", "QF_LIA", "QF_UFLRA"]
 DIFFICULTIES = ["easy", "medium", "hard"]
@@ -644,7 +647,26 @@ def validate(self):
 
 
 def validate_sat_witness(benchmark_path, witness):
-    WitnessChecker(benchmark_path, witness).validate()
+    # Hard files nest deeply enough to overflow the default stack, which kills the pool worker and ends the
+    # whole evaluation, and to pass 20000 recursions. Too deep even for this is a rejected model, not a crash.
+    box = {}
+
+    def run():
+        limit = sys.getrecursionlimit()
+        sys.setrecursionlimit(VALIDATOR_RECURSION_LIMIT)
+        try:
+            WitnessChecker(benchmark_path, witness).validate()
+        except BaseException as exc:
+            box["exc"] = exc
+        finally:
+            sys.setrecursionlimit(limit)
+
+    threading.stack_size(VALIDATOR_STACK_BYTES)
+    thread = threading.Thread(target=run)
+    thread.start()
+    thread.join()
+    if "exc" in box:
+        raise box["exc"]
 
 
 def parse_solver_output(stdout):
@@ -898,7 +920,7 @@ def main():
     solver = os.path.abspath(args.solver)
     if not os.path.isfile(solver) or not os.access(solver, os.X_OK):
         print(f"Error: solver is not executable: {args.solver}", file=sys.stderr)
-        sys.exit(1)
+        sys.exit(2)
     if not os.path.isdir(args.benchmarks):
         print(f"Error: benchmark directory does not exist: {args.benchmarks}", file=sys.stderr)
         sys.exit(1)
diff --git a/edgebench/tasks/smt_solver/judge/parse_result.py b/edgebench/tasks/smt_solver/judge/parse_result.py
index af176e94..a4f10075 100644
--- a/edgebench/tasks/smt_solver/judge/parse_result.py
+++ b/edgebench/tasks/smt_solver/judge/parse_result.py
@@ -1,7 +1,14 @@
-# v1's /tmp/sebench_parse_result.py (heredoc in judge.eval_cmd), verbatim except that the
-# score file path comes from argv[1] instead of the fixed /tmp/smt_hidden_score.json.
+# v1's /tmp/sebench_parse_result.py (heredoc in judge.eval_cmd), except that the score file path comes
+# from argv[1] instead of the fixed /tmp/smt_hidden_score.json, and that an evaluator crash is invalid.
+# argv[2] = evaluate.py's exit status, empty if it did not run. 2 = it rejected the submission.
 import json, pathlib, sys
 p = pathlib.Path(sys.argv[1])
+status = sys.argv[2] if len(sys.argv) > 2 else ''
+if not p.exists() and status not in ('', '0', '2'):
+    print('>>>>> Start Structured Result')
+    print(json.dumps({'valid': False, 'score': None, 'summary': 'evaluator exited with status {} before writing a score file'.format(status), 'details': [], 'metrics': {}}))
+    print('>>>>> End Structured Result')
+    sys.exit(0)
 raw = json.loads(p.read_text()) if p.exists() else {'final_score': 0.0, 'logic_summary': {}}
 raw_score = float(raw.get('final_score', 0.0) or 0.0)
 score = raw_score / 100.0 if raw_score > 1.0 else raw_score
diff --git a/edgebench/tasks/smt_solver/judge/run.sh b/edgebench/tasks/smt_solver/judge/run.sh
index 7daec838..9df734fb 100644
--- a/edgebench/tasks/smt_solver/judge/run.sh
+++ b/edgebench/tasks/smt_solver/judge/run.sh
@@ -17,7 +17,7 @@ LOG=$(mktemp)
 T=$(mktemp -d)
 
 (
-cd /home/workspace/smt_solver && rm -rf benchmarks hidden_benchmarks scripts expected_answers.json selection_manifest.json hidden_score.json public_score.json; chmod +x build.sh solve; build_status=0; ./build.sh >"$T/smt_build.out" 2>"$T/smt_build.err" || build_status=$?; if [ "$build_status" -eq 0 ]; then python3 /home/workspace/smt_judge/scripts/evaluate.py --solver ./solve --benchmarks /home/workspace/smt_judge/hidden_benchmarks --expected /home/workspace/smt_judge/hidden_benchmarks/expected_answers.json --manifest /home/workspace/smt_judge/hidden_benchmarks/selection_manifest.json --timeout 60 --parallel 16 --perturb --perturb-salt hidden-sebench --submission-root /home/workspace/smt_solver --output "$T/smt_hidden_score.json" >"$T/smt_eval.out" 2>"$T/smt_eval.err"; eval_status=$?; else eval_status=$build_status; fi; if [ -f "$T/smt_build.out" ]; then cat "$T/smt_build.out"; fi; if [ -f "$T/smt_build.err" ]; then cat "$T/smt_build.err"; fi; if [ -f "$T/smt_eval.out" ]; then cat "$T/smt_eval.out"; fi; if [ -f "$T/smt_eval.err" ]; then cat "$T/smt_eval.err"; fi; python3 /judge/parse_result.py "$T/smt_hidden_score.json"
+cd /home/workspace/smt_solver && rm -rf benchmarks hidden_benchmarks scripts expected_answers.json selection_manifest.json hidden_score.json public_score.json; chmod +x build.sh solve; build_status=0; ./build.sh >"$T/smt_build.out" 2>"$T/smt_build.err" || build_status=$?; if [ "$build_status" -eq 0 ]; then python3 /home/workspace/smt_judge/scripts/evaluate.py --solver ./solve --benchmarks /home/workspace/smt_judge/hidden_benchmarks --expected /home/workspace/smt_judge/hidden_benchmarks/expected_answers.json --manifest /home/workspace/smt_judge/hidden_benchmarks/selection_manifest.json --timeout 60 --parallel 16 --perturb --perturb-salt hidden-sebench --submission-root /home/workspace/smt_solver --output "$T/smt_hidden_score.json" >"$T/smt_eval.out" 2>"$T/smt_eval.err"; eval_status=$?; evaluator_status=$eval_status; else eval_status=$build_status; evaluator_status=; fi; if [ -f "$T/smt_build.out" ]; then cat "$T/smt_build.out"; fi; if [ -f "$T/smt_build.err" ]; then cat "$T/smt_build.err"; fi; if [ -f "$T/smt_eval.out" ]; then cat "$T/smt_eval.out"; fi; if [ -f "$T/smt_eval.err" ]; then cat "$T/smt_eval.err"; fi; python3 /judge/parse_result.py "$T/smt_hidden_score.json" "$evaluator_status"
 ) > "$LOG" 2>&1
 EXIT_CODE=$?
 cat "$LOG"
diff --git a/edgebench/tasks/smt_solver/judge/smt_judge/scripts/evaluate.py b/edgebench/tasks/smt_solver/judge/smt_judge/scripts/evaluate.py
index a43158c8..8d6ab996 100755
--- a/edgebench/tasks/smt_solver/judge/smt_judge/scripts/evaluate.py
+++ b/edgebench/tasks/smt_solver/judge/smt_judge/scripts/evaluate.py
@@ -26,11 +26,14 @@
 import subprocess
 import sys
 import tempfile
+import threading
 import time
 from concurrent.futures import ProcessPoolExecutor, as_completed
 from pathlib import Path
 
 sys.setrecursionlimit(max(sys.getrecursionlimit(), 20000))
+VALIDATOR_RECURSION_LIMIT = 1_000_000
+VALIDATOR_STACK_BYTES = 2 * 1024**3  # reserved, not used, until a file nests this deep
 
 LOGICS = ["QF_UF", "QF_LRA", "QF_LIA", "QF_UFLRA"]
 DIFFICULTIES = ["easy", "medium", "hard"]
@@ -644,7 +647,26 @@ def validate(self):
 
 
 def validate_sat_witness(benchmark_path, witness):
-    WitnessChecker(benchmark_path, witness).validate()
+    # Hard files nest deeply enough to overflow the default stack, which kills the pool worker and ends the
+    # whole evaluation, and to pass 20000 recursions. Too deep even for this is a rejected model, not a crash.
+    box = {}
+
+    def run():
+        limit = sys.getrecursionlimit()
+        sys.setrecursionlimit(VALIDATOR_RECURSION_LIMIT)
+        try:
+            WitnessChecker(benchmark_path, witness).validate()
+        except BaseException as exc:
+            box["exc"] = exc
+        finally:
+            sys.setrecursionlimit(limit)
+
+    threading.stack_size(VALIDATOR_STACK_BYTES)
+    thread = threading.Thread(target=run)
+    thread.start()
+    thread.join()
+    if "exc" in box:
+        raise box["exc"]
 
 
 def parse_solver_output(stdout):
@@ -898,7 +920,7 @@ def main():
     solver = os.path.abspath(args.solver)
     if not os.path.isfile(solver) or not os.access(solver, os.X_OK):
         print(f"Error: solver is not executable: {args.solver}", file=sys.stderr)
-        sys.exit(1)
+        sys.exit(2)
     if not os.path.isdir(args.benchmarks):
         print(f"Error: benchmark directory does not exist: {args.benchmarks}", file=sys.stderr)
         sys.exit(1)
diff --git a/edgebench/tasks/smt_solver/task.toml b/edgebench/tasks/smt_solver/task.toml
index 4b295bfa..f64c86d2 100644
--- a/edgebench/tasks/smt_solver/task.toml
+++ b/edgebench/tasks/smt_solver/task.toml
@@ -4,7 +4,7 @@ name = "Smt Solver"
 category = "Combinatorial Optimization"
 language = "Python"
 description = "Build an SMT solver from scratch for four quantifier-free theories (uninterpreted functions, linear real and integer arithmetic, and their combination). External SMT solvers are forbidden; model witnesses are independently validated."
-version = "1.0.0"
+version = "1.1.0"
 status = "migrated"
 
 [environment]

From ccc29a88863fe9637b8723f4be92298fccdc2f8d Mon Sep 17 00:00:00 2001
From: findalexli <shengzhi@berkeley.edu>
Date: Tue, 3 Nov 2026 12:24:27 -0800
Subject: [PATCH 2/9] smt_solver: end the evaluation when the validator cannot
 run

---
 .../environment/workspace/scripts/evaluate.py  | 18 ++++++++++++++----
 .../judge/smt_judge/scripts/evaluate.py        | 18 ++++++++++++++----
 2 files changed, 28 insertions(+), 8 deletions(-)

diff --git a/edgebench/tasks/smt_solver/environment/workspace/scripts/evaluate.py b/edgebench/tasks/smt_solver/environment/workspace/scripts/evaluate.py
index 8d6ab996..846e3d8c 100644
--- a/edgebench/tasks/smt_solver/environment/workspace/scripts/evaluate.py
+++ b/edgebench/tasks/smt_solver/environment/workspace/scripts/evaluate.py
@@ -33,7 +33,7 @@
 
 sys.setrecursionlimit(max(sys.getrecursionlimit(), 20000))
 VALIDATOR_RECURSION_LIMIT = 1_000_000
-VALIDATOR_STACK_BYTES = 2 * 1024**3  # reserved, not used, until a file nests this deep
+VALIDATOR_STACK_BYTES = 2 * 1024**3  # address space; pages are committed as the recursion reaches them
 
 LOGICS = ["QF_UF", "QF_LRA", "QF_LIA", "QF_UFLRA"]
 DIFFICULTIES = ["easy", "medium", "hard"]
@@ -646,6 +646,11 @@ def validate(self):
             seen[key] = result
 
 
+class ValidatorFailure(BaseException):
+    """The validator could not run, which says nothing about the model. Not an Exception, so that
+    run_solver_case does not record it as an invalid model: it ends the evaluation without a score."""
+
+
 def validate_sat_witness(benchmark_path, witness):
     # Hard files nest deeply enough to overflow the default stack, which kills the pool worker and ends the
     # whole evaluation, and to pass 20000 recursions. Too deep even for this is a rejected model, not a crash.
@@ -661,10 +666,15 @@ def run():
         finally:
             sys.setrecursionlimit(limit)
 
-    threading.stack_size(VALIDATOR_STACK_BYTES)
-    thread = threading.Thread(target=run)
-    thread.start()
+    try:
+        threading.stack_size(VALIDATOR_STACK_BYTES)
+        thread = threading.Thread(target=run)
+        thread.start()
+    except (RuntimeError, ValueError, MemoryError) as exc:
+        raise ValidatorFailure(f"cannot start the validator thread: {exc}") from exc
     thread.join()
+    if isinstance(box.get("exc"), MemoryError):
+        raise ValidatorFailure("the validator ran out of memory")
     if "exc" in box:
         raise box["exc"]
 
diff --git a/edgebench/tasks/smt_solver/judge/smt_judge/scripts/evaluate.py b/edgebench/tasks/smt_solver/judge/smt_judge/scripts/evaluate.py
index 8d6ab996..846e3d8c 100755
--- a/edgebench/tasks/smt_solver/judge/smt_judge/scripts/evaluate.py
+++ b/edgebench/tasks/smt_solver/judge/smt_judge/scripts/evaluate.py
@@ -33,7 +33,7 @@
 
 sys.setrecursionlimit(max(sys.getrecursionlimit(), 20000))
 VALIDATOR_RECURSION_LIMIT = 1_000_000
-VALIDATOR_STACK_BYTES = 2 * 1024**3  # reserved, not used, until a file nests this deep
+VALIDATOR_STACK_BYTES = 2 * 1024**3  # address space; pages are committed as the recursion reaches them
 
 LOGICS = ["QF_UF", "QF_LRA", "QF_LIA", "QF_UFLRA"]
 DIFFICULTIES = ["easy", "medium", "hard"]
@@ -646,6 +646,11 @@ def validate(self):
             seen[key] = result
 
 
+class ValidatorFailure(BaseException):
+    """The validator could not run, which says nothing about the model. Not an Exception, so that
+    run_solver_case does not record it as an invalid model: it ends the evaluation without a score."""
+
+
 def validate_sat_witness(benchmark_path, witness):
     # Hard files nest deeply enough to overflow the default stack, which kills the pool worker and ends the
     # whole evaluation, and to pass 20000 recursions. Too deep even for this is a rejected model, not a crash.
@@ -661,10 +666,15 @@ def run():
         finally:
             sys.setrecursionlimit(limit)
 
-    threading.stack_size(VALIDATOR_STACK_BYTES)
-    thread = threading.Thread(target=run)
-    thread.start()
+    try:
+        threading.stack_size(VALIDATOR_STACK_BYTES)
+        thread = threading.Thread(target=run)
+        thread.start()
+    except (RuntimeError, ValueError, MemoryError) as exc:
+        raise ValidatorFailure(f"cannot start the validator thread: {exc}") from exc
     thread.join()
+    if isinstance(box.get("exc"), MemoryError):
+        raise ValidatorFailure("the validator ran out of memory")
     if "exc" in box:
         raise box["exc"]
 

From 31893aeafcf0c74b8673e6ecf04131cbcaea04d2 Mon Sep 17 00:00:00 2001
From: findalexli <shengzhi@berkeley.edu>
Date: Tue, 3 Nov 2026 14:43:52 -0800
Subject: [PATCH 3/9] smt_solver: state the final behaviour and results in
 NOTES

---
 edgebench/tasks/smt_solver/NOTES.md | 22 ++++++++++++++--------
 1 file changed, 14 insertions(+), 8 deletions(-)

diff --git a/edgebench/tasks/smt_solver/NOTES.md b/edgebench/tasks/smt_solver/NOTES.md
index e3de4565..efd66992 100644
--- a/edgebench/tasks/smt_solver/NOTES.md
+++ b/edgebench/tasks/smt_solver/NOTES.md
@@ -60,16 +60,22 @@ near the 60 s limit; the old-new difference of means is smaller than either side
 `validate_sat_witness` walks the formula recursively with a recursion limit of 20000, more than the
 default 8 MiB stack can hold. On deep files a correct `sat` model segfaulted the evaluator's worker,
 the pool broke, no score file was written, and the outer judge reported a valid 0 for the whole
-submission (`correct=0/0`). Validation now runs in a thread with a 2 GiB reserved stack and a
-recursion limit of 1,000,000. A file deeper than that gives a clean rejection of that case. And if
-the evaluator exits with anything but 0 or 2 and no score file, the result is now invalid rather than
-a valid 0. A build failure, a missing `solve` and a preflight rejection stay a valid 0 (the missing
-`solve` exit changes from 1 to 2 to keep that).
+submission (`correct=0/0`). Validation now runs in a thread with a 2 GiB stack (address space; pages
+are committed as the recursion reaches them) and a recursion limit of 1,000,000. A formula deeper
+than that was rejected cleanly for the one shape tested. If the validator cannot start its thread or
+runs out of memory, the evaluation now ends instead of rejecting the model. And if the evaluator
+exits with anything but 0 or 2 and no score file, the result is now invalid rather than a valid 0. A
+build failure, a missing `solve` and a preflight rejection stay a valid 0 (the missing `solve` exit
+changes from 1 to 2 to keep that). A pool worker killed for memory still ends the evaluation, which
+is now invalid.
 
 The score formula and scale are unchanged. Regrade crashed evaluations (a valid 0 with `correct=0/0`
-from a submission that built and ran) and models rejected because of the old recursion limit. Other
-validation verdicts are unchanged, while timed reruns can vary. A real solver goes from 0.00 to 47.36-48.14 (n=2 per judge) at 8 CPUs and 7 GiB; failure-path controls and a low-scoring
-solver are unchanged. Source, Deviations and Regression summary describe 1.0.0. Issue: https://github.com/ByteDance-Seed/EdgeBench/issues/42
+from a submission that built and ran) and models rejected because of the old recursion limit or
+because the validator ran out of memory. Other validation verdicts are unchanged, while timed reruns
+can vary. With a 1 GiB or unlimited stack the old judge does not crash and rejects these models
+instead. On the same worker at 8 CPUs and 7 GiB, a real solver goes from 0.00 to 46.58; failure-path
+controls and a replay fixture with correct models on 42 files are unchanged. Source, Deviations and
+Regression summary describe 1.0.0. Issue: https://github.com/ByteDance-Seed/EdgeBench/issues/42
 
 ## Known issues
 

From 00a5aa61dc6018f0bc9f6cd442fb9ad8bb471d29 Mon Sep 17 00:00:00 2001
From: findalexli <shengzhi@berkeley.edu>
Date: Tue, 3 Nov 2026 14:50:10 -0800
Subject: [PATCH 4/9] smt_solver: qualify verdict preservation in NOTES

---
 edgebench/tasks/smt_solver/NOTES.md | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/edgebench/tasks/smt_solver/NOTES.md b/edgebench/tasks/smt_solver/NOTES.md
index efd66992..235011df 100644
--- a/edgebench/tasks/smt_solver/NOTES.md
+++ b/edgebench/tasks/smt_solver/NOTES.md
@@ -71,15 +71,15 @@ is now invalid.
 
 The score formula and scale are unchanged. Regrade crashed evaluations (a valid 0 with `correct=0/0`
 from a submission that built and ran) and models rejected because of the old recursion limit or
-because the validator ran out of memory. Other validation verdicts are unchanged, while timed reruns
-can vary. With a 1 GiB or unlimited stack the old judge does not crash and rejects these models
-instead. On the same worker at 8 CPUs and 7 GiB, a real solver goes from 0.00 to 46.58; failure-path
+because the validator ran out of memory. Other validation verdicts are unchanged, provided the host can reserve 2 GiB of address space per
+validation, while timed reruns can vary. With a 1 GiB or unlimited stack the old judge did not crash
+on the one model tested and rejected it instead. On the same worker at 8 CPUs and 7 GiB, a real solver goes from 0.00 to 46.58; failure-path
 controls and a replay fixture with correct models on 42 files are unchanged. Source, Deviations and
 Regression summary describe 1.0.0. Issue: https://github.com/ByteDance-Seed/EdgeBench/issues/42
 
 ## Known issues
 
-Kept as in v1, so scores stay comparable. Fixing any of them changes scores and bumps `version`.
+Kept as in v1. Fixing any of them changes scores and bumps `version`.
 
 1. **The submission can forge its score file.** The score is read from a file the submitted
    `build.sh` (running as root) can write before the evaluator does, and an early evaluator exit is

From d1fb541b157ac0ba0b2cad5b18d538ee4ddaf2ac Mon Sep 17 00:00:00 2001
From: findalexli <shengzhi@berkeley.edu>
Date: Tue, 3 Nov 2026 15:46:12 -0800
Subject: [PATCH 5/9] smt_solver: record both same-worker pairs in NOTES

---
 edgebench/tasks/smt_solver/NOTES.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/edgebench/tasks/smt_solver/NOTES.md b/edgebench/tasks/smt_solver/NOTES.md
index 235011df..950230d2 100644
--- a/edgebench/tasks/smt_solver/NOTES.md
+++ b/edgebench/tasks/smt_solver/NOTES.md
@@ -73,7 +73,7 @@ The score formula and scale are unchanged. Regrade crashed evaluations (a valid
 from a submission that built and ran) and models rejected because of the old recursion limit or
 because the validator ran out of memory. Other validation verdicts are unchanged, provided the host can reserve 2 GiB of address space per
 validation, while timed reruns can vary. With a 1 GiB or unlimited stack the old judge did not crash
-on the one model tested and rejected it instead. On the same worker at 8 CPUs and 7 GiB, a real solver goes from 0.00 to 46.58; failure-path
+on the one model tested and rejected it instead. On one worker at a time, at 8 CPUs and 7 GiB, a real solver goes from 0.00 to 46.58 and from 0.00 to 46.45; failure-path
 controls and a replay fixture with correct models on 42 files are unchanged. Source, Deviations and
 Regression summary describe 1.0.0. Issue: https://github.com/ByteDance-Seed/EdgeBench/issues/42
 

From 2058aa8c7bf5e2724a140c7009f9a845025bf5fe Mon Sep 17 00:00:00 2001
From: findalexli <shengzhi@berkeley.edu>
Date: Tue, 3 Nov 2026 18:58:36 -0800
Subject: [PATCH 6/9] smt_solver: NOTES, deep files and preservation results

---
 edgebench/tasks/smt_solver/NOTES.md | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/edgebench/tasks/smt_solver/NOTES.md b/edgebench/tasks/smt_solver/NOTES.md
index 950230d2..627035b5 100644
--- a/edgebench/tasks/smt_solver/NOTES.md
+++ b/edgebench/tasks/smt_solver/NOTES.md
@@ -62,7 +62,8 @@ default 8 MiB stack can hold. On deep files a correct `sat` model segfaulted the
 the pool broke, no score file was written, and the outer judge reported a valid 0 for the whole
 submission (`correct=0/0`). Validation now runs in a thread with a 2 GiB stack (address space; pages
 are committed as the recursion reaches them) and a recursion limit of 1,000,000. A formula deeper
-than that was rejected cleanly for the one shape tested. If the validator cannot start its thread or
+than that is rejected as an invalid model, in every shape tested; five `sat` files could need more if a
+model visits all their definitions, though three real models on them passed. If the validator cannot start its thread or
 runs out of memory, the evaluation now ends instead of rejecting the model. And if the evaluator
 exits with anything but 0 or 2 and no score file, the result is now invalid rather than a valid 0. A
 build failure, a missing `solve` and a preflight rejection stay a valid 0 (the missing `solve` exit
@@ -74,7 +75,9 @@ from a submission that built and ran) and models rejected because of the old rec
 because the validator ran out of memory. Other validation verdicts are unchanged, provided the host can reserve 2 GiB of address space per
 validation, while timed reruns can vary. With a 1 GiB or unlimited stack the old judge did not crash
 on the one model tested and rejected it instead. On one worker at a time, at 8 CPUs and 7 GiB, a real solver goes from 0.00 to 46.58 and from 0.00 to 46.45; failure-path
-controls and a replay fixture with correct models on 42 files are unchanged. Source, Deviations and
+controls and a replay fixture with correct models on 42 files are unchanged. The same solver with the
+crashing files answered `unknown` counts 325/774 correct on both judges (45.84 and 45.58), and of its 367
+models, 362 get identical verdicts and the other 5 are the crashes. Source, Deviations and
 Regression summary describe 1.0.0. Issue: https://github.com/ByteDance-Seed/EdgeBench/issues/42
 
 ## Known issues

From 02823bf29f7481f8c57e42dc199fe4e8dbb3a905 Mon Sep 17 00:00:00 2001
From: findalexli <shengzhi@berkeley.edu>
Date: Tue, 3 Nov 2026 19:33:04 -0800
Subject: [PATCH 7/9] smt_solver: do not swallow MemoryError in numeric parsing

---
 .../tasks/smt_solver/environment/workspace/scripts/evaluate.py  | 2 ++
 edgebench/tasks/smt_solver/judge/smt_judge/scripts/evaluate.py  | 2 ++
 2 files changed, 4 insertions(+)

diff --git a/edgebench/tasks/smt_solver/environment/workspace/scripts/evaluate.py b/edgebench/tasks/smt_solver/environment/workspace/scripts/evaluate.py
index 846e3d8c..91933c3f 100644
--- a/edgebench/tasks/smt_solver/environment/workspace/scripts/evaluate.py
+++ b/edgebench/tasks/smt_solver/environment/workspace/scripts/evaluate.py
@@ -539,6 +539,8 @@ def eval(self, term, env=None):
             try:
                 if self.logic != "QF_UF":
                     return ("num", parse_numeric_literal(term))
+            except MemoryError:
+                raise
             except Exception:
                 pass
             if term in self.decls:
diff --git a/edgebench/tasks/smt_solver/judge/smt_judge/scripts/evaluate.py b/edgebench/tasks/smt_solver/judge/smt_judge/scripts/evaluate.py
index 846e3d8c..91933c3f 100755
--- a/edgebench/tasks/smt_solver/judge/smt_judge/scripts/evaluate.py
+++ b/edgebench/tasks/smt_solver/judge/smt_judge/scripts/evaluate.py
@@ -539,6 +539,8 @@ def eval(self, term, env=None):
             try:
                 if self.logic != "QF_UF":
                     return ("num", parse_numeric_literal(term))
+            except MemoryError:
+                raise
             except Exception:
                 pass
             if term in self.decls:

From 47824b5ef0381ffcd5a5ad61156f34b80713d199 Mon Sep 17 00:00:00 2001
From: findalexli <shengzhi@berkeley.edu>
Date: Tue, 3 Nov 2026 21:18:13 -0800
Subject: [PATCH 8/9] smt_solver: NOTES match the final runs

---
 edgebench/tasks/smt_solver/NOTES.md | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/edgebench/tasks/smt_solver/NOTES.md b/edgebench/tasks/smt_solver/NOTES.md
index 627035b5..bd6481b4 100644
--- a/edgebench/tasks/smt_solver/NOTES.md
+++ b/edgebench/tasks/smt_solver/NOTES.md
@@ -61,9 +61,10 @@ near the 60 s limit; the old-new difference of means is smaller than either side
 default 8 MiB stack can hold. On deep files a correct `sat` model segfaulted the evaluator's worker,
 the pool broke, no score file was written, and the outer judge reported a valid 0 for the whole
 submission (`correct=0/0`). Validation now runs in a thread with a 2 GiB stack (address space; pages
-are committed as the recursion reaches them) and a recursion limit of 1,000,000. A formula deeper
-than that is rejected as an invalid model, in every shape tested; five `sat` files could need more if a
-model visits all their definitions, though three real models on them passed. If the validator cannot start its thread or
+are committed as the recursion reaches them) and a recursion limit of 1,000,000. A correct model that
+goes deeper than that is scored as an invalid model, which is wrong for that file but no longer ends
+the evaluation. By a heuristic estimate five `sat` files could go deeper if a model visits all their
+definitions; three real models on them passed. If the validator cannot start its thread or
 runs out of memory, the evaluation now ends instead of rejecting the model. And if the evaluator
 exits with anything but 0 or 2 and no score file, the result is now invalid rather than a valid 0. A
 build failure, a missing `solve` and a preflight rejection stay a valid 0 (the missing `solve` exit
@@ -74,10 +75,9 @@ The score formula and scale are unchanged. Regrade crashed evaluations (a valid
 from a submission that built and ran) and models rejected because of the old recursion limit or
 because the validator ran out of memory. Other validation verdicts are unchanged, provided the host can reserve 2 GiB of address space per
 validation, while timed reruns can vary. With a 1 GiB or unlimited stack the old judge did not crash
-on the one model tested and rejected it instead. On one worker at a time, at 8 CPUs and 7 GiB, a real solver goes from 0.00 to 46.58 and from 0.00 to 46.45; failure-path
-controls and a replay fixture with correct models on 42 files are unchanged. The same solver with the
-crashing files answered `unknown` counts 325/774 correct on both judges (45.84 and 45.58), and of its 367
-models, 362 get identical verdicts and the other 5 are the crashes. Source, Deviations and
+on the one model tested and rejected it instead. On one worker at a time, at 8 CPUs and 7 GiB, a real solver goes from 0.00 to 47.34; failure-path
+controls and a replay fixture with correct models on 42 files are unchanged. Of that solver's 354
+models, 350 get the same verdict from both validators and the other 4 are the crashes. Source, Deviations and
 Regression summary describe 1.0.0. Issue: https://github.com/ByteDance-Seed/EdgeBench/issues/42
 
 ## Known issues

From 366ee51265db03ee519fcbbbbc4511385ff9358b Mon Sep 17 00:00:00 2001
From: findalexli <shengzhi@berkeley.edu>
Date: Tue, 3 Nov 2026 23:12:51 -0800
Subject: [PATCH 9/9] smt_solver: move the evaluator-status change to its own
 PR

Keeps the validator change here, with shorter NOTES.
---
 edgebench/tasks/smt_solver/NOTES.md           | 38 ++++++++-----------
 .../environment/workspace/scripts/evaluate.py |  2 +-
 .../tasks/smt_solver/judge/parse_result.py    | 11 +-----
 edgebench/tasks/smt_solver/judge/run.sh       |  2 +-
 .../judge/smt_judge/scripts/evaluate.py       |  2 +-
 5 files changed, 20 insertions(+), 35 deletions(-)

diff --git a/edgebench/tasks/smt_solver/NOTES.md b/edgebench/tasks/smt_solver/NOTES.md
index bd6481b4..0c6e2e81 100644
--- a/edgebench/tasks/smt_solver/NOTES.md
+++ b/edgebench/tasks/smt_solver/NOTES.md
@@ -57,32 +57,24 @@ near the 60 s limit; the old-new difference of means is smaller than either side
 
 ### 1.1.0
 
-`validate_sat_witness` walks the formula recursively with a recursion limit of 20000, more than the
-default 8 MiB stack can hold. On deep files a correct `sat` model segfaulted the evaluator's worker,
-the pool broke, no score file was written, and the outer judge reported a valid 0 for the whole
-submission (`correct=0/0`). Validation now runs in a thread with a 2 GiB stack (address space; pages
-are committed as the recursion reaches them) and a recursion limit of 1,000,000. A correct model that
-goes deeper than that is scored as an invalid model, which is wrong for that file but no longer ends
-the evaluation. By a heuristic estimate five `sat` files could go deeper if a model visits all their
-definitions; three real models on them passed. If the validator cannot start its thread or
-runs out of memory, the evaluation now ends instead of rejecting the model. And if the evaluator
-exits with anything but 0 or 2 and no score file, the result is now invalid rather than a valid 0. A
-build failure, a missing `solve` and a preflight rejection stay a valid 0 (the missing `solve` exit
-changes from 1 to 2 to keep that). A pool worker killed for memory still ends the evaluation, which
-is now invalid.
-
-The score formula and scale are unchanged. Regrade crashed evaluations (a valid 0 with `correct=0/0`
-from a submission that built and ran) and models rejected because of the old recursion limit or
-because the validator ran out of memory. Other validation verdicts are unchanged, provided the host can reserve 2 GiB of address space per
-validation, while timed reruns can vary. With a 1 GiB or unlimited stack the old judge did not crash
-on the one model tested and rejected it instead. On one worker at a time, at 8 CPUs and 7 GiB, a real solver goes from 0.00 to 47.34; failure-path
-controls and a replay fixture with correct models on 42 files are unchanged. Of that solver's 354
-models, 350 get the same verdict from both validators and the other 4 are the crashes. Source, Deviations and
-Regression summary describe 1.0.0. Issue: https://github.com/ByteDance-Seed/EdgeBench/issues/42
+`validate_sat_witness` recursed with a limit of 20000, more than the default 8 MiB stack holds. On deep
+files a correct `sat` model segfaulted the pool worker and ended the evaluation with no score file,
+which the judge reported as a valid 0 (`correct=0/0`). Validation now runs in a thread with a 2 GiB
+stack (address space; pages are committed as the recursion reaches them) and a recursion limit of
+1,000,000. A correct model deeper than that scores as an invalid model, but the evaluation continues.
+If the thread cannot start or the validator runs out of memory, the evaluation ends as it did on a
+crash, rather than rejecting the model.
+
+The formula and scale are unchanged. Regrade crashed evaluations (a valid 0 with `correct=0/0` from a
+submission that built and ran), and models rejected at the old recursion limit or because the validator
+ran out of memory. Other verdicts stay, on a host that can reserve 2 GiB of address space per validation. At 8 CPUs and 7 GiB a real solver goes from 0.00 to 46.15; of its 354
+models, 350 get the same verdict from both validators and the other 4 are the crashes. Failure-path
+controls are unchanged. Source, Deviations and Regression summary describe 1.0.0. Issue:
+https://github.com/ByteDance-Seed/EdgeBench/issues/42
 
 ## Known issues
 
-Kept as in v1. Fixing any of them changes scores and bumps `version`.
+Kept as in v1, so scores stay comparable. Fixing any of them changes scores and bumps `version`.
 
 1. **The submission can forge its score file.** The score is read from a file the submitted
    `build.sh` (running as root) can write before the evaluator does, and an early evaluator exit is
diff --git a/edgebench/tasks/smt_solver/environment/workspace/scripts/evaluate.py b/edgebench/tasks/smt_solver/environment/workspace/scripts/evaluate.py
index 91933c3f..ea768ed6 100644
--- a/edgebench/tasks/smt_solver/environment/workspace/scripts/evaluate.py
+++ b/edgebench/tasks/smt_solver/environment/workspace/scripts/evaluate.py
@@ -932,7 +932,7 @@ def main():
     solver = os.path.abspath(args.solver)
     if not os.path.isfile(solver) or not os.access(solver, os.X_OK):
         print(f"Error: solver is not executable: {args.solver}", file=sys.stderr)
-        sys.exit(2)
+        sys.exit(1)
     if not os.path.isdir(args.benchmarks):
         print(f"Error: benchmark directory does not exist: {args.benchmarks}", file=sys.stderr)
         sys.exit(1)
diff --git a/edgebench/tasks/smt_solver/judge/parse_result.py b/edgebench/tasks/smt_solver/judge/parse_result.py
index a4f10075..af176e94 100644
--- a/edgebench/tasks/smt_solver/judge/parse_result.py
+++ b/edgebench/tasks/smt_solver/judge/parse_result.py
@@ -1,14 +1,7 @@
-# v1's /tmp/sebench_parse_result.py (heredoc in judge.eval_cmd), except that the score file path comes
-# from argv[1] instead of the fixed /tmp/smt_hidden_score.json, and that an evaluator crash is invalid.
-# argv[2] = evaluate.py's exit status, empty if it did not run. 2 = it rejected the submission.
+# v1's /tmp/sebench_parse_result.py (heredoc in judge.eval_cmd), verbatim except that the
+# score file path comes from argv[1] instead of the fixed /tmp/smt_hidden_score.json.
 import json, pathlib, sys
 p = pathlib.Path(sys.argv[1])
-status = sys.argv[2] if len(sys.argv) > 2 else ''
-if not p.exists() and status not in ('', '0', '2'):
-    print('>>>>> Start Structured Result')
-    print(json.dumps({'valid': False, 'score': None, 'summary': 'evaluator exited with status {} before writing a score file'.format(status), 'details': [], 'metrics': {}}))
-    print('>>>>> End Structured Result')
-    sys.exit(0)
 raw = json.loads(p.read_text()) if p.exists() else {'final_score': 0.0, 'logic_summary': {}}
 raw_score = float(raw.get('final_score', 0.0) or 0.0)
 score = raw_score / 100.0 if raw_score > 1.0 else raw_score
diff --git a/edgebench/tasks/smt_solver/judge/run.sh b/edgebench/tasks/smt_solver/judge/run.sh
index 9df734fb..7daec838 100644
--- a/edgebench/tasks/smt_solver/judge/run.sh
+++ b/edgebench/tasks/smt_solver/judge/run.sh
@@ -17,7 +17,7 @@ LOG=$(mktemp)
 T=$(mktemp -d)
 
 (
-cd /home/workspace/smt_solver && rm -rf benchmarks hidden_benchmarks scripts expected_answers.json selection_manifest.json hidden_score.json public_score.json; chmod +x build.sh solve; build_status=0; ./build.sh >"$T/smt_build.out" 2>"$T/smt_build.err" || build_status=$?; if [ "$build_status" -eq 0 ]; then python3 /home/workspace/smt_judge/scripts/evaluate.py --solver ./solve --benchmarks /home/workspace/smt_judge/hidden_benchmarks --expected /home/workspace/smt_judge/hidden_benchmarks/expected_answers.json --manifest /home/workspace/smt_judge/hidden_benchmarks/selection_manifest.json --timeout 60 --parallel 16 --perturb --perturb-salt hidden-sebench --submission-root /home/workspace/smt_solver --output "$T/smt_hidden_score.json" >"$T/smt_eval.out" 2>"$T/smt_eval.err"; eval_status=$?; evaluator_status=$eval_status; else eval_status=$build_status; evaluator_status=; fi; if [ -f "$T/smt_build.out" ]; then cat "$T/smt_build.out"; fi; if [ -f "$T/smt_build.err" ]; then cat "$T/smt_build.err"; fi; if [ -f "$T/smt_eval.out" ]; then cat "$T/smt_eval.out"; fi; if [ -f "$T/smt_eval.err" ]; then cat "$T/smt_eval.err"; fi; python3 /judge/parse_result.py "$T/smt_hidden_score.json" "$evaluator_status"
+cd /home/workspace/smt_solver && rm -rf benchmarks hidden_benchmarks scripts expected_answers.json selection_manifest.json hidden_score.json public_score.json; chmod +x build.sh solve; build_status=0; ./build.sh >"$T/smt_build.out" 2>"$T/smt_build.err" || build_status=$?; if [ "$build_status" -eq 0 ]; then python3 /home/workspace/smt_judge/scripts/evaluate.py --solver ./solve --benchmarks /home/workspace/smt_judge/hidden_benchmarks --expected /home/workspace/smt_judge/hidden_benchmarks/expected_answers.json --manifest /home/workspace/smt_judge/hidden_benchmarks/selection_manifest.json --timeout 60 --parallel 16 --perturb --perturb-salt hidden-sebench --submission-root /home/workspace/smt_solver --output "$T/smt_hidden_score.json" >"$T/smt_eval.out" 2>"$T/smt_eval.err"; eval_status=$?; else eval_status=$build_status; fi; if [ -f "$T/smt_build.out" ]; then cat "$T/smt_build.out"; fi; if [ -f "$T/smt_build.err" ]; then cat "$T/smt_build.err"; fi; if [ -f "$T/smt_eval.out" ]; then cat "$T/smt_eval.out"; fi; if [ -f "$T/smt_eval.err" ]; then cat "$T/smt_eval.err"; fi; python3 /judge/parse_result.py "$T/smt_hidden_score.json"
 ) > "$LOG" 2>&1
 EXIT_CODE=$?
 cat "$LOG"
diff --git a/edgebench/tasks/smt_solver/judge/smt_judge/scripts/evaluate.py b/edgebench/tasks/smt_solver/judge/smt_judge/scripts/evaluate.py
index 91933c3f..ea768ed6 100755
--- a/edgebench/tasks/smt_solver/judge/smt_judge/scripts/evaluate.py
+++ b/edgebench/tasks/smt_solver/judge/smt_judge/scripts/evaluate.py
@@ -932,7 +932,7 @@ def main():
     solver = os.path.abspath(args.solver)
     if not os.path.isfile(solver) or not os.access(solver, os.X_OK):
         print(f"Error: solver is not executable: {args.solver}", file=sys.stderr)
-        sys.exit(2)
+        sys.exit(1)
     if not os.path.isdir(args.benchmarks):
         print(f"Error: benchmark directory does not exist: {args.benchmarks}", file=sys.stderr)
         sys.exit(1)