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 PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
-BitwuzlaBitwuzlaBitwuzlaBitwuzla

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla0944645.571752.27954100100
Yices20355081.79434.49330160160
Bitwuzla-32core n000.000.0000019000
Bitwuzla-64core n000.000.0000019000
n: non-competing solver

SAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla0544334.591739.4555011310
Yices20355081.79434.4933031330
Bitwuzla-32core n000.000.0000061300
Bitwuzla-64core n000.000.0000061300
n: non-competing solver

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla04310.9712.8240401500
Yices2000.000.0000041540
Bitwuzla-32core n000.000.0000041500
Bitwuzla-64core n000.000.0000041500
n: non-competing solver

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla04310.9712.8240401500
Yices20176.601.2011001800
Bitwuzla-32core n000.000.0000019000
Bitwuzla-64core n000.000.0000019000
n: non-competing solver