SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_LinearIntArith (Single Query Track)

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

Results were generated on 2025-08-11

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

Logics:

Winners

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

Sequential Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
OpenSMT 0 5471 317917.99 318645.54 5471 3355 2116 562 7 553 0
Yices2 0 5378 89078.61 89758.64 5378 3296 2082 662 0 649 7
cvc5 0 5370 379623.11 380336.32 5370 3297 2073 670 0 659 5
Z3-alpha 0 5179
(base +139) 		222282.46 60479.52 5316 3371 1945 724 0 700 18
SMTInterpol 0 4801 267924.64 205361.47 4805 2823 1982 1235 0 883 0
Z3-alpha-base n 0 5040 173202.74 173852.15 5040 3186 1854 1000 0 971 22
(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
OpenSMT 0 5471 317917.99 318645.54 5471 3355 2116 562 7 553 0
Yices2 0 5378 89078.61 89758.64 5378 3296 2082 662 0 649 7
cvc5 0 5370 379623.11 380336.32 5370 3297 2073 670 0 659 5
Z3-alpha 0 5316
(base +276) 		558629.74 145316.44 5316 3371 1945 724 0 700 18
SMTInterpol 0 4805 274831.06 209356.87 4805 2823 1982 1235 0 883 0
Z3-alpha-base n 0 5040 173202.74 173852.15 5040 3186 1854 1000 0 971 22
(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 3371
(base +185) 		352652.82 91128.81 3371 3371 0 316 2353 306 10
OpenSMT 0 3355 238639.05 239090.37 3355 3355 0 331 2354 331 0
cvc5 0 3297 191610.23 192041.52 3297 3297 0 390 2353 385 5
Yices2 0 3296 72989.67 73408.42 3296 3296 0 391 2353 391 0
SMTInterpol 0 2823 156237.31 129397.05 2823 2823 0 864 2353 703 0
Z3-alpha-base n 0 3186 117803.80 118215.74 3186 3186 0 501 2353 499 2
(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
OpenSMT 0 2116 79278.94 79555.17 2116 0 2116 152 3772 149 0
Yices2 0 2082 16088.94 16350.21 2082 0 2082 191 3767 191 0
cvc5 0 2073 188012.87 188294.79 2073 0 2073 200 3767 200 0
SMTInterpol 0 1982 118593.75 79959.82 1982 0 1982 291 3767 152 0
Z3-alpha 0 1945
(base +91) 		205976.92 54187.64 1945 0 1945 328 3767 327 1
Z3-alpha-base n 0 1854 55398.93 55636.41 1854 0 1854 419 3767 401 17
(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
Yices2 0 5085 4793.62 5426.72 5085 3066 2019 6 949 0 0
Z3-alpha 0 4648
(base +342) 		33837.64 11756.41 4648 2934 1714 6 1386 0 0
OpenSMT 0 3973 11065.23 11559.63 3973 2351 1622 9 2058 0 0
cvc5 0 3782 7747.19 8211.92 3782 2402 1380 6 2252 0 0
SMTInterpol 0 3381 26943.96 12293.03 3381 2102 1279 217 2442 0 0
Z3-alpha-base n 0 4306 10224.64 10757.48 4306 2753 1553 6 1728 0 0
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver