SMT-COMP 2024

The International Satisfiability Modulo Theories (SMT) Competition.

SMT-COMP 2024

Largest Contribution Ranking - Unsat Core 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_Equality_Bitvec	Yices2	0.021395	0.007555
QF_Equality_Bitvec	cvc5	0.014733	0.018494
QF_Equality_LinearArith	Yices2	0.003829	0.001854
QF_Equality_LinearArith	OpenSMT	0.002458	-0.003951
QF_Equality	Yices2	0.001718	0.022762
QF_LinearIntArith	cvc5	0.000537	-0.000388
QF_Equality_Bitvec	Bitwuzla	0.000536	0.00425
QF_Equality	cvc5	0.000233	0.000739
QF_Equality	SMTInterpol	0.000177	0
QF_LinearIntArith	Yices2	0.000165	0.010551
QF_Equality_LinearArith	cvc5	0.000156	0.00022
QF_LinearIntArith	OpenSMT	0.000154	-0.001545
QF_Equality	plat-smt	0.000132	0.00231
QF_Equality	OpenSMT	0.000113	0.024802
QF_Equality_LinearArith	SMTInterpol	0.000102	-0.000219
QF_LinearIntArith	SMTInterpol	0.000101	0.005519
QF_LinearRealArith	OpenSMT	5.7e-05	0.003635
QF_LinearRealArith	Yices2	2.3e-05	0.000192
QF_LinearRealArith	SMTInterpol	1e-05	0

Parallel Performance

Division	Solver	Correct Score	Time Score
QF_Equality_Bitvec	Yices2	0.021395	0.00744
QF_Equality_Bitvec	cvc5	0.014733	0.018279
QF_Equality_LinearArith	Yices2	0.003829	0.001092
QF_Equality_LinearArith	OpenSMT	0.002416	-0.002579
QF_Equality	Yices2	0.001718	0.020765
QF_LinearIntArith	cvc5	0.000537	-0.008795
QF_Equality_Bitvec	Bitwuzla	0.000536	0.004182
QF_Equality	cvc5	0.000233	0.000665
QF_Equality	SMTInterpol	0.000177	0
QF_LinearIntArith	Yices2	0.000165	0.009732
QF_Equality_LinearArith	cvc5	0.000156	0.000144
QF_LinearIntArith	OpenSMT	0.000154	-0.002089
QF_Equality	plat-smt	0.000132	0.002087
QF_Equality	OpenSMT	0.000113	0.022934
QF_Equality_LinearArith	SMTInterpol	0.000102	-4.1e-05
QF_LinearIntArith	SMTInterpol	0.000101	0.008287
QF_LinearRealArith	OpenSMT	5.7e-05	0.003609
QF_LinearRealArith	Yices2	2.3e-05	0.000192
QF_LinearRealArith	SMTInterpol	1e-05	0

UNSAT Performance

Division	Solver	Correct Score	Time Score
QF_Equality_Bitvec	Yices2	0.021395	0.00744
QF_Equality_Bitvec	cvc5	0.014733	0.018279
QF_Equality_LinearArith	Yices2	0.003829	0.001092
QF_Equality_LinearArith	OpenSMT	0.002416	-0.002579
QF_Equality	Yices2	0.001718	0.020765
QF_LinearIntArith	cvc5	0.000537	-0.008795
QF_Equality_Bitvec	Bitwuzla	0.000536	0.004182
QF_Equality	cvc5	0.000233	0.000665
QF_Equality	SMTInterpol	0.000177	0
QF_LinearIntArith	Yices2	0.000165	0.009732
QF_Equality_LinearArith	cvc5	0.000156	0.000144
QF_LinearIntArith	OpenSMT	0.000154	-0.002089
QF_Equality	plat-smt	0.000132	0.002087
QF_Equality	OpenSMT	0.000113	0.022934
QF_Equality_LinearArith	SMTInterpol	0.000102	-4.1e-05
QF_LinearIntArith	SMTInterpol	0.000101	0.008287
QF_LinearRealArith	OpenSMT	5.7e-05	0.003609
QF_LinearRealArith	Yices2	2.3e-05	0.000192
QF_LinearRealArith	SMTInterpol	1e-05	0

24 seconds Performance

Division	Solver	Correct Score	Time Score
QF_Equality_Bitvec	Yices2	0.042594	-0.112505
QF_Equality_LinearArith	Yices2	0.013945	-0.001734
QF_LinearIntArith	Yices2	0.006902	0.01255
QF_Equality	Yices2	0.00177	0.030807
QF_LinearRealArith	Yices2	0.001362	0.000203
QF_Equality_LinearArith	cvc5	0.001131	-0.00028
QF_Equality_Bitvec	Bitwuzla	0.000771	-6.5e-05
QF_LinearRealArith	OpenSMT	0.000709	-0.000287
QF_LinearIntArith	SMTInterpol	0.000318	-0.001083
QF_Equality_LinearArith	SMTInterpol	0.000238	-0.000993
QF_Equality	SMTInterpol	0.000183	0
QF_Equality_Bitvec	cvc5	0.000157	-0.001066
QF_Equality	plat-smt	0.000137	0.000844
QF_Equality	OpenSMT	0.000117	0.00016
QF_Equality	cvc5	0.000105	0.000291
QF_LinearRealArith	cvc5	6.6e-05	-5.4e-05
QF_LinearIntArith	OpenSMT	1.9e-05	0.002629
QF_LinearRealArith	SMTInterpol	1e-05	0
QF_Equality_LinearArith	OpenSMT	2e-06	0.000163