SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

LRA (Single Query Track)

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

Results were generated on 2025-08-11

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

Winners

Sequential Performance Parallel Performance SAT Performance (parallel) UNSAT Performance (parallel) 24 seconds Performance (parallel)
YicesQS YicesQS YicesQS YicesQS YicesQS

Sequential Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
YicesQS 0 1002 295.71 418.07 1002 408 594 11 0 11 0
Z3-alpha 0 909
(base -40) 		27366.04 7144.37 948 395 553 65 0 59 6
UltimateEliminator+MathSAT 0 864 12006.23 8235.00 864 345 519 149 0 149 0
cvc5 0 847 23380.45 23488.45 847 346 501 166 0 166 0
SMTInterpol 0 159 2506.71 1834.22 159 2 157 854 0 37 0
iProver v3.9.3 0 157 24515.90 6428.01 217 0 217 796 0 796 0
Z3-alpha-base n 0 949 40598.12 40719.62 949 397 552 64 0 64 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
YicesQS 0 1002 295.71 418.07 1002 408 594 11 0 11 0
Z3-alpha 0 948
(base -1) 		136229.10 34387.24 948 395 553 65 0 59 6
UltimateEliminator+MathSAT 0 864 12006.23 8235.00 864 345 519 149 0 149 0
cvc5 0 847 23380.45 23488.45 847 346 501 166 0 166 0
iProver v3.9.3 0 217 199987.31 50738.47 217 0 217 796 0 796 0
SMTInterpol 0 159 2506.71 1834.22 159 2 157 854 0 37 0
Z3-alpha-base n 0 949 40598.12 40719.62 949 397 552 64 0 64 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
YicesQS 0 408 123.38 173.23 408 408 0 4 601 4 0
Z3-alpha 0 395
(base -2) 		19463.43 4997.79 395 395 0 17 601 15 2
cvc5 0 346 6051.92 6095.53 346 346 0 66 601 66 0
UltimateEliminator+MathSAT 0 345 4650.25 3082.08 345 345 0 67 601 67 0
SMTInterpol 0 2 0.86 0.90 2 2 0 410 601 23 0
iProver v3.9.3 0 0 0.00 0.00 0 0 0 412 601 412 0
Z3-alpha-base n 0 397 5946.24 5995.70 397 397 0 15 601 15 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
YicesQS 0 594 172.34 244.84 594 0 594 7 412 7 0
Z3-alpha 0 553
(base +1) 		116765.67 29389.45 553 0 553 48 412 44 4
UltimateEliminator+MathSAT 0 519 7355.97 5152.92 519 0 519 82 412 82 0
cvc5 0 501 17328.53 17392.92 501 0 501 100 412 100 0
iProver v3.9.3 0 217 199987.31 50738.47 217 0 217 384 412 384 0
SMTInterpol 0 157 2505.85 1833.33 157 0 157 444 412 14 0
Z3-alpha-base n 0 552 34651.88 34723.93 552 0 552 49 412 49 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
YicesQS 0 1002 295.71 418.07 1002 408 594 0 11 0 0
Z3-alpha 0 855
(base +12) 		4613.57 1434.84 855 380 475 0 158 0 0
UltimateEliminator+MathSAT 0 822 5721.96 2469.27 822 332 490 0 191 0 0
cvc5 0 718 301.65 390.64 718 291 427 0 295 0 0
SMTInterpol 0 156 1005.85 413.47 156 2 154 793 64 0 0
iProver v3.9.3 0 97 1997.31 599.82 97 0 97 0 916 0 0
Z3-alpha-base n 0 843 1504.32 1608.47 843 376 467 0 170 0 0
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver