SMT-COMP 2024

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2024

Biggest Lead Ranking - Model Validation Track

Page generated on 2024-07-08

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
SMTInterpolSMTInterpolSMTInterpol-Yices2

Sequential Performance

DivisionSolverCorrect ScoreTime Score
QF_DatatypesSMTInterpol1.3970811.068508
QF_NonLinearIntArithYices21.2863153.587279
QF_NonLinearRealArithSMT-RAT1.2503790.455465
QF_Equality_NonLinearArithcvc51.1655630.845419
QF_ADT_BitVecBitwuzla1.05437621.368207
QF_ADT_LinArithSMTInterpol1.0532064.341208
QF_Equality_LinearArithOpenSMT1.0197222.142144
QF_LinearRealArithOpenSMT1.0154640.278057
QF_LinearIntArithOpenSMT1.0050780.488718
QF_Equality_BitvecYices21.0026110.35351
QF_BitvecSTP1.0014691.003336
QF_FPArithcvc51.0008220.584413
QF_EqualityOpenSMT11.266637

Parallel Performance

DivisionSolverCorrect ScoreTime Score
QF_DatatypesSMTInterpol1.3993860.995698
QF_NonLinearIntArithYices21.2863153.562623
QF_NonLinearRealArithSMT-RAT1.2503790.458443
QF_Equality_NonLinearArithcvc51.1655630.686088
QF_ADT_BitVecBitwuzla1.05437619.69604
QF_ADT_LinArithSMTInterpol1.0532066.624121
QF_LinearRealArithOpenSMT1.0154640.280329
QF_Equality_LinearArithOpenSMT1.0138411.336485
QF_LinearIntArithOpenSMT1.0050780.489563
QF_Equality_BitvecYices21.0026110.358111
QF_BitvecSTP1.0014691.003269
QF_FPArithcvc51.0008220.663964
QF_EqualityOpenSMT11.196066

SAT Performance

DivisionSolverCorrect ScoreTime Score
QF_DatatypesSMTInterpol1.3993860.995698
QF_NonLinearIntArithYices21.2863153.562623
QF_NonLinearRealArithSMT-RAT1.2503790.458443
QF_Equality_NonLinearArithcvc51.1655630.686088
QF_ADT_BitVecBitwuzla1.05437619.69604
QF_ADT_LinArithSMTInterpol1.0532066.624121
QF_LinearRealArithOpenSMT1.0154640.280329
QF_Equality_LinearArithOpenSMT1.0138411.336485
QF_LinearIntArithOpenSMT1.0050780.489563
QF_Equality_BitvecYices21.0026110.358111
QF_BitvecSTP1.0014691.003269
QF_FPArithcvc51.0008220.663964
QF_EqualityOpenSMT11.196066

24 seconds Performance

DivisionSolverCorrect ScoreTime Score
QF_NonLinearIntArithYices21.5822221.236011
QF_DatatypesSMTInterpol1.4962410.622119
QF_Equality_NonLinearArithcvc51.2533940.989898
QF_ADT_BitVecBitwuzla1.2444183.518218
QF_NonLinearRealArithSMT-RAT1.2442711.185209
QF_LinearIntArithYices21.1390461.518656
QF_ADT_LinArithSMTInterpol1.1179940.647366
QF_LinearRealArithYices21.0707271.199011
QF_Equality_BitvecYices21.0248621.329869
QF_Equality_LinearArithOpenSMT1.016231.068294
QF_BitvecSTP1.0042290.899381
QF_EqualityOpenSMT11.196066
QF_FPArithcvc50.9993010.852216