SMT-COMP 2024

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2024

QF_BVFPLRA (Single Query Track)

Competition results for the QF_BVFPLRA logic in the Single Query Track.

Results were generated on 2024-07-08

Benchmarks: 75
Time Limit: 1200 seconds
Memory Limit: 20480 GB

Winners

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

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla0752314.8375212323.1157187542330000
COLIBRI0561128.8290451134.61066756322419080
cvc50564978.6838514985.205086563224190100

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla0752314.8375212323.1157187542330000
COLIBRI0561128.8290451134.61066756322419080
cvc50564978.6838514985.205086563224190100

SAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla042235.950634240.203494242003300
cvc5032190.239299193.50324632320103310
COLIBRI0321098.9291551102.20515432320103310

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla0332078.8868872082.9122273303304200
COLIBRI02429.89989132.4055142402494270
cvc50244788.4445524791.7018412402494290

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla067120.752068127.4780896739280800
COLIBRI05564.50342170.18597155312411900
cvc5045158.856834163.36921445301592100