SMT-COMP 2024

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2024

QF_UFLIA (Unsat Core Track)

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

Results were generated on 2024-07-08

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

Winners

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

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices20166638448.789917450.912171190190000
SMTInterpol01665971326.261382968.226961190190000
cvc50149120261.098371262.915393180181010
OpenSMT050226.36784627.981339160163020

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices20166638448.789917450.912171190190000
SMTInterpol01665971326.261382968.226961190190000
cvc50149120261.098371262.915393180181010
OpenSMT050226.36784627.981339160163020

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices20166638448.789917450.912171190190000
SMTInterpol01665971326.261382968.226961190190000
cvc50149120261.098371262.915393180181010
OpenSMT050226.36784627.981339160163020

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices2014915510.37931512.187951180180100
cvc505152.6052894.306694170170200
SMTInterpol051513.9586189.231826170170200
OpenSMT0191.9211573.433748150151300