SMT-COMP 2024

The International Satisfiability Modulo Theories (SMT) Competition.

SMT-COMP 2024

Largest Contribution Ranking - Model Validation Track

Page generated on 2024-07-08

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24 seconds Performance (parallel)
Yices2	Yices2	Yices2	-	Yices2

Sequential Performance

Division	Solver	Correct Score	Time Score
QF_NonLinearIntArith	Yices2	0.021408	0.056533
QF_NonLinearRealArith	SMT-RAT	0.007896	-0.000364
QF_ADT_BitVec	Bitwuzla	0.00463	0.107268
QF_NonLinearIntArith	cvc5	0.003282	-0.015906
QF_LinearIntArith	OpenSMT	0.001566	0.00525
QF_LinearIntArith	cvc5	0.001247	0.046596
QF_NonLinearRealArith	cvc5	0.001099	0.017369
QF_LinearIntArith	SMTInterpol	0.000812	-0.009409
QF_LinearIntArith	Yices2	0.000638	0.080433
QF_Bitvec	Bitwuzla	0.00031	0.044374
QF_Equality_LinearArith	OpenSMT	0.000301	0.019186
QF_LinearRealArith	OpenSMT	0.00018	-0.000328
QF_ADT_BitVec	cvc5	0.000129	0.009433
QF_Bitvec	STP	0.000103	0.046151
QF_LinearRealArith	Yices2	9e-05	0.008729
QF_Equality_Bitvec	Yices2	5.8e-05	0.005665
QF_NonLinearRealArith	SMTInterpol	4.1e-05	-0.004266
QF_Bitvec	Yices2	3.4e-05	0.031249
QF_Bitvec	cvc5	3.4e-05	0.002216

Parallel Performance

Division	Solver	Correct Score	Time Score
QF_NonLinearIntArith	Yices2	0.021408	0.05637
QF_NonLinearRealArith	SMT-RAT	0.007896	-0.000505
QF_ADT_BitVec	Bitwuzla	0.00463	0.10655
QF_NonLinearIntArith	cvc5	0.003282	-0.016024
QF_LinearIntArith	OpenSMT	0.001564	0.005071
QF_LinearIntArith	cvc5	0.001246	0.046117
QF_NonLinearRealArith	cvc5	0.001099	0.01731
QF_LinearIntArith	SMTInterpol	0.000927	-0.005109
QF_LinearIntArith	Yices2	0.000637	0.075384
QF_Bitvec	Bitwuzla	0.00031	0.043516
QF_Equality_LinearArith	OpenSMT	0.00027	0.017358
QF_LinearRealArith	OpenSMT	0.00018	-0.000944
QF_ADT_BitVec	cvc5	0.000129	0.004092
QF_Bitvec	STP	0.000103	0.045303
QF_LinearRealArith	Yices2	9e-05	0.008692
QF_Equality_LinearArith	SMTInterpol	6e-05	0.006655
QF_Equality_Bitvec	Yices2	5.8e-05	0.005503
QF_NonLinearRealArith	SMTInterpol	4.1e-05	-0.003418
QF_Bitvec	Yices2	3.4e-05	0.030645

SAT Performance

Division	Solver	Correct Score	Time Score
QF_NonLinearIntArith	Yices2	0.021408	0.05637
QF_NonLinearRealArith	SMT-RAT	0.007896	-0.000505
QF_ADT_BitVec	Bitwuzla	0.00463	0.10655
QF_NonLinearIntArith	cvc5	0.003282	-0.016024
QF_LinearIntArith	OpenSMT	0.001564	0.005071
QF_LinearIntArith	cvc5	0.001246	0.046117
QF_NonLinearRealArith	cvc5	0.001099	0.01731
QF_LinearIntArith	SMTInterpol	0.000927	-0.005109
QF_LinearIntArith	Yices2	0.000637	0.075384
QF_Bitvec	Bitwuzla	0.00031	0.043516
QF_Equality_LinearArith	OpenSMT	0.00027	0.017358
QF_LinearRealArith	OpenSMT	0.00018	-0.000944
QF_ADT_BitVec	cvc5	0.000129	0.004092
QF_Bitvec	STP	0.000103	0.045303
QF_LinearRealArith	Yices2	9e-05	0.008692
QF_Equality_LinearArith	SMTInterpol	6e-05	0.006655
QF_Equality_Bitvec	Yices2	5.8e-05	0.005503
QF_NonLinearRealArith	SMTInterpol	4.1e-05	-0.003418
QF_Bitvec	Yices2	3.4e-05	0.030645

24 seconds Performance

Division	Solver	Correct Score	Time Score
QF_NonLinearIntArith	Yices2	0.033595	0.017361
QF_ADT_BitVec	Bitwuzla	0.02205	0.080164
QF_LinearIntArith	Yices2	0.015045	0.065342
QF_NonLinearRealArith	SMT-RAT	0.008043	-0.008035
QF_LinearIntArith	cvc5	0.004056	0.012151
QF_NonLinearIntArith	cvc5	0.003856	0.001539
QF_Bitvec	STP	0.002136	0.000913
QF_LinearIntArith	OpenSMT	0.001665	-0.007189
QF_Bitvec	Bitwuzla	0.001611	0.016357
QF_NonLinearRealArith	cvc5	0.001489	-0.015313
QF_Equality_LinearArith	OpenSMT	0.001256	-0.011039
QF_Bitvec	Yices2	0.001226	0.063456
QF_LinearRealArith	Yices2	0.00101	0.003909
QF_LinearIntArith	SMTInterpol	0.000484	-0.006345
QF_Equality_Bitvec	Yices2	0.000475	0.001945
QF_Equality_LinearArith	SMTInterpol	0.000408	-0.00435
QF_Bitvec	cvc5	0.000385	0.008001
QF_Equality_Bitvec	Bitwuzla	0.000238	-0.001781
QF_LinearRealArith	OpenSMT	0.000228	3.7e-05