SMT-COMP 2024

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2024

Largest Contribution 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_LinearArithcvc50.0141140.037274
Equality_MachineArithcvc50.004619-0.013513
QF_NonLinearIntArithZ3-alpha0.004550.035187
Equalitycvc50.003519-0.010586
Equality_MachineArithBitwuzla0.001660.00026
QF_Stringscvc50.001278-0.131284
QF_LinearIntArithZ3-alpha0.001091-0.006994
QF_NonLinearIntArithcvc50.001003-0.033074
QF_NonLinearIntArithYices20.0009890.030697
QF_FPArithBitwuzla0.0009720.00313
Arithcvc50.000861-0.126032
ArithYicesQS0.0008440.004269
Equality_LinearArithiProver v3.90.0006170.000399
QF_StringsZ3-Noodler0.0005980.248282
QF_BitvecSTP0.0004650.009836
Equality_MachineArithSMTInterpol0.000395-0.000742
Bitveccvc50.000353-0.006367
QF_Equality_LinearArithSMTInterpol0.000333-0.005263
QF_LinearIntArithYices20.0003010.030162

Parallel Performance

DivisionSolverCorrect ScoreTime Score
Equality_LinearArithcvc50.0119370.041923
Equality_MachineArithcvc50.004619-0.015242
QF_NonLinearIntArithZ3-alpha0.004550.035105
Equalitycvc50.003167-0.016745
Equality_MachineArithBitwuzla0.001660.000258
QF_Stringscvc50.001278-0.148142
QF_LinearIntArithZ3-alpha0.001028-0.004747
QF_NonLinearIntArithcvc50.001003-0.032888
QF_NonLinearIntArithYices20.0009890.030622
QF_FPArithBitwuzla0.0009720.003092
Arithcvc50.000861-0.119096
Equality_LinearArithiProver v3.90.000858-0.004615
ArithYicesQS0.0008440.004251
QF_StringsZ3-Noodler0.0005360.223144
QF_BitvecSTP0.0004650.009504
Equality_MachineArithSMTInterpol0.000395-0.00061
Bitveccvc50.000353-0.006274
QF_Equality_LinearArithSMTInterpol0.000344-0.004381
QF_LinearIntArithYices20.0003010.025794

SAT Performance

DivisionSolverCorrect ScoreTime Score
Equality_LinearArithcvc50.027531-12.591577
Equality_MachineArithcvc50.005423-0.104339
Equalitycvc50.005062-0.170063
QF_NonLinearIntArithZ3-alpha0.0035750.039387
Equality_LinearArithSMTInterpol0.0032450.008291
Equality_MachineArithBitwuzla0.002868-0.000237
QF_Stringscvc50.001617-0.274484
QF_NonLinearIntArithcvc50.001378-0.046981
QF_LinearIntArithZ3-alpha0.001271-0.002145
QF_BitvecSTP0.0008130.013015
ArithYicesQS0.0008090.007821
QF_StringsZ3-Noodler0.0007460.227464
QF_NonLinearIntArithYices20.0006780.031531
QF_FPArithBitwuzla0.0006470.000206
QF_Equality_LinearArithSMTInterpol0.000518-0.005511
QF_NonLinearRealArithZ3-alpha0.0004510.003355
QF_LinearIntArithYices20.0003830.02282
Arithcvc50.0003740.004268
QF_LinearIntArithOpenSMT0.0003430.006253

UNSAT Performance

DivisionSolverCorrect ScoreTime Score
Equality_LinearArithcvc50.0108340.05325
QF_NonLinearIntArithZ3-alpha0.006485-0.019885
Equality_MachineArithcvc50.004223-0.004624
Equalitycvc50.0023150.004389
QF_NonLinearIntArithYices20.0016050.025724
QF_FPArithBitwuzla0.0011810.004055
Arithcvc50.001151-0.625802
Equality_MachineArithBitwuzla0.0010640.000667
Equality_LinearArithiProver v3.90.000918-0.006205
ArithYicesQS0.0008660.003791
QF_LinearIntArithZ3-alpha0.000629-0.011017
QF_Stringscvc50.0006110.191955
QF_LinearIntArithcvc50.000463-0.000684
Equality_MachineArithSMTInterpol0.000452-0.001256
QF_Equality_BitvecBitwuzla0.000450.035374
QF_Equality_NonLinearArithSMTInterpol0.0004280.000471
Bitveccvc50.000405-0.006972
QF_Equality_NonLinearArithcvc50.0003670.000319
EqualityiProver v3.90.0003340.001137

24 seconds Performance

DivisionSolverCorrect ScoreTime Score
Equality_LinearArithcvc50.0166860.055423
QF_LinearIntArithYices20.0088370.041471
QF_NonLinearIntArithYices20.0080540.033092
QF_NonLinearIntArithZ3-alpha0.00598-0.016436
Equality_MachineArithcvc50.004290.000105
QF_StringsZ3-Noodler0.0031650.234368
Equalitycvc50.0031130.004005
EqualityiProver v3.90.002125-0.009155
Equality_MachineArithBitwuzla0.0018-0.004023
ArithYicesQS0.0016270.002371
QF_Equality_BitvecYices20.0012340.007402
QF_BitvecSTP0.0012260.005793
Equality_LinearArithiProver v3.90.001094-0.005936
QF_FPArithBitwuzla0.0010920.004771
QF_LinearIntArithZ3-alpha0.0009690.00052
QF_DatatypesAlgaroba0.000944-0.002046
QF_Stringscvc50.0008580.039605
QF_Equality_BitvecBitwuzla0.000817-0.006024
QF_BitvecYices20.0007440.02985