smt_solver: report an evaluator crash as invalid

edgebench/tasks/smt_solver/NOTES.md

@@ -53,6 +53,15 @@ 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
+
+If the evaluator exits with anything but 0 or 2 and leaves no score file, the result is now invalid,
+not 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). No score changes unless the evaluator crashed. 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`.

edgebench/tasks/smt_solver/environment/workspace/scripts/evaluate.py

@@ -898,7 +898,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)

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

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"

edgebench/tasks/smt_solver/judge/smt_judge/scripts/evaluate.py

@@ -898,7 +898,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)

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]