QF_NonLinearRealArith (Single Query Track)

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

Page generated on 2023-07-06 16:04:54 +0000

Benchmarks: 2795
Time Limit: 1200 seconds
Memory Limit: 60 GB

Logics:

• QF_NRA : 2795 benchmarks

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24s Performance (parallel)
Z3++	Z3++	Z3++	cvc5	cvc5

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Z3++	0	2540	64738.87	64580.634	2540	1298	1242	255	0	252	1
2019-Par4n	0	2525	60717.654	20394.74	2525	1251	1274	270	0	208	62
cvc5	0	2461	105852.553	106138.836	2461	1200	1261	334	0	334	0
cvc5-NRA-LS	0	2401	71685.803	71546.255	2401	1158	1243	394	0	5	0
Yices2	0	2334	44594.326	44499.527	2334	1144	1190	461	0	461	0
z3-alpha	0	2321	30779.786	30690.846	2321	1208	1113	474	0	345	0
SMT-RAT-MCSAT	0	2251	86525.153	86425.654	2251	1130	1121	544	0	529	13
2022-Z3++-fixedn	1	2541	66187.862	66166.712	2541	1299	1242	254	0	250	1

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
2019-Par4n	0	2550	105836.155	35494.272	2550	1269	1281	245	0	183	62
Z3++	0	2540	64738.87	64580.634	2540	1298	1242	255	0	252	1
cvc5	0	2462	107056.453	107043.662	2462	1201	1261	333	0	333	0
cvc5-NRA-LS	0	2401	71685.803	71546.255	2401	1158	1243	394	0	5	0
Yices2	0	2334	44594.326	44499.527	2334	1144	1190	461	0	461	0
z3-alpha	0	2321	30779.786	30690.846	2321	1208	1113	474	0	345	0
SMT-RAT-MCSAT	0	2251	86525.153	86425.654	2251	1130	1121	544	0	529	13
2022-Z3++-fixedn	1	2541	66187.862	66166.712	2541	1299	1242	254	0	250	1

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
2022-Z3++-fixedn	0	1299	32946.233	32923.564	1299	1299	0	84	1412	250	1
Z3++	0	1298	26033.992	25931.666	1298	1298	0	85	1412	252	1
2019-Par4n	0	1269	64823.731	21715.962	1269	1269	0	114	1412	183	62
z3-alpha	0	1208	11623.185	11590.259	1208	1208	0	175	1412	345	0
cvc5	0	1201	44690.919	44450.053	1201	1201	0	182	1412	333	0
cvc5-NRA-LS	0	1158	36394.897	36361.985	1158	1158	0	225	1412	5	0
Yices2	0	1144	18293.402	18248.366	1144	1144	0	239	1412	461	0
SMT-RAT-MCSAT	0	1130	34399.215	34388.553	1130	1130	0	253	1412	529	13

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
2019-Par4n	0	1281	41012.423	13778.31	1281	0	1281	29	1485	183	62
cvc5	0	1261	62365.534	62593.608	1261	0	1261	49	1485	333	0
cvc5-NRA-LS	0	1243	35290.906	35184.27	1243	0	1243	67	1485	5	0
Z3++	0	1242	38704.878	38648.967	1242	0	1242	68	1485	252	1
Yices2	0	1190	26300.924	26251.161	1190	0	1190	120	1485	461	0
SMT-RAT-MCSAT	0	1121	52125.938	52037.102	1121	0	1121	189	1485	529	13
z3-alpha	0	1113	19156.602	19100.586	1113	0	1113	197	1485	345	0
2022-Z3++-fixedn	1	1242	33241.629	33243.148	1242	0	1242	68	1485	250	1

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
2019-Par4n	0	2377	7495.074	2623.115	2377	1188	1189	418	0	356	62
cvc5	0	2186	2782.178	2733.827	2186	1092	1094	609	0	609	0
2022-Z3++-fixedn	0	2156	2288.065	2284.674	2156	1120	1036	639	0	638	1
Z3++	0	2156	2332.078	2326.967	2156	1120	1036	639	0	638	1
Yices2	0	2138	1138.719	1125.004	2138	1057	1081	657	0	657	0
z3-alpha	0	2130	3897.837	3897.797	2130	1140	990	665	0	665	0
cvc5-NRA-LS	0	2110	3474.944	3404.137	2110	1020	1090	685	0	685	0
SMT-RAT-MCSAT	0	1918	3041.189	2963.338	1918	1033	885	877	0	864	13

n Non-competing.
Abstained: Total of benchmarks in logics in this division that solver chose to abstain from. For SAT/UNSAT scores, this column also includes benchmarks not known to be SAT/UNSAT.