SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

Best Overall Ranking - Model Validation Track

Page generated on 2025-08-11

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
cvc5 (31.577255)cvc5 (31.577255)cvc5 (31.577255)—cvc5 (25.834537)

Sequential Performance

DivisionSolverContribution
QF_FPArithcvc54.381439
QF_FPArithBitwuzla4.377482
QF_BitvecBitwuzla3.871608
QF_BitvecYices23.829056
QF_Bitveccvc53.761461
QF_ADT_BitVecBitwuzla3.687547
QF_LinearIntArithOpenSMT3.234384
QF_EqualitySMTInterpol3.196176
QF_Equalitycvc53.196176
QF_EqualityOpenSMT3.196176
QF_EqualityYices23.192109
QF_LinearIntArithYices23.165592
QF_ADT_BitVeccvc53.073389
QF_NonLinearIntArithYices23.05528
QF_DatatypesSMTInterpol2.933059
QF_ADT_LinArithSMTInterpol2.880141
QF_Equality_LinearArithOpenSMT2.844885
QF_ADT_LinArithcvc52.798545
QF_Equality_LinearArithSMTInterpol2.767389
QF_Equality_LinearArithcvc52.729042
QF_NonLinearIntArithcvc52.655395
QF_Equality_BitvecYices22.6542
QF_Equality_BitvecBitwuzla2.6542
QF_LinearRealArithYices22.646431
QF_LinearRealArithOpenSMT2.637483
QF_LinearIntArithSMTInterpol2.58352
QF_Equality_LinearArithYices22.516797
QF_LinearRealArithSMTInterpol2.275342
QF_LinearIntArithcvc52.241202
QF_ADT_BitVecSMTInterpol2.038939
QF_NonLinearRealArithSMT-RAT1.95052
QF_NonLinearRealArithcvc51.816643
QF_LinearRealArithcvc51.680844
QF_Datatypescvc51.506261
QF_Equality_NonLinearArithcvc51.46993
QF_Equality_BitvecSMTInterpol1.162252
QF_Equality_NonLinearArithSMTInterpol0.936751
QF_BitvecSMTInterpol0.873149
QF_Equality_Bitveccvc50.266928
QF_NonLinearRealArithSMTInterpol7.5e-05
QF_NonLinearIntArithSMTInterpol0
QF_Equality_NonLinearArithYices2-5.353387
QF_NonLinearRealArithYices2-6.887152

Parallel Performance

DivisionSolverContribution
QF_FPArithcvc54.381439
QF_FPArithBitwuzla4.377482
QF_BitvecBitwuzla3.871608
QF_BitvecYices23.829056
QF_Bitveccvc53.761461
QF_ADT_BitVecBitwuzla3.687547
QF_LinearIntArithOpenSMT3.234384
QF_EqualitySMTInterpol3.196176
QF_Equalitycvc53.196176
QF_EqualityOpenSMT3.196176
QF_EqualityYices23.192109
QF_LinearIntArithYices23.165592
QF_ADT_BitVeccvc53.073389
QF_NonLinearIntArithYices23.05528
QF_DatatypesSMTInterpol2.933059
QF_ADT_LinArithSMTInterpol2.880141
QF_Equality_LinearArithOpenSMT2.844885
QF_ADT_LinArithcvc52.798545
QF_Equality_LinearArithSMTInterpol2.767389
QF_Equality_LinearArithcvc52.729042
QF_NonLinearIntArithcvc52.655395
QF_Equality_BitvecYices22.6542
QF_Equality_BitvecBitwuzla2.6542
QF_LinearRealArithYices22.646431
QF_LinearRealArithOpenSMT2.637483
QF_LinearIntArithSMTInterpol2.586043
QF_Equality_LinearArithYices22.516797
QF_LinearRealArithSMTInterpol2.275342
QF_LinearIntArithcvc52.241202
QF_ADT_BitVecSMTInterpol2.051551
QF_NonLinearRealArithSMT-RAT1.95052
QF_NonLinearRealArithcvc51.816643
QF_LinearRealArithcvc51.680844
QF_Datatypescvc51.506261
QF_Equality_NonLinearArithcvc51.46993
QF_Equality_BitvecSMTInterpol1.162252
QF_Equality_NonLinearArithSMTInterpol0.936751
QF_BitvecSMTInterpol0.877206
QF_Equality_Bitveccvc50.266928
QF_NonLinearRealArithSMTInterpol7.5e-05
QF_NonLinearIntArithSMTInterpol0
QF_Equality_NonLinearArithYices2-5.353387
QF_NonLinearRealArithYices2-6.887152

SAT Performance

DivisionSolverContribution
QF_FPArithcvc54.381439
QF_FPArithBitwuzla4.377482
QF_BitvecBitwuzla3.871608
QF_BitvecYices23.829056
QF_Bitveccvc53.761461
QF_ADT_BitVecBitwuzla3.687547
QF_LinearIntArithOpenSMT3.234384
QF_EqualitySMTInterpol3.196176
QF_Equalitycvc53.196176
QF_EqualityOpenSMT3.196176
QF_EqualityYices23.192109
QF_LinearIntArithYices23.165592
QF_ADT_BitVeccvc53.073389
QF_NonLinearIntArithYices23.05528
QF_DatatypesSMTInterpol2.933059
QF_ADT_LinArithSMTInterpol2.880141
QF_Equality_LinearArithOpenSMT2.844885
QF_ADT_LinArithcvc52.798545
QF_Equality_LinearArithSMTInterpol2.767389
QF_Equality_LinearArithcvc52.729042
QF_NonLinearIntArithcvc52.655395
QF_Equality_BitvecYices22.6542
QF_Equality_BitvecBitwuzla2.6542
QF_LinearRealArithYices22.646431
QF_LinearRealArithOpenSMT2.637483
QF_LinearIntArithSMTInterpol2.586043
QF_Equality_LinearArithYices22.516797
QF_LinearRealArithSMTInterpol2.275342
QF_LinearIntArithcvc52.241202
QF_ADT_BitVecSMTInterpol2.051551
QF_NonLinearRealArithSMT-RAT1.95052
QF_NonLinearRealArithcvc51.816643
QF_LinearRealArithcvc51.680844
QF_Datatypescvc51.506261
QF_Equality_NonLinearArithcvc51.46993
QF_Equality_BitvecSMTInterpol1.162252
QF_Equality_NonLinearArithSMTInterpol0.936751
QF_BitvecSMTInterpol0.877206
QF_Equality_Bitveccvc50.266928
QF_NonLinearRealArithSMTInterpol7.5e-05
QF_NonLinearIntArithSMTInterpol0
QF_Equality_NonLinearArithYices2-5.353387
QF_NonLinearRealArithYices2-6.887152

24 seconds Performance

DivisionSolverContribution
QF_FPArithBitwuzla4.369573
QF_FPArithcvc54.359518
QF_BitvecBitwuzla3.710231
QF_ADT_BitVecBitwuzla3.656565
QF_BitvecYices23.476403
QF_EqualitySMTInterpol3.196176
QF_Equalitycvc53.196176
QF_EqualityOpenSMT3.196176
QF_EqualityYices23.192109
QF_Bitveccvc53.069453
QF_LinearIntArithYices22.857875
QF_DatatypesSMTInterpol2.844232
QF_NonLinearIntArithYices22.797245
QF_ADT_LinArithSMTInterpol2.776494
QF_Equality_LinearArithSMTInterpol2.590726
QF_ADT_LinArithcvc52.581967
QF_Equality_LinearArithOpenSMT2.522917
QF_ADT_BitVeccvc52.404494
QF_Equality_LinearArithYices22.289749
QF_Equality_LinearArithcvc52.249095
QF_LinearRealArithYices22.160569
QF_LinearRealArithOpenSMT2.033036
QF_LinearIntArithOpenSMT2.019059
QF_NonLinearRealArithSMT-RAT1.829275
QF_NonLinearRealArithcvc51.78615
QF_LinearIntArithSMTInterpol1.779075
QF_Equality_BitvecYices21.722112
QF_LinearIntArithcvc51.697337
QF_Equality_BitvecBitwuzla1.58051
QF_LinearRealArithcvc51.520693
QF_LinearRealArithSMTInterpol1.433719
QF_Datatypescvc51.298614
QF_ADT_BitVecSMTInterpol1.093625
QF_Equality_NonLinearArithcvc50.871265
QF_Equality_BitvecSMTInterpol0.622132
QF_NonLinearIntArithcvc50.593067
QF_BitvecSMTInterpol0.581227
QF_Equality_NonLinearArithSMTInterpol0.518208
QF_Equality_Bitveccvc50.206709
QF_NonLinearRealArithSMTInterpol2.2e-05
QF_NonLinearIntArithSMTInterpol0
QF_Equality_NonLinearArithYices2-5.353387
QF_NonLinearRealArithYices2-6.887152