SMT-COMP 2024

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2024

QF_IDL (Unsat Core Track)

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

Results were generated on 2024-07-08

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

Winners

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

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc504431916771.3146386774.34673518018820820
SMTInterpol04043975619.3197822514.13187517017830830
OpenSMT0575083935.389573936.579624606940940
Yices20472076116.1599746118.72627909910910

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc504431916771.3146386774.34673518018820820
SMTInterpol04052787000.3951773135.45897517017830830
OpenSMT0575083935.389573936.579624606940940
Yices20472076116.1599746118.72627909910910

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc504431916771.3146386774.34673518018820820
SMTInterpol04052787000.3951773135.45897517017830830
OpenSMT0575083935.389573936.579624606940940
Yices20472076116.1599746118.72627909910910

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
SMTInterpol05665396.59043734.53197650509500
cvc50193765.8470715.94834710109900
OpenSMT0192826.4098976.51261410109900