SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_ABV (Parallel Track)

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

Results were generated on 2025-08-11

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

Winners

Sequential Performance Parallel Performance SAT Performance (parallel) UNSAT Performance (parallel) 24 seconds Performance (parallel)
- Yices2 - Yices2 -

Parallel 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 17 0 17 0
Bitwuzla 0 2 48940.03 825.37 2 0 2 22 0 22 0
Bitwuzla-32core n 0 0 0.00 0.00 0 0 0 24 0 0 0
Bitwuzla-64core n 0 0 0.00 0.00 0 0 0 24 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 0 0.00 0.00 0 0 0 1 23 1 0
Yices2 0 0 0.00 0.00 0 0 0 1 23 1 0
Bitwuzla-32core n 0 0 0.00 0.00 0 0 0 1 23 0 0
Bitwuzla-64core n 0 0 0.00 0.00 0 0 0 1 23 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 16 1 16 0
Bitwuzla 0 2 48940.03 825.37 2 0 2 21 1 21 0
Bitwuzla-32core n 0 0 0.00 0.00 0 0 0 23 1 0 0
Bitwuzla-64core n 0 0 0.00 0.00 0 0 0 23 1 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-32core n 0 0 0.00 0.00 0 0 0 24 0 0 0
Bitwuzla-64core n 0 0 0.00 0.00 0 0 0 24 0 0 0
n: non-competing solver