SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_UFNIA (Model Validation Track)

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

Results were generated on 2025-08-11

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

Winners

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

Sequential Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
cvc5 0 205 9890.86 9917.28 205 205 95 0 53 0
SMTInterpol 0 141 19067.46 17386.75 141 141 159 0 2 0
Yices2 105 142 1618.20 1636.25 142 142 158 0 0 0

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
cvc5 0 205 9890.86 9917.28 205 205 95 0 53 0
SMTInterpol 0 141 19067.46 17386.75 141 141 159 0 2 0
Yices2 105 142 1618.20 1636.25 142 142 158 0 0 0

SAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
cvc5 0 205 9890.86 9917.28 205 205 95 0 53 0
SMTInterpol 0 141 19067.46 17386.75 141 141 159 0 2 0
Yices2 105 142 1618.20 1636.25 142 142 158 0 0 0

24 seconds Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Unsolved Abstained Timeout Memout
cvc5 0 173 88.59 109.65 173 173 39 88 0 0
SMTInterpol 0 79 212.09 130.19 79 79 148 73 0 0
Yices2 98 130 236.46 252.78 130 130 150 20 0 0