QF_AUFBV (Unsat Core Track)

Competition results for the QF_AUFBV logic in the Unsat Core Track. Chart

Results were generated on 2026-07-25

Benchmarks: 36
Time Limit: 1200 seconds
Memory Limit: 30720 GB

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24 seconds Performance (parallel)
Bitwuzla	Bitwuzla	-	Bitwuzla	Bitwuzla

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Timeout
Bitwuzla	18349	1390.49	1394.69	33	33	3	3
Yices2	18229	422.09	425.97	31	31	5	5
z3-BooledASS ^ne	16859 (base +0)	1381.44	1385.37	31	31	5	5
SMTInterpol	10116	225.50	132.29	22	22	14	13
cvc5	4427	23.37	26.49	25	25	11	11
z3-BooledASS-base ⁿ	16859	1378.85	1382.83	31	31	5	5

(base +/- n): for derived solvers: increment over base solver
^ne: not eligible for winning as it does not substantially improve over the base solver (at least 10 % improvement in PAR2 score) ⁿ: non-competing solver

Parallel Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Timeout
Bitwuzla	18349	1390.49	1394.69	33	33	3	3
Yices2	18229	422.09	425.97	31	31	5	5
z3-BooledASS ^ne	16859 (base +0)	1381.44	1385.37	31	31	5	5
SMTInterpol	10116	225.50	132.29	22	22	14	13
cvc5	4427	23.37	26.49	25	25	11	11
z3-BooledASS-base ⁿ	16859	1378.85	1382.83	31	31	5	5

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Timeout
Bitwuzla	18349	1390.49	1394.69	33	33	3	3
Yices2	18229	422.09	425.97	31	31	5	5
z3-BooledASS ^ne	16859 (base +0)	1381.44	1385.37	31	31	5	5
SMTInterpol	10116	225.50	132.29	22	22	14	13
cvc5	4427	23.37	26.49	25	25	11	11
z3-BooledASS-base ⁿ	16859	1378.85	1382.83	31	31	5	5

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Abstained
z3-BooledASS ^ne	15168 (base +0)	33.82	36.66	23	23	13
Bitwuzla	14133	131.82	135.12	27	27	9
Yices2	13251	74.75	77.87	25	25	11
SMTInterpol	9348	110.17	40.34	21	21	15
cvc5	4427	23.37	26.49	25	25	11
z3-BooledASS-base ⁿ	15168	33.29	36.15	23	23	13

SMT-COMP 2026