SMT-COMP 2024

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2024

UFLRA (Single Query Track)

Competition results for the UFLRA logic in the Single Query Track.

Results were generated on 2024-07-08

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

Winners

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

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc5020.261770.4609422025040
SMTInterpol020.9282390.8782992025040
iProver v3.90248.31718514.8333612025040

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc5020.261770.4609422025040
SMTInterpol020.9282390.8782992025040
iProver v3.90248.31718514.8333612025040

SAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
SMTInterpol00000005240
cvc500000005240
iProver v3.900000005240

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc5020.261770.4609422020500
SMTInterpol020.9282390.8782992020500
iProver v3.90248.31718514.8333612020500

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc5020.261770.4609422020500
SMTInterpol020.9282390.8782992021400
iProver v3.90248.31718514.8333612021400