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

fix(ostrich-benchmark): add safeoutputs keepalive noop calls before long benchmark run (#9313)

Browse source 
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/7d129a85-614d-4927-a598-05ae902ab771

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
Copilot 2026-04-16 03:22:33 +02:00 • committed by GitHub
parent 1d19d4a0dc
commit daf2506b60
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 102 additions and 75 deletions
Download patch file Download diff file Expand all files Collapse all files

4
.github/workflows/ostrich-benchmark.md vendored
View file

@ -88,6 +88,8 @@ echo "Found Microsoft.Z3.dll at: $Z3_DOTNET_DLL"
If the build fails, report the error clearly and exit without proceeding.
Once the binary is confirmed working, call the `noop` safe-output tool with the message `"Z3 built successfully from the c3 branch. Starting ZIPT build and benchmark — results will be posted as a GitHub Discussion once complete."` This keepalive call refreshes the safe-output MCP session before the long build and benchmark phases begin, preventing a session timeout.
## Phase 2a: Clone and Build ZIPT
Clone the ZIPT solver from the `parikh` branch and compile it against the Z3 .NET bindings built in Phase 1.
@ -153,6 +155,8 @@ if [ "$TOTAL_FILES" -eq 0 ]; then
fi
```
Once the benchmark files are confirmed, call the `noop` safe-output tool with the message `"Benchmark files ready: <TOTAL_FILES> Ostrich .smt2 files extracted. Starting benchmark run — this may take over an hour."` This second keepalive refreshes the safe-output MCP session immediately before the long per-file benchmark loop begins.
## Phase 3: Run Benchmarks
Run every file from `/tmp/all_ostrich_files.txt` with both Z3 string solvers and ZIPT. Use a **5-second timeout** per run.