SMT-COMP 2024

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2024

AUFDTLIRA (Single Query Track)

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

Results were generated on 2024-07-08

Benchmarks: 4721
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
cvc5041945060.9307565482.68247341940419452705241
iProver v3.903567182529.9152650218.54094237520375296909690
SMTInterpol0343327412.86894417010.7667613433034331288011520

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc5041945060.9307565482.68247341940419452705241
iProver v3.903752645752.432163167847.83242737520375296909690
SMTInterpol0343327412.86894417010.7667613433034331288011520

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc5041945060.9307565482.682473419404194152610
iProver v3.903752645752.432163167847.8324273752037524435264430
SMTInterpol0343327412.86894417010.7667613433034337625267190

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc504165699.0140951116.615134416504165055600
SMTInterpol0336415278.1067276572.327005336403364104125300
iProver v3.90305928843.6569829892.8252223059030590166200