QF_UFLIA (Unsat Core Track)

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

Results were generated on 2026-07-25

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

Winners

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

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Timeout
z3-BooledASS ^ne	307375 (base +0)	1876.19	1879.18	23	23	1	1
Yices2	307200	1562.82	1565.86	23	23	1	1
SMTInterpol	31774	1299.98	1162.42	23	23	1	1
OpenSMT	10398	1246.84	1249.45	20	20	4	4
cvc5	9575	37.20	39.54	19	19	5	5
OpenSMT (min-ucore)	9359	1060.71	1063.21	19	19	5	5
z3-BooledASS-base ⁿ	307375	1814.76	1817.75	23	23	1	1

(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
z3-BooledASS ^ne	307375 (base +0)	1876.19	1879.18	23	23	1	1
Yices2	307200	1562.82	1565.86	23	23	1	1
SMTInterpol	31774	1299.98	1162.42	23	23	1	1
OpenSMT	10398	1246.84	1249.45	20	20	4	4
cvc5	9575	37.20	39.54	19	19	5	5
OpenSMT (min-ucore)	9359	1060.71	1063.21	19	19	5	5
z3-BooledASS-base ⁿ	307375	1814.76	1817.75	23	23	1	1

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Timeout
z3-BooledASS ^ne	307375 (base +0)	1876.19	1879.18	23	23	1	1
Yices2	307200	1562.82	1565.86	23	23	1	1
SMTInterpol	31774	1299.98	1162.42	23	23	1	1
OpenSMT	10398	1246.84	1249.45	20	20	4	4
cvc5	9575	37.20	39.54	19	19	5	5
OpenSMT (min-ucore)	9359	1060.71	1063.21	19	19	5	5
z3-BooledASS-base ⁿ	307375	1814.76	1817.75	23	23	1	1

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Abstained
Yices2	285946	9.73	12.26	20	20	4
z3-BooledASS ^ne	11767 (base +0)	24.53	26.90	19	19	5
SMTInterpol	10471	61.60	28.09	20	20	4
cvc5	8810	7.60	9.80	18	18	6
OpenSMT	1064	5.09	7.31	18	18	6
OpenSMT (min-ucore)	587	5.12	7.23	17	17	7
z3-BooledASS-base ⁿ	11767	24.15	26.51	19	19	5

SMT-COMP 2026