alive2: Implement Z3 perf regression tracking

Z3 4.8.9 regressed perf compared to 4.8.8 in a few benchmarks (e.g., just see CI bots, both linux & Mac). It would be nice to have an automated way of diffing new timeouts in unit tests & LLVM test suite and then produce Z3 logs using Z3_open_log and friends. Similarly, we could have an automated way of running John’s perl script to detect score degradations with new Z3 releases.

@NikolajBjorner says he’ll fix any reported regression in 24 hours 😁

About this issue

Original URL
State: open
Created 4 years ago
Reactions: 2
Comments: 17 (14 by maintainers)

Commits related to this issue

SMT: add functionality to log all interactions with Z3 (#492) — committed to AliveToolkit/alive2 by nunoplopes 4 years ago

Most upvoted comments

As Nuno wrote use a few samples. The seeds don’t need to be random, just numbers 1-10 will do the trick.

for i in range(10):
     os.system("z3.exe smt.random_seed=%d %s -st" % (i, file))

NikolajBjorner on Oct 1, 2020