QF_Equality+Bitvec (Single Query Track)

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

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

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

Logics:

• QF_ABV : 1341 benchmarks
• QF_AUFBV : 38 benchmarks
• QF_UFBV : 300 benchmarks
• QF_UFBVDT : 76 benchmarks

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	Abstained	Timeout	Memout
Bitwuzla	0	1641	37488.466	37312.01	1641	1010	631	38	76	37	0
Bitwuzla Fixedn	0	1640	37261.165	37191.259	1640	1010	630	39	76	38	0
2022-Bitwuzlan	0	1602	23750.751	23670.478	1602	978	624	77	76	32	1
Yices2	0	1590	57168.083	57138.996	1590	995	595	89	76	89	0
cvc5	0	1545	71784.017	71588.833	1545	972	573	210	0	199	9
Z3-Owl Fixedn	2	1316	48789.278	48849.557	1316	808	508	363	76	199	0
UltimateIntBlastingWrapper+SMTInterpol	3	497	54166.313	45090.752	497	309	188	1258	0	1019	1
Z3-Owl	295	1271	47988.607	48196.816	1271	965	306	408	76	100	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Bitwuzla	0	1641	37488.466	37312.01	1641	1010	631	38	76	37	0
Bitwuzla Fixedn	0	1640	37261.165	37191.259	1640	1010	630	39	76	38	0
2022-Bitwuzlan	0	1602	23750.751	23670.478	1602	978	624	77	76	32	1
Yices2	0	1590	57168.083	57138.996	1590	995	595	89	76	89	0
cvc5	0	1545	71784.017	71588.833	1545	972	573	210	0	199	9
Z3-Owl Fixedn	2	1316	48789.278	48849.557	1316	808	508	363	76	199	0
UltimateIntBlastingWrapper+SMTInterpol	3	499	56628.693	47445.032	499	311	188	1256	0	1016	1
Z3-Owl	295	1271	47988.607	48196.816	1271	965	306	408	76	100	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Bitwuzla	0	1010	22082.316	22079.535	1010	1010	0	9	736	37	0
Bitwuzla Fixedn	0	1010	22106.272	22096.658	1010	1010	0	9	736	38	0
Yices2	0	995	23735.162	23704.311	995	995	0	24	736	89	0
2022-Bitwuzlan	0	978	11969.547	11889.593	978	978	0	41	736	32	1
cvc5	0	972	37862.398	37777.535	972	972	0	90	693	199	9
Z3-Owl Fixedn	2	808	26038.104	26091.913	808	808	0	211	736	199	0
UltimateIntBlastingWrapper+SMTInterpol	3	311	46885.182	40084.954	311	311	0	751	693	1016	1
Z3-Owl	295	965	27791.669	27990.057	965	965	0	54	736	100	0

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Bitwuzla	0	631	15406.15	15232.475	631	0	631	18	1106	37	0
Bitwuzla Fixedn	0	630	15154.893	15094.601	630	0	630	19	1106	38	0
2022-Bitwuzlan	0	624	11781.204	11780.885	624	0	624	25	1106	32	1
Yices2	0	595	33432.921	33434.685	595	0	595	54	1106	89	0
cvc5	0	573	33921.619	33811.298	573	0	573	82	1100	199	9
Z3-Owl Fixedn	0	508	22751.174	22757.644	508	0	508	141	1106	199	0
Z3-Owl	0	306	20196.937	20206.758	306	0	306	343	1106	100	0
UltimateIntBlastingWrapper+SMTInterpol	0	188	9743.511	7360.078	188	0	188	467	1100	1016	1

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Bitwuzla	0	1455	5122.558	5084.169	1455	909	546	224	76	224	0
Bitwuzla Fixedn	0	1451	5079.899	5001.429	1451	909	542	228	76	228	0
Yices2	0	1444	1905.747	1870.89	1444	933	511	235	76	235	0
2022-Bitwuzlan	0	1442	1915.952	1908.58	1442	886	556	237	76	192	1
cvc5	0	1146	2820.528	2779.329	1146	799	347	609	0	600	9
UltimateIntBlastingWrapper+SMTInterpol	0	381	5754.866	2122.372	381	214	167	1374	0	1200	1
Z3-Owl Fixedn	2	1129	2428.856	2413.901	1129	728	401	550	76	483	0
Z3-Owl	286	1122	2570.86	2606.361	1122	869	253	557	76	260	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.