SMT-COMP 2024

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2024

QF_BV (Unsat Core Track)

Competition results for the QF_BV logic in the Unsat Core Track.

Results were generated on 2024-07-08

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

Winners

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

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla02.370581e+0678406.50840778700.41284128080280813901371
Yices202.146412e+0639010.51663239281.1391126160261633103300
cvc501.037741e+06209137.991512209407.57247223270232762006127

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla02.370581e+0678406.50840778700.41284128080280813901371
Yices202.146412e+0639010.51663239281.1391126160261633103300
cvc501.037741e+06209137.991512209407.57247223270232762006127

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla02.370581e+0678406.50840778700.41284128080280813901371
Yices202.146412e+0639010.51663239281.1391126160261633103300
cvc501.037741e+06209137.991512209407.57247223270232762006127

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices202.111442e+061918.087982166.84742248702487145900
Bitwuzla01.986098e+063091.5159943340.88699249302493145300
cvc503484865318.5134825479.2805931605016051134100