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

winner_seqwinner_parwinner_satwinner_unsatwinner_24s
Yices2Yices2Yices2Yices2Yices2

Sequential Performance

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

Parallel Performance

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

SAT Performance

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

UNSAT Performance

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

24 seconds Performance

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