SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

NIA (Single Query Track)

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

Results were generated on 2025-08-11

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

Winners

Sequential Performance Parallel Performance SAT Performance (parallel) UNSAT Performance (parallel) 24 seconds Performance (parallel)
Z3-alpha Z3-alpha Z3-alpha Z3-alpha Z3-alpha

Sequential Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
Z3-alpha 0 238
(base +17) 		2042.11 730.14 238 79 159 16 0 13 1
cvc5 0 225 25317.53 25348.31 225 78 147 29 0 29 0
UltimateEliminator+MathSAT 0 138 664.54 298.42 138 42 96 116 0 30 0
YicesQS 0 107 583.24 596.44 107 65 42 147 0 147 0
iProver v3.9.3 0 35 1450.49 402.10 47 0 47 207 0 207 0
SMTInterpol 0 20 29.01 16.51 20 14 6 234 0 1 0
Amaya 2 206 585.67 611.64 208 51 157 46 0 6 0
Z3-alpha-base n 0 221 1653.49 1681.16 221 72 149 33 0 26 1
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver

Parallel Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
Z3-alpha 0 238
(base +17) 		2042.11 730.14 238 79 159 16 0 13 1
cvc5 0 225 25317.53 25348.31 225 78 147 29 0 29 0
UltimateEliminator+MathSAT 0 138 664.54 298.42 138 42 96 116 0 30 0
YicesQS 0 107 583.24 596.44 107 65 42 147 0 147 0
iProver v3.9.3 0 47 43167.83 10889.39 47 0 47 207 0 207 0
SMTInterpol 0 20 29.01 16.51 20 14 6 234 0 1 0
Amaya 2 206 585.67 611.64 208 51 157 46 0 6 0
Z3-alpha-base n 0 221 1653.49 1681.16 221 72 149 33 0 26 1
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver

SAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
Z3-alpha 0 79
(base +7) 		138.89 112.87 79 79 0 3 172 2 1
cvc5 0 78 314.35 324.02 78 78 0 4 172 4 0
YicesQS 0 65 31.81 39.79 65 65 0 17 172 17 0
UltimateEliminator+MathSAT 0 42 200.97 90.11 42 42 0 40 172 12 0
SMTInterpol 0 14 24.05 13.09 14 14 0 68 172 0 0
iProver v3.9.3 0 0 0.00 0.00 0 0 0 82 172 82 0
Amaya 2 51 302.44 309.04 53 51 2 29 172 2 0
Z3-alpha-base n 0 72 1107.06 1116.17 72 72 0 10 172 6 0
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver

UNSAT Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
Z3-alpha 0 159
(base +10) 		1903.21 617.26 159 0 159 8 87 6 0
Amaya 0 155 283.23 302.60 155 0 155 12 87 4 0
cvc5 0 147 25003.18 25024.30 147 0 147 20 87 20 0
UltimateEliminator+MathSAT 0 96 463.57 208.31 96 0 96 71 87 16 0
iProver v3.9.3 0 47 43167.83 10889.39 47 0 47 120 87 120 0
YicesQS 0 42 551.42 556.66 42 0 42 125 87 125 0
SMTInterpol 0 6 4.96 3.42 6 0 6 161 87 1 0
Z3-alpha-base n 0 149 546.43 564.99 149 0 149 18 87 16 0
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver

24 seconds Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
Z3-alpha 0 235
(base +20) 		540.21 311.38 235 78 157 0 19 0 0
cvc5 0 142 101.52 119.06 142 77 65 0 112 0 0
UltimateEliminator+MathSAT 0 138 664.54 298.42 138 42 96 85 31 0 0
YicesQS 0 105 78.20 91.11 105 65 40 0 149 0 0
iProver v3.9.3 0 29 541.58 164.92 29 0 29 0 225 0 0
SMTInterpol 0 20 29.01 16.51 20 14 6 229 5 0 0
Amaya 2 205 452.54 478.37 207 50 157 36 11 0 0
Z3-alpha-base n 0 215 298.03 324.66 215 70 145 2 37 0 0
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver