Given an SMT-LIB2 formula or file, run Z3 with statistics enabled and report performance characteristics. This is useful for identifying performance regressions, comparing tactic strategies, and profiling theory solver workload distribution.

Step 1: Run Z3 with statistics

Action: Invoke benchmark.py with the formula or file. Use --runs N for repeated timing.

Expectation: The script invokes z3 -st, parses the statistics block, and prints a performance summary. A run entry is logged to z3agent.db.

Result: Timing and statistics are displayed. Proceed to Step 2 to interpret.

python3 scripts/benchmark.py --file problem.smt2
python3 scripts/benchmark.py --file problem.smt2 --runs 5
python3 scripts/benchmark.py --formula "(declare-const x Int)..." --debug

Step 2: Interpret the output

Action: Review wall-clock time, memory usage, conflict counts, and per-theory breakdowns.

Expectation: A complete performance profile including min/median/max timing when multiple runs are requested.

Result: If performance is acceptable, no action needed. If slow, try simplify to reduce the formula or adjust tactic strategies.

The output includes:

• wall-clock time (ms)
• result (sat/unsat/unknown/timeout)
• memory usage (MB)
• conflicts, decisions, propagations
• per-theory breakdown (arithmetic, bv, array, etc.)

With --runs N, the script runs Z3 N times and reports min/median/max timing.

Step 3: Compare over time

Action: Query past benchmark runs from z3agent.db to detect regressions or improvements.

Expectation: Historical run data is available for comparison, ordered by recency.

Result: If performance regressed, investigate recent formula or tactic changes. If improved, record the successful configuration.

python3 ../../shared/z3db.py runs --skill benchmark --last 20
python3 ../../shared/z3db.py query "SELECT smtlib2, result, stats FROM formulas WHERE run_id IN (SELECT run_id FROM runs WHERE skill='benchmark') ORDER BY run_id DESC LIMIT 5"

Parameters