QF_AUFLIA (Unsat Core Track)

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

Results were generated on 2026-07-25

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

Winners

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

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Timeout
cvc5	24092	118.09	155.33	300	300	0	0
z3-BooledASS ^ne	23010 (base +0)	60.33	97.15	300	300	0	0
Yices2	16180	53.36	90.60	300	300	0	0
OpenSMT (min-ucore)	3439	9465.82	9499.62	265	265	35	35
OpenSMT	2741	123.07	160.89	300	300	0	0
SMTInterpol	1309	1184.63	585.10	300	300	0	0
z3-BooledASS-base ⁿ	23010	60.27	97.11	300	300	0	0

(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
cvc5	24092	118.09	155.33	300	300	0	0
z3-BooledASS ^ne	23010 (base +0)	60.33	97.15	300	300	0	0
Yices2	16180	53.36	90.60	300	300	0	0
OpenSMT (min-ucore)	3439	9465.82	9499.62	265	265	35	35
OpenSMT	2741	123.07	160.89	300	300	0	0
SMTInterpol	1309	1184.63	585.10	300	300	0	0
z3-BooledASS-base ⁿ	23010	60.27	97.11	300	300	0	0

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Timeout
cvc5	24092	118.09	155.33	300	300	0	0
z3-BooledASS ^ne	23010 (base +0)	60.33	97.15	300	300	0	0
Yices2	16180	53.36	90.60	300	300	0	0
OpenSMT (min-ucore)	3439	9465.82	9499.62	265	265	35	35
OpenSMT	2741	123.07	160.89	300	300	0	0
SMTInterpol	1309	1184.63	585.10	300	300	0	0
z3-BooledASS-base ⁿ	23010	60.27	97.11	300	300	0	0

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Abstained
cvc5	24092	118.09	155.33	300	300	0
z3-BooledASS ^ne	23010 (base +0)	60.33	97.15	300	300	0
Yices2	16180	53.36	90.60	300	300	0
OpenSMT	2741	123.07	160.89	300	300	0
OpenSMT (min-ucore)	1523	345.67	373.47	224	224	76
SMTInterpol	1303	614.29	320.99	297	297	3
z3-BooledASS-base ⁿ	23010	60.27	97.11	300	300	0

SMT-COMP 2026