SMT-COMP 2024

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2024

Largest Contribution Ranking - Unsat Core Track

Page generated on 2024-07-08

Winners

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

Sequential Performance

DivisionSolverCorrect ScoreTime Score
QF_Equality_BitvecYices20.0242980.008289
QF_Equality_Bitveccvc50.0167320.020982
QF_Bitveccvc50.005366-0.010709
QF_BitvecBitwuzla0.0037610.026653
QF_Equality_LinearArithYices20.003610.001397
QF_BitvecYices20.0027340.012588
QF_Equality_LinearArithOpenSMT0.002488-0.003518
QF_EqualityYices20.0015150.019825
QF_LinearIntArithcvc50.0006670.001026
QF_Equality_BitvecBitwuzla0.0006090.017798
QF_EqualityOpenSMT0.0003720.004917
QF_Equalitycvc50.00021-0.005464
QF_LinearIntArithYices20.0002050.010666
QF_LinearIntArithOpenSMT0.000193-0.001823
QF_Equality_LinearArithcvc50.0001460.000196
QF_EqualitySMTInterpol0.000138-0.008611
QF_LinearIntArithSMTInterpol0.0001250.006083
QF_Equality_LinearArithSMTInterpol9.6e-05-0.000194
QF_LinearRealArithOpenSMT7.6e-050.004092

Parallel Performance

DivisionSolverCorrect ScoreTime Score
QF_Equality_BitvecYices20.0242980.008073
QF_Equality_Bitveccvc50.0167320.020738
QF_Bitveccvc50.005366-0.010628
QF_BitvecBitwuzla0.0037610.026528
QF_Equality_LinearArithYices20.003610.000683
QF_BitvecYices20.0027340.012511
QF_Equality_LinearArithOpenSMT0.002448-0.002326
QF_EqualityYices20.0015150.015153
QF_LinearIntArithcvc50.000667-0.009121
QF_Equality_BitvecBitwuzla0.0006090.017577
QF_EqualityOpenSMT0.0003720.003637
QF_Equalitycvc50.00021-0.011657
QF_LinearIntArithYices20.0002050.01013
QF_LinearIntArithOpenSMT0.000193-0.002713
QF_Equality_LinearArithcvc50.0001460.000127
QF_EqualitySMTInterpol0.000138-0.002819
QF_LinearIntArithSMTInterpol0.0001250.009624
QF_Equality_LinearArithSMTInterpol9.6e-05-3.6e-05
QF_LinearRealArithOpenSMT7.6e-050.004058

UNSAT Performance

DivisionSolverCorrect ScoreTime Score
QF_Equality_BitvecYices20.0242980.008073
QF_Equality_Bitveccvc50.0167320.020738
QF_Bitveccvc50.005366-0.010628
QF_BitvecBitwuzla0.0037610.026528
QF_Equality_LinearArithYices20.003610.000683
QF_BitvecYices20.0027340.012511
QF_Equality_LinearArithOpenSMT0.002448-0.002326
QF_EqualityYices20.0015150.015153
QF_LinearIntArithcvc50.000667-0.009121
QF_Equality_BitvecBitwuzla0.0006090.017577
QF_EqualityOpenSMT0.0003720.003637
QF_Equalitycvc50.00021-0.011657
QF_LinearIntArithYices20.0002050.01013
QF_LinearIntArithOpenSMT0.000193-0.002713
QF_Equality_LinearArithcvc50.0001460.000127
QF_EqualitySMTInterpol0.000138-0.002819
QF_LinearIntArithSMTInterpol0.0001250.009624
QF_Equality_LinearArithSMTInterpol9.6e-05-3.6e-05
QF_LinearRealArithOpenSMT7.6e-050.004058

24 seconds Performance

DivisionSolverCorrect ScoreTime Score
QF_Equality_BitvecYices20.048374-0.157522
QF_Equality_LinearArithYices20.013276-0.003874
QF_LinearIntArithYices20.0085780.015057
QF_BitvecYices20.0058110.032537
QF_LinearRealArithYices20.0016610.000249
QF_EqualityYices20.0015610.019495
QF_Equality_BitvecBitwuzla0.0015420.000851
QF_BitvecBitwuzla0.0014890.003189
QF_Equality_LinearArithcvc50.001077-0.000356
QF_LinearRealArithOpenSMT0.000865-0.000499
QF_LinearIntArithSMTInterpol0.000394-0.000644
QF_EqualityOpenSMT0.000386-0.000366
QF_Equality_LinearArithSMTInterpol0.000227-0.000994
QF_Equality_Bitveccvc50.000179-0.001485
QF_EqualitySMTInterpol0.000143-0.004907
QF_Equalitycvc59.5e-05-0.001204
QF_LinearRealArithcvc58.1e-05-0.00025
QF_Equalityplat-smt7.1e-050.000178
QF_LinearIntArithOpenSMT2.4e-050.004377