SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_UFIDL (Model Validation Track)

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

Results were generated on 2025-08-11

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

Winners

Sequential Performance Parallel Performance SAT Performance (parallel) UNSAT Performance (parallel) 24 seconds Performance (parallel)
OpenSMT OpenSMT OpenSMT - SMTInterpol

Sequential Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
OpenSMT 0 201 7873.14 7899.44 201 201 5 0 5 0
SMTInterpol 0 181 9092.28 7717.80 181 181 25 0 25 0
cvc5 0 177 24902.53 24928.37 177 177 29 0 29 0
Yices2 0 143 14617.50 14637.50 143 143 63 0 63 0

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
OpenSMT 0 201 7873.14 7899.44 201 201 5 0 5 0
SMTInterpol 0 181 9092.28 7717.80 181 181 25 0 25 0
cvc5 0 177 24902.53 24928.37 177 177 29 0 29 0
Yices2 0 143 14617.50 14637.50 143 143 63 0 63 0

SAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
OpenSMT 0 201 7873.14 7899.44 201 201 5 0 5 0
SMTInterpol 0 181 9092.28 7717.80 181 181 25 0 25 0
cvc5 0 177 24902.53 24928.37 177 177 29 0 29 0
Yices2 0 143 14617.50 14637.50 143 143 63 0 63 0

24 seconds Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
SMTInterpol 0 164 1430.07 605.32 164 164 0 42 0 0
OpenSMT 0 162 504.17 524.47 162 162 0 44 0 0
Yices2 0 109 64.88 78.44 109 109 0 97 0 0
cvc5 0 107 75.54 88.71 107 107 0 99 0 0