QF_Equality_NonLinearArith (Model Validation Track)

Competition results for the QF_Equality_NonLinearArith division in the Model Validation Track. Chart

Results were generated on 2026-07-25

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

Logics:

QF_ANIA : 121 benchmarks
QF_AUFNIA : 5 benchmarks
QF_UFDTNIA : 47 benchmarks
QF_UFNIA : 300 benchmarks
QF_UFNRA : 33 benchmarks

Winners

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

Sequential Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
cvc5	0	337	14564.49	14607.08	337	337	169	0	114
SMTInterpol	0	250	9943.83	8821.25	250	250	256	0	5
z3-BooledASS ^ne	0	169 (base +2)	8263.21	8284.93	169	169	337	0	64
Yices2	81	300	2435.31	2473.04	300	300	159	47	11
z3-BooledASS-base ⁿ	0	167	8087.82	8109.48	167	167	339	0	64

(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	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
cvc5	0	337	14564.49	14607.08	337	337	169	0	114
SMTInterpol	0	250	9943.83	8821.25	250	250	256	0	5
z3-BooledASS ^ne	0	169 (base +2)	8263.21	8284.93	169	169	337	0	64
Yices2	81	300	2435.31	2473.04	300	300	159	47	11
z3-BooledASS-base ⁿ	0	167	8087.82	8109.48	167	167	339	0	64

SAT Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
cvc5	0	337	14564.49	14607.08	337	337	169	0	114
SMTInterpol	0	250	9943.83	8821.25	250	250	256	0	5
z3-BooledASS ^ne	0	169 (base +2)	8263.21	8284.93	169	169	337	0	64
Yices2	81	300	2435.31	2473.04	300	300	159	47	11
z3-BooledASS-base ⁿ	0	167	8087.82	8109.48	167	167	339	0	64

24 seconds Performance Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained
cvc5	0	282	362.61	397.34	282	282	49	175
SMTInterpol	0	216	558.37	279.00	216	216	218	72
z3-BooledASS ^ne	0	141 (base +2)	576.13	593.64	141	141	255	110
Yices2	54	282	324.48	359.75	282	282	120	104
z3-BooledASS-base ⁿ	0	139	534.74	552.21	139	139	255	112

SMT-COMP 2026