SMT-COMP 2024

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2024

QF_UFIDL (Model Validation Track)

Competition results for the QF_UFIDL logic in the Model Validation Track.

Results were generated on 2024-07-08

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

Winners

winner_seqwinner_parwinner_satwinner_unsatwinner_24s
OpenSMTOpenSMTOpenSMT-OpenSMT

Sequential Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
OpenSMT02018703.4085578725.48991420120105050
cvc5017826043.15288126065.1655641781780280280
SMTInterpol017723556.16236511336.3243541821820240240
Yices2014214321.4259914338.4877971421420640640

Parallel Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
OpenSMT02018703.4085578725.48991420120105050
SMTInterpol018232661.46427315531.2178131821820240240
cvc5017826043.15288126065.1655641781780280280
Yices2014214321.4259914338.4877971421420640640

SAT Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
OpenSMT02018703.4085578725.48991420120105050
SMTInterpol018232661.46427315531.2178131821820240240
cvc5017826043.15288126065.1655641781780280280
Yices2014214321.4259914338.4877971421420640640

24 seconds Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
OpenSMT0153495.861243511.250952153153005300
SMTInterpol01291400.184953481.493826129129007700
Yices2010956.60009767.524245109109009700
cvc5010772.41375783.122387107107009900