SAT and SMT
SMT-LIB coverage and speed
Axeyum implements its own SAT and SMT solvers. The regression scoreboard measures supported fragments against Z3, while the parity ledger provides same-machine comparisons with cvc5 and Bitwuzla on fixed benchmark lists.
a103b3db3 Measured Source bench-results Components
Regression scoreboard
762 of 992 files were decided across 24 logic fragments. 674 decisions were compared with z3 4.13.3; the ledger records 0 disagreements.
| Division | Slice | Files | Decided | Rate | Unknown | Unsupported | Compared | Disagree | PAR-2 s |
|---|---|---|---|---|---|---|---|---|---|
| BV | bv-bitwuzla-regress-clean-quantified | 5 | 5 | 100% | 0 | 0 | 0 | 0 | 0.000 |
| BV | bv-cvc5-regress-clean-quantified | 54 | 54 | 100% | 0 | 0 | 52 | 0 | 0.033 |
| LIA | lia-cvc5-regress-clean-quantified | 12 | 0 | 0% | 8 | 4 | 0 | 0 | 30.000 |
| QF_ABV | qf-abv-cvc5-bitwuzla-regress-clean | 193 | 169 | 88% | 0 | 24 | 165 | 0 | 1.666 |
| QF_ALIA | qf-alia-cvc5-regress-clean | 6 | 6 | 100% | 0 | 0 | 5 | 0 | 0.000 |
| QF_AUFBV | qf-aufbv-bitwuzla-regress-clean | 44 | 41 | 93% | 0 | 3 | 41 | 0 | 1.979 |
| QF_AUFBV | qf-aufbv-cvc5-regress-clean | 9 | 5 | 56% | 1 | 3 | 4 | 0 | 3.334 |
| QF_AUFLIA | qf-auflia-cvc5-regress-clean | 7 | 5 | 71% | 2 | 0 | 4 | 0 | 5.715 |
| QF_AX | qf-ax-cvc5-regress-clean | 8 | 8 | 100% | 0 | 0 | 8 | 0 | 0.004 |
| QF_BV | qf-bv-curated-bvred | 6 | 6 | 100% | 0 | 0 | 6 | 0 | 0.000 |
| QF_BVFP | qf-bvfp-bitwuzla-regress-clean | 8 | 7 | 88% | 0 | 1 | 6 | 0 | 0.005 |
| QF_DT | qf-dt-cvc5-regress-clean | 3 | 3 | 100% | 0 | 0 | 3 | 0 | 0.003 |
| QF_FF | qf-ff-cvc5-regress-clean | 30 | 24 | 80% | 0 | 6 | 24 | 0 | 0.010 |
| QF_FP | qf-fp-bitwuzla-regress-clean | 16 | 16 | 100% | 0 | 0 | 16 | 0 | 0.010 |
| QF_LIA | qf-lia-cvc5-regress-clean | 11 | 10 | 91% | 1 | 0 | 9 | 0 | 1.819 |
| QF_LRA | qf-lra-cvc5-regress-clean | 11 | 9 | 82% | 2 | 0 | 5 | 0 | 3.637 |
| QF_NIA | qf-nia-curated-iand | 3 | 3 | 100% | 0 | 0 | 0 | 0 | 0.003 |
| QF_NIA | qf-nia-synthetic-graduated | 32 | 32 | 100% | 0 | 0 | 32 | 0 | 6.772 |
| QF_NIA | qf-nia-cvc5-regress-clean | 39 | 33 | 85% | 5 | 1 | 23 | 0 | 2.730 |
| QF_NRA | qf-nra-synthetic-graduated | 33 | 30 | 91% | 3 | 0 | 30 | 0 | 5.455 |
| QF_NRA | qf-nra-cvc5-regress-clean | 38 | 32 | 84% | 6 | 0 | 32 | 0 | 3.169 |
| QF_S | qf-s-cvc5-regress-clean | 134 | 93 | 69% | 9 | 32 | 79 | 0 | 1.886 |
| QF_SEQ | qf-seq-cvc5-regress-clean | 33 | 22 | 67% | 10 | 1 | 10 | 0 | 6.252 |
| QF_SLIA | qf-slia-cvc5-regress-clean | 50 | 25 | 50% | 4 | 21 | 18 | 0 | 2.844 |
| QF_UF | qf-uf-cvc5-regress-clean-overbound-uninterp-sorts | 6 | 4 | 67% | 2 | 0 | 4 | 0 | 7.489 |
| QF_UF | qf-uf-cvc5-regress-clean-bounded | 82 | 44 | 54% | 13 | 24 | 37 | 0 | 4.845 |
| QF_UF | qf-uf-cvc5-regress-clean-bounded-uninterp-sorts | 82 | 44 | 54% | 13 | 24 | 37 | 0 | 4.845 |
| QF_UFBV | qf-ufbv-bitwuzla-regress-clean | 2 | 2 | 100% | 0 | 0 | 2 | 0 | 0.000 |
| QF_UFBV | qf-ufbv-cvc5-regress-clean | 4 | 4 | 100% | 0 | 0 | 4 | 0 | 0.001 |
| QF_UFFF | qf-ufff-cvc5-regress-clean | 8 | 8 | 100% | 0 | 0 | 0 | 0 | 0.003 |
| QF_UFLIA | qf-uflia-curated-named | 2 | 2 | 100% | 0 | 0 | 2 | 0 | 0.001 |
| QF_UFLIA | qf-uflia-cvc5-regress-clean | 8 | 8 | 100% | 0 | 0 | 8 | 0 | 0.572 |
| QF_UFLIA | qf-uflia-cvc5-regress-clean-bounded-uninterp-sorts | 6 | 6 | 100% | 0 | 0 | 6 | 0 | 0.002 |
| QF_UFLIA | qf-uflia-cvc5-regress-clean-overbound-uninterp-sorts | 2 | 2 | 100% | 0 | 0 | 2 | 0 | 2.294 |
| UF | uf-cvc5-regress-clean-quantified | 5 | 0 | 0% | 0 | 5 | 0 | 0 | 0.000 |
How to read the table
Decided means sat or unsat. Unknown means the implemented method
did not decide the file. Unsupported means the required fragment was not wired for that
route.
PAR-2 is mean elapsed time with each timeout counted twice. Lower is faster. It describes this benchmark slice and command, not general solver speed.
The separate parity runs use 200 committed files per division, with 24 seconds and 8 GiB per file. See the source ledger for exact commands and solver versions.