SMT-COMP 2024

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2024

UFDTLIA (Single Query Track)

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

Results were generated on 2024-07-08

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
cvc5cvc5cvc5cvc5cvc5

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc5021157389.55553857422.4111872111210830830
iProver v3.90426057.8784271627.566855205224202420
SMTInterpol0373266.5127892871.5997873703725702550

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc5021157389.55553857422.4111872111210830830
iProver v3.905231756.2428998154.2669955205224202420
SMTInterpol0373266.5127892871.5997873703725702550

SAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc501580.876725581.213734110029300
SMTInterpol0000000129300
iProver v3.90000000129310

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc5021056808.67881356841.197452210021008400
iProver v3.905231756.2428998154.26699552052158841580
SMTInterpol0373266.5127892871.59978737037173841720

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc503914.68494618.57054439039025500
SMTInterpol028188.71759987.75898928028026600
iProver v3.9014227.03017470.54794314014028000