SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_Bitvec (Model Validation Track)

Competition results for the QF_Bitvec division in the Model Validation Track. Chart

Results were generated on 2025-08-11

Benchmarks: 8211
Time Limit: 1200 seconds
Memory Limit: 30720 GB

Logics:

Winners

Sequential Performance Parallel Performance SAT Performance (parallel) UNSAT Performance (parallel) 24 seconds Performance (parallel)
Bitwuzla Bitwuzla Bitwuzla - Bitwuzla

Sequential Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
Bitwuzla 0 8166 38291.19 39296.71 8166 8166 45 0 39 4
Yices2 0 8121 73011.21 74029.36 8121 8121 90 0 89 0
cvc5 0 8049 118478.39 119484.19 8049 8049 162 0 149 12
SMTInterpol 0 3878 192678.88 166115.10 3887 3887 4324 0 3525 0

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
Bitwuzla 0 8166 38291.19 39296.71 8166 8166 45 0 39 4
Yices2 0 8121 73011.21 74029.36 8121 8121 90 0 89 0
cvc5 0 8049 118478.39 119484.19 8049 8049 162 0 149 12
SMTInterpol 0 3887 203622.49 176633.66 3887 3887 4324 0 3525 0

SAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
Bitwuzla 0 8166 38291.19 39296.71 8166 8166 45 0 39 4
Yices2 0 8121 73011.21 74029.36 8121 8121 90 0 89 0
cvc5 0 8049 118478.39 119484.19 8049 8049 162 0 149 12
SMTInterpol 0 3887 203622.49 176633.66 3887 3887 4324 0 3525 0

24 seconds Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
Bitwuzla 0 7994 8678.44 9656.84 7994 7994 0 217 0 0
Yices2 0 7738 6171.97 7132.82 7738 7738 0 473 0 0
cvc5 0 7271 14982.41 15875.25 7271 7271 0 940 0 0
SMTInterpol 0 3164 19399.80 9266.46 3164 3164 321 4726 0 0