QF_UF (Unsat Core Track)

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

Results were generated on 2026-07-25

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

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24 seconds Performance (parallel)
OpenSMT (min-ucore)	OpenSMT (min-ucore)	-	OpenSMT (min-ucore)	OpenSMT

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Timeout
OpenSMT (min-ucore)	105056	35158.52	35260.51	799	799	13	13
z3-BooledASS ^ne	98573 (base +0)	1109.69	1209.09	812	812	0	0
Yices2	98456	721.54	822.11	812	812	0	0
OpenSMT	97975	915.36	1016.31	812	812	0	0
SMTInterpol	94028	6104.39	2823.04	803	803	9	0
plat-smt	93181	2017.35	2117.64	811	811	1	1
cvc5	47209	2018.92	2118.34	812	812	0	0
z3-BooledASS-base ⁿ	98573	1109.71	1209.39	812	812	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
OpenSMT (min-ucore)	105056	35158.52	35260.51	799	799	13	13
z3-BooledASS ^ne	98573 (base +0)	1109.69	1209.09	812	812	0	0
Yices2	98456	721.54	822.11	812	812	0	0
OpenSMT	97975	915.36	1016.31	812	812	0	0
SMTInterpol	94028	6104.39	2823.04	803	803	9	0
plat-smt	93181	2017.35	2117.64	811	811	1	1
cvc5	47209	2018.92	2118.34	812	812	0	0
z3-BooledASS-base ⁿ	98573	1109.71	1209.39	812	812	0	0

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Timeout
OpenSMT (min-ucore)	105056	35158.52	35260.51	799	799	13	13
z3-BooledASS ^ne	98573 (base +0)	1109.69	1209.09	812	812	0	0
Yices2	98456	721.54	822.11	812	812	0	0
OpenSMT	97975	915.36	1016.31	812	812	0	0
SMTInterpol	94028	6104.39	2823.04	803	803	9	0
plat-smt	93181	2017.35	2117.64	811	811	1	1
cvc5	47209	2018.92	2118.34	812	812	0	0
z3-BooledASS-base ⁿ	98573	1109.71	1209.39	812	812	0	0

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Abstained
OpenSMT	97973	536.63	636.54	804	804	8
z3-BooledASS ^ne	94313 (base +0)	491.57	589.83	803	803	9
Yices2	94129	254.35	353.75	803	803	9
SMTInterpol	89704	5573.26	2517.10	796	796	16
plat-smt	84658	398.76	497.51	800	800	12
OpenSMT (min-ucore)	51836	1324.46	1392.39	549	549	263
cvc5	42207	518.95	616.96	802	802	10
z3-BooledASS-base ⁿ	94313	492.65	591.17	803	803	9

SMT-COMP 2026