Equality+MachineArith (Single Query Track)

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

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

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

Logics:

• ABV : 169 benchmarks
• ABVFP : 30 benchmarks
• ABVFPLRA : 75 benchmarks
• AUFBV : 761 benchmarks
• AUFBVDTLIA : 842 benchmarks
• AUFBVDTNIA : 1 benchmarks
• AUFBVFP : 57 benchmarks
• AUFFPDTLIRA : 132 benchmarks
• UFBV : 143 benchmarks
• UFBVFP : 2 benchmarks
• UFBVLIA : 208 benchmarks
• UFFPDTLIRA : 381 benchmarks
• UFFPDTNIRA : 21 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
cvc5	0	1165	998180.158	1854513.694	1165	242	923	1657	0	1422	0
cvc5 - fixedn	0	1153	962542.62	1859009.154	1153	235	918	1669	0	1424	0
2020-CVC4n	0	985	601599.311	617306.436	985	258	727	808	1029	432	0
z3n	0	310	825181.219	827144.574	310	107	203	763	1749	646	10
2020-z3n	0	147	164325.721	164347.253	147	60	87	165	2510	131	0
2018-Z3n	0	106	45221.546	45229.165	106	34	72	37	2679	36	0
UltimateEliminator+MathSAT	0	31	1086812.502	1082236.838	31	20	11	1414	1377	861	6

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
cvc5	0	1165	1849169.384	1854430.554	1165	242	923	1657	0	1422	0
cvc5 - fixedn	0	1153	1853416.404	1858923.324	1153	235	918	1669	0	1424	0
2020-CVC4n	0	985	613497.101	617284.756	985	258	727	808	1029	432	0
z3n	0	310	826577.999	827117.574	310	107	203	763	1749	646	10
2020-z3n	0	147	164341.561	164342.113	147	60	87	165	2510	131	0
2018-Z3n	0	106	45226.966	45227.585	106	34	72	37	2679	36	0
UltimateEliminator+MathSAT	0	31	1086886.292	1082219.408	31	20	11	1414	1377	859	6

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	258	73263.62	76389.425	258	258	0	84	2480	432	0
cvc5	0	242	186196.746	188508.879	242	242	0	174	2406	1422	0
cvc5 - fixedn	0	235	193349.477	195478.458	235	235	0	181	2406	1424	0
z3n	0	107	13159.486	13159.961	107	107	0	11	2704	646	10
2020-z3n	0	60	4789.427	4788.804	60	60	0	4	2758	131	0
2018-Z3n	0	34	2971.38	2971.558	34	34	0	2	2786	36	0
UltimateEliminator+MathSAT	0	20	67144.915	66091.64	20	20	0	151	2651	859	6

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
cvc5	0	923	135089.184	136275.926	923	0	923	91	1808	1422	0
cvc5 - fixedn	0	918	139953.789	141077.653	918	0	918	96	1808	1424	0
2020-CVC4n	0	727	37132.15	37615.686	727	0	727	72	2023	432	0
z3n	0	203	118696.143	118661.505	203	0	203	95	2524	646	10
2020-z3n	0	87	25581.371	25581.49	87	0	87	22	2713	131	0
2018-Z3n	0	72	14723.815	14723.838	72	0	72	12	2738	36	0
UltimateEliminator+MathSAT	0	11	210256.018	209068.205	11	0	11	319	2492	859	6

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
cvc5 - fixedn	0	915	45680.425	45678.932	915	87	828	1907	0	1856	0
cvc5	0	915	45688.719	45683.936	915	87	828	1907	0	1856	0
2020-CVC4n	0	717	18857.669	18858.606	717	66	651	1076	1029	765	0
z3n	0	242	19953.148	19952.279	242	91	151	831	1749	784	10
2020-z3n	0	134	4191.824	4190.819	134	55	79	178	2510	163	0
2018-Z3n	0	94	1257.607	1257.622	94	26	68	49	2679	49	0
UltimateEliminator+MathSAT	0	27	26532.029	25376.181	27	18	9	1418	1377	970	6

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.