Equality+MachineArith (Single Query Track)

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

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

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

Logics:

• ABV : 169 benchmarks
• ABVFP : 30 benchmarks
• ABVFPLRA : 75 benchmarks
• AUFBV : 761 benchmarks
• AUFBVDTLIA : 742 benchmarks
• AUFBVDTNIA : 8 benchmarks
• AUFBVDTNIRA : 1062 benchmarks
• AUFBVFP : 57 benchmarks
• AUFFPDTNIRA : 159 benchmarks
• UFBV : 143 benchmarks
• UFBVFP : 2 benchmarks
• UFBVLIA : 208 benchmarks
• UFFPDTNIRA : 396 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
z3-4.8.17n	0	1460	2647289.743	2655840.309	1460	336	1124	2352	0	2128	12
cvc5	0	1385	2728354.012	2805353.604	1385	333	1052	2427	0	2148	0
2021-cvc5n	0	994	957278.171	1804299.248	994	249	745	1597	1221	1378	0
Bitwuzla	0	424	670917.812	671049.654	424	21	403	813	2575	539	0
UltimateEliminator+MathSAT	0	34	1057160.991	1047799.543	34	20	14	3778	0	840	5

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
z3-4.8.17n	0	1460	2655764.593	2655748.339	1460	336	1124	2352	0	2128	12
cvc5	0	1385	2795672.078	2805243.114	1385	333	1052	2427	0	2148	0
2021-cvc5n	0	994	1798694.083	1804225.128	994	249	745	1597	1221	1378	0
Bitwuzla	0	424	671018.952	671026.074	424	21	403	813	2575	539	0
UltimateEliminator+MathSAT	0	34	1057163.211	1047799.433	34	20	14	3778	0	840	5

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
z3-4.8.17n	0	336	222004.033	221984.356	336	336	0	190	3286	2128	12
cvc5	0	333	197600.975	201658.285	333	333	0	193	3286	2148	0
2021-cvc5n	0	249	280957.502	283684.696	249	249	0	277	3286	1378	0
Bitwuzla	0	21	113034.207	113035.605	21	21	0	231	3560	539	0
UltimateEliminator+MathSAT	0	20	87625.156	86061.619	20	20	0	506	3286	840	5

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
z3-4.8.17n	0	1124	1197772.559	1197678.154	1124	0	1124	1033	1655	2128	12
cvc5	0	1052	1354750.393	1358800.527	1052	0	1052	1105	1655	2148	0
2021-cvc5n	0	745	271140.153	272994.576	745	0	745	215	2852	1378	0
Bitwuzla	0	403	69584.291	69589.067	403	0	403	72	3337	539	0
UltimateEliminator+MathSAT	0	14	371820.731	367233.155	14	0	14	2143	1655	840	5

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
z3-4.8.17n	0	1284	61644.469	61548.803	1284	303	981	2528	0	2436	12
cvc5	0	998	68259.578	68241.748	998	88	910	2814	0	2770	0
2021-cvc5n	0	743	45061.013	45033.792	743	88	655	1848	1221	1822	0
Bitwuzla	0	312	16573.369	16576.101	312	19	293	925	2575	651	0
UltimateEliminator+MathSAT	0	29	37924.509	32339.986	29	18	11	3783	0	977	5

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.