SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

BVFPLRA (Single Query Track)

Competition results for the BVFPLRA logic in the Single Query Track. Chart

Results were generated on 2025-08-11

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
BitwuzlaBitwuzlaBitwuzlacvc5Bitwuzla

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla0257101.82133.76257232259090
cvc50252124.36155.6425222725140140
UltimateEliminator+MathSAT01693.5957.6216133250000

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla0257101.82133.76257232259090
cvc50252124.36155.6425222725140140
UltimateEliminator+MathSAT01693.5957.6216133250000

SAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla023279.36108.19232232013310
cvc50227108.32136.49227227063360
UltimateEliminator+MathSAT01377.8148.63131302203300

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc502516.0419.1525025024100
Bitwuzla02522.4625.5725025024100
UltimateEliminator+MathSAT0315.789.003032224100

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla0257101.82133.76257232250900
cvc50252124.36155.642522272501400
UltimateEliminator+MathSAT01693.5957.6216133250000