SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_Equality_Bitvec (Single Query Track)

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

Results were generated on 2025-08-11

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

Logics:

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 8279 27920.69 28953.07 8279 5416 2863 134 76 132 2
Yices2 0 8230 71312.92 72346.37 8230 5411 2819 183 76 182 1
Z3-Owl 0 8056
(base +182) 		99548.31 100577.24 8056 5312 2744 357 76 301 28
cvc5 0 8009 293515.59 294553.59 8009 5260 2749 480 0 395 83
SMTInterpol 0 6442 399199.02 347593.54 6453 3976 2477 2036 0 1797 0
Z3-Owl-base n 0 7874 90158.59 91142.29 7874 5277 2597 539 76 535 4
(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 8279 27920.69 28953.07 8279 5416 2863 134 76 132 2
Yices2 0 8230 71312.92 72346.37 8230 5411 2819 183 76 182 1
Z3-Owl 0 8056
(base +182) 		99548.31 100577.24 8056 5312 2744 357 76 301 28
cvc5 0 8009 293515.59 294553.59 8009 5260 2749 480 0 395 83
SMTInterpol 0 6453 413241.74 360487.89 6453 3976 2477 2036 0 1797 0
Z3-Owl-base n 0 7874 90158.59 91142.29 7874 5277 2597 539 76 535 4
(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 5416 12534.36 13208.61 5416 5416 0 6 3067 4 2
Yices2 0 5411 31070.94 31748.18 5411 5411 0 11 3067 10 1
Z3-Owl 0 5312
(base +35) 		34911.75 35586.70 5312 5312 0 110 3067 97 4
cvc5 0 5260 118715.24 119381.79 5260 5260 0 202 3027 165 36
SMTInterpol 0 3976 323230.20 285768.88 3976 3976 0 1486 3027 1304 0
Z3-Owl-base n 0 5277 50083.74 50741.20 5277 5277 0 145 3067 144 1
(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 2863 15386.34 15744.46 2863 0 2863 77 5549 77 0
Yices2 0 2819 40241.98 40598.18 2819 0 2819 121 5549 121 0
cvc5 0 2749 174800.35 175171.80 2749 0 2749 197 5543 173 23
Z3-Owl 0 2744
(base +147) 		64636.56 64990.54 2744 0 2744 196 5549 163 19
SMTInterpol 0 2477 90011.54 74719.01 2477 0 2477 469 5543 457 0
Z3-Owl-base n 0 2597 40074.85 40401.09 2597 0 2597 343 5549 343 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 8090 9829.84 10835.10 8090 5285 2805 0 399 0 0
Yices2 0 7879 5536.43 6517.07 7879 5287 2592 0 610 0 0
Z3-Owl 0 7706
(base +282) 		12036.32 13009.40 7706 5197 2509 0 783 0 0
cvc5 0 6978 8937.21 9799.98 6978 4705 2273 2 1509 0 0
SMTInterpol 0 5112 28233.85 12419.02 5112 2904 2208 137 3240 0 0
Z3-Owl-base n 0 7424 4630.43 5546.58 7424 5096 2328 0 1065 0 0
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver