Equality+LinearArith (Single Query Track)

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

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

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

Logics:

• ALIA : 19 benchmarks
• AUFDTLIA : 147 benchmarks
• AUFDTLIRA : 5520 benchmarks
• AUFLIA : 1638 benchmarks
• AUFLIRA : 1683 benchmarks
• UFDTLIA : 277 benchmarks
• UFDTLIRA : 3900 benchmarks
• UFIDL : 20 benchmarks
• UFLIA : 2848 benchmarks
• UFLRA : 7 benchmarks

Winners

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

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
2020-CVC4n	0	12789	2198545.037	2229197.995	12789	267	12522	3270	0	1719	0
cvc5 - fixedn	0	12658	1172128.091	2361091.31	12658	229	12429	3401	0	1886	0
cvc5	0	12640	1164296.04	2378711.969	12640	224	12416	3419	0	1905	0
Vampire	0	11894	5770393.631	5169278.179	11894	110	11784	4165	0	4112	0
Vampire - fixedn	0	11846	5699209.151	5101574.686	11846	108	11738	4213	0	4048	0
2020-z3n	0	4208	1964563.826	1969487.123	4208	188	4020	2007	9844	1336	20
z3n	0	4143	2005979.983	2015193.445	4143	190	3953	2072	9844	1362	18
veriT	0	4118	2311610.571	2311793.807	4118	0	4118	2097	9844	1809	75
2019-Par4n	0	3261	1572421.056	1556656.598	3261	63	3198	1290	11508	1245	45
iProver	0	3251	4639943.481	4575799.433	3251	0	3251	3801	9007	3748	45
SMTInterpol	0	2798	3943483.185	3932124.114	2798	96	2702	3417	9844	3221	0
2018-CVC4n	0	1320	353668.453	361479.018	1320	143	1177	465	14274	256	0
2019-CVC4n	0	197	198426.842	204478.296	197	0	197	80	15782	80	0
UltimateEliminator+MathSAT	0	60	94277.917	74897.359	60	15	45	6155	9844	28	2
2018-Z3n	0	24	3656.063	3656.703	24	4	20	2	16033	2	0
2020-Vampiren	14	12353	4788854.112	4261475.426	12353	104	12249	3706	0	3356	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
2020-CVC4n	0	12789	2226187.067	2229115.295	12789	267	12522	3270	0	1728	0
cvc5 - fixedn	0	12658	2359173.718	2360990.77	12658	229	12429	3401	0	1886	0
cvc5	0	12640	2376849.306	2378613.589	12640	224	12416	3419	0	1905	0
Vampire	0	12169	6123549.751	4959419.122	12169	110	12059	3890	0	3800	0
Vampire - fixedn	0	12083	6029972.931	4930900.188	12083	108	11975	3976	0	3775	0
2020-z3n	0	4208	1966733.116	1969429.863	4208	188	4020	2007	9844	1346	20
z3n	0	4143	2009114.623	2015133.815	4143	190	3953	2072	9844	1362	18
veriT	0	4118	2311830.951	2311701.497	4118	0	4118	2097	9844	1808	75
iProver	0	3325	4745136.931	4535983.447	3325	0	3325	3727	9007	3674	45
2019-Par4n	0	3280	1583409.106	1545192.443	3280	65	3215	1271	11508	1226	45
SMTInterpol	0	2801	4045606.255	3903347.559	2801	96	2705	3414	9844	3145	0
2018-CVC4n	0	1320	360739.893	361468.448	1320	143	1177	465	14274	256	0
2019-CVC4n	0	197	202450.312	204473.486	197	0	197	80	15782	80	0
UltimateEliminator+MathSAT	0	60	94277.917	74897.359	60	15	45	6155	9844	28	2
2018-Z3n	0	24	3656.443	3656.663	24	4	20	2	16033	2	0
2020-Vampiren	14	12485	5022665.732	4128823.666	12485	104	12381	3574	0	3150	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
2020-CVC4n	0	267	127517.451	128094.656	267	267	0	119	15673	1728	0
cvc5 - fixedn	0	229	162025.165	162362.644	229	229	0	157	15673	1886	0
cvc5	0	224	166539.821	166903.445	224	224	0	162	15673	1905	0
z3n	0	190	71897.722	71898.282	190	190	0	64	15805	1362	18
2020-z3n	0	188	68035.058	68036.263	188	188	0	66	15805	1346	20
2018-CVC4n	0	143	57621.393	57992.731	143	143	0	132	15784	256	0
Vampire	0	110	349179.606	332182.365	110	110	0	276	15673	3800	0
Vampire - fixedn	0	108	338220.568	332187.049	108	108	0	278	15673	3775	0
2020-Vampiren	0	104	326004.742	321846.45	104	104	0	282	15673	3150	0
SMTInterpol	0	96	95315.096	95121.098	96	96	0	158	15805	3145	0
2019-Par4n	0	65	5406.579	2837.636	65	65	0	1	15993	1226	45
UltimateEliminator+MathSAT	0	15	2397.603	1572.943	15	15	0	239	15805	28	2
2018-Z3n	0	4	3655.216	3655.434	4	4	0	2	16053	2	0
2019-CVC4n	0	0	0.0	0.0	0	0	0	0	16059	80	0
iProver	0	0	63601.575	63602.292	0	0	0	56	16003	3674	45
veriT	0	0	124465.909	124465.675	0	0	0	254	15805	1808	75

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
2020-CVC4n	0	12522	371050.295	373379.509	12522	0	12522	827	2710	1728	0
cvc5 - fixedn	0	12429	461331.291	462799.978	12429	0	12429	920	2710	1886	0
cvc5	0	12416	474465.275	475848.91	12416	0	12416	933	2710	1905	0
Vampire	0	12059	2923511.585	1839222.365	12059	0	12059	1290	2710	3800	0
Vampire - fixedn	0	11975	2863350.563	1809960.43	11975	0	11975	1374	2710	3775	0
veriT	0	4118	602309.744	602203.921	4118	0	4118	473	11468	1808	75
2020-z3n	0	4020	584349.729	585124.021	4020	0	4020	571	11468	1346	20
z3n	0	3953	653956.826	655967.594	3953	0	3953	638	11468	1362	18
iProver	0	3325	2565935.356	2356781.155	3325	0	3325	1908	10826	3674	45
2019-Par4n	0	3215	144002.527	108354.807	3215	0	3215	75	12769	1226	45
SMTInterpol	0	2705	2358306.434	2290795.236	2705	0	2705	1886	11468	3145	0
2018-CVC4n	0	1177	93747.574	94104.275	1177	0	1177	158	14724	256	0
2019-CVC4n	0	197	118450.312	120473.486	197	0	197	10	15852	80	0
UltimateEliminator+MathSAT	0	45	69394.931	55859.032	45	0	45	4546	11468	28	2
2018-Z3n	0	20	1.227	1.229	20	0	20	0	16039	2	0
2020-Vampiren	14	12381	1883945.29	1024735.503	12381	0	12381	968	2710	3150	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
cvc5	0	12227	59087.82	59054.118	12227	179	12048	3832	0	2344	0
cvc5 - fixedn	0	12226	59126.696	59078.162	12226	179	12047	3833	0	2345	0
2020-CVC4n	0	12183	59650.653	59643.018	12183	178	12005	3876	0	2361	0
Vampire	0	10391	162813.025	145811.733	10391	100	10291	5668	0	5668	0
Vampire - fixedn	0	10299	162726.246	145844.129	10299	98	10201	5760	0	5666	0
2020-z3n	0	4094	52445.386	52444.784	4094	185	3909	2121	9844	2087	20
veriT	0	4030	50802.887	50798.527	4030	0	4030	2185	9844	1925	75
z3n	0	4009	54371.569	54370.656	4009	186	3823	2206	9844	2171	18
2019-Par4n	0	3192	34432.399	33469.061	3192	62	3130	1359	11508	1314	45
iProver	0	3073	116544.627	102390.161	3073	0	3073	3979	9007	3930	45
SMTInterpol	0	2608	89953.086	85810.541	2608	96	2512	3607	9844	3430	0
2018-CVC4n	0	1318	11374.132	11369.42	1318	142	1176	467	14274	459	0
UltimateEliminator+MathSAT	0	60	37575.162	22494.247	60	15	45	6155	9844	105	2
2019-CVC4n	0	26	6053.864	6053.854	26	0	26	251	15782	251	0
2018-Z3n	0	22	113.959	113.963	22	2	20	4	16033	4	0
2020-Vampiren	13	10343	174141.507	152322.138	10343	100	10243	5716	0	5572	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.