SMT-COMP 2024

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2024

QF_RDL (Model Validation Track)

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

Results were generated on 2024-07-08

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

Winners

winner_seqwinner_parwinner_satwinner_unsatwinner_24s
Yices2Yices2Yices2-Yices2

Sequential Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices20109380.563705391.56803810910900000
cvc501062251.3436542262.57122110610603030
OpenSMT01068039.5203268052.18013510610603030
SMTInterpol01056558.560285517.72712710510504040

Parallel Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices20109380.563705391.56803810910900000
cvc501062251.3436542262.57122110610603030
OpenSMT01068039.5203268052.18013510610603030
SMTInterpol01056558.560285517.72712710510504040

SAT Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices20109380.563705391.56803810910900000
cvc501062251.3436542262.57122110610603030
OpenSMT01068039.5203268052.18013510610603030
SMTInterpol01056558.560285517.72712710510504040

24 seconds Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices20103101.380241111.71787610310300600
cvc5093328.443694337.8058129393001600
OpenSMT084151.190852159.6257288484002500
SMTInterpol079843.668873373.9683527979003000