SMT-COMP 2026

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2026

Best Overall Ranking - Model Validation Track

Page generated on 2026-07-25

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
cvc5 (28.262747)cvc5 (28.262747)cvc5 (28.262747)—cvc5 (22.884283)

Sequential Performance

DivisionSolverContribution
QF_FPArithcvc53.783672
QF_FPArithBitwuzla3.7655
QF_FPArithz3-BooledASS-base3.711247
QF_BitvecBitwuzla3.212422
QF_Bitveccvc53.151492
QF_Bitvecbv_decide-nokernel3.064513
QF_Bitvecbv_decide3.061192
QF_ADT_BitVecBitwuzla2.956908
QF_ADT_BitVecYices22.920541
QF_Equality_LinearArithOpenSMT2.857905
QF_EqualitySMTInterpol2.853698
QF_Equalitycvc52.853698
QF_EqualityOpenSMT2.853698
QF_EqualityYices22.853698
QF_Bitvecz3-BooledASS-base2.817243
QF_Equalityplat-smt2.766446
QF_Equality_LinearArithSMTInterpol2.748182
QF_LinearIntArithYices22.740987
QF_Equality_LinearArithcvc52.716319
QF_LinearIntArithOpenSMT2.680637
QF_ADT_LinArithcvc52.66695
QF_ADT_LinArithSMTInterpol2.659982
QF_LinearRealArithOpenSMT2.649114
QF_ADT_BitVeccvc52.645364
QF_Equality_BitvecYices22.640481
QF_Equality_BitvecBitwuzla2.640481
QF_LinearIntArithz3-BooledASS-base2.630858
QF_LinearRealArithYices22.613011
QF_NonLinearIntArithz3-BooledASS-base2.597619
QF_NonLinearIntArithYices22.579229
QF_Equality_LinearArithYices22.547471
QF_LinearIntArithz3-BooledASS2.535943
QF_LinearRealArithz3-BooledASS2.506187
QF_LinearRealArithz3-BooledASS-base2.506187
QF_LinearRealArithSMTInterpol2.41887
QF_NonLinearIntArithcvc52.293871
QF_Equality_Bitvecz3-BooledASS-base2.124674
QF_LinearIntArithSMTInterpol2.058202
QF_ADT_LinArithYices21.991109
QF_Equality_LinearArithz3-BooledASS1.974712
QF_Equality_LinearArithz3-BooledASS-base1.974712
QF_LinearIntArithcvc51.881053
QF_NonLinearRealArithz3-BooledASS-base1.872272
QF_NonLinearRealArithz3-BooledASS1.872272
QF_LinearRealArithcvc51.768662
QF_NonLinearRealArithSMT-RAT1.767932
QF_NonLinearRealArithYices21.758151
QF_NonLinearRealArithcvc51.628762
QF_ADT_BitVecSMTInterpol1.519815
QF_Equality_BitvecSMTInterpol1.398217
QF_Equality_NonLinearArithcvc51.199471
QF_Datatypescvc51.125878
QF_Datatypesz3-BooledASS-base1.064085
QF_Datatypesz3-BooledASS1.064085
QF_Equality_Bitvecz3-BooledASS1.00797
QF_NonLinearIntArithz3-BooledASS0.992746
QF_BitvecSMTInterpol0.833142
QF_ADT_LinArithz3-BooledASS-base0.6967
QF_ADT_LinArithz3-BooledASS0.6967
QF_Equality_NonLinearArithSMTInterpol0.6601
QF_Equality_Bitveccvc50.547553
QF_FPArithz3-BooledASS0.516446
QF_DatatypesSMTInterpol0.399322
QF_Equality_NonLinearArithz3-BooledASS0.30165
QF_Equality_NonLinearArithz3-BooledASS-base0.294553
QF_Bitvecz3-BooledASS0.231411
QF_NonLinearRealArithSMTInterpol3.1e-05
QF_Equalityz3-BooledASS-base2.2e-05
QF_Equalityz3-BooledASS2.2e-05
QF_NonLinearIntArithSMTInterpol1e-06
QF_Equality_NonLinearArithYices2-5.408301
QF_ADT_BitVecz3-BooledASS-6.359678
QF_ADT_BitVecz3-BooledASS-base-6.359678
QF_BitvecYices2-6.561612

Parallel Performance

DivisionSolverContribution
QF_FPArithcvc53.783672
QF_FPArithBitwuzla3.7655
QF_FPArithz3-BooledASS-base3.711247
QF_BitvecBitwuzla3.212422
QF_Bitveccvc53.151492
QF_Bitvecbv_decide-nokernel3.064513
QF_Bitvecbv_decide3.061192
QF_ADT_BitVecBitwuzla2.956908
QF_ADT_BitVecYices22.920541
QF_Equality_LinearArithOpenSMT2.857905
QF_EqualitySMTInterpol2.853698
QF_Equalitycvc52.853698
QF_EqualityOpenSMT2.853698
QF_EqualityYices22.853698
QF_Bitvecz3-BooledASS-base2.817243
QF_Equalityplat-smt2.766446
QF_Equality_LinearArithSMTInterpol2.754577
QF_LinearIntArithYices22.740987
QF_Equality_LinearArithcvc52.716319
QF_LinearIntArithOpenSMT2.680637
QF_ADT_LinArithcvc52.66695
QF_ADT_LinArithSMTInterpol2.659982
QF_LinearRealArithOpenSMT2.649114
QF_ADT_BitVeccvc52.645364
QF_Equality_BitvecYices22.640481
QF_Equality_BitvecBitwuzla2.640481
QF_LinearIntArithz3-BooledASS-base2.630858
QF_LinearRealArithYices22.613011
QF_NonLinearIntArithz3-BooledASS-base2.597619
QF_NonLinearIntArithYices22.579229
QF_Equality_LinearArithYices22.547471
QF_LinearIntArithz3-BooledASS2.535943
QF_LinearRealArithz3-BooledASS2.506187
QF_LinearRealArithz3-BooledASS-base2.506187
QF_LinearRealArithSMTInterpol2.41887
QF_NonLinearIntArithcvc52.293871
QF_Equality_Bitvecz3-BooledASS-base2.124674
QF_LinearIntArithSMTInterpol2.061124
QF_ADT_LinArithYices21.991109
QF_Equality_LinearArithz3-BooledASS-base1.974712
QF_Equality_LinearArithz3-BooledASS1.974712
QF_LinearIntArithcvc51.881053
QF_NonLinearRealArithz3-BooledASS1.872272
QF_NonLinearRealArithz3-BooledASS-base1.872272
QF_LinearRealArithcvc51.768662
QF_NonLinearRealArithSMT-RAT1.767932
QF_NonLinearRealArithYices21.758151
QF_NonLinearRealArithcvc51.628762
QF_ADT_BitVecSMTInterpol1.5373
QF_Equality_BitvecSMTInterpol1.398217
QF_Equality_NonLinearArithcvc51.199471
QF_Datatypescvc51.125878
QF_Datatypesz3-BooledASS-base1.064085
QF_Datatypesz3-BooledASS1.064085
QF_Equality_Bitvecz3-BooledASS1.00797
QF_NonLinearIntArithz3-BooledASS0.992746
QF_BitvecSMTInterpol0.834875
QF_ADT_LinArithz3-BooledASS-base0.6967
QF_ADT_LinArithz3-BooledASS0.6967
QF_Equality_NonLinearArithSMTInterpol0.6601
QF_Equality_Bitveccvc50.547553
QF_FPArithz3-BooledASS0.516446
QF_DatatypesSMTInterpol0.399322
QF_Equality_NonLinearArithz3-BooledASS0.30165
QF_Equality_NonLinearArithz3-BooledASS-base0.294553
QF_Bitvecz3-BooledASS0.231411
QF_NonLinearRealArithSMTInterpol3.1e-05
QF_Equalityz3-BooledASS-base2.2e-05
QF_Equalityz3-BooledASS2.2e-05
QF_NonLinearIntArithSMTInterpol1e-06
QF_Equality_NonLinearArithYices2-5.408301
QF_ADT_BitVecz3-BooledASS-6.359678
QF_ADT_BitVecz3-BooledASS-base-6.359678
QF_BitvecYices2-6.561612

SAT Performance

DivisionSolverContribution
QF_FPArithcvc53.783672
QF_FPArithBitwuzla3.7655
QF_FPArithz3-BooledASS-base3.711247
QF_BitvecBitwuzla3.212422
QF_Bitveccvc53.151492
QF_Bitvecbv_decide-nokernel3.064513
QF_Bitvecbv_decide3.061192
QF_ADT_BitVecBitwuzla2.956908
QF_ADT_BitVecYices22.920541
QF_Equality_LinearArithOpenSMT2.857905
QF_EqualitySMTInterpol2.853698
QF_Equalitycvc52.853698
QF_EqualityOpenSMT2.853698
QF_EqualityYices22.853698
QF_Bitvecz3-BooledASS-base2.817243
QF_Equalityplat-smt2.766446
QF_Equality_LinearArithSMTInterpol2.754577
QF_LinearIntArithYices22.740987
QF_Equality_LinearArithcvc52.716319
QF_LinearIntArithOpenSMT2.680637
QF_ADT_LinArithcvc52.66695
QF_ADT_LinArithSMTInterpol2.659982
QF_LinearRealArithOpenSMT2.649114
QF_ADT_BitVeccvc52.645364
QF_Equality_BitvecYices22.640481
QF_Equality_BitvecBitwuzla2.640481
QF_LinearIntArithz3-BooledASS-base2.630858
QF_LinearRealArithYices22.613011
QF_NonLinearIntArithz3-BooledASS-base2.597619
QF_NonLinearIntArithYices22.579229
QF_Equality_LinearArithYices22.547471
QF_LinearIntArithz3-BooledASS2.535943
QF_LinearRealArithz3-BooledASS2.506187
QF_LinearRealArithz3-BooledASS-base2.506187
QF_LinearRealArithSMTInterpol2.41887
QF_NonLinearIntArithcvc52.293871
QF_Equality_Bitvecz3-BooledASS-base2.124674
QF_LinearIntArithSMTInterpol2.061124
QF_ADT_LinArithYices21.991109
QF_Equality_LinearArithz3-BooledASS-base1.974712
QF_Equality_LinearArithz3-BooledASS1.974712
QF_LinearIntArithcvc51.881053
QF_NonLinearRealArithz3-BooledASS1.872272
QF_NonLinearRealArithz3-BooledASS-base1.872272
QF_LinearRealArithcvc51.768662
QF_NonLinearRealArithSMT-RAT1.767932
QF_NonLinearRealArithYices21.758151
QF_NonLinearRealArithcvc51.628762
QF_ADT_BitVecSMTInterpol1.5373
QF_Equality_BitvecSMTInterpol1.398217
QF_Equality_NonLinearArithcvc51.199471
QF_Datatypescvc51.125878
QF_Datatypesz3-BooledASS-base1.064085
QF_Datatypesz3-BooledASS1.064085
QF_Equality_Bitvecz3-BooledASS1.00797
QF_NonLinearIntArithz3-BooledASS0.992746
QF_BitvecSMTInterpol0.834875
QF_ADT_LinArithz3-BooledASS-base0.6967
QF_ADT_LinArithz3-BooledASS0.6967
QF_Equality_NonLinearArithSMTInterpol0.6601
QF_Equality_Bitveccvc50.547553
QF_FPArithz3-BooledASS0.516446
QF_DatatypesSMTInterpol0.399322
QF_Equality_NonLinearArithz3-BooledASS0.30165
QF_Equality_NonLinearArithz3-BooledASS-base0.294553
QF_Bitvecz3-BooledASS0.231411
QF_NonLinearRealArithSMTInterpol3.1e-05
QF_Equalityz3-BooledASS-base2.2e-05
QF_Equalityz3-BooledASS2.2e-05
QF_NonLinearIntArithSMTInterpol1e-06
QF_Equality_NonLinearArithYices2-5.408301
QF_ADT_BitVecz3-BooledASS-6.359678
QF_ADT_BitVecz3-BooledASS-base-6.359678
QF_BitvecYices2-6.561612

24 seconds Performance

DivisionSolverContribution
QF_FPArithcvc53.760662
QF_FPArithBitwuzla3.744958
QF_FPArithz3-BooledASS-base3.627636
QF_BitvecBitwuzla3.024779
QF_ADT_BitVecBitwuzla2.888403
QF_ADT_BitVecYices22.876397
QF_EqualitySMTInterpol2.853698
QF_Equalitycvc52.853698
QF_EqualityOpenSMT2.853698
QF_EqualityYices22.853698
QF_Equalityplat-smt2.766446
QF_ADT_LinArithSMTInterpol2.583938
QF_Equality_LinearArithSMTInterpol2.572144
QF_Bitveccvc52.522781
QF_Equality_LinearArithOpenSMT2.516797
QF_ADT_LinArithcvc52.468583
QF_LinearIntArithYices22.404727
QF_NonLinearIntArithYices22.334444
QF_Equality_LinearArithYices22.289749
QF_Equality_LinearArithcvc52.249095
QF_LinearRealArithYices22.215626
QF_Bitvecbv_decide-nokernel2.199311
QF_Bitvecbv_decide2.196498
QF_Bitvecz3-BooledASS-base2.171259
QF_Equality_BitvecYices22.168256
QF_LinearIntArithz3-BooledASS-base2.046532
QF_Equality_BitvecBitwuzla2.038838
QF_LinearRealArithOpenSMT2.0213
QF_ADT_BitVeccvc52.00361
QF_NonLinearIntArithz3-BooledASS-base1.990146
QF_ADT_LinArithYices21.985089
QF_LinearIntArithz3-BooledASS1.977212
QF_Equality_LinearArithz3-BooledASS-base1.920907
QF_Equality_LinearArithz3-BooledASS1.920907
QF_Equality_Bitvecz3-BooledASS-base1.892883
QF_NonLinearRealArithz3-BooledASS-base1.812283
QF_NonLinearRealArithz3-BooledASS1.812283
QF_LinearRealArithz3-BooledASS-base1.783493
QF_LinearRealArithz3-BooledASS1.768662
QF_NonLinearRealArithYices21.70484
QF_NonLinearRealArithSMT-RAT1.661833
QF_NonLinearRealArithcvc51.605344
QF_LinearIntArithOpenSMT1.594077
QF_LinearRealArithcvc51.588493
QF_LinearRealArithSMTInterpol1.532883
QF_LinearIntArithSMTInterpol1.342612
QF_LinearIntArithcvc51.234001
QF_Datatypesz3-BooledASS-base1.023859
QF_Datatypesz3-BooledASS1.023859
QF_Equality_Bitvecz3-BooledASS0.956383
QF_Equality_NonLinearArithcvc50.839901
QF_Datatypescvc50.823599
QF_ADT_BitVecSMTInterpol0.819313
QF_Equality_BitvecSMTInterpol0.744211
QF_NonLinearIntArithz3-BooledASS0.680473
QF_ADT_LinArithz3-BooledASS0.617146
QF_ADT_LinArithz3-BooledASS-base0.617146
QF_BitvecSMTInterpol0.608292
QF_NonLinearIntArithcvc50.525465
QF_FPArithz3-BooledASS0.516446
QF_Equality_NonLinearArithSMTInterpol0.492762
QF_Equality_Bitveccvc50.409051
QF_DatatypesSMTInterpol0.358147
QF_Bitvecz3-BooledASS0.231411
QF_Equality_NonLinearArithz3-BooledASS0.209975
QF_Equality_NonLinearArithz3-BooledASS-base0.204061
QF_Equalityz3-BooledASS-base2.2e-05
QF_Equalityz3-BooledASS2.2e-05
QF_NonLinearRealArithSMTInterpol3e-06
QF_NonLinearIntArithSMTInterpol1e-06
QF_Equality_NonLinearArithYices2-5.408301
QF_ADT_BitVecz3-BooledASS-base-6.359678
QF_ADT_BitVecz3-BooledASS-6.359678
QF_BitvecYices2-6.561612