SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_Equality_Bitvec (Model Validation Track)

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

Results were generated on 2025-08-11

Benchmarks: 475
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 - Yices2

Sequential Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
Bitwuzla 0 473 9788.51 9848.53 473 473 2 0 2 0
Yices2 0 473 21591.43 21652.99 473 473 2 0 2 0
SMTInterpol 0 313 24034.28 19084.40 313 313 162 0 40 0
cvc5 0 150 3950.16 3969.09 150 150 325 0 325 0

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
Bitwuzla 0 473 9788.51 9848.53 473 473 2 0 2 0
Yices2 0 473 21591.43 21652.99 473 473 2 0 2 0
SMTInterpol 0 313 24034.28 19084.40 313 313 162 0 40 0
cvc5 0 150 3950.16 3969.09 150 150 325 0 325 0

SAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
Bitwuzla 0 473 9788.51 9848.53 473 473 2 0 2 0
Yices2 0 473 21591.43 21652.99 473 473 2 0 2 0
SMTInterpol 0 313 24034.28 19084.40 313 313 162 0 40 0
cvc5 0 150 3950.16 3969.09 150 150 325 0 325 0

24 seconds Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
Yices2 0 381 1028.54 1075.66 381 381 0 94 0 0
Bitwuzla 0 365 1046.24 1091.23 365 365 0 110 0 0
SMTInterpol 0 229 4377.91 1810.41 229 229 58 188 0 0
cvc5 0 132 86.33 102.39 132 132 0 343 0 0