SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_Equality_Bitvec (Unsat Core Track)

Competition results for the QF_Equality_Bitvec division in the Unsat Core Track. Chart

Results were generated on 2025-08-11

Benchmarks: 2470
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 UNSAT Unsolved Abstained Timeout Memout
Bitwuzla 0 504470 17878.47 18180.69 2406 2406 61 3 61 0
Yices2 0 463183 88066.95 88370.60 2376 2376 91 3 91 0
SMTInterpol 0 413985 21110.24 12709.87 2284 2284 186 0 163 0
cvc5 0 204488 140288.60 140609.34 2373 2373 97 0 64 33

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
Bitwuzla 0 504470 17878.47 18180.69 2406 2406 61 3 61 0
Yices2 0 463183 88066.95 88370.60 2376 2376 91 3 91 0
SMTInterpol 0 413985 21110.24 12709.87 2284 2284 186 0 163 0
cvc5 0 204488 140288.60 140609.34 2373 2373 97 0 64 33

UNSAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
Bitwuzla 0 504470 17878.47 18180.69 2406 2406 61 3 61 0
Yices2 0 463183 88066.95 88370.60 2376 2376 91 3 91 0
SMTInterpol 0 413985 21110.24 12709.87 2284 2284 186 0 163 0
cvc5 0 204488 140288.60 140609.34 2373 2373 97 0 64 33

24 seconds Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
Bitwuzla 0 433718 6306.66 6585.46 2235 2235 0 235 0 0
Yices2 0 389019 2898.10 3149.02 2042 2042 0 428 0 0
SMTInterpol 0 367414 12529.75 5538.72 2228 2228 12 230 0 0
cvc5 0 150176 731.86 959.88 1839 1839 0 631 0 0