SMT-COMP 2024

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2024

QF_Datatypes (Unsat Core Track)

Competition results for the QF_Datatypes division in the Unsat Core Track.

Results were generated on 2024-07-08

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

Logics:

Winners

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

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc501.352497e+0629842.40733929865.063551174017422602260
SMTInterpol013931933837.32749819158.354062260026014001390

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc501.352497e+0629842.40733929865.063551174017422602260
SMTInterpol021325873302.82007339995.570686260026014001390

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
cvc501.352497e+0629842.40733929865.063551174017422602260
SMTInterpol021325873302.82007339995.570686260026014001390

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
SMTInterpol031711364.929553568.4595651580158024200
cvc50507164.733038175.0624851030103029700