SMT-COMP 2026

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2026

Largest Contribution Ranking - Unsat Core Track

Page generated on 2026-07-25

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
BitwuzlaBitwuzla-BitwuzlaYices2

Sequential Performance

DivisionSolverCorrect ScoreTime Score
QF_Equality_BitvecBitwuzla0.019814-0.005709
Equality_LinearArithcvc50.011993-0.003004
Equalitycvc50.007525-0.034841
QF_Datatypescvc50.007351-0.001944
QF_EqualityOpenSMT (min-ucore)0.005379-2.160255
QF_BitvecBitwuzla0.0045930.02255
QF_Equality_LinearArithOpenSMT0.0045840.001696
Equality_MachineArithSMTInterpol0.0039470.014662
QF_Bitveccvc50.003539-0.00517
Equality_NonLinearArithcvc50.002919-0.082728
Arithcvc50.001409-0.718949
Equality_NonLinearArithz3-BooledASS0.0013280.01424
Equality_MachineArithcvc50.0012510.029086
QF_NonLinearIntArithYices20.0012250.002695
QF_FPArithBitwuzla0.0011210.034505
QF_LinearIntArithcvc50.0009310.000165
QF_LinearIntArithSMTInterpol0.0005450.005867
QF_Equality_LinearArithYices20.0005030.000955
QF_FPArithcvc50.0004330.001031

Parallel Performance

DivisionSolverCorrect ScoreTime Score
QF_Equality_BitvecBitwuzla0.019814-0.007755
Equality_LinearArithcvc50.0118760.013405
Equalitycvc50.007525-0.039978
QF_Datatypescvc50.007351-0.002378
QF_EqualityOpenSMT (min-ucore)0.005379-1.842887
QF_BitvecBitwuzla0.0045930.021626
QF_Equality_LinearArithOpenSMT0.0045840.001694
Equality_MachineArithSMTInterpol0.0039470.017571
QF_Bitveccvc50.003539-0.00556
Equality_NonLinearArithcvc50.002919-0.083879
Arithcvc50.001409-0.638122
Equality_NonLinearArithz3-BooledASS0.0013280.014173
Equality_MachineArithcvc50.0012510.027742
QF_NonLinearIntArithYices20.0012250.002608
QF_FPArithBitwuzla0.0011210.033943
QF_LinearIntArithcvc50.0009310.000166
QF_LinearIntArithSMTInterpol0.0005450.006711
QF_Equality_LinearArithYices20.0005030.000951
QF_FPArithcvc50.0004330.000962

UNSAT Performance

DivisionSolverCorrect ScoreTime Score
QF_Equality_BitvecBitwuzla0.019814-0.007755
Equality_LinearArithcvc50.0118760.013405
Equalitycvc50.007525-0.039978
QF_Datatypescvc50.007351-0.002378
QF_EqualityOpenSMT (min-ucore)0.005379-1.842887
QF_BitvecBitwuzla0.0045930.021626
QF_Equality_LinearArithOpenSMT0.0045840.001694
Equality_MachineArithSMTInterpol0.0039470.017571
QF_Bitveccvc50.003539-0.00556
Equality_NonLinearArithcvc50.002919-0.083879
Arithcvc50.001409-0.638122
Equality_NonLinearArithz3-BooledASS0.0013280.014173
Equality_MachineArithcvc50.0012510.027742
QF_NonLinearIntArithYices20.0012250.002608
QF_FPArithBitwuzla0.0011210.033943
QF_LinearIntArithcvc50.0009310.000166
QF_LinearIntArithSMTInterpol0.0005450.006711
QF_Equality_LinearArithYices20.0005030.000951
QF_FPArithcvc50.0004330.000962

24 seconds Performance

DivisionSolverCorrect ScoreTime Score
QF_Equality_LinearArithYices20.028791-0.002141
Equality_LinearArithcvc50.0114540.021069
Equalitycvc50.0063680.003105
QF_FPArithBitwuzla0.0055440.022621
QF_EqualityOpenSMT (min-ucore)0.004704-0.004027
QF_BitvecBitwuzla0.0034350.01372
Equality_MachineArithSMTInterpol0.002832-0.015306
Equality_NonLinearArithcvc50.0026020.004754
QF_LinearIntArithYices20.0024010.016766
QF_EqualityOpenSMT0.00206-0.002872
Equality_MachineArithcvc50.0019840.018364
QF_NonLinearIntArithYices20.0011780.002619
QF_LinearIntArithcvc50.001107-0.003377
QF_Equality_BitvecBitwuzla0.001071-0.001761
QF_NonLinearRealArithYices20.001068-0.000508
Equality_NonLinearArithz3-BooledASS0.0010.000859
Arithcvc50.0009170.000489
QF_LinearIntArithSMTInterpol0.000914-0.003498
QF_DatatypesSMTInterpol0.000909-0.004448