SMT-COMP 2024

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2024

QF_ABV (Unsat Core Track)

Competition results for the QF_ABV logic in the Unsat Core Track.

Results were generated on 2024-07-08

Benchmarks: 1865
Time Limit: 1200 seconds
Memory Limit: 20480 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 SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla01693815317.0619915503.3272781859018596060
Yices2016787711149.74871211337.26798185101851140140
cvc501255478418.8025348605.404013185401854110110

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla01693815317.0619915503.3272781859018596060
Yices2016787711149.74871211337.26798185101851140140
cvc501255478418.8025348605.404013185401854110110

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla01693815317.0619915503.3272781859018596060
Yices2016787711149.74871211337.26798185101851140140
cvc501255478418.8025348605.404013185401854110110

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla0163807300.900856472.703527172201722014300
Yices201577341961.1856522144.20936918280182803700
cvc50115667510.137756680.907532171001710015500