mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-16 15:15:35 +00:00
Code Activity

Fix comment discrepancies found in code review (timeout buffer 3s, clarify -T: flag and date units)

Browse source 
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/834244bd-f780-46e8-b66a-d0e8c88f8dc8

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-05-13 09:30:49 +00:00 • committed by GitHub
parent df0abab788
commit a2a3c520b3
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

8
.github/workflows/tptp-benchmark.md vendored
View file

@ -251,8 +251,8 @@ set -euo pipefail
Z3=/tmp/z3-build/z3
TPTP_ROOT=/tmp/tptp
TIMEOUT_HARD=8 # outer OS-level guard (seconds)
Z3_TIMEOUT=5 # Z3 internal timeout flag -T:5
TIMEOUT_HARD=8 # outer OS-level guard (seconds; 3 s beyond Z3's -T:5)
Z3_TIMEOUT=5 # Z3 internal timeout: -T:N sets N-second limit (uppercase -T is seconds)
RESULTS=/tmp/tptp_results.tsv
PROBLEM_LIST=/tmp/selected_benchmarks.txt
@ -271,7 +271,7 @@ run_benchmark() {
local file="$1"
local start end elapsed output exit_code verdict
start=$(date +%s%3N)
start=$(date +%s%3N) # milliseconds since epoch
output=$(TPTP="$TPTP_ROOT" timeout "$TIMEOUT_HARD" \
"$Z3" -tptp -T:"$Z3_TIMEOUT" "$file" 2>&1) || exit_code=$?
exit_code=${exit_code:-0}
@ -546,7 +546,7 @@ Failing to produce any safe output triggers an automatic workflow-failure issue
- **Never run `ninja` in the background with `&`**: Concurrent C++ compilation and LLM inference exhausts available RAM and kills the agent process (exit 137). Always wait for build commands to finish before continuing.
- **TPTP environment variable**: Set `TPTP=/tmp/tptp` when invoking `z3 -tptp` so that `include()` directives in problem files resolve correctly against the downloaded Axioms directory.
- **Timeout detection**: Use `timeout 8` as the outer OS-level guard (2 seconds beyond Z3's `-T:5`) to allow Z3 to exit cleanly before the shell kills it. If the exit code from `timeout` is 124, record the verdict as `Timeout`.
- **Timeout detection**: Use `timeout 8` as the outer OS-level guard (3 seconds beyond Z3's `-T:5`) to allow Z3 to exit cleanly before the shell kills it. If the exit code from `timeout` is 124, record the verdict as `Timeout`.
- **Crash detection**: A crash is a non-zero exit code with no `% SZS status` line in the output and no timeout. Record it separately from `GaveUp`.
- **SZS status semantics**: Z3 outputs `Theorem` (not `Unsatisfiable`) when it proves a conjecture; `CounterSatisfiable` (not `Satisfiable`) when it finds a counterexample to a conjecture. A status mismatch between `Theorem` and `Unsatisfiable` for the same problem may be innocuous and depends on whether the problem file uses a conjecture formula.
- **Report soundness bugs prominently**: Any case where the polarity of the answer conflicts (expected Theorem/Unsatisfiable but got CounterSatisfiable/Satisfiable, or vice versa) is a potential soundness bug and must be highlighted as critical.