SMT-COMP 2024

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2024

QF_UFNRA (Single Query Track)

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

Results were generated on 2024-07-08

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

Winners

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

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices204755.63856660.352924731161010
cvc50395976.9579235981.6556243925149090
SMTInterpol03148.167324110.31867231245000

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices204755.63856660.352924731161010
cvc50395976.9579235981.6556243925149090
SMTInterpol03148.167324110.31867231245000

SAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices203151.43897454.5530653131001700
cvc50254507.9523484511.0908222525061760
SMTInterpol010.4642140.432074110301700

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices20164.1995925.7998551601603200
cvc50141469.0055751470.5648021401423220
SMTInterpol02147.70311109.886598202143200

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices204755.63856660.352924731160100
cvc501966.5843668.4968361991002900
SMTInterpol010.4642140.43207411045200