SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

UFNIRA (Single Query Track)

Competition results for the UFNIRA logic in the Single Query Track. Chart

Results were generated on 2025-08-11

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

Winners

Sequential Performance Parallel Performance SAT Performance (parallel) UNSAT Performance (parallel) 24 seconds Performance (parallel)
cvc5 iProver v3.9.3 - iProver v3.9.3 cvc5

Sequential Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
cvc5 0 83 616.93 627.38 83 0 83 183 0 46 1
iProver v3.9.3 0 81 1846.06 531.06 90 0 90 176 0 176 0
SMTInterpol 0 18 10.30 9.10 18 0 18 248 0 118 0
UltimateEliminator+MathSAT 0 0 0.00 0.00 0 0 0 266 0 7 0

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
iProver v3.9.3 0 90 28316.47 7209.67 90 0 90 176 0 176 0
cvc5 0 83 616.93 627.38 83 0 83 183 0 46 1
SMTInterpol 0 18 10.30 9.10 18 0 18 248 0 118 0
UltimateEliminator+MathSAT 0 0 0.00 0.00 0 0 0 266 0 7 0

SAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
SMTInterpol 0 0 0.00 0.00 0 0 0 79 187 51 0
UltimateEliminator+MathSAT 0 0 0.00 0.00 0 0 0 79 187 1 0
cvc5 0 0 0.00 0.00 0 0 0 79 187 4 0
iProver v3.9.3 0 0 0.00 0.00 0 0 0 79 187 79 0

UNSAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
iProver v3.9.3 0 90 28316.47 7209.67 90 0 90 97 79 97 0
cvc5 0 83 616.93 627.38 83 0 83 104 79 42 1
SMTInterpol 0 18 10.30 9.10 18 0 18 169 79 67 0
UltimateEliminator+MathSAT 0 0 0.00 0.00 0 0 0 187 79 6 0

24 seconds Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
cvc5 0 81 52.31 62.40 81 0 81 136 49 0 0
iProver v3.9.3 0 73 181.01 92.86 73 0 73 0 193 0 0
SMTInterpol 0 18 10.30 9.10 18 0 18 130 118 0 0
UltimateEliminator+MathSAT 0 0 0.00 0.00 0 0 0 259 7 0 0