QF_NIA (Model Validation Track)

Competition results for the QF_NIA logic in the Model Validation Track. Chart

Results were generated on 2026-07-25

Benchmarks: 1901
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	1686	15376.89	15588.15	1686	1686	215	206
cvc5	1590	395345.60	395582.42	1590	1590	311	302
z3-BooledASS ^ne	1046 (base -646)	38440.52	38573.30	1046	1046	855	194
SMTInterpol	1	0.42	0.43	1	1	1900	2
z3-BooledASS-base ⁿ	1692	44277.81	44490.51	1692	1692	209	190

(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	1686	15376.89	15588.15	1686	1686	215	206
cvc5	1590	395345.60	395582.42	1590	1590	311	302
z3-BooledASS ^ne	1046 (base -646)	38440.52	38573.30	1046	1046	855	194
SMTInterpol	1	0.42	0.43	1	1	1900	2
z3-BooledASS-base ⁿ	1692	44277.81	44490.51	1692	1692	209	190

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Timeout
Yices2	1686	15376.89	15588.15	1686	1686	215	206
cvc5	1590	395345.60	395582.42	1590	1590	311	302
z3-BooledASS ^ne	1046 (base -646)	38440.52	38573.30	1046	1046	855	194
SMTInterpol	1	0.42	0.43	1	1	1900	2
z3-BooledASS-base ⁿ	1692	44277.81	44490.51	1692	1692	209	190

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained
Yices2	1604	3266.57	3466.38	1604	1604	9	288
z3-BooledASS ^ne	866 (base -615)	3222.67	3329.85	866	866	625	410
cvc5	761	1729.64	1823.93	761	761	9	1131
SMTInterpol	1	0.42	0.43	1	1	1888	12
z3-BooledASS-base ⁿ	1481	4465.76	4648.43	1481	1481	16	404

SMT-COMP 2026