SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_NonLinearIntArith (Single Query Track)

Competition results for the QF_NonLinearIntArith division in the Single Query Track. Chart

Results were generated on 2025-08-11

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

Logics:

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 9965
(base +311) 		370769.84 108145.76 10094 6735 3359 2186 0 2107 22
z3siri 0 9693
(base +68) 		364276.43 365522.37 9693 6302 3391 2587 0 2385 8
Yices2 0 9071 78210.95 79338.42 9071 6259 2812 3209 0 3189 9
cvc5 0 8509 1735785.76 1737085.76 8509 5986 2523 3771 0 3499 262
SMTInterpol 0 81 2239.89 1738.06 81 7 74 12199 0 9 0
Z3-alpha-base n 0 9654 222112.03 223338.45 9654 6311 3343 2626 0 2432 1
z3siri-base n 0 9625 244756.16 245977.71 9625 6289 3336 2655 0 2468 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 10094
(base +440) 		646037.05 183609.69 10094 6735 3359 2186 0 2107 22
z3siri 0 9693
(base +68) 		364276.43 365522.37 9693 6302 3391 2587 0 2385 8
Yices2 0 9071 78210.95 79338.42 9071 6259 2812 3209 0 3189 9
cvc5 0 8509 1735785.76 1737085.76 8509 5986 2523 3771 0 3499 262
SMTInterpol 0 81 2239.89 1738.06 81 7 74 12199 0 9 0
Z3-alpha-base n 0 9654 222112.03 223338.45 9654 6311 3343 2626 0 2432 1
z3siri-base n 0 9625 244756.16 245977.71 9625 6289 3336 2655 0 2468 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 5126 405 6
z3siri 0 6302
(base +13) 		255299.99 256112.03 6302 6302 0 852 5126 763 1
Yices2 0 6259 48507.31 49284.07 6259 6259 0 895 5126 889 0
cvc5 0 5986 1641703.85 1642679.93 5986 5986 0 1168 5126 1046 116
SMTInterpol 0 7 1411.61 1242.41 7 7 0 7147 5126 1 0
Z3-alpha-base n 0 6311 159742.03 160544.96 6311 6311 0 843 5126 773 0
z3siri-base n 0 6289 178877.37 179677.35 6289 6289 0 865 5126 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 3391
(base +55) 		108976.44 109410.35 3391 0 3391 268 8621 250 0
Z3-alpha 0 3359
(base +16) 		203670.57 57857.05 3359 0 3359 300 8621 297 3
Yices2 0 2812 29703.64 30054.35 2812 0 2812 847 8621 837 9
cvc5 0 2523 94081.92 94405.83 2523 0 2523 1136 8621 1131 5
SMTInterpol 0 74 828.28 495.65 74 0 74 3585 8621 3 0
Z3-alpha-base n 0 3343 62370.01 62793.49 3343 0 3343 316 8621 315 0
z3siri-base n 0 3336 65878.79 66300.36 3336 0 3336 323 8621 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 9079
(base +589) 		80828.26 24950.28 9079 6019 3060 10 3191 0 0
Yices2 0 8589 19652.73 20711.53 8589 5943 2646 10 3681 0 0
z3siri 0 7070
(base -1372) 		21951.09 22824.44 7070 4524 2546 20 5190 0 0
cvc5 0 4745 13431.09 14015.16 4745 2595 2150 10 7525 0 0
SMTInterpol 0 71 264.13 128.80 71 3 68 12084 125 0 0
Z3-alpha-base n 0 8490 29783.42 30836.90 8490 5502 2988 11 3779 0 0
z3siri-base n 0 8442 30648.13 31692.42 8442 5472 2970 11 3827 0 0
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver