SMT-COMP 2024

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2024

QF_UFNRA (Model Validation Track)

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

Results were generated on 2024-07-08

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
cvc5cvc5cvc5-cvc5

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc50275401.400265405.387439272704040
SMTInterpol020.8527620.82703322029000
Yices232844.35372347.157414282803000

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc50275401.400265405.387439272704040
SMTInterpol020.8527620.82703322029000
Yices232844.35372347.157414282803000

SAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc50275401.400265405.387439272704040
SMTInterpol020.8527620.82703322029000
Yices232844.35372347.157414282803000

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc501024.2296325.235121010002100
SMTInterpol020.8527620.82703322029000
Yices232844.35372347.157414282803000