SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_LinearRealArith (Single Query Track)

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

Results were generated on 2025-08-11

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

Logics:

Winners

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

Sequential Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
Yices2 0 776 29318.57 29417.94 776 426 350 66 0 66 0
OpenSMT 0 775 33493.57 33594.38 775 429 346 67 0 67 0
cvc5 0 758 30920.43 31017.99 758 410 348 84 0 84 0
Z3-alpha 0 717
(base -40) 		74569.31 19122.77 756 411 345 86 0 86 0
SMTInterpol 0 653 60173.16 51180.97 656 394 262 186 0 176 0
Z3-alpha-base n 0 757 38522.79 38622.60 757 417 340 85 0 85 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
Yices2 0 776 29318.57 29417.94 776 426 350 66 0 66 0
OpenSMT 0 775 33493.57 33594.38 775 429 346 67 0 67 0
cvc5 0 758 30920.43 31017.99 758 410 348 84 0 84 0
Z3-alpha 0 756
(base -1) 		180518.24 45665.82 756 411 345 86 0 86 0
SMTInterpol 0 656 64164.41 54376.94 656 394 262 186 0 176 0
Z3-alpha-base n 0 757 38522.79 38622.60 757 417 340 85 0 85 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
OpenSMT 0 429 22536.72 22593.32 429 429 0 12 401 12 0
Yices2 0 426 12397.66 12451.93 426 426 0 15 401 15 0
Z3-alpha 0 411
(base -6) 		92370.66 23468.30 411 411 0 30 401 30 0
cvc5 0 410 15074.71 15127.09 410 410 0 31 401 31 0
SMTInterpol 0 394 35258.50 30823.23 394 394 0 47 401 47 0
Z3-alpha-base n 0 417 18842.20 18896.70 417 417 0 24 401 24 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
Yices2 0 350 16920.90 16966.01 350 0 350 14 478 14 0
cvc5 0 348 15845.73 15890.89 348 0 348 16 478 16 0
OpenSMT 0 346 10956.86 11001.06 346 0 346 18 478 18 0
Z3-alpha 0 345
(base +5) 		88147.59 22197.52 345 0 345 19 478 19 0
SMTInterpol 0 262 28905.91 23553.71 262 0 262 102 478 93 0
Z3-alpha-base n 0 340 19680.59 19725.90 340 0 340 24 478 24 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
Yices2 0 661 1418.20 1499.88 661 376 285 0 181 0 0
OpenSMT 0 638 1918.95 1998.14 638 352 286 0 204 0 0
cvc5 0 585 2198.13 2270.28 585 325 260 0 257 0 0
Z3-alpha 0 532
(base -39) 		5968.15 1706.25 532 294 238 0 310 0 0
SMTInterpol 0 449 4476.13 2063.29 449 272 177 0 393 0 0
Z3-alpha-base n 0 571 1651.30 1722.58 571 323 248 0 271 0 0
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver