SMT-COMP 2024

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2024

QF_Bitvec (Unsat Core Track)

Competition results for the QF_Bitvec division in the Unsat Core Track.

Results were generated on 2024-07-08

Benchmarks: 2947
Time Limit: 1200 seconds
Memory Limit: 20480 GB

Logics:

Winners

winner_seqwinner_parwinner_satwinner_unsatwinner_24s
Yices2Yices2-Yices2Yices2

Sequential Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices212.146414e+0640196.79152140467.69332726171261633003300
cvc511.037781e+06210764.344196211022.54018123260232662106137
Bitwuzla32.370855e+0680058.71379880352.41792328071280614001371

Parallel Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices213.047972e+06436506.27788436884.33516526171261633003300
cvc512.002948e+06946972.067034947692.59425923260232662106137
Bitwuzla32.910067e+06243392.269891243728.93143328071280614001371

UNSAT Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices213.047972e+06436506.27788436884.33516526171261633003300
cvc512.002948e+06946972.067034947692.59425923260232662106137
Bitwuzla32.910067e+06243392.269891243728.93143328071280614001371

24 seconds Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices202.111442e+061918.087982166.84742248702487046000
Bitwuzla01.986098e+063091.5159943340.88699249302493045400
cvc503484865318.5134825479.2805931605016050134200