QF_LIA (Single Query Track)

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

Page generated on 2022-08-10 11:17:45 +0000

Benchmarks: 6219
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++	OpenSMT	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	6130	140043.783	118346.02	6130	3934	2196	89	80	9
MathSATn	0	5958	553315.545	553075.922	5958	3832	2126	261	261	0
OpenSMT	0	5944	652049.605	651755.096	5944	3770	2174	275	269	0
cvc5	0	5883	714348.079	714223.408	5883	3764	2119	336	335	0
Yices2	0	5794	573550.856	573562.693	5794	3675	2119	425	425	0
Z3++	0	5756	767677.447	771051.335	5756	3846	1910	463	434	10
smtinterpol	0	5734	879776.132	802314.108	5734	3580	2154	485	485	0
z3-4.8.17n	0	5661	886152.571	885787.336	5661	3801	1860	558	553	5
veriT	0	4218	2011885.057	2011878.961	4218	2984	1234	2001	1589	1

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
2019-Par4n	0	6148	157760.723	109860.898	6148	3948	2200	71	62	9
MathSATn	0	5958	553347.845	553065.482	5958	3832	2126	261	261	0
OpenSMT	0	5944	652078.445	651746.156	5944	3770	2174	275	269	0
cvc5	0	5883	714386.799	714211.528	5883	3764	2119	336	335	0
Yices2	0	5794	573586.896	573549.653	5794	3675	2119	425	425	0
Z3++	0	5756	767734.517	771033.045	5756	3846	1910	463	434	10
smtinterpol	0	5739	881456.452	800949.122	5739	3580	2159	480	480	0
z3-4.8.17n	0	5661	886222.851	885764.586	5661	3801	1860	558	553	5
veriT	0	4218	2012010.187	2011819.481	4218	2984	1234	2001	1589	1

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	3948	87536.025	49461.107	3948	3948	0	25	2246	62	9
Z3++	0	3846	233702.734	235083.052	3846	3846	0	127	2246	434	10
MathSATn	0	3832	272245.712	272069.988	3832	3832	0	141	2246	261	0
z3-4.8.17n	0	3801	289109.916	288871.546	3801	3801	0	172	2246	553	5
OpenSMT	0	3770	468636.104	468478.726	3770	3770	0	203	2246	269	0
cvc5	0	3764	403213.167	403136.037	3764	3764	0	209	2246	335	0
Yices2	0	3675	413697.322	413666.344	3675	3675	0	298	2246	425	0
smtinterpol	0	3580	616031.878	592734.794	3580	3580	0	393	2246	480	0
veriT	0	2984	865084.879	864890.676	2984	2984	0	989	2246	1589	1

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	2200	35424.698	25599.791	2200	0	2200	17	4002	62	9
OpenSMT	0	2174	148642.341	148467.431	2174	0	2174	43	4002	269	0
smtinterpol	0	2159	230624.574	173414.328	2159	0	2159	58	4002	480	0
MathSATn	0	2126	246302.133	246195.494	2126	0	2126	91	4002	261	0
Yices2	0	2119	125089.573	125083.309	2119	0	2119	98	4002	425	0
cvc5	0	2119	276373.632	276275.491	2119	0	2119	98	4002	335	0
Z3++	0	1910	504969.617	505865.179	1910	0	1910	307	4002	434	10
z3-4.8.17n	0	1860	562312.935	562093.039	1860	0	1860	357	4002	553	5
veriT	0	1234	1112125.307	1112128.804	1234	0	1234	983	4002	1589	1

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	6055	12134.983	7124.107	6055	3872	2183	164	155	9
Yices2	0	5574	19127.999	19129.302	5574	3495	2079	645	645	0
MathSATn	0	4824	39496.037	39325.86	4824	3285	1539	1395	1395	0
z3-4.8.17n	0	4781	42766.789	42565.543	4781	3348	1433	1438	1433	5
Z3++	0	4711	43768.222	43697.012	4711	3325	1386	1508	1497	10
OpenSMT	0	4562	48072.266	47962.402	4562	2927	1635	1657	1651	0
cvc5	0	4417	49972.982	49864.096	4417	3032	1385	1802	1802	0
smtinterpol	0	4389	67997.942	54319.341	4389	2915	1474	1830	1830	0
veriT	0	3909	51076.631	51007.979	3909	2825	1084	2310	1979	1

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