SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_Bitvec (Unsat Core Track)

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

Results were generated on 2025-08-11

Benchmarks: 2949
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 2362905 66262.55 66626.81 2828 2828 121 0 121 0
Yices2 0 1966197 33688.25 34017.58 2653 2653 296 0 296 0
cvc5 0 1217420 165420.98 165742.96 2378 2378 571 0 565 6
SMTInterpol 0 697411 165525.20 148359.62 2104 2104 845 0 731 0

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
Bitwuzla 0 2362905 66262.55 66626.81 2828 2828 121 0 121 0
Yices2 0 1966197 33688.25 34017.58 2653 2653 296 0 296 0
cvc5 0 1217420 165420.98 165742.96 2378 2378 571 0 565 6
SMTInterpol 0 699169 170931.22 153111.74 2104 2104 845 0 731 0

UNSAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
Bitwuzla 0 2362905 66262.55 66626.81 2828 2828 121 0 121 0
Yices2 0 1966197 33688.25 34017.58 2653 2653 296 0 296 0
cvc5 0 1217420 165420.98 165742.96 2378 2378 571 0 565 6
SMTInterpol 0 699169 170931.22 153111.74 2104 2104 845 0 731 0

24 seconds Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved UNSAT Unsolved Abstained Timeout Memout
Bitwuzla 0 1946208 3551.09 3874.13 2591 2591 0 358 0 0
Yices2 0 1926132 1768.65 2078.24 2529 2529 0 420 0 0
cvc5 0 524459 6545.77 6762.21 1745 1745 0 1204 0 0
SMTInterpol 0 291954 12231.19 5177.74 1614 1614 47 1288 0 0