QF_LIA (Single Query Track)

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

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

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

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24s Performance (parallel)
OpenSMT	OpenSMT	Z3++	SMTInterpol	Yices2

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
2019-Par4n	0	5118	30698.177	10664.845	5118	3225	1893	111	99	12
OpenSMT	0	4936	285996.012	285658.723	4936	3066	1870	293	289	0
cvc5	0	4895	290263.674	290125.359	4895	3056	1839	334	330	0
Yices2	0	4807	63199.736	63197.124	4807	2980	1827	422	423	0
Z3++	0	4778	229774.501	229450.323	4778	3149	1629	451	418	14
SMTInterpol	0	4753	282495.581	206748.276	4753	2883	1870	476	476	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
2019-Par4n	0	5146	94762.667	32027.202	5146	3244	1902	83	71	12
OpenSMT	0	4936	285996.012	285658.723	4936	3066	1870	293	289	0
cvc5	0	4895	290263.674	290125.359	4895	3056	1839	334	330	0
Yices2	0	4806	61999.916	61997.104	4806	2979	1827	423	423	0
Z3++	0	4778	229774.501	229450.323	4778	3149	1629	451	418	14
SMTInterpol	0	4754	283744.501	207474.941	4754	2883	1871	475	475	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
2019-Par4n	0	3244	69470.178	23421.12	3244	3244	0	38	1947	71	12
Z3++	0	3149	78476.441	78253.377	3149	3149	0	133	1947	418	14
OpenSMT	0	3066	203987.309	203815.467	3066	3066	0	216	1947	289	0
cvc5	0	3056	140554.068	140497.08	3056	3056	0	226	1947	330	0
Yices2	0	2979	52987.23	52992.59	2979	2979	0	303	1947	423	0
SMTInterpol	0	2883	140673.806	116407.564	2883	2883	0	399	1947	475	0

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
2019-Par4n	0	1902	25292.489	8606.082	1902	0	1902	15	3312	71	12
SMTInterpol	0	1871	143070.695	91067.376	1871	0	1871	46	3312	475	0
OpenSMT	0	1870	82008.704	81843.256	1870	0	1870	47	3312	289	0
cvc5	0	1839	149709.606	149628.279	1839	0	1839	78	3312	330	0
Yices2	0	1827	9012.687	9004.514	1827	0	1827	90	3312	423	0
Z3++	0	1629	151298.059	151196.946	1629	0	1629	288	3312	418	14

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
2019-Par4n	0	5039	7051.867	2775.368	5039	3154	1885	190	178	12
Yices2	0	4596	3407.644	3398.367	4596	2799	1797	633	633	0
Z3++	0	3760	7494.064	7402.04	3760	2638	1122	1469	1455	14
OpenSMT	0	3665	8211.474	8109.856	3665	2282	1383	1564	1560	0
cvc5	0	3544	4619.999	4562.803	3544	2361	1183	1685	1685	0
SMTInterpol	0	3456	23599.286	9812.805	3456	2236	1220	1773	1773	0

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