SMT-COMP 2024

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2024

QF_AUFBV (Unsat Core Track)

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

Results were generated on 2024-07-08

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
Yices2Yices2-Yices2Bitwuzla

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices20183671198.0894931201.629549320324040
Bitwuzla015923319.644676322.981413320324040
cvc50442719.16272221.66403625025110110

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices20183671198.0894931201.629549320324040
Bitwuzla015923319.644676322.981413320324040
cvc50442719.16272221.66403625025110110

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices20183671198.0894931201.629549320324040
Bitwuzla015923319.644676322.981413320324040
cvc50442719.16272221.66403625025110110

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Bitwuzla01443080.37072183.402691300300600
Yices201313590.28469792.706152402401200
cvc50442719.16272221.6640362502501100