Summary
Differential vs Z3 4.16.0 on QF_BV: OxiZ returns sat where Z3 returns unsat.
Unsound samples
| file |
z3 |
oz |
main |
integrate |
non-incremental/QF_BV/sage/app9/bench_679.smt2 |
unsat |
unsat ✓ |
sat |
sat |
non-incremental/QF_BV/bruttomesso/core/ext_con_064_002_0512.smt2 |
unsat |
sat (~7s) |
sat (~10s) |
sat (~10s) |
Repro
f=non-incremental/QF_BV/sage/app9/bench_679.smt2
z3 "$f" # unsat
oxiz -q "$f" # sat on main/integrate; unsat on 0.3.2 upstream in our run
f2=non-incremental/QF_BV/bruttomesso/core/ext_con_064_002_0512.smt2
z3 "$f2" # unsat
# oxiz may need >5s; observed sat on oz/main/integrate within ~7–10s
Notes
bench_679: main regression vs upstream (upstream matched z3 unsat).ext_con_064_002_0512: shared false sat; larger bit-vector core / extract-concat family.
Summary
Differential vs Z3 4.16.0 on QF_BV: OxiZ returns sat where Z3 returns unsat.
Unsound samples
non-incremental/QF_BV/sage/app9/bench_679.smt2non-incremental/QF_BV/bruttomesso/core/ext_con_064_002_0512.smt2Repro
Notes
bench_679: main regression vs upstream (upstream matched z3 unsat).ext_con_064_002_0512: shared false sat; larger bit-vector core / extract-concat family.