QF_Equality_NonLinearArith (Single Query Track)

Competition results for the QF_Equality_NonLinearArith division in the Single Query Track. Chart

Results were generated on 2026-07-25

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

Logics:

QF_ANIA : 155 benchmarks
QF_AUFNIA : 9 benchmarks
QF_UFDTNIA : 80 benchmarks
QF_UFNIA : 339 benchmarks
QF_UFNRA : 48 benchmarks

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24 seconds Performance (parallel)
Yices2	Yices2	Yices2	Z3-alpha2	Yices2

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout
Z3-alpha2 ^ne	489 (base +14)	23259.43	23049.90	489	364	125	142	0	141
Z3-alpha2-debug ⁿ	489	24276.93	23601.64	489	364	125	142	0	141
Yices2	473	11292.71	11352.33	473	384	89	78	80	78
z3-BooledASS ^ne	470 (base -2)	15994.08	16052.86	470	348	122	161	0	161
cvc5-cvc5-xyz ^ne	422 (base +1)	19666.58	19720.02	422	318	104	209	0	209
cvc5	420	15580.75	15634.11	420	317	103	211	0	211
SMTInterpol	292	17239.04	15198.58	292	224	68	339	0	63
Xolver	159	269.63	289.45	159	137	22	472	0	453
Z3-alpha2-base ⁿ	475	18681.52	18742.11	475	353	122	156	0	152
z3-BooledASS-base ⁿ	472	20150.60	20211.33	472	349	123	159	0	159
cvc5-cvc5-xyz-base ⁿ	421	19066.18	19119.99	421	318	103	210	0	210

(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	Abstained	Timeout
Z3-alpha2 ^ne	489 (base +14)	23259.43	23049.90	489	364	125	142	0	141
Z3-alpha2-debug ⁿ	489	24276.93	23601.64	489	364	125	142	0	141
Yices2	473	11292.71	11352.33	473	384	89	78	80	78
z3-BooledASS ^ne	470 (base -2)	15994.08	16052.86	470	348	122	161	0	161
cvc5-cvc5-xyz ^ne	422 (base +1)	19666.58	19720.02	422	318	104	209	0	209
cvc5	420	15580.75	15634.11	420	317	103	211	0	211
SMTInterpol	292	17239.04	15198.58	292	224	68	339	0	63
Xolver	159	269.63	289.45	159	137	22	472	0	453
Z3-alpha2-base ⁿ	475	18681.52	18742.11	475	353	122	156	0	152
z3-BooledASS-base ⁿ	472	20150.60	20211.33	472	349	123	159	0	159
cvc5-cvc5-xyz-base ⁿ	421	19066.18	19119.99	421	318	103	210	0	210

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
Yices2	384	9939.38	9987.86	384	384	13	234	13
Z3-alpha2 ^ne	364 (base +11)	19304.94	19146.50	364	364	82	185	81
Z3-alpha2-debug ⁿ	364	20048.39	19543.46	364	364	82	185	81
z3-BooledASS ^ne	348 (base -1)	13317.73	13361.54	348	348	98	185	98
cvc5-cvc5-xyz ^ne	318 (base +0)	13105.14	13145.26	318	318	128	185	128
cvc5	317	9898.53	9938.61	317	317	129	185	129
SMTInterpol	224	13004.44	11557.32	224	224	222	185	27
Xolver	137	189.01	206.07	137	137	309	185	293
Z3-alpha2-base ⁿ	353	14108.41	14153.46	353	353	93	185	89
z3-BooledASS-base ⁿ	349	16376.98	16422.26	349	349	97	185	97
cvc5-cvc5-xyz-base ⁿ	318	12644.00	12684.43	318	318	128	185	128

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
Z3-alpha2	125 (base +3)	3954.49	3903.40	125	125	21	485	21
Z3-alpha2-debug ⁿ	125	4228.54	4058.17	125	125	21	485	21
z3-BooledASS ^ne	122 (base -1)	2676.35	2691.32	122	122	24	485	24
cvc5-cvc5-xyz ^ne	104 (base +1)	6561.45	6574.76	104	104	42	485	42
cvc5	103	5682.23	5695.50	103	103	43	485	43
Yices2	89	1353.33	1364.47	89	89	39	503	39
SMTInterpol	68	4234.60	3641.26	68	68	78	485	17
Xolver	22	80.62	83.38	22	22	124	485	121
z3-BooledASS-base ⁿ	123	3773.62	3789.07	123	123	23	485	23
Z3-alpha2-base ⁿ	122	4573.11	4588.66	122	122	24	485	24
cvc5-cvc5-xyz-base ⁿ	103	6422.18	6435.56	103	103	43	485	43

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained
Z3-alpha2 ^ne	420 (base +14)	2268.52	2087.86	420	310	110	0	211
Z3-alpha2-debug ⁿ	419	3151.86	2572.17	419	309	110	0	212
z3-BooledASS ^ne	405 (base +2)	884.72	934.22	405	301	104	0	226
Yices2	401	613.70	663.30	401	317	84	0	230
cvc5	348	767.47	810.53	348	267	81	0	283
cvc5-cvc5-xyz ^ne	344 (base +3)	712.53	754.73	344	263	81	0	287
SMTInterpol	233	1051.87	483.35	233	178	55	236	162
Xolver	159	269.63	289.45	159	137	22	12	460
Z3-alpha2-base ⁿ	406	941.52	991.89	406	300	106	0	225
z3-BooledASS-base ⁿ	403	860.42	910.74	403	300	103	0	228
cvc5-cvc5-xyz-base ⁿ	341	703.48	745.63	341	261	80	0	290

SMT-COMP 2026