SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

Bitvec (Unsat Core Track)

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

Results were generated on 2025-08-11

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

Logics:

Winners

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

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc506412549.6112586.29283283170170
Bitwuzla0191448.511477.61230230700700
UltimateEliminator+MathSAT0010.204.3322298000
SMTInterpol0016.555.62112990360

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc506412549.6112586.29283283170170
Bitwuzla0191448.511477.61230230700700
UltimateEliminator+MathSAT0010.204.3322298000
SMTInterpol0016.555.62112990360

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc506412549.6112586.29283283170170
Bitwuzla0191448.511477.61230230700700
UltimateEliminator+MathSAT0010.204.3322298000
SMTInterpol0016.555.62112990360

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc5046353.63379.7121221208800
Bitwuzla01986.88113.8721621608400
UltimateEliminator+MathSAT0010.204.3322298000
SMTInterpol0016.555.62112128700