SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_NIA (Single Query Track)

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

Results were generated on 2025-08-11

Benchmarks: 12278
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 z3siri 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 9964
(base +311) 		370765.20 108141.00 10093 6735 3358 2185 0 2106 22
z3siri 0 9692
(base +68) 		364271.71 365517.53 9692 6302 3390 2586 0 2384 8
Yices2 0 9071 78210.95 79338.42 9071 6259 2812 3207 0 3187 9
cvc5 0 8508 1735548.85 1736848.67 8508 5986 2522 3770 0 3498 262
SMTInterpol 0 81 2239.89 1738.06 81 7 74 12197 0 8 0
Z3-alpha-base n 0 9653 222107.49 223333.78 9653 6311 3342 2625 0 2431 1
z3siri-base n 0 9624 244751.36 245972.78 9624 6289 3335 2654 0 2467 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 10093
(base +440) 		646032.41 183604.93 10093 6735 3358 2185 0 2106 22
z3siri 0 9692
(base +68) 		364271.71 365517.53 9692 6302 3390 2586 0 2384 8
Yices2 0 9071 78210.95 79338.42 9071 6259 2812 3207 0 3187 9
cvc5 0 8508 1735548.85 1736848.67 8508 5986 2522 3770 0 3498 262
SMTInterpol 0 81 2239.89 1738.06 81 7 74 12197 0 8 0
Z3-alpha-base n 0 9653 222107.49 223333.78 9653 6311 3342 2625 0 2431 1
z3siri-base n 0 9624 244751.36 245972.78 9624 6289 3335 2654 0 2467 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 6735
(base +424) 		442366.48 125752.64 6735 6735 0 419 5124 405 6
z3siri 0 6302
(base +13) 		255299.99 256112.03 6302 6302 0 852 5124 763 1
Yices2 0 6259 48507.31 49284.07 6259 6259 0 895 5124 889 0
cvc5 0 5986 1641703.85 1642679.93 5986 5986 0 1168 5124 1046 116
SMTInterpol 0 7 1411.61 1242.41 7 7 0 7147 5124 1 0
Z3-alpha-base n 0 6311 159742.03 160544.96 6311 6311 0 843 5124 773 0
z3siri-base n 0 6289 178877.37 179677.35 6289 6289 0 865 5124 797 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
z3siri 0 3390
(base +55) 		108971.72 109405.50 3390 0 3390 268 8620 250 0
Z3-alpha 0 3358
(base +16) 		203665.93 57852.29 3358 0 3358 300 8620 297 3
Yices2 0 2812 29703.64 30054.35 2812 0 2812 846 8620 836 9
cvc5 0 2522 93845.00 94168.74 2522 0 2522 1136 8620 1131 5
SMTInterpol 0 74 828.28 495.65 74 0 74 3584 8620 3 0
Z3-alpha-base n 0 3342 62365.46 62788.82 3342 0 3342 316 8620 315 0
z3siri-base n 0 3335 65873.99 66295.43 3335 0 3335 323 8620 322 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 9078
(base +589) 		80823.62 24945.52 9078 6019 3059 10 3190 0 0
Yices2 0 8589 19652.73 20711.53 8589 5943 2646 10 3679 0 0
z3siri 0 7069
(base -1372) 		21946.36 22819.59 7069 4524 2545 20 5189 0 0
cvc5 0 4745 13431.09 14015.16 4745 2595 2150 10 7523 0 0
SMTInterpol 0 71 264.13 128.80 71 3 68 12084 123 0 0
Z3-alpha-base n 0 8489 29778.88 30832.23 8489 5502 2987 11 3778 0 0
z3siri-base n 0 8441 30643.32 31687.49 8441 5472 2969 11 3826 0 0
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver