SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_UFBV (Parallel Track)

Competition results for the QF_UFBV logic in the Parallel Track. Chart

Results were generated on 2025-08-11

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

Winners

Sequential Performance Parallel Performance SAT Performance (parallel) UNSAT Performance (parallel) 24 seconds Performance (parallel)
- Bitwuzla Bitwuzla Bitwuzla 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 9 44645.57 1752.27 9 5 4 10 0 10 0
Yices2 0 3 55081.79 434.49 3 3 0 16 0 16 0
Bitwuzla-32core n 0 0 0.00 0.00 0 0 0 19 0 0 0
Bitwuzla-64core n 0 0 0.00 0.00 0 0 0 19 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 1 13 1 0
Yices2 0 3 55081.79 434.49 3 3 0 3 13 3 0
Bitwuzla-32core n 0 0 0.00 0.00 0 0 0 6 13 0 0
Bitwuzla-64core n 0 0 0.00 0.00 0 0 0 6 13 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
Bitwuzla 0 4 310.97 12.82 4 0 4 0 15 0 0
Yices2 0 0 0.00 0.00 0 0 0 4 15 4 0
Bitwuzla-32core n 0 0 0.00 0.00 0 0 0 4 15 0 0
Bitwuzla-64core n 0 0 0.00 0.00 0 0 0 4 15 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 15 0 0
Yices2 0 1 76.60 1.20 1 1 0 0 18 0 0
Bitwuzla-32core n 0 0 0.00 0.00 0 0 0 19 0 0 0
Bitwuzla-64core n 0 0 0.00 0.00 0 0 0 19 0 0 0
n: non-competing solver