QF_Equality+LinearArith (Single Query Track)

Competition results for the QF_Equality+LinearArith division in the Single Query Track.

Page generated on 2021-07-18 17:29:06 +0000

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

Logics:

• QF_ALIA : 116 benchmarks
• QF_AUFLIA : 558 benchmarks
• QF_UFDTLIRA : 146 benchmarks
• QF_UFIDL : 300 benchmarks
• QF_UFLIA : 300 benchmarks
• QF_UFLRA : 541 benchmarks

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24s Performance (parallel)
SMTInterpol	SMTInterpol	SMTInterpol	cvc5	SMTInterpol

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
SMTInterpol	0	1902	93061.969	83843.958	1902	1053	849	59	0	50	0
cvc5 - fixedn	0	1887	128239.471	128254.724	1887	1037	850	74	0	74	0
cvc5	0	1884	126774.948	132087.677	1884	1033	851	77	0	77	0
z3n	0	1751	101147.535	101123.215	1751	952	799	64	146	64	0
Yices2	0	1750	97692.72	97709.034	1750	955	795	65	146	65	0
MathSAT5n	0	1735	115621.521	115629.253	1735	932	803	80	146	80	0
veriT	0	1064	140520.755	140525.427	1064	604	460	751	146	89	0
2019-Yices 2.6.2n	0	912	96049.713	96059.792	912	391	521	62	987	62	0
2019-SMTInterpoln	0	539	5163.662	3823.686	539	326	213	2	1420	2	0
mc2	0	522	1326.472	1326.805	522	314	208	19	1420	0	0
2018-Yicesn	0	300	67.685	64.858	300	238	62	0	1661	0	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
SMTInterpol	0	1903	93094.459	83733.758	1903	1053	850	58	0	49	0
cvc5 - fixedn	0	1887	128249.131	128251.384	1887	1037	850	74	0	74	0
cvc5	0	1884	132085.57	132084.847	1884	1033	851	77	0	77	0
z3n	0	1751	101154.325	101120.345	1751	952	799	64	146	64	0
Yices2	0	1750	97699.14	97707.224	1750	955	795	65	146	65	0
MathSAT5n	0	1735	115635.191	115625.303	1735	932	803	80	146	80	0
veriT	0	1064	140527.095	140522.797	1064	604	460	751	146	89	0
2019-Yices 2.6.2n	0	912	96055.123	96057.902	912	391	521	62	987	62	0
2019-SMTInterpoln	0	539	5163.662	3823.686	539	326	213	2	1420	2	0
mc2	0	522	1326.472	1326.805	522	314	208	19	1420	0	0
2018-Yicesn	0	300	67.685	64.858	300	238	62	0	1661	0	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
SMTInterpol	0	1053	11566.389	8032.457	1053	1053	0	7	901	49	0
cvc5 - fixedn	0	1037	40980.528	40982.638	1037	1037	0	23	901	74	0
cvc5	0	1033	45022.275	45023.494	1033	1033	0	27	901	77	0
Yices2	0	955	38481.393	38486.725	955	955	0	25	981	65	0
z3n	0	952	39344.989	39311.048	952	952	0	28	981	64	0
MathSAT5n	0	932	59735.726	59729.967	932	932	0	48	981	80	0
veriT	0	604	47802.545	47797.842	604	604	0	376	981	89	0
2019-Yices 2.6.2n	0	391	37551.49	37553.531	391	391	0	24	1546	62	0
2019-SMTInterpoln	0	326	2947.918	2101.65	326	326	0	1	1634	2	0
mc2	0	314	832.002	832.218	314	314	0	13	1634	0	0
2018-Yicesn	0	238	5.873	6.184	238	238	0	0	1723	0	0

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
cvc5	0	851	85863.295	85861.353	851	0	851	49	1061	77	0
SMTInterpol	0	850	80328.07	74501.301	850	0	850	50	1061	49	0
cvc5 - fixedn	0	850	86068.603	86068.746	850	0	850	50	1061	74	0
MathSAT5n	0	803	54699.464	54695.336	803	0	803	31	1127	80	0
z3n	0	799	60609.335	60609.297	799	0	799	35	1127	64	0
Yices2	0	795	58017.747	58020.499	795	0	795	39	1127	65	0
2019-Yices 2.6.2n	0	521	58503.634	58504.371	521	0	521	38	1402	62	0
veriT	0	460	91524.55	91524.955	460	0	460	374	1127	89	0
2019-SMTInterpoln	0	213	1015.744	522.036	213	0	213	0	1748	2	0
mc2	0	208	408.103	408.216	208	0	208	5	1748	0	0
2018-Yicesn	0	62	61.813	58.673	62	0	62	0	1899	0	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
SMTInterpol	0	1815	10459.008	6194.297	1815	1022	793	146	0	137	0
cvc5	0	1756	6125.254	6117.826	1756	990	766	205	0	205	0
cvc5 - fixedn	0	1756	6127.676	6123.359	1756	990	766	205	0	205	0
Yices2	0	1706	2920.859	2927.131	1706	932	774	109	146	109	0
z3n	0	1689	3804.127	3796.163	1689	927	762	126	146	126	0
MathSAT5n	0	1662	4722.883	4709.945	1662	918	744	153	146	153	0
veriT	0	962	6600.287	6593.074	962	526	436	853	146	213	0
2019-Yices 2.6.2n	0	869	2714.726	2715.176	869	369	500	105	987	105	0
2019-SMTInterpoln	0	531	1960.273	892.372	531	321	210	10	1420	10	0
mc2	0	521	502.539	502.759	521	314	207	20	1420	13	0
2018-Yicesn	0	299	54.979	52.148	299	238	61	1	1661	1	0

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.