SMT-COMP 2024

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2024

Biggest Lead Ranking - Unsat Core Track

Page generated on 2024-07-08

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
cvc5cvc5-cvc5cvc5

Sequential Performance

DivisionSolverCorrect ScoreTime Score
QF_NonLinearRealArithcvc516950.000154
Equality_MachineArithcvc5476.4074070.151354
QF_NonLinearIntArithcvc543.3855020.008912
Arithcvc535.1250.273844
QF_Datatypescvc59.7078521.133863
Bitveccvc52.1142862.530031
Equalitycvc51.57405913.517844
QF_Equality_LinearArithYices21.5076971.26466
Equality_NonLinearArithcvc51.4911390.376125
QF_Equality_NonLinearArithcvc51.4022390.597741
Equality_LinearArithcvc51.2457174.903751
QF_Equality_Bitveccvc51.1480570.707893
QF_EqualityYices21.11720.985014
QF_BitvecBitwuzla1.1044390.497548
QF_LinearRealArithOpenSMT1.0729052.389696
FPArithBitwuzla1.043.642815
QF_FPArithBitwuzla1.0151433.380306
QF_LinearIntArithSMTInterpol1.0038630.374635

Parallel Performance

DivisionSolverCorrect ScoreTime Score
QF_NonLinearRealArithcvc516950.000143
Equality_MachineArithcvc5476.4074070.148141
QF_NonLinearIntArithcvc543.3855020.004754
Arithcvc535.1250.199452
QF_Datatypescvc56.3420441.339198
Bitveccvc52.1142862.485118
Equalitycvc51.56427111.071479
QF_Equality_LinearArithYices21.5076971.264036
Equality_NonLinearArithcvc51.4911290.264779
QF_Equality_NonLinearArithcvc51.4022390.403152
Equality_LinearArithcvc51.2443444.050839
QF_Equality_Bitveccvc51.1480570.710824
QF_EqualityYices21.1163794.868116
QF_BitvecBitwuzla1.1044390.499129
QF_LinearRealArithOpenSMT1.0729052.385878
FPArithBitwuzla1.043.08071
QF_FPArithBitwuzla1.0151432.97441
QF_LinearIntArithSMTInterpol1.0040760.502156

UNSAT Performance

DivisionSolverCorrect ScoreTime Score
QF_NonLinearRealArithcvc516950.000143
Equality_MachineArithcvc5476.4074070.148141
QF_NonLinearIntArithcvc543.3855020.004754
Arithcvc535.1250.199452
QF_Datatypescvc56.3420441.339198
Bitveccvc52.1142862.485118
Equalitycvc51.56427111.071479
QF_Equality_LinearArithYices21.5076971.264036
Equality_NonLinearArithcvc51.4911290.264779
QF_Equality_NonLinearArithcvc51.4022390.403152
Equality_LinearArithcvc51.2443444.050839
QF_Equality_Bitveccvc51.1480570.710824
QF_EqualityYices21.1163794.868116
QF_BitvecBitwuzla1.1044390.499129
QF_LinearRealArithOpenSMT1.0729052.385878
FPArithBitwuzla1.043.08071
QF_FPArithBitwuzla1.0151432.97441
QF_LinearIntArithSMTInterpol1.0040760.502156

24 seconds Performance

DivisionSolverCorrect ScoreTime Score
QF_NonLinearRealArithcvc511360.001896
Equality_MachineArithcvc5461.3150680.019431
Arithcvc532.750.712802
QF_NonLinearIntArithcvc57.7821780.015576
QF_Equality_LinearArithYices26.2892631.251539
QF_DatatypesSMTInterpol6.2440940.309175
QF_Equality_BitvecYices24.3480780.311001
Bitveccvc52.1142860.982364
Equalitycvc51.8136053.817632
QF_LinearIntArithYices21.5673661.175136
Equality_NonLinearArithcvc51.4832072.090929
Equality_LinearArithcvc51.2656843.03393
QF_Equality_NonLinearArithSMTInterpol1.1582510.791444
QF_EqualityYices21.1186662.17006
QF_LinearRealArithYices21.1136891.32032
QF_BitvecYices21.0631111.541569
FPArithBitwuzla1.043.08071
QF_FPArithBitwuzla1.0277291.487998