SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_LIA (Single Query Track)

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

Results were generated on 2025-08-11

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

Winners

Sequential Performance Parallel Performance SAT Performance (parallel) UNSAT Performance (parallel) 24 seconds Performance (parallel)
OpenSMT OpenSMT OpenSMT 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 4579 272280.40 272891.46 4579 2784 1795 246 0 237 0
cvc5 0 4443 311878.34 312467.20 4443 2752 1691 382 0 376 0
Yices2 0 4395 57937.67 58491.75 4395 2653 1742 430 0 417 7
Z3-alpha 0 4204
(base +206) 		149811.20 41325.09 4271 2702 1569 554 0 535 13
SMTInterpol 0 4203 227287.72 173651.57 4207 2491 1716 618 0 527 0
Z3-alpha-base n 0 3998 122151.77 122664.35 3998 2531 1467 827 0 798 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 4579 272280.40 272891.46 4579 2784 1795 246 0 237 0
cvc5 0 4443 311878.34 312467.20 4443 2752 1691 382 0 376 0
Yices2 0 4395 57937.67 58491.75 4395 2653 1742 430 0 417 7
Z3-alpha 0 4271
(base +273) 		306454.92 81046.39 4271 2702 1569 554 0 535 13
SMTInterpol 0 4207 234194.14 177646.97 4207 2491 1716 618 0 527 0
Z3-alpha-base n 0 3998 122151.77 122664.35 3998 2531 1467 827 0 798 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
OpenSMT 0 2784 201903.25 202278.99 2784 2784 0 175 1866 175 0
cvc5 0 2752 149143.95 149501.80 2752 2752 0 207 1866 207 0
Z3-alpha 0 2702
(base +171) 		207881.32 54171.60 2702 2702 0 257 1866 252 5
Yices2 0 2653 51275.14 51611.30 2653 2653 0 306 1866 306 0
SMTInterpol 0 2491 131371.72 108236.85 2491 2491 0 468 1866 461 0
Z3-alpha-base n 0 2531 91157.88 91484.46 2531 2531 0 428 1866 426 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 1795 70377.15 70612.48 1795 0 1795 47 2983 44 0
Yices2 0 1742 6662.53 6880.45 1742 0 1742 100 2983 100 0
SMTInterpol 0 1716 102822.43 69410.12 1716 0 1716 126 2983 55 0
cvc5 0 1691 162734.40 162965.40 1691 0 1691 151 2983 151 0
Z3-alpha 0 1569
(base +102) 		98573.61 26874.79 1569 0 1569 273 2983 272 1
Z3-alpha-base n 0 1467 30993.89 31179.88 1467 0 1467 375 2983 357 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 4216 3518.54 4043.76 4216 2501 1715 6 603 0 0
Z3-alpha 0 3837
(base +356) 		26294.17 9483.85 3837 2402 1435 6 982 0 0
OpenSMT 0 3329 8996.70 9411.05 3329 1980 1349 9 1487 0 0
cvc5 0 3143 5509.61 5895.61 3143 2058 1085 6 1676 0 0
SMTInterpol 0 2955 22204.94 10092.25 2955 1874 1081 44 1826 0 0
Z3-alpha-base n 0 3481 8193.26 8623.78 3481 2224 1257 6 1338 0 0
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver