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, Bitwuzla and Z3 on fixed benchmark lists.
03ae4a3c9 Measured Source bench-results Components
Read SMT logics explained for the meaning of each division, worked examples, and use cases. Division names in the table link to their guides.
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 |
Parity ledger
Each row is one committed list of 200 SMT-LIB files, run through Axeyum and the division's reference solver on the same idle machine with 24 seconds and 8 GiB per file. The ratio is what Axeyum decided as a share of what the reference decided; a disagreement voids the row. When a reference count changes between runs, read the counts, not the ratio.
The ledger covers 16 of the 84 logic divisions in the SMT-LIB 2024 non-incremental corpus, which is 286,256 of 438,631 files. The file share is the larger of the two because the measured divisions include several of the largest logics. The remaining divisions have not been run, and nothing is claimed about them.
Each of the 16 rows is the latest ledger entry for its division, and no entry has
been added since 2026-09-11. Fifteen ran at one Axeyum commit; QF_UFLRA was re-measured the same
day at a later commit, after a missing integer-to-real coercion on distinct was fixed,
and that row replaces the earlier one. The per-row commit is in the last column.
| Division | Axeyum | Reference | Ratio | Disagree | Both / Axeyum only / reference only | Reference solver | Axeyum commit, date |
|---|---|---|---|---|---|---|---|
| QF_UF | 200/200 | 200/200 | 100.0% | 0 | 200 / 0 / 0 | cvc5 1.3.4 | c1d6db6fe, 2026-09-11 |
| QF_FP | 199/200 | 200/200 | 99.5% | 0 | 199 / 0 / 1 | bitwuzla 0.9.1 | c1d6db6fe, 2026-09-11 |
| QF_SLIA | 193/200 | 194/200 | 99.5% | 0 | 187 / 6 / 7 | cvc5 1.3.4 | c1d6db6fe, 2026-09-11 |
| QF_RDL | 152/200 | 154/200 | 98.7% | 0 | 147 / 5 / 7 | cvc5 1.3.4 | c1d6db6fe, 2026-09-11 |
| UF | 90/200 | 93/200 | 96.8% | 0 | 65 / 25 / 28 | cvc5 1.3.4 | c1d6db6fe, 2026-09-11 |
| QF_BV | 186/200 | 194/200 | 95.9% | 0 | 186 / 0 / 8 | bitwuzla 0.9.1 | c1d6db6fe, 2026-09-11 |
| QF_ABV | 186/200 | 197/200 | 94.4% | 0 | 185 / 1 / 12 | bitwuzla 0.9.1 | c1d6db6fe, 2026-09-11 |
| QF_S | 186/200 | 197/200 | 94.4% | 0 | 183 / 3 / 14 | cvc5 1.3.4 | c1d6db6fe, 2026-09-11 |
| QF_IDL | 113/200 | 123/200 | 91.9% | 0 | 109 / 4 / 14 | cvc5 1.3.4 | c1d6db6fe, 2026-09-11 |
| QF_UFLIA | 161/200 | 180/200 | 89.4% | 0 | 161 / 0 / 19 | cvc5 1.3.4 | c1d6db6fe, 2026-09-11 |
| QF_LIA | 119/200 | 139/200 | 85.6% | 0 | 117 / 2 / 22 | cvc5 1.3.4 | c1d6db6fe, 2026-09-11 |
| QF_LRA | 107/200 | 145/200 | 73.8% | 0 | 105 / 2 / 40 | cvc5 1.3.4 | c1d6db6fe, 2026-09-11 |
| QF_UFLRA | 142/200 | 198/200 | 71.7% | 0 | 142 / 0 / 56 | Z3 4.13.3 | 14712b1f4, 2026-09-11 |
| QF_NRA | 117/200 | 186/200 | 62.9% | 0 | 116 / 1 / 70 | cvc5 1.3.4 | c1d6db6fe, 2026-09-11 |
| QF_DT | 114/200 | 192/200 | 59.4% | 0 | 111 / 3 / 81 | cvc5 1.3.4 | c1d6db6fe, 2026-09-11 |
| QF_NIA | 41/200 | 87/200 | 47.1% | 0 | 27 / 14 / 60 | cvc5 1.3.4 | c1d6db6fe, 2026-09-11 |
Measurements after the ledger
The measurements below are not ledger entries and do not replace any row above. They use a different protocol and no reference solver.
On 2026-09-17, an interleaved A/B ran commit 60e23fa39 against its parent over
the same 16 lists of 200 files. Both arms ran each
file back to back on one pinned core, with 24 seconds and 8 GiB per file. Commit 60e23fa39 decided 2,432 of 3,200 files, with 0 disagreements in 4,380 comparisons
against declared :status. The table lists the divisions where its count differs
most from the ledger. After each changed verdict was re-run three times per arm, QF_UFLIA
reads 166 and QF_UFLRA reads 150.
| Division | Ledger, 2026-09-11 | A/B board, 2026-09-17 |
|---|---|---|
| QF_NIA | 41/200 | 87/200 |
| QF_DT | 114/200 | 171/200 |
| QF_NRA | 117/200 | 124/200 |
| QF_UFLIA | 161/200 | 167/200 |
| QF_UFLRA | 142/200 | 149/200 |
Two changes shipped after that board. Each was measured by its own A/B on the division's pinned list of 200 files. UFNIA has no ledger row.
Source: PLAN.md § Status @ 03ae4a3c9; ADR-2147 and ADR-2148, both 2026-09-17.
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.