QF_Equality+Bitvec (Single Query Track)

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

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

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

Logics:

• QF_ABV : 2880 benchmarks
• QF_AUFBV : 41 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
2020-Bitwuzlan	0	3168	61845.826	61807.232	3168	2095	1073	53	0	30	0
Bitwuzla	0	3168	87441.499	87369.389	3168	2094	1074	53	0	38	0
2020-Yices2n	0	3132	159266.862	159292.16	3132	2093	1039	89	0	89	0
2020-Yices2-fixedn	0	3132	159917.698	159885.159	3132	2093	1039	89	0	89	0
Yices2	0	3128	159776.613	159751.534	3128	2093	1035	93	0	93	0
MathSAT5n	0	3067	231362.214	231437.963	3067	2045	1022	154	0	153	1
z3n	0	3047	251226.948	251294.57	3047	2027	1020	174	0	174	0
cvc5	0	3042	240953.738	267667.433	3042	2020	1022	179	0	179	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
2020-Bitwuzlan	0	3168	61849.836	61805.812	3168	2095	1073	53	0	30	0
Bitwuzla	0	3168	87446.399	87368.099	3168	2094	1074	53	0	38	0
2020-Yices2n	0	3132	159277.492	159288.67	3132	2093	1039	89	0	89	0
2020-Yices2-fixedn	0	3132	159928.558	159881.629	3132	2093	1039	89	0	89	0
Yices2	0	3128	159784.393	159748.504	3128	2093	1035	93	0	93	0
MathSAT5n	0	3067	231474.284	231430.743	3067	2045	1022	154	0	153	1
z3n	0	3047	251309.848	251286.86	3047	2027	1020	174	0	174	0
cvc5	0	3042	267544.514	267659.383	3042	2020	1022	179	0	179	0

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	2095	11777.402	11758.503	2095	2095	0	9	1117	30	0
Bitwuzla	0	2094	11699.235	11634.489	2094	2094	0	10	1117	38	0
2020-Yices2n	0	2093	27298.751	27300.796	2093	2093	0	11	1117	89	0
2020-Yices2-fixedn	0	2093	27397.449	27393.972	2093	2093	0	11	1117	89	0
Yices2	0	2093	27464.966	27477.042	2093	2093	0	11	1117	93	0
MathSAT5n	0	2045	84797.618	84786.679	2045	2045	0	59	1117	153	1
z3n	0	2027	106766.483	106738.766	2027	2027	0	77	1117	174	0
cvc5	0	2020	116714.068	116833.232	2020	2020	0	84	1117	179	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	1074	70947.164	70933.609	1074	0	1074	39	2108	38	0
2020-Bitwuzlan	0	1073	45272.435	45247.31	1073	0	1073	40	2108	30	0
2020-Yices2n	0	1039	127178.741	127187.874	1039	0	1039	74	2108	89	0
2020-Yices2-fixedn	0	1039	127731.109	127687.658	1039	0	1039	74	2108	89	0
Yices2	0	1035	127519.427	127471.462	1035	0	1035	78	2108	93	0
MathSAT5n	0	1022	141876.666	141844.064	1022	0	1022	91	2108	153	1
cvc5	0	1022	146030.446	146026.152	1022	0	1022	91	2108	179	0
z3n	0	1020	139743.365	139748.094	1020	0	1020	93	2108	174	0

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	3004	6840.692	6789.064	3004	2029	975	217	0	202	0
2020-Bitwuzlan	0	3002	6631.569	6634.803	3002	2023	979	219	0	196	0
2020-Yices2-fixedn	0	2985	7236.469	7234.425	2985	2040	945	236	0	236	0
2020-Yices2n	0	2985	7232.054	7235.545	2985	2040	945	236	0	236	0
Yices2	0	2985	7242.18	7256.884	2985	2040	945	236	0	236	0
MathSAT5n	0	2893	10763.888	10710.986	2893	1971	922	328	0	327	1
z3n	0	2866	10768.995	10739.066	2866	1953	913	355	0	355	0
cvc5	0	2838	14342.347	14244.26	2838	1928	910	383	0	383	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.