SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_Equality_Bitvec (Parallel Track)

Competition results for the QF_Equality_Bitvec division in the Parallel Track. Chart

Results were generated on 2025-08-11

Benchmarks: 47
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 Yices2 Bitwuzla

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
Bitwuzla 0 11 93585.60 2577.64 11 5 6 36 0 36 0
Yices2 0 10 437330.95 3425.46 10 3 7 37 0 37 0
Bitwuzla-32core n 0 0 0.00 0.00 0 0 0 47 0 0 0
Bitwuzla-64core n 0 0 0.00 0.00 0 0 0 47 0 0 0
n: non-competing solver

SAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
Bitwuzla 0 5 44334.59 1739.45 5 5 0 2 40 2 0
Yices2 0 3 55081.79 434.49 3 3 0 4 40 4 0
Bitwuzla-32core n 0 0 0.00 0.00 0 0 0 7 40 0 0
Bitwuzla-64core n 0 0 0.00 0.00 0 0 0 7 40 0 0
n: non-competing solver

UNSAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
Yices2 0 7 382249.16 2990.98 7 0 7 20 20 20 0
Bitwuzla 0 6 49251.01 838.19 6 0 6 21 20 21 0
Bitwuzla-32core n 0 0 0.00 0.00 0 0 0 27 20 0 0
Bitwuzla-64core n 0 0 0.00 0.00 0 0 0 27 20 0 0
n: non-competing solver

24 seconds Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
Bitwuzla 0 4 310.97 12.82 4 0 4 0 43 0 0
Yices2 0 1 76.60 1.20 1 1 0 0 46 0 0
Bitwuzla-32core n 0 0 0.00 0.00 0 0 0 47 0 0 0
Bitwuzla-64core n 0 0 0.00 0.00 0 0 0 47 0 0 0
n: non-competing solver