SMT-COMP 2024

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2024

QF_UFBV (Unsat Core Track)

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

Results were generated on 2024-07-08

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

Winners

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

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc5083031012084.83179712118.6946033170317100100
Yices206511142190.2132512218.058062700270570561
Bitwuzla038850415225.36116515260.17543732103216051

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc5083031012084.83179712118.6946033170317100100
Yices206511142190.2132512218.058062700270570561
Bitwuzla038850415225.36116515260.17543732103216051

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc5083031012084.83179712118.6946033170317100100
Yices206511142190.2132512218.058062700270570561
Bitwuzla038850415225.36116515260.17543732103216051

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices2064864752.79652979.466031267026706000
Bitwuzla010240136.644758163.601521270027005700
cvc501945675.132252700.135835249024907800