QF_NonLinearRealArith (Single Query Track)

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

Results were generated on 2026-07-25

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

Logics:

QF_NRA : 1020 benchmarks

Winners

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

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout
Z3-GEX ^ne	946 (base +1)	25567.48	9056.24	953	479	474	67	67
Z3-alpha2	946 (base +30)	18730.60	18731.02	946	473	473	74	74
Z3-alpha2-debug ⁿ	946	22659.60	21744.95	946	473	473	74	74
Z3-siri ^ne	943 (base -1)	16751.36	16870.44	943	471	472	77	77
cvc5	913	37872.83	37989.11	913	441	472	107	107
cvc5-cvc5-xyz ^ne	910 (base +0)	37080.70	37195.91	910	441	469	110	110
Yices2	909	10676.71	10790.59	909	456	453	111	111
z3-BooledASS ^ne	900 (base +1)	12887.12	12998.20	900	470	430	120	120
SMT-RAT	849	28874.87	28983.25	849	422	427	171	171
Xolver	510	8014.01	8077.82	510	238	272	510	459
SMTInterpol	175	1446.92	1083.24	175	4	171	845	0
Z3-GEX-base ⁿ	945	16576.64	16695.44	945	472	473	75	75
Z3-siri-base ⁿ	944	16702.16	16821.62	944	472	472	76	76
Z3-alpha2-base ⁿ	916	14104.16	14219.02	916	461	455	104	75
cvc5-cvc5-xyz-base ⁿ	910	37117.64	37233.45	910	441	469	110	110
z3-BooledASS-base ⁿ	899	12859.29	12970.56	899	469	430	121	121

(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
Z3-GEX	953 (base +8)	39698.36	12823.89	953	479	474	67	67
Z3-alpha2	946 (base +30)	18730.60	18731.02	946	473	473	74	74
Z3-alpha2-debug ⁿ	946	22659.60	21744.95	946	473	473	74	74
Z3-siri ^ne	943 (base -1)	16751.36	16870.44	943	471	472	77	77
cvc5	913	37872.83	37989.11	913	441	472	107	107
cvc5-cvc5-xyz ^ne	910 (base +0)	37080.70	37195.91	910	441	469	110	110
Yices2	909	10676.71	10790.59	909	456	453	111	111
z3-BooledASS ^ne	900 (base +1)	12887.12	12998.20	900	470	430	120	120
SMT-RAT	849	28874.87	28983.25	849	422	427	171	171
Xolver	510	8014.01	8077.82	510	238	272	510	459
SMTInterpol	175	1446.92	1083.24	175	4	171	845	0
Z3-GEX-base ⁿ	945	16576.64	16695.44	945	472	473	75	75
Z3-siri-base ⁿ	944	16702.16	16821.62	944	472	472	76	76
Z3-alpha2-base ⁿ	916	14104.16	14219.02	916	461	455	104	75
cvc5-cvc5-xyz-base ⁿ	910	37117.64	37233.45	910	441	469	110	110
z3-BooledASS-base ⁿ	899	12859.29	12970.56	899	469	430	121	121

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained	Timeout
Z3-GEX	479 (base +7)	13111.81	5132.57	479	479	16	525	16
Z3-alpha2	473 (base +12)	10208.30	10232.84	473	473	22	525	22
Z3-alpha2-debug ⁿ	473	11920.82	11489.41	473	473	22	525	22
Z3-siri ^ne	471 (base -1)	4177.54	4236.83	471	471	24	525	24
z3-BooledASS ^ne	470 (base +1)	4502.62	4560.53	470	470	25	525	25
Yices2	456	6797.02	6854.26	456	456	39	525	39
cvc5	441	14026.23	14082.09	441	441	54	525	54
cvc5-cvc5-xyz ^ne	441 (base +0)	14590.21	14645.91	441	441	54	525	54
SMT-RAT	422	11766.08	11819.69	422	422	73	525	73
Xolver	238	4846.84	4876.74	238	238	257	525	222
SMTInterpol	4	1024.28	910.74	4	4	491	525	0
Z3-GEX-base ⁿ	472	4150.54	4209.39	472	472	23	525	23
Z3-siri-base ⁿ	472	4196.94	4256.03	472	472	23	525	23
z3-BooledASS-base ⁿ	469	4480.30	4538.19	469	469	26	525	26
Z3-alpha2-base ⁿ	461	3871.05	3928.40	461	461	34	525	24
cvc5-cvc5-xyz-base ⁿ	441	14645.78	14701.78	441	441	54	525	54

UNSAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved UNSAT	Unsolved	Abstained	Timeout
Z3-GEX	474 (base +1)	26586.54	7691.32	474	474	13	533	13
Z3-alpha2	473 (base +18)	8522.31	8498.18	473	473	14	533	14
Z3-alpha2-debug ⁿ	473	10738.79	10255.53	473	473	14	533	14
Z3-siri ^ne	472 (base +0)	12573.82	12633.61	472	472	15	533	15
cvc5	472	23846.59	23907.01	472	472	15	533	15
cvc5-cvc5-xyz ^ne	469 (base +0)	22490.48	22550.01	469	469	18	533	18
Yices2	453	3879.70	3936.34	453	453	34	533	34
z3-BooledASS ^ne	430 (base +0)	8384.50	8437.67	430	430	57	533	57
SMT-RAT	427	17108.79	17163.56	427	427	60	533	60
Xolver	272	3167.18	3201.08	272	272	215	533	203
SMTInterpol	171	422.64	172.50	171	171	316	533	0
Z3-GEX-base ⁿ	473	12426.10	12486.05	473	473	14	533	14
Z3-siri-base ⁿ	472	12505.22	12565.59	472	472	15	533	15
cvc5-cvc5-xyz-base ⁿ	469	22471.86	22531.67	469	469	18	533	18
Z3-alpha2-base ⁿ	455	10233.11	10290.62	455	455	32	533	16
z3-BooledASS-base ⁿ	430	8379.00	8432.37	430	430	57	533	57

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained
Z3-GEX ^ne	894 (base +109)	3254.07	1416.11	894	462	432	0	126
Z3-alpha2 ^ne	869 (base +93)	2201.53	2234.99	869	445	424	0	151
Yices2	868	549.54	657.38	868	436	432	0	152
Z3-alpha2-debug ⁿ	867	5273.19	4469.99	867	445	422	0	153
cvc5	826	869.46	971.98	826	410	416	0	194
cvc5-cvc5-xyz ^ne	820 (base -1)	879.69	980.83	820	408	412	0	200
Z3-siri ^ne	783 (base -1)	1005.41	1103.15	783	438	345	0	237
z3-BooledASS ^ne	777 (base +1)	897.65	992.86	777	434	343	0	243
SMT-RAT	758	1025.08	1119.45	758	388	370	0	262
Xolver	482	690.87	750.59	482	223	259	23	515
SMTInterpol	171	422.64	172.50	171	0	171	831	18
cvc5-cvc5-xyz-base ⁿ	821	907.83	1009.68	821	409	412	0	199
Z3-GEX-base ⁿ	785	998.15	1095.62	785	439	346	0	235
Z3-siri-base ⁿ	784	991.56	1089.43	784	439	345	0	236
z3-BooledASS-base ⁿ	776	879.05	974.32	776	433	343	0	244
Z3-alpha2-base ⁿ	776	909.12	1005.30	776	433	343	0	244

SMT-COMP 2026