SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_AUFBV (Unsat Core Track)

Competition results for the QF_AUFBV logic in the Unsat Core Track. Chart

Results were generated on 2025-08-11

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

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
Bitwuzla0183981388.501392.7933333030
Yices2018036480.00483.8531315050
SMTInterpol010228223.51136.772222140130
cvc50442716.8019.882525110101

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla0183981388.501392.7933333030
Yices2018036480.00483.8531315050
SMTInterpol010228223.51136.772222140130
cvc50442716.8019.882525110101

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla0183981388.501392.7933333030
Yices2018036480.00483.8531315050
SMTInterpol010228223.51136.772222140130
cvc50442716.8019.882525110101

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla016038132.30135.8929290700
Yices201309491.3194.36252501100
SMTInterpol09450105.0342.80212101500
cvc50442716.8019.88252501100