QF_LRA (Single Query Track)

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

Page generated on 2022-08-10 11:17:45 +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	Yices2	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	546	56831.572	56786.674	546	324	222	32	32	0
2021-Yices2n	0	537	76062.52	76020.002	537	324	213	41	41	0
Yices2	0	537	76227.401	76169.643	537	324	213	41	41	0
cvc5	0	536	91742.195	92122.457	536	317	219	42	42	0
z3-4.8.17n	0	520	108041.614	108043.282	520	318	202	58	58	0
veriT	0	497	135628.1	135603.778	497	292	205	81	81	0
smtinterpol	0	476	194600.81	185732.144	476	303	173	102	102	0
MathSATn	0	473	164662.433	164673.871	473	297	176	105	105	0
solsmt	0	160	521934.123	521951.443	160	90	70	418	205	206

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
OpenSMT	0	546	56834.782	56785.444	546	324	222	32	32	0
2021-Yices2n	0	537	76068.3	76018.322	537	324	213	41	41	0
Yices2	0	537	76230.771	76168.263	537	324	213	41	41	0
cvc5	0	536	92012.015	92120.737	536	317	219	42	42	0
z3-4.8.17n	0	520	108049.324	108040.922	520	318	202	58	58	0
veriT	0	497	135637.97	135600.888	497	292	205	81	81	0
smtinterpol	0	481	195185.43	185318.824	481	303	178	97	97	0
MathSATn	0	473	164676.603	164670.111	473	297	176	105	105	0
solsmt	0	160	521976.163	521942.173	160	90	70	418	205	206

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
Yices2	0	324	32722.197	32681.124	324	324	0	18	236	41	0
2021-Yices2n	0	324	32765.768	32726.806	324	324	0	18	236	41	0
OpenSMT	0	324	33262.743	33241.947	324	324	0	18	236	32	0
z3-4.8.17n	0	318	49141.915	49131.65	318	318	0	24	236	58	0
cvc5	0	317	52649.914	52760.163	317	317	0	25	236	42	0
smtinterpol	0	303	85701.496	81218.908	303	303	0	39	236	97	0
MathSATn	0	297	74780.615	74775.467	297	297	0	45	236	105	0
veriT	0	292	80406.55	80381.871	292	292	0	50	236	81	0
solsmt	0	90	316240.043	316206.339	90	90	0	252	236	205	206

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	222	13972.039	13943.497	222	0	222	6	350	32	0
cvc5	0	219	29762.101	29760.574	219	0	219	9	350	42	0
2021-Yices2n	0	213	33702.533	33691.517	213	0	213	15	350	41	0
Yices2	0	213	33908.574	33887.139	213	0	213	15	350	41	0
veriT	0	205	45631.42	45619.016	205	0	205	23	350	81	0
z3-4.8.17n	0	202	49307.409	49309.272	202	0	202	26	350	58	0
smtinterpol	0	178	99883.934	94499.916	178	0	178	50	350	97	0
MathSATn	0	176	80295.988	80294.644	176	0	176	52	350	105	0
solsmt	0	70	196136.12	196135.834	70	0	70	158	350	205	206

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
OpenSMT	0	444	4945.542	4919.116	444	265	179	134	134	0
Yices2	0	428	4922.349	4855.851	428	273	155	150	150	0
2021-Yices2n	0	428	4883.704	4856.591	428	273	155	150	150	0
veriT	0	343	6859.34	6817.695	343	209	134	235	235	0
z3-4.8.17n	0	342	6844.455	6829.899	342	212	130	236	236	0
cvc5	0	331	7241.185	7228.889	331	208	123	247	247	0
MathSATn	0	330	6800.229	6786.822	330	215	115	248	248	0
smtinterpol	0	278	10560.58	8551.988	278	191	87	300	300	0
solsmt	0	83	12026.268	12024.8	83	42	41	495	282	206

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