SMT-COMP 2024

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2024

QF_NonLinearIntArith (Model Validation Track)

Competition results for the QF_NonLinearIntArith division in the Model Validation Track.

Results were generated on 2024-07-08

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

Logics:

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
Yices2Yices2Yices2-Yices2

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices20611869531.47207870159.091226118611801385013841
cvc504756249431.399861249952.9843924756475602747027470
SMTInterpol04424.651403264.4056474407499030

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices20611869531.47207870159.091226118611801385013841
cvc504756249431.399861249952.9843924756475602747027470
SMTInterpol04424.651403264.4056474407499030

SAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices20611869531.47207870159.091226118611801385013841
cvc504756249431.399861249952.9843924756475602747027470
SMTInterpol04424.651403264.4056474407499030

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
Yices20569510801.16213311372.7799655695569500180800
cvc50359913696.46910314057.1218583599359900390400
SMTInterpol0219.6624486.68042122074505100