SMT-COMP 2024

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2024

QF_LRA (Unsat Core Track)

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

Results were generated on 2024-07-08

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
OpenSMTOpenSMT-OpenSMTYices2

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
OpenSMT01638228427.1170418449.80848820202022020
Yices2015269020139.63920420161.6020821660166380380
cvc5014190924285.65789224309.661611940194100100
SMTInterpol010836844952.20121339793.9316991690169350350

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
OpenSMT01638228427.1170418449.80848820202022020
Yices2015269020139.63920420161.6020821660166380380
cvc5014190924285.65789224309.661611940194100100
SMTInterpol010893747436.61786942040.3605711690169350350

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
OpenSMT01638228427.1170418449.80848820202022020
Yices2015269020139.63920420161.6020821660166380380
cvc5014190924285.65789224309.661611940194100100
SMTInterpol010893747436.61786942040.3605711690169350350

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices20106706613.715135622.6133687087011700
OpenSMT095813808.135665822.368894140014006400
cvc5034158697.048152704.3335272072013200
SMTInterpol020920763.391416354.59690131031017300