SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_BVFP (Single Query Track)

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

Results were generated on 2025-08-11

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

Winners

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

Sequential Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
Bitwuzla 0 527 558.10 622.80 527 238 289 0 0 0 0
cvc5 0 527 3213.56 3278.46 527 238 289 0 0 0 0
Z3-Owl 0 510
(base +9) 		10278.54 10344.55 510 230 280 17 0 10 5
COLIBRI 0 462 385.91 442.71 462 228 234 65 0 21 0
colibri2 0 382 1915.19 1962.08 382 167 215 145 0 19 0
Z3-Owl-base n 0 501 18398.34 18462.61 501 228 273 26 0 21 3
(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
Bitwuzla 0 527 558.10 622.80 527 238 289 0 0 0 0
cvc5 0 527 3213.56 3278.46 527 238 289 0 0 0 0
Z3-Owl 0 510
(base +9) 		10278.54 10344.55 510 230 280 17 0 10 5
COLIBRI 0 462 385.91 442.71 462 228 234 65 0 21 0
colibri2 0 382 1915.19 1962.08 382 167 215 145 0 19 0
Z3-Owl-base n 0 501 18398.34 18462.61 501 228 273 26 0 21 3
(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
Bitwuzla 0 238 97.52 126.70 238 238 0 0 289 0 0
cvc5 0 238 1105.79 1135.03 238 238 0 0 289 0 0
Z3-Owl 0 230
(base +2) 		2718.39 2747.89 230 230 0 8 289 3 5
COLIBRI 0 228 179.20 207.25 228 228 0 10 289 2 0
colibri2 0 167 657.86 678.33 167 167 0 71 289 7 0
Z3-Owl-base n 0 228 4606.74 4635.42 228 228 0 10 289 7 3
(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
Bitwuzla 0 289 460.58 496.11 289 0 289 0 238 0 0
cvc5 0 289 2107.77 2143.43 289 0 289 0 238 0 0
Z3-Owl 0 280
(base +7) 		7560.15 7596.66 280 0 280 9 238 7 0
COLIBRI 0 234 206.71 235.47 234 0 234 55 238 19 0
colibri2 0 215 1257.33 1283.75 215 0 215 74 238 12 0
Z3-Owl-base n 0 273 13791.60 13827.19 273 0 273 16 238 14 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
Bitwuzla 0 523 374.50 438.69 523 238 285 0 4 0 0
cvc5 0 500 998.99 1060.27 500 226 274 0 27 0 0
COLIBRI 0 461 339.99 396.66 461 228 233 44 22 0 0
Z3-Owl 0 416
(base +12) 		1988.93 2041.99 416 208 208 0 111 0 0
colibri2 0 375 182.81 228.64 375 165 210 82 70 0 0
Z3-Owl-base n 0 404 1392.52 1442.36 404 205 199 0 123 0 0
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver