QF_UFNIA (Model Validation Track)

Competition results for the QF_UFNIA logic in the Model Validation 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)
Yices2	Yices2	Yices2	-	Yices2

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Timeout
Yices2	230	1221.24	1250.24	230	230	70	6
cvc5	207	2593.06	2618.69	207	207	93	46
SMTInterpol	125	9430.10	8555.13	125	125	175	2
z3-BooledASS ^ne	45 (base +2)	3835.38	3841.25	45	45	255	15
z3-BooledASS-base ⁿ	43	3632.22	3637.97	43	43	257	17

(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	Unsolved	Timeout
Yices2	230	1221.24	1250.24	230	230	70	6
cvc5	207	2593.06	2618.69	207	207	93	46
SMTInterpol	125	9430.10	8555.13	125	125	175	2
z3-BooledASS ^ne	45 (base +2)	3835.38	3841.25	45	45	255	15
z3-BooledASS-base ⁿ	43	3632.22	3637.97	43	43	257	17

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Timeout
Yices2	230	1221.24	1250.24	230	230	70	6
cvc5	207	2593.06	2618.69	207	207	93	46
SMTInterpol	125	9430.10	8555.13	125	125	175	2
z3-BooledASS ^ne	45 (base +2)	3835.38	3841.25	45	45	255	15
z3-BooledASS-base ⁿ	43	3632.22	3637.97	43	43	257	17

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained
Yices2	217	215.19	242.43	217	217	63	20
cvc5	196	156.28	180.38	196	196	45	59
SMTInterpol	93	172.43	98.43	93	93	163	44
z3-BooledASS ^ne	32 (base +2)	278.60	282.58	32	32	238	30
z3-BooledASS-base ⁿ	30	237.44	241.26	30	30	238	32

SMT-COMP 2026