QF_ABV (Single Query Track)

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

Page generated on 2023-07-06 16:04:54 +0000

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

Winners

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

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
Bitwuzla	0	1324	15092.356	14971.484	1324	817	507	17	17	0
Bitwuzla Fixedn	0	1323	14873.013	14816.766	1323	817	506	18	18	0
Yices2	0	1315	19713.922	19702.315	1315	814	501	26	26	0
2022-Bitwuzlan	0	1296	10747.611	10668.912	1296	790	506	45	16	0
cvc5	0	1238	26222.376	26076.371	1238	770	468	103	103	0
UltimateIntBlastingWrapper+SMTInterpol	1	483	49863.699	41358.427	483	299	184	858	788	0
Z3-Owl Fixedn	2	1233	42406.998	42462.421	1233	761	472	108	105	0
Z3-Owl	285	1029	6211.749	6411.543	1029	807	222	312	14	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
Bitwuzla	0	1324	15092.356	14971.484	1324	817	507	17	17	0
Bitwuzla Fixedn	0	1323	14873.013	14816.766	1323	817	506	18	18	0
Yices2	0	1315	19713.922	19702.315	1315	814	501	26	26	0
2022-Bitwuzlan	0	1296	10747.611	10668.912	1296	790	506	45	16	0
cvc5	0	1238	26222.376	26076.371	1238	770	468	103	103	0
UltimateIntBlastingWrapper+SMTInterpol	1	484	51103.529	42549.677	484	300	184	857	787	0
Z3-Owl Fixedn	2	1233	42406.998	42462.421	1233	761	472	108	105	0
Z3-Owl	285	1029	6211.749	6411.543	1029	807	222	312	14	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
Bitwuzla Fixedn	0	817	6085.398	6070.623	817	817	0	2	522	18	0
Bitwuzla	0	817	6102.084	6097.685	817	817	0	2	522	17	0
Yices2	0	814	8432.453	8420.738	814	814	0	5	522	26	0
2022-Bitwuzlan	0	790	6148.914	6072.504	790	790	0	29	522	16	0
cvc5	0	770	13376.717	13336.357	770	770	0	49	522	103	0
UltimateIntBlastingWrapper+SMTInterpol	1	300	41474.438	35220.387	300	300	0	519	522	787	0
Z3-Owl Fixedn	2	761	21831.644	21882.248	761	761	0	58	522	105	0
Z3-Owl	285	807	4260.169	4454.006	807	807	0	12	522	14	0

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
Bitwuzla	0	507	8990.272	8873.799	507	0	507	15	819	17	0
2022-Bitwuzlan	0	506	4598.697	4596.408	506	0	506	16	819	16	0
Bitwuzla Fixedn	0	506	8787.614	8746.143	506	0	506	16	819	18	0
Yices2	0	501	11281.469	11281.577	501	0	501	21	819	26	0
Z3-Owl Fixedn	0	472	20575.354	20580.173	472	0	472	50	819	105	0
cvc5	0	468	12845.659	12740.015	468	0	468	54	819	103	0
Z3-Owl	0	222	1951.58	1957.537	222	0	222	300	819	14	0
UltimateIntBlastingWrapper+SMTInterpol	0	184	9629.091	7329.29	184	0	184	338	819	787	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
Bitwuzla	0	1258	4280.023	4243.216	1258	785	473	83	83	0
Bitwuzla Fixedn	0	1255	4242.41	4184.1	1255	785	470	86	86	0
Yices2	0	1246	1482.366	1468.734	1246	786	460	95	95	0
2022-Bitwuzlan	0	1235	1137.253	1134.327	1235	749	486	106	77	0
cvc5	0	982	1758.902	1740.686	982	678	304	359	359	0
UltimateIntBlastingWrapper+SMTInterpol	0	375	5571.356	2067.52	375	212	163	966	907	0
Z3-Owl Fixedn	2	1066	2222.494	2207.206	1066	690	376	275	273	0
Z3-Owl	282	987	1874.768	1911.976	987	773	214	354	61	0

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