SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_LRA (Single Query Track)

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

Results were generated on 2025-08-11

Benchmarks: 595
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 OpenSMT

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 578 19618.61 19693.28 578 326 252 17 0 17 0
Yices2 0 561 25527.85 25600.28 561 320 241 34 0 34 0
cvc5 0 549 26942.01 27013.30 549 309 240 46 0 46 0
Z3-alpha 0 514
(base -33) 		64169.74 16445.90 549 312 237 46 0 46 0
SMTInterpol 0 476 51585.82 44844.68 479 295 184 116 0 111 0
Z3-alpha-base n 0 547 31112.89 31185.34 547 315 232 48 0 48 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
OpenSMT 0 578 19618.61 19693.28 578 326 252 17 0 17 0
Yices2 0 561 25527.85 25600.28 561 320 241 34 0 34 0
cvc5 0 549 26942.01 27013.30 549 309 240 46 0 46 0
Z3-alpha 0 549
(base +2) 		157972.00 39949.93 549 312 237 46 0 46 0
SMTInterpol 0 479 55577.07 48040.64 479 295 184 116 0 111 0
Z3-alpha-base n 0 547 31112.89 31185.34 547 315 232 48 0 48 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 326 14009.48 14052.30 326 326 0 9 260 9 0
Yices2 0 320 11051.56 11092.59 320 320 0 15 260 15 0
Z3-alpha 0 312
(base -3) 		80314.24 20415.71 312 312 0 23 260 23 0
cvc5 0 309 13979.69 14019.58 309 309 0 26 260 26 0
SMTInterpol 0 295 30818.38 27232.72 295 295 0 40 260 40 0
Z3-alpha-base n 0 315 12960.71 13001.68 315 315 0 20 260 20 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
OpenSMT 0 252 5609.12 5640.98 252 0 252 3 340 3 0
Yices2 0 241 14476.28 14507.69 241 0 241 14 340 14 0
cvc5 0 240 12962.32 12993.72 240 0 240 15 340 15 0
Z3-alpha 0 237
(base +5) 		77657.77 19534.22 237 0 237 18 340 18 0
SMTInterpol 0 184 24758.69 20807.92 184 0 184 71 340 66 0
Z3-alpha-base n 0 232 18152.18 18183.67 232 0 232 23 340 23 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
OpenSMT 0 488 1533.60 1594.23 488 271 217 0 107 0 0
Yices2 0 464 1086.75 1144.13 464 277 187 0 131 0 0
cvc5 0 407 1596.52 1646.72 407 232 175 0 188 0 0
Z3-alpha 0 353
(base -33) 		4148.52 1186.60 353 205 148 0 242 0 0
SMTInterpol 0 313 2924.42 1333.15 313 196 117 0 282 0 0
Z3-alpha-base n 0 386 1227.25 1275.30 386 233 153 0 209 0 0
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver