SMT-COMP 2024

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2024

QF_ANIA (Single Query Track)

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

Results were generated on 2024-07-08

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

Winners

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

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices201344748.7169114763.12241913411816210210
SMTInterpol01331486.5740461031.17189313311617220100
cvc501246069.2965556082.76473712410915310310

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices201344748.7169114763.12241913411816210210
SMTInterpol01331486.5740461031.17189313311617220100
cvc501246069.2965556082.76473712410915310310

SAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices201183811.7790793824.406876118118043340
SMTInterpol0116672.115192444.414735116116063300
cvc501094057.5979634069.33476310910901333130

UNSAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
SMTInterpol017814.458853586.7571591701713125100
Yices2016936.937832938.7155441601614125140
cvc50152011.6985922013.4299741501515125150

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
SMTInterpol0126444.498727203.67316712611412101900
cvc50108332.820394343.684679108981004700
Yices20100186.469326196.500517100871305500