SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

Biggest Lead Ranking - Unsat Core Track

Page generated on 2025-08-11

Winners

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
cvc5cvc5-cvc5cvc5

Sequential Performance

DivisionSolverCorrect ScoreTime Score
Arithcvc533.3750.001466
QF_NonLinearRealArithYices210.875640.001603
QF_Datatypescvc59.1504350.333423
QF_Equality_LinearArithYices24.4935130.227272
Bitveccvc53.250.115493
Equality_NonLinearArithcvc52.0765650.180614
Equalitycvc51.7325143.405705
Equality_LinearArithcvc51.6183711.872232
Equality_MachineArithcvc51.2800371.127433
QF_Equality_NonLinearArithcvc51.2109540.761002
QF_BitvecBitwuzla1.2017640.508413
QF_EqualityYices21.1790178.192068
QF_LinearIntArithYices21.1070691.675866
QF_NonLinearIntArithYices21.1064063.344723
QF_Equality_BitvecBitwuzla1.0891374.925647
FPArithBitwuzla1.046.025612
QF_LinearRealArithOpenSMT1.0323082.428354
QF_FPArithBitwuzla1.031632.122405

Parallel Performance

DivisionSolverCorrect ScoreTime Score
Arithcvc533.3750.001266
QF_NonLinearRealArithYices210.875640.000647
QF_Datatypescvc59.1504350.177871
QF_Equality_LinearArithYices24.4935130.229122
Bitveccvc53.250.117468
Equality_NonLinearArithcvc52.0765650.122326
Equalitycvc51.7311062.704698
Equality_LinearArithcvc51.6168641.512142
Equality_MachineArithcvc51.2800370.820552
QF_Equality_NonLinearArithcvc51.2109540.623924
QF_BitvecBitwuzla1.2017640.510576
QF_EqualityYices21.1790173.333792
QF_LinearIntArithYices21.1070691.422869
QF_NonLinearIntArithYices21.1064063.320464
QF_Equality_BitvecBitwuzla1.0891374.860473
FPArithBitwuzla1.044.855741
QF_LinearRealArithOpenSMT1.0323082.423808
QF_FPArithBitwuzla1.031631.944569

UNSAT Performance

DivisionSolverCorrect ScoreTime Score
Arithcvc533.3750.001266
QF_NonLinearRealArithYices210.875640.000647
QF_Datatypescvc59.1504350.177871
QF_Equality_LinearArithYices24.4935130.229122
Bitveccvc53.250.117468
Equality_NonLinearArithcvc52.0765650.122326
Equalitycvc51.7311062.704698
Equality_LinearArithcvc51.6168641.512142
Equality_MachineArithcvc51.2800370.820552
QF_Equality_NonLinearArithcvc51.2109540.623924
QF_BitvecBitwuzla1.2017640.510576
QF_EqualityYices21.1790173.333792
QF_LinearIntArithYices21.1070691.422869
QF_NonLinearIntArithYices21.1064063.320464
QF_Equality_BitvecBitwuzla1.0891374.860473
FPArithBitwuzla1.044.855741
QF_LinearRealArithOpenSMT1.0323082.423808
QF_FPArithBitwuzla1.031631.944569

24 seconds Performance

DivisionSolverCorrect ScoreTime Score
Arithcvc515.3750.172157
QF_DatatypesSMTInterpol4.6679610.865089
QF_Equality_LinearArithYices23.9813141.349514
QF_NonLinearRealArithYices23.5698580.008459
Bitveccvc52.350.301727
QF_LinearIntArithYices21.9816491.232029
Equalitycvc51.9043382.901647
Equality_LinearArithcvc51.5977442.005157
Equality_NonLinearArithcvc51.5925451.600613
Equality_MachineArithcvc51.3160413.245535
QF_NonLinearIntArithYices21.2688921.268057
QF_EqualityYices21.2114047.070112
QF_Equality_BitvecBitwuzla1.1149020.478257
QF_LinearRealArithYices21.0779081.53046
QF_FPArithBitwuzla1.0430471.019561
FPArithBitwuzla1.044.855741
QF_Equality_NonLinearArithYices21.0325751.277959
QF_BitvecBitwuzla1.0104230.536561