QF_Equality+Bitvec (Single Query Track)

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

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

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

Logics:

• QF_ABV : 1830 benchmarks
• QF_AUFBV : 38 benchmarks
• QF_UFBV : 300 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	2116	67450.111	67447.508	2116	1317	799	52	0	37	0
2020-Bitwuzlan	0	2108	66425.303	66440.853	2108	1317	791	60	0	36	0
Yices2	0	2078	158041.811	158045.617	2078	1312	766	90	0	90	0
z3-4.8.17n	0	2017	235105.34	235063.73	2017	1253	764	151	0	150	0
cvc5	0	2014	233887.285	238340.269	2014	1259	755	154	0	154	0
MathSATn	0	2011	234170.64	234192.474	2011	1260	751	157	0	152	5

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Bitwuzla	0	2116	67456.391	67445.868	2116	1317	799	52	0	37	0
2020-Bitwuzlan	0	2108	66430.063	66439.283	2108	1317	791	60	0	36	0
Yices2	0	2078	158052.771	158042.587	2078	1312	766	90	0	90	0
z3-4.8.17n	0	2017	235131.58	235057.18	2017	1253	764	151	0	150	0
cvc5	0	2014	238221.866	238331.869	2014	1259	755	154	0	154	0
MathSATn	0	2011	234201.91	234184.834	2011	1260	751	157	0	152	5

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
2020-Bitwuzlan	0	1317	13733.51	13739.41	1317	1317	0	12	839	36	0
Bitwuzla	0	1317	14760.689	14748.317	1317	1317	0	12	839	37	0
Yices2	0	1312	31410.653	31396.974	1312	1312	0	17	839	90	0
MathSATn	0	1260	95231.649	95219.105	1260	1260	0	69	839	152	5
cvc5	0	1259	101600.645	101758.198	1259	1259	0	70	839	154	0
z3-4.8.17n	0	1253	115008.607	114984.008	1253	1253	0	76	839	150	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	799	47895.702	47897.551	799	0	799	36	1333	37	0
2020-Bitwuzlan	0	791	47896.553	47899.873	791	0	791	44	1333	36	0
Yices2	0	766	121842.118	121845.613	766	0	766	69	1333	90	0
z3-4.8.17n	0	764	116253.972	116204.158	764	0	764	71	1333	150	0
cvc5	0	755	131821.221	131773.671	755	0	755	80	1333	154	0
MathSATn	0	751	134170.261	134165.729	751	0	751	84	1333	152	5

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	1955	6728.887	6713.752	1955	1244	711	213	0	198	0
2020-Bitwuzlan	0	1947	6567.669	6571.506	1947	1238	709	221	0	197	0
Yices2	0	1939	7087.71	7070.217	1939	1264	675	229	0	229	0
MathSATn	0	1836	10796.865	10769.898	1836	1187	649	332	0	327	5
z3-4.8.17n	0	1813	10391.838	10368.236	1813	1167	646	355	0	355	0
cvc5	0	1811	13701.506	13623.614	1811	1169	642	357	0	357	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.