SMT-COMP 2024

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2024

Largest Contribution Ranking - Model Validation Track

Page generated on 2024-07-08

Winners

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

Sequential Performance

DivisionSolverCorrect ScoreTime Score
QF_NonLinearIntArithYices20.0177410.04685
QF_NonLinearRealArithSMT-RAT0.007074-0.010048
QF_ADT_BitVecBitwuzla0.0038370.088895
QF_NonLinearIntArithcvc50.00272-0.013181
QF_LinearIntArithOpenSMT0.0012980.004351
QF_LinearIntArithcvc50.0010330.038615
QF_Equality_NonLinearArithcvc50.0010220.00038
QF_LinearIntArithSMTInterpol0.000673-0.007798
QF_NonLinearRealArithcvc50.0005910.005975
QF_Equality_NonLinearArithSMTInterpol0.0005840.002248
QF_LinearIntArithYices20.0005290.066656
QF_BitvecBitwuzla0.0002570.036774
QF_Equality_LinearArithOpenSMT0.0002490.0159
QF_LinearRealArithOpenSMT0.00015-0.000272
QF_NonLinearRealArithYices20.0001150.017733
QF_ADT_BitVeccvc50.0001070.007818
QF_BitvecSTP8.6e-050.038246
QF_LinearRealArithYices27.5e-050.007234
QF_Equality_NonLinearArithYices26.1e-050.003221

Parallel Performance

DivisionSolverCorrect ScoreTime Score
QF_NonLinearIntArithYices20.0177410.046715
QF_NonLinearRealArithSMT-RAT0.007074-0.010001
QF_ADT_BitVecBitwuzla0.0038370.0883
QF_NonLinearIntArithcvc50.00272-0.01328
QF_LinearIntArithOpenSMT0.0012970.004203
QF_LinearIntArithcvc50.0010320.038218
QF_Equality_NonLinearArithcvc50.0010220.00035
QF_LinearIntArithSMTInterpol0.000768-0.004234
QF_NonLinearRealArithcvc50.0005910.005813
QF_Equality_NonLinearArithSMTInterpol0.0005840.002812
QF_LinearIntArithYices20.0005280.062471
QF_BitvecBitwuzla0.0002570.036063
QF_Equality_LinearArithOpenSMT0.0002240.014385
QF_LinearRealArithOpenSMT0.00015-0.000783
QF_NonLinearRealArithYices20.0001150.016933
QF_ADT_BitVeccvc50.0001070.003391
QF_BitvecSTP8.6e-050.037543
QF_LinearRealArithYices27.5e-050.007203
QF_Equality_NonLinearArithYices26.1e-050.003342

SAT Performance

DivisionSolverCorrect ScoreTime Score
QF_NonLinearIntArithYices20.0177410.046715
QF_NonLinearRealArithSMT-RAT0.007074-0.010001
QF_ADT_BitVecBitwuzla0.0038370.0883
QF_NonLinearIntArithcvc50.00272-0.01328
QF_LinearIntArithOpenSMT0.0012970.004203
QF_LinearIntArithcvc50.0010320.038218
QF_Equality_NonLinearArithcvc50.0010220.00035
QF_LinearIntArithSMTInterpol0.000768-0.004234
QF_NonLinearRealArithcvc50.0005910.005813
QF_Equality_NonLinearArithSMTInterpol0.0005840.002812
QF_LinearIntArithYices20.0005280.062471
QF_BitvecBitwuzla0.0002570.036063
QF_Equality_LinearArithOpenSMT0.0002240.014385
QF_LinearRealArithOpenSMT0.00015-0.000783
QF_NonLinearRealArithYices20.0001150.016933
QF_ADT_BitVeccvc50.0001070.003391
QF_BitvecSTP8.6e-050.037543
QF_LinearRealArithYices27.5e-050.007203
QF_Equality_NonLinearArithYices26.1e-050.003342

24 seconds Performance

DivisionSolverCorrect ScoreTime Score
QF_NonLinearIntArithYices20.027840.014387
QF_ADT_BitVecBitwuzla0.0182730.066433
QF_LinearIntArithYices20.0124680.05415
QF_NonLinearRealArithSMT-RAT0.007083-0.009207
QF_LinearIntArithcvc50.0033610.010069
QF_NonLinearIntArithcvc50.0031950.001276
QF_BitvecSTP0.001770.000756
QF_LinearIntArithOpenSMT0.00138-0.005957
QF_BitvecBitwuzla0.0013350.013555
QF_Equality_NonLinearArithcvc50.001225-0.000308
QF_Equality_LinearArithOpenSMT0.001041-0.009148
QF_BitvecYices20.0010160.052587
QF_LinearRealArithYices20.0008370.00324
QF_Equality_NonLinearArithSMTInterpol0.000706-0.000227
QF_NonLinearRealArithcvc50.0007-0.003616
QF_Equality_NonLinearArithYices20.000576-0.000482
QF_NonLinearRealArithYices20.0005330.003357
QF_LinearIntArithSMTInterpol0.000401-0.005258
QF_Equality_BitvecYices20.0003940.001612