SMT-COMP 2024

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2024

QF_AX (Unsat Core Track)

Competition results for the QF_AX logic in the Unsat Core Track.

Results were generated on 2024-07-08

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
Yices2Yices2-Yices2Yices2

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices203864028.78786549.0076720202020000
cvc5032252107.124549127.31185520202020000
SMTInterpol0484564.812213239.9680720202020000
OpenSMT0395200.699124220.9189120202020000

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices203864028.78786549.0076720202020000
cvc5032252107.124549127.31185520202020000
SMTInterpol0484564.812213239.9680720202020000
OpenSMT0395200.699124220.9189120202020000

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices203864028.78786549.0076720202020000
cvc5032252107.124549127.31185520202020000
SMTInterpol0484564.812213239.9680720202020000
OpenSMT0395200.699124220.9189120202020000

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices203864028.78786549.0076720202020000
cvc5032252107.124549127.31185520202020000
SMTInterpol0484564.812213239.9680720202020000
OpenSMT0395138.079686158.19744320102010100