SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_Equality_Bitvec (Unsat Core Track)

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

Results were generated on 2025-08-11

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

Logics:

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
BitwuzlaBitwuzla-BitwuzlaBitwuzla

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla050447017878.4718180.6924062406613610
Yices2046318388066.9588370.6023762376913910
SMTInterpol041398521110.2412709.872284228418601630
cvc50204488140288.60140609.34237323739706433

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla050447017878.4718180.6924062406613610
Yices2046318388066.9588370.6023762376913910
SMTInterpol041398521110.2412709.872284228418601630
cvc50204488140288.60140609.34237323739706433

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla050447017878.4718180.6924062406613610
Yices2046318388066.9588370.6023762376913910
SMTInterpol041398521110.2412709.872284228418601630
cvc50204488140288.60140609.34237323739706433

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla04337186306.666585.4622352235023500
Yices203890192898.103149.0220422042042800
SMTInterpol036741412529.755538.72222822281223000
cvc50150176731.86959.8818391839063100