SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

Largest Contribution Ranking - Model Validation Track

Page generated on 2025-08-11

Winners

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
Yices2Yices2Yices2-Yices2

Sequential Performance

DivisionSolverCorrect ScoreTime Score
QF_NonLinearIntArithYices20.0106450.07692
QF_ADT_BitVecBitwuzla0.0056760.093672
QF_NonLinearIntArithcvc50.00489-0.376271
QF_NonLinearRealArithSMT-RAT0.0016190.012491
QF_LinearIntArithOpenSMT0.0014420.011649
QF_LinearIntArithYices20.001020.073495
QF_LinearIntArithSMTInterpol0.000821-0.009001
QF_LinearIntArithcvc50.0007460.029471
QF_NonLinearRealArithcvc50.0007230.019901
QF_BitvecBitwuzla0.0004570.074115
QF_Equality_LinearArithOpenSMT0.0004020.013239
QF_BitvecYices20.0001680.039288
QF_Equality_LinearArithSMTInterpol0.0001340.007096
QF_ADT_BitVeccvc55.5e-050.028876
QF_LinearRealArithYices25.1e-050.008336
QF_LinearRealArithOpenSMT5.1e-050.005579
QF_Equality_BitvecBitwuzla4.1e-050.006252
QF_NonLinearRealArithSMTInterpol2.7e-05-0.002319
QF_LinearRealArithSMTInterpol2.6e-056.8e-05

Parallel Performance

DivisionSolverCorrect ScoreTime Score
QF_NonLinearIntArithYices20.0106450.076878
QF_ADT_BitVecBitwuzla0.0056570.093065
QF_NonLinearIntArithcvc50.00489-0.369607
QF_NonLinearRealArithSMT-RAT0.0016190.012394
QF_LinearIntArithOpenSMT0.0014420.011463
QF_LinearIntArithYices20.001020.069615
QF_LinearIntArithSMTInterpol0.000821-0.006172
QF_LinearIntArithcvc50.0007460.029469
QF_NonLinearRealArithcvc50.0007230.019832
QF_BitvecBitwuzla0.0004570.072539
QF_Equality_LinearArithOpenSMT0.0004020.01316
QF_BitvecYices20.0001680.038192
QF_Equality_LinearArithSMTInterpol0.0001340.008104
QF_ADT_BitVeccvc55.5e-050.024148
QF_LinearRealArithYices25.1e-050.008231
QF_LinearRealArithOpenSMT5.1e-050.005451
QF_Equality_BitvecBitwuzla4.1e-050.006306
QF_NonLinearRealArithSMTInterpol2.7e-05-0.001488
QF_LinearRealArithSMTInterpol2.6e-050.000224

SAT Performance

DivisionSolverCorrect ScoreTime Score
QF_NonLinearIntArithYices20.0106450.076878
QF_ADT_BitVecBitwuzla0.0056570.093065
QF_NonLinearIntArithcvc50.00489-0.369607
QF_NonLinearRealArithSMT-RAT0.0016190.012394
QF_LinearIntArithOpenSMT0.0014420.011463
QF_LinearIntArithYices20.001020.069615
QF_LinearIntArithSMTInterpol0.000821-0.006172
QF_LinearIntArithcvc50.0007460.029469
QF_NonLinearRealArithcvc50.0007230.019832
QF_BitvecBitwuzla0.0004570.072539
QF_Equality_LinearArithOpenSMT0.0004020.01316
QF_BitvecYices20.0001680.038192
QF_Equality_LinearArithSMTInterpol0.0001340.008104
QF_ADT_BitVeccvc55.5e-050.024148
QF_LinearRealArithYices25.1e-050.008231
QF_LinearRealArithOpenSMT5.1e-050.005451
QF_Equality_BitvecBitwuzla4.1e-050.006306
QF_NonLinearRealArithSMTInterpol2.7e-05-0.001488
QF_LinearRealArithSMTInterpol2.6e-050.000224

24 seconds Performance

DivisionSolverCorrect ScoreTime Score
QF_NonLinearIntArithYices20.049027-0.059794
QF_ADT_BitVecBitwuzla0.0180280.066877
QF_LinearIntArithYices20.014270.042706
QF_BitvecBitwuzla0.0048860.020794
QF_LinearIntArithcvc50.002227-0.00205
QF_NonLinearRealArithSMT-RAT0.001738-0.002897
QF_LinearIntArithOpenSMT0.001632-0.004751
QF_NonLinearRealArithcvc50.0014280.000542
QF_NonLinearIntArithcvc50.0011670.006425
QF_Equality_BitvecBitwuzla0.000855-0.0022
QF_BitvecYices20.0008310.049541
QF_Equality_BitvecYices20.0006240.000167
QF_LinearRealArithYices20.0004740.004921
QF_LinearIntArithSMTInterpol0.000466-0.003219
QF_Equality_LinearArithSMTInterpol0.000417-0.002471
QF_Bitveccvc50.000391-9.7e-05
QF_LinearRealArithOpenSMT0.000362-0.002374
QF_Equality_LinearArithOpenSMT0.000361-0.001531
QF_ADT_BitVeccvc50.00013-0.001637