SMT-COMP 2024

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2024

QF_NRA (Model Validation Track)

Competition results for the QF_NRA logic in the Model Validation Track.

Results were generated on 2024-07-08

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24 seconds Performance (parallel)
SMT-RATSMT-RATSMT-RAT-SMT-RAT

Sequential Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
SMT-RAT0247128629.11401928880.65959424712471029501640
cvc50197613039.01786113239.58836519761976079001670
SMTInterpol0203613.6086673184.852273202002746010
Yices243520726743.974196953.1966320722072069401190

Parallel Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
SMT-RAT0247128629.11401928880.65959424712471029501640
cvc50197613039.01786113239.58836519761976079001670
SMTInterpol0203613.6086673184.852273202002746010
Yices243520726743.974196953.1966320722072069401190

SAT Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
SMT-RAT0247128629.11401928880.65959424712471029501640
cvc50197613039.01786113239.58836519761976079001670
SMTInterpol0203613.6086673184.852273202002746010
Yices243520726743.974196953.1966320722072069401190

24 seconds Performance Performance

SolverError ScoreCorrect ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeoutMemout
SMT-RAT02388693.493476932.34488623882388012525300
cvc501919913.4271191105.20920119191919061623100
SMTInterpol0839.19938115.83226488027401800
Yices24322041712.648246917.03920220412041056915600