SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

LIA (Single Query Track)

Competition results for the LIA logic in the Single Query 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)
Z3-alpha Z3-alpha Z3-alpha cvc5 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 232
(base -2) 		633.23 233.32 234 111 123 66 0 66 0
cvc5 0 223 62.53 89.98 223 100 123 77 0 77 0
Amaya 0 190 5109.81 5134.13 190 88 102 110 0 12 93
YicesQS 0 181 56.23 78.61 181 98 83 119 0 119 0
UltimateEliminator+MathSAT 0 176 6824.91 5749.27 176 59 117 124 0 42 0
iProver v3.9.3 0 89 4177.28 1138.83 90 0 90 210 0 201 0
SMTInterpol 0 34 30.17 22.12 34 3 31 266 0 60 0
Z3-alpha-base n 0 234 598.98 627.85 234 111 123 66 0 66 0
(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 234
(base +0) 		5473.23 1444.28 234 111 123 66 0 66 0
cvc5 0 223 62.53 89.98 223 100 123 77 0 77 0
Amaya 0 190 5109.81 5134.13 190 88 102 110 0 12 93
YicesQS 0 181 56.23 78.61 181 98 83 119 0 119 0
UltimateEliminator+MathSAT 0 176 6824.91 5749.27 176 59 117 124 0 42 0
iProver v3.9.3 0 90 5468.75 1466.60 90 0 90 210 0 201 0
SMTInterpol 0 34 30.17 22.12 34 3 31 266 0 60 0
Z3-alpha-base n 0 234 598.98 627.85 234 111 123 66 0 66 0
(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 111
(base +0) 		5433.46 1394.49 111 111 0 66 123 66 0
cvc5 0 100 38.88 51.14 100 100 0 77 123 77 0
YicesQS 0 98 42.60 54.73 98 98 0 79 123 79 0
Amaya 0 88 3276.58 3287.90 88 88 0 89 123 8 79
UltimateEliminator+MathSAT 0 59 5497.56 4880.93 59 59 0 118 123 38 0
SMTInterpol 0 3 1.26 1.31 3 3 0 174 123 50 0
iProver v3.9.3 0 0 0.00 0.00 0 0 0 177 123 174 0
Z3-alpha-base n 0 111 576.71 590.47 111 111 0 66 123 66 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
cvc5 0 123 23.65 38.85 123 0 123 0 177 0 0
Z3-alpha 0 123
(base +0) 		39.76 49.79 123 0 123 0 177 0 0
UltimateEliminator+MathSAT 0 117 1327.36 868.34 117 0 117 6 177 4 0
Amaya 0 102 1833.24 1846.23 102 0 102 21 177 4 14
iProver v3.9.3 0 90 5468.75 1466.60 90 0 90 33 177 27 0
YicesQS 0 83 13.63 23.88 83 0 83 40 177 40 0
SMTInterpol 0 31 28.91 20.81 31 0 31 92 177 10 0
Z3-alpha-base n 0 123 22.27 37.39 123 0 123 0 177 0 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 230
(base +1) 		139.93 109.32 230 107 123 0 70 0 0
cvc5 0 223 62.53 89.98 223 100 123 0 77 0 0
YicesQS 0 180 29.81 52.06 180 97 83 0 120 0 0
Amaya 0 170 361.76 382.99 170 72 98 0 130 0 0
UltimateEliminator+MathSAT 0 163 1423.37 610.02 163 48 115 82 55 0 0
iProver v3.9.3 0 82 849.95 280.68 82 0 82 4 214 0 0
SMTInterpol 0 34 30.17 22.12 34 3 31 174 92 0 0
Z3-alpha-base n 0 229 46.48 74.64 229 106 123 0 71 0 0
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver