SMT-COMP 2024

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2024

Biggest Lead Ranking - Single Query Track

Page generated on 2024-07-08

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
cvc5cvc5cvc5cvc5cvc5

Sequential Performance

DivisionSolverCorrect ScoreTime Score
Equality_MachineArithcvc52.4234140.273547
Equality_NonLinearArithcvc51.6993231.430003
Equalitycvc51.6031160.346443
Equality_LinearArithcvc51.3171722.659134
QF_NonLinearIntArithZ3-alpha1.1402360.288477
QF_Equality_NonLinearArithYices21.1356382.282715
QF_FPArithBitwuzla1.1063832.535239
Bitveccvc51.0648040.482954
QF_StringsZ3-Noodler1.05706227.656317
Arithcvc51.0454220.063012
FPArithBitwuzla1.042491.114266
QF_DatatypesAlgaroba1.0214071.466151
QF_Equality_LinearArithSMTInterpol1.0208450.701218
QF_NonLinearRealArithZ3-alpha1.0089642.005491
QF_Equality_BitvecBitwuzla1.0088041.772492
QF_LinearRealArithOpenSMT1.0078640.816145
QF_LinearIntArithOpenSMT1.0064950.859468
QF_BitvecBitwuzla1.0000951.242485
QF_EqualityYices212.450318

Parallel Performance

DivisionSolverCorrect ScoreTime Score
Equality_MachineArithcvc52.4234140.273824
Equality_NonLinearArithcvc52.184760.079809
Equalitycvc51.4834610.254512
Equality_LinearArithcvc51.2474572.786645
QF_NonLinearIntArithZ3-alpha1.1402360.290182
QF_Equality_NonLinearArithYices21.1356382.278922
QF_FPArithBitwuzla1.1063832.522017
Bitveccvc51.0648040.484345
QF_StringsZ3-Noodler1.05706225.051391
Arithcvc51.0454220.065625
FPArithBitwuzla1.042491.113379
QF_Equality_LinearArithSMTInterpol1.0264790.846474
QF_DatatypesAlgaroba1.0214071.46591
QF_NonLinearRealArithZ3-alpha1.0089641.999977
QF_Equality_BitvecBitwuzla1.0088041.752739
QF_LinearRealArithOpenSMT1.0078640.816576
QF_LinearIntArithOpenSMT1.0064950.859668
QF_BitvecBitwuzla1.0000951.240664
QF_EqualityYices212.147915

SAT Performance

DivisionSolverCorrect ScoreTime Score
Equality_NonLinearArithcvc59.0117650.006928
Equalitycvc52.0671640.031408
Equality_MachineArithcvc51.5714290.093123
Equality_LinearArithcvc51.397260.006351
QF_Equality_NonLinearArithYices21.229731.992379
FPArithBitwuzla1.1089491.728558
QF_NonLinearIntArithZ3-alpha1.0937456.747529
QF_StringsZ3-Noodler1.06744635.718979
QF_Equality_LinearArithSMTInterpol1.067210.702407
QF_FPArithBitwuzla1.0534481.545209
ArithYicesQS1.0449642.813061
QF_NonLinearRealArithZ3-alpha1.0410860.603506
BitvecBitwuzla1.0381363.600894
QF_Datatypescvc51.0165290.522524
QF_LinearRealArithOpenSMT1.0142180.452013
QF_LinearIntArithZ3-alpha1.0054041.869282
QF_Equality_BitvecBitwuzla1.0025921.530426
QF_BitvecSTP1.0024451.1071
QF_EqualityYices211.386241

UNSAT Performance

DivisionSolverCorrect ScoreTime Score
Equality_MachineArithcvc52.4427240.434441
Equality_NonLinearArithcvc51.3511391.90971
QF_DatatypesZ3-alpha1.3317760.707804
Equalitycvc51.3114041.731495
QF_Equality_NonLinearArithcvc51.2656250.197926
Equality_LinearArithcvc51.1669793.826325
QF_FPArithBitwuzla1.1432013.129052
QF_NonLinearIntArithZ3-alpha1.1376460.327164
Arithcvc51.1073580.029848
Bitveccvc51.0796990.608053
QF_NonLinearRealArithcvc51.0236390.479048
QF_Equality_BitvecBitwuzla1.0225781.875746
FPArithBitwuzla1.0129530.576907
QF_LinearRealArithcvc51.0116280.810103
QF_LinearIntArithcvc51.0090740.66585
QF_StringsZ3-Noodler1.0086616.351717
QF_Equality_LinearArithOpenSMT1.0037930.590017
QF_BitvecBitwuzla1.0023341.542147
QF_EqualityYices212.350283

24 seconds Performance

DivisionSolverCorrect ScoreTime Score
Equality_MachineArithcvc52.3128210.767823
Equality_NonLinearArithcvc51.8710772.819624
QF_DatatypesAlgaroba1.532110.485893
Equality_LinearArithcvc51.3482993.021138
QF_Equality_NonLinearArithYices21.2287821.070505
QF_LinearIntArithYices21.2183571.323832
Equalitycvc51.1890243.920408
QF_FPArithBitwuzla1.1346151.219901
QF_StringsZ3-Noodler1.127191.594997
ArithYicesQS1.1095241.285809
BitvecYicesQS1.0784811.69936
QF_LinearRealArithYices21.0582521.242084
QF_NonLinearIntArithYices21.0312662.372563
QF_NonLinearRealArithYices21.0270161.379349
FPArithBitwuzla1.0222791.298062
QF_Equality_BitvecYices21.0076091.252626
QF_EqualityYices21.0049972.16344
QF_BitvecBitwuzla1.0035920.636515
QF_Equality_LinearArithYices21.0023654.622515