SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_RDL (Model Validation Track)

Competition results for the QF_RDL logic in the Model Validation Track. Chart

Results were generated on 2025-08-11

Benchmarks: 109
Time Limit: 1200 seconds
Memory Limit: 30720 GB

Winners

Sequential Performance Parallel Performance SAT Performance (parallel) UNSAT Performance (parallel) 24 seconds Performance (parallel)
Yices2 Yices2 Yices2 - Yices2

Sequential Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
Yices2 0 109 593.97 607.42 109 109 0 0 0 0
OpenSMT 0 107 8468.73 8482.97 107 107 2 0 2 0
cvc5 0 105 1128.11 1140.95 105 105 4 0 4 0
SMTInterpol 0 103 4438.33 3574.03 103 103 6 0 6 0

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
Yices2 0 109 593.97 607.42 109 109 0 0 0 0
OpenSMT 0 107 8468.73 8482.97 107 107 2 0 2 0
cvc5 0 105 1128.11 1140.95 105 105 4 0 4 0
SMTInterpol 0 103 4438.33 3574.03 103 103 6 0 6 0

SAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
Yices2 0 109 593.97 607.42 109 109 0 0 0 0
OpenSMT 0 107 8468.73 8482.97 107 107 2 0 2 0
cvc5 0 105 1128.11 1140.95 105 105 4 0 4 0
SMTInterpol 0 103 4438.33 3574.03 103 103 6 0 6 0

24 seconds Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
Yices2 0 103 88.53 101.13 103 103 0 6 0 0
cvc5 0 97 348.59 360.34 97 97 0 12 0 0
OpenSMT 0 85 189.60 200.04 85 85 0 24 0 0
SMTInterpol 0 80 807.75 383.56 80 80 0 29 0 0