SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_UFBV (Single Query Track)

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

Results were generated on 2025-08-11

Benchmarks: 764
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 SMTInterpol SMTInterpol

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 659 16970.39 17055.21 659 200 459 105 0 104 1
Yices2 0 623 55409.17 55494.10 623 200 423 141 0 141 0
SMTInterpol 0 595 21253.20 12627.67 595 84 511 169 0 42 0
cvc5 0 583 195891.80 195998.87 583 165 418 181 0 111 70
Z3-Owl 0 528
(base +140) 		59892.03 59966.62 528 153 375 236 0 192 20
Z3-Owl-base n 0 388 47740.49 47794.89 388 145 243 376 0 376 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
Bitwuzla 0 659 16970.39 17055.21 659 200 459 105 0 104 1
Yices2 0 623 55409.17 55494.10 623 200 423 141 0 141 0
SMTInterpol 0 595 21253.20 12627.67 595 84 511 169 0 42 0
cvc5 0 583 195891.80 195998.87 583 165 418 181 0 111 70
Z3-Owl 0 528
(base +140) 		59892.03 59966.62 528 153 375 236 0 192 20
Z3-Owl-base n 0 388 47740.49 47794.89 388 145 243 376 0 376 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
Bitwuzla 0 200 8407.60 8434.04 200 200 0 2 562 1 1
Yices2 0 200 22621.40 22649.51 200 200 0 2 562 2 0
cvc5 0 165 34710.63 34736.81 165 165 0 37 562 5 32
Z3-Owl 0 153
(base +8) 		7873.82 7894.49 153 153 0 49 562 40 1
SMTInterpol 0 84 5886.75 4637.65 84 84 0 118 562 25 0
Z3-Owl-base n 0 145 21865.19 21885.83 145 145 0 57 562 57 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
SMTInterpol 0 511 15366.45 7990.01 511 0 511 4 249 4 0
Bitwuzla 0 459 8562.80 8621.17 459 0 459 56 249 56 0
Yices2 0 423 32787.77 32844.59 423 0 423 92 249 92 0
cvc5 0 418 161181.17 161262.06 418 0 418 97 249 76 21
Z3-Owl 0 375
(base +132) 		52018.21 52072.13 375 0 375 140 249 111 15
Z3-Owl-base n 0 243 25875.30 25909.07 243 0 243 272 249 272 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
SMTInterpol 0 529 12103.55 5029.45 529 64 465 93 142 0 0
Bitwuzla 0 521 5163.91 5229.33 521 94 427 0 243 0 0
Yices2 0 342 3301.40 3344.29 342 110 232 0 422 0 0
Z3-Owl 0 307
(base +216) 		2552.57 2591.73 307 119 188 0 457 0 0
cvc5 0 29 473.70 477.40 29 25 4 0 735 0 0
Z3-Owl-base n 0 91 881.70 893.02 91 68 23 0 673 0 0
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver