UFNIA (Single Query Track)

Competition results for the UFNIA logic in the Single Query Track. Chart

Results were generated on 2026-07-25

Benchmarks: 1662
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	cvc5

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout
cvc5	995	30409.40	30536.01	995	186	809	667	667
cvc5-cvc5-xyz ^ne	995 (base +0)	31098.35	31223.84	995	186	809	667	667
z3-BooledASS ^ne	868 (base +2)	2893.02	3000.14	868	188	680	794	745
SMTInterpol	278	2038.69	1524.36	278	17	261	1384	462
UltimateEliminator+MathSAT	184	1484.88	1068.59	184	132	52	1478	96
cvc5-cvc5-xyz-base ⁿ	995	30659.66	30785.13	995	186	809	667	667
z3-BooledASS-base ⁿ	866	3672.31	3779.05	866	188	678	796	713

(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 SAT	Solved UNSAT	Unsolved	Timeout
cvc5	995	30409.40	30536.01	995	186	809	667	667
cvc5-cvc5-xyz ^ne	995 (base +0)	31098.35	31223.84	995	186	809	667	667
z3-BooledASS ^ne	868 (base +2)	2893.02	3000.14	868	188	680	794	745
SMTInterpol	278	2038.69	1524.36	278	17	261	1384	462
UltimateEliminator+MathSAT	184	1484.88	1068.59	184	132	52	1478	96
cvc5-cvc5-xyz-base ⁿ	995	30659.66	30785.13	995	186	809	667	667
z3-BooledASS-base ⁿ	866	3672.31	3779.05	866	188	678	796	713

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
z3-BooledASS ^ne	188 (base +0)	64.30	87.48	188	188	2	1472	2
cvc5	186	6960.83	6984.62	186	186	4	1472	4
cvc5-cvc5-xyz ^ne	186 (base +0)	6970.01	6993.74	186	186	4	1472	4
UltimateEliminator+MathSAT	132	1261.46	960.54	132	132	58	1472	42
SMTInterpol	17	7.76	7.67	17	17	173	1472	3
z3-BooledASS-base ⁿ	188	66.32	89.45	188	188	2	1472	1
cvc5-cvc5-xyz-base ⁿ	186	6970.35	6993.96	186	186	4	1472	4

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
cvc5	809	23448.57	23551.40	809	809	49	804	49
cvc5-cvc5-xyz ^ne	809 (base +0)	24128.34	24230.10	809	809	49	804	49
z3-BooledASS ^ne	680 (base +2)	2828.72	2912.66	680	680	178	804	142
SMTInterpol	261	2030.93	1516.69	261	261	597	804	231
UltimateEliminator+MathSAT	52	223.42	108.05	52	52	806	804	36
cvc5-cvc5-xyz-base ⁿ	809	23689.31	23791.17	809	809	49	804	49
z3-BooledASS-base ⁿ	678	3605.99	3689.59	678	678	180	804	131

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained
cvc5	863	1041.28	1148.98	863	171	692	0	799
cvc5-cvc5-xyz ^ne	859 (base +0)	1043.45	1149.58	859	171	688	0	803
z3-BooledASS ^ne	847 (base +2)	802.03	906.40	847	188	659	36	779
SMTInterpol	275	842.83	380.74	275	17	258	786	601
UltimateEliminator+MathSAT	180	1057.94	652.06	180	128	52	1373	109
cvc5-cvc5-xyz-base ⁿ	859	1045.46	1151.66	859	171	688	0	803
z3-BooledASS-base ⁿ	845	802.91	906.81	845	188	657	36	781

SMT-COMP 2026