SMT-COMP 2024

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2024

QF_AUFBV (Model Validation Track)

Competition results for the QF_AUFBV logic in the Model Validation Track.

Results were generated on 2024-07-08

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
BitwuzlaBitwuzlaBitwuzla-Bitwuzla

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla024682.356556684.958289242401001
cvc50131520.5613121522.20286413130120102
SMTInterpol03429.440649380.250857330220150

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla024682.356556684.958289242401001
cvc50131520.5613121522.20286413130120102
SMTInterpol03429.440649380.250857330220150

SAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla024682.356556684.958289242401001
cvc50131520.5613121522.20286413130120102
SMTInterpol03429.440649380.250857330220150

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla01522.62201624.1415821515001000
cvc501044.99532146.0174791010001500
SMTInterpol026.1049772.43076422061700