QF_LRA (Single Query Track)

Competition results for the QF_LRA logic in the Single Query Track.

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

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

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24s Performance (parallel)
OpenSMT	OpenSMT	OpenSMT	OpenSMT	OpenSMT

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
OpenSMT	0	554	24449.972	24416.327	554	320	234	24	24	0
cvc5	0	535	37122.853	37274.362	535	308	227	43	43	0
2021-Yices2n	0	534	32857.658	32813.124	534	311	223	44	44	0
2022-Yices2n	0	534	32989.221	32916.507	534	311	223	44	44	0
Yices2	0	534	34496.122	34486.394	534	311	223	44	44	0
SMTInterpol	0	472	68336.862	59562.986	472	284	188	106	106	0
Yaga	0	408	31066.564	31072.422	408	243	165	170	170	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
OpenSMT	0	554	24449.972	24416.327	554	320	234	24	24	0
cvc5	0	535	37122.853	37274.362	535	308	227	43	43	0
2021-Yices2n	0	534	32857.658	32813.124	534	311	223	44	44	0
2022-Yices2n	0	534	32989.221	32916.507	534	311	223	44	44	0
Yices2	0	534	34496.122	34486.394	534	311	223	44	44	0
SMTInterpol	0	475	72929.062	62961.246	475	286	189	103	103	0
Yaga	0	408	31066.564	31072.422	408	243	165	170	170	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
OpenSMT	0	320	16532.127	16518.654	320	320	0	15	243	24	0
2021-Yices2n	0	311	14507.811	14508.34	311	311	0	24	243	44	0
2022-Yices2n	0	311	14647.97	14626.063	311	311	0	24	243	44	0
Yices2	0	311	14988.869	14991.223	311	311	0	24	243	44	0
cvc5	0	308	21183.376	21323.483	308	308	0	27	243	43	0
SMTInterpol	0	286	39092.038	34695.28	286	286	0	49	243	103	0
Yaga	0	243	18681.405	18684.858	243	243	0	92	243	170	0

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
OpenSMT	0	234	7917.845	7897.673	234	0	234	6	338	24	0
cvc5	0	227	15939.477	15950.879	227	0	227	13	338	43	0
2022-Yices2n	0	223	18341.251	18290.444	223	0	223	17	338	44	0
2021-Yices2n	0	223	18349.846	18304.784	223	0	223	17	338	44	0
Yices2	0	223	19507.253	19495.171	223	0	223	17	338	44	0
SMTInterpol	0	189	33837.024	28265.966	189	0	189	51	338	103	0
Yaga	0	165	12385.159	12387.564	165	0	165	75	338	170	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
OpenSMT	0	428	1518.776	1481.885	428	239	189	150	150	0
2021-Yices2n	0	414	1027.288	1003.152	414	258	156	164	164	0
2022-Yices2n	0	414	1056.694	1004.351	414	258	156	164	164	0
Yices2	0	413	1027.701	1014.194	413	258	155	165	165	0
cvc5	0	350	1238.821	1234.779	350	206	144	228	228	0
Yaga	0	292	830.658	831.445	292	175	117	286	286	0
SMTInterpol	0	273	2904.035	1213.326	273	174	99	305	305	0

n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.