SMT-COMP 2024

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2024

Largest Contribution Ranking - Incremental Track

Page generated on 2024-07-08

Winners

Parallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
Yices2--Yices2

Parallel Performance

DivisionSolverCorrect ScoreTime Score
QF_Equality_LinearArithYices20.0189710.044844
QF_Equality_BitvecBitwuzla0.0011840.079048
QF_Equality_LinearArithSMTInterpol0.0007350.004863
QF_LinearIntArithYices20.0005240.0015
QF_BitvecYices20.0004080.00706
QF_BitvecBitwuzla0.0003630.011245
QF_NonLinearIntArithSMTInterpol0.0003360.000408
QF_Equality_Bitvec_ArithYices20.0001940.031662
QF_LinearRealArithOpenSMT0.0001110.00021
QF_Equality_BitvecYices24.6e-050.046099
QF_LinearRealArithYices24.5e-050
Bitveccvc52.5e-050.000403
QF_Equality_NonLinearArithYices22.3e-050.022754
BitvecSMTInterpol1.3e-050.000616
BitvecBitwuzla4e-060.000899
QF_Equality_LinearArithcvc52e-060.006129
QF_Equality_LinearArithOpenSMT00.00473
QF_LinearIntArithOpenSMT00.000543
QF_NonLinearIntArithYices20-0.000296

24 seconds Performance

DivisionSolverCorrect ScoreTime Score
QF_Equality_LinearArithYices20.119470.043189
QF_Equality_NonLinearArithSMTInterpol0.0078870.006746
QF_LinearIntArithYices20.004961-0.002402
QF_Equality_LinearArithSMTInterpol0.0022950.000887
QF_Equality_Bitvec_ArithYices20.0016290.019952
QF_Equality_BitvecYices20.0012930.037407
QF_Equality_BitvecBitwuzla0.0006640.006673
QF_BitvecBitwuzla0.0003250.001338
BitvecBitwuzla0.000231-0.000152
QF_Equality_NonLinearArithYices20.000160.00833
BitvecSMTInterpol0.000131-2.8e-05
Bitveccvc50.00012-0.000164
QF_BitvecSTP0.0001190.008135
QF_Equality_Bitveccvc57e-050.007959
QF_BitvecYices24e-060.010734
QF_Equality_LinearArithcvc53e-06-0.000362
QF_Equality_LinearArithOpenSMT3e-060.00989
QF_LinearIntArithOpenSMT2e-06-0.002364
QF_LinearIntArithcvc51e-06-0.000638