Largest Contribution Ranking - Single Query Track

Page generated on 2022-08-10 11:18:05 +0000

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24 seconds Performance (parallel)
cvc5	cvc5	cvc5	cvc5	cvc5

Sequential Performance

Solver	Correct Score	Time Score	Division
cvc5	0.02293044	0.00978661	Equality+MachineArith
cvc5	0.02197364	0.08007088	Equality+LinearArith
cvc5	0.01422021	0.02484675	Equality+NonLinearArith
cvc5	0.01013353	0.00564358	Equality
cvc5	0.00453546	0.1003793	QF_Strings
YicesQS	0.00178084	0.0263983	Arith
Bitwuzla	0.00135428	0.00675031	FPArith
Z3++	0.00094022	0.02392435	QF_LinearIntArith
SMT-RAT-MCSAT 22.06	0.000913	0.00814609	QF_NonLinearRealArith
Bitwuzla	0.00058693	0.02143423	QF_Bitvec
cvc5	0.00030775	0.00233372	QF_Equality+NonLinearArith
COLIBRI	0.0002383	0.00791574	QF_FPArith
Yices2	0.00022799	0.01028138	QF_Equality+LinearArith
Bitwuzla	0.00021442	0.00287094	Bitvec
Bitwuzla	0.00018042	0.0082733	QF_Equality+Bitvec
Yices2	0.00010827	0.00223611	QF_LinearRealArith
veriT	0.0	0.02378649	QF_Equality

Parallel Performance

Solver	Correct Score	Time Score	Division
cvc5	0.02293044	0.00975924	Equality+MachineArith
cvc5	0.01863765	0.06412353	Equality+LinearArith
cvc5	0.01162292	0.02034542	Equality+NonLinearArith
cvc5	0.00827626	0.00481218	Equality
cvc5	0.00453546	0.10099144	QF_Strings
YicesQS	0.00178084	0.02637699	Arith
Bitwuzla	0.00135428	0.00676214	FPArith
Z3++	0.00094022	0.02395678	QF_LinearIntArith
SMT-RAT-MCSAT 22.06	0.000913	0.00814995	QF_NonLinearRealArith
Bitwuzla	0.000587	0.02144062	QF_Bitvec
cvc5	0.00030775	0.00234814	QF_Equality+NonLinearArith
COLIBRI	0.0002383	0.00791845	QF_FPArith
Yices2	0.00022799	0.01012272	QF_Equality+LinearArith
Bitwuzla	0.00019655	0.00277585	Bitvec
Bitwuzla	0.00018042	0.00827495	QF_Equality+Bitvec
Yices2	0.00010827	0.0021968	QF_LinearRealArith
veriT	0.0	0.0236945	QF_Equality

SAT Performance

Solver	Correct Score	Time Score	Division
cvc5	0.1685148	0.00893539	Equality+LinearArith
cvc5	0.03438715	0.00250079	Equality+NonLinearArith
cvc5	0.02840936	0.00218083	Equality+MachineArith
cvc5	0.01442777	0.00142316	Equality
cvc5	0.00590496	0.01339416	QF_Strings
YicesQS	0.00237769	0.00152893	Arith
Bitwuzla	0.00225681	0.00079922	FPArith
Bitwuzla	0.00146084	0.00082241	QF_Bitvec
Z3++	0.00082287	0.00078177	QF_NonLinearRealArith
Z3++	0.000818	0.00149372	QF_LinearIntArith
Bitwuzla	0.00032325	0.00010942	Bitvec
smtinterpol	0.00031997	0.00066628	QF_Equality+NonLinearArith
Bitwuzla	0.00016607	0.00030415	QF_Equality+Bitvec
Yices2	0.00015835	0.00036162	QF_LinearRealArith
smtinterpol	0.00010599	0.00010089	QF_Equality+LinearArith
COLIBRI	4.818e-05	7.553e-05	QF_FPArith
Yices2	0.0	1.64e-06	QF_Equality

UNSAT Performance

Solver	Correct Score	Time Score	Division
cvc5	0.01876725	0.00636699	Equality+MachineArith
Z3++	0.0090453	0.00401385	QF_NonLinearIntArith
cvc5	0.00780429	0.012038	Equality+NonLinearArith
cvc5	0.00471552	0.00211145	Equality
cvc5	0.00458981	0.01596357	Equality+LinearArith
OSTRICH	0.00163314	0.00066081	QF_Strings
YicesQS	0.00123626	0.00195113	Arith
Z3++	0.00101593	0.0006139	QF_LinearIntArith
cvc5	0.00087951	0.00026868	QF_Equality+NonLinearArith
Bitwuzla	0.00087942	0.00155703	FPArith
SMT-RAT-MCSAT 22.06	0.00045094	0.00032699	QF_NonLinearRealArith
Yices2	0.00043342	0.00048042	QF_Equality+LinearArith
COLIBRI	0.00031876	0.00061364	QF_FPArith
Yices2	0.00028065	0.00047489	QF_Bitvec
Yices2	0.00021898	0.00012838	QF_Equality+Bitvec
Bitwuzla	0.00013019	0.00028952	Bitvec
OpenSMT	7.371e-05	0.00018547	QF_LinearRealArith
veriT	0.0	1.629e-05	QF_Equality

24s Performance

Solver	Correct Score	Time Score	Division
cvc5	0.02410528	0.02480675	Equality+NonLinearArith
cvc5	0.01998829	0.00643714	Equality+MachineArith
Vampire	0.01978803	0.00893529	Equality
Yices2	0.01184931	0.06553996	QF_LinearIntArith
cvc5	0.00962355	0.03141742	Equality+LinearArith
Z3++	0.00935787	0.01605178	QF_NonLinearIntArith
cvc5	0.00790622	0.08892742	QF_Strings
YicesQS	0.0026162	0.02288083	Arith
Bitwuzla	0.00155748	0.00479638	FPArith
Bitwuzla	0.00097344	0.01372932	QF_Bitvec
Yices2	0.00075469	0.00445278	QF_NonLinearRealArith
COLIBRI	0.00070545	0.00628567	QF_FPArith
Yices2	0.00060445	0.00215568	QF_LinearRealArith
Bitwuzla	0.00043256	0.00416881	QF_Equality+Bitvec
smtinterpol	0.00040399	0.00170196	QF_Equality+NonLinearArith
Yices2	0.00034961	0.00587208	QF_Equality+LinearArith
Bitwuzla	0.00028858	0.00293861	Bitvec
Yices2	2.481e-05	0.02349606	QF_Equality

n Non-competing.
e Experimental.