SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

QF_Bitvec (Single Query Track)

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

Results were generated on 2025-08-11

Benchmarks: 10703
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-MachBV Bitwuzla-MachBV Bitwuzla Bitwuzla-MachBV Bitwuzla-MachBV

Sequential Performance Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Abstained Timeout Memout
Bitwuzla-MachBV 0 10523
(base +38) 		97390.14 98711.15 10523 4929 5594 180 0 179 1
Bitwuzla 0 10498 100202.01 101517.47 10498 4931 5567 205 0 203 2
Yices2 0 10491 120555.40 121864.36 10491 4924 5567 212 0 211 1
cvc5 0 9938 302092.27 303362.99 9938 4790 5148 765 0 727 32
z3siri 0 9308
(base +364) 		429081.45 430296.03 9308 4435 4873 1395 0 1204 11
Z3-alpha 0 8970
(base +25) 		544609.75 144055.13 9370 4592 4778 1333 0 1254 76
bv_decide-nokernel 0 8862 426162.80 427483.91 8862 4713 4149 1841 0 1802 37
Z3-Owl 0 8656
(base +115) 		345612.16 346754.50 8656 4501 4155 2047 0 2031 9
bv_decide 0 8638 638058.46 639387.52 8638 4627 4011 2065 0 2025 37
SMTInterpol 0 2917 337337.08 303061.00 2925 596 2329 7778 0 6807 0
Bitwuzla-MachBV-base n 0 10485 113665.37 114969.55 10485 4928 5557 218 0 213 5
Z3-alpha-base n 0 8945 389801.87 390962.90 8945 4467 4478 1758 0 1746 10
z3siri-base n 0 8944 391867.14 393027.61 8944 4467 4477 1759 0 1747 10
Z3-Owl-base n 0 8541 587768.50 588896.66 8541 4281 4260 2162 0 2152 8
(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-MachBV 0 10523
(base +38) 		97390.14 98711.15 10523 4929 5594 180 0 179 1
Bitwuzla 0 10498 100202.01 101517.47 10498 4931 5567 205 0 203 2
Yices2 0 10491 120555.40 121864.36 10491 4924 5567 212 0 211 1
cvc5 0 9938 302092.27 303362.99 9938 4790 5148 765 0 727 32
Z3-alpha 0 9370
(base +425) 		1532034.50 393050.52 9370 4592 4778 1333 0 1254 76
z3siri 0 9308
(base +364) 		429081.45 430296.03 9308 4435 4873 1395 0 1204 11
bv_decide-nokernel 0 8862 426162.80 427483.91 8862 4713 4149 1841 0 1802 37
Z3-Owl 0 8656
(base +115) 		345612.16 346754.50 8656 4501 4155 2047 0 2031 9
bv_decide 0 8638 638058.46 639387.52 8638 4627 4011 2065 0 2025 37
SMTInterpol 0 2925 347054.64 312426.58 2925 596 2329 7778 0 6807 0
Bitwuzla-MachBV-base n 0 10485 113665.37 114969.55 10485 4928 5557 218 0 213 5
Z3-alpha-base n 0 8945 389801.87 390962.90 8945 4467 4478 1758 0 1746 10
z3siri-base n 0 8944 391867.14 393027.61 8944 4467 4477 1759 0 1747 10
Z3-Owl-base n 0 8541 587768.50 588896.66 8541 4281 4260 2162 0 2152 8
(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 4931 44557.48 45173.98 4931 4931 0 31 5741 29 2
Bitwuzla-MachBV 0 4929
(base +1) 		50034.86 50653.33 4929 4929 0 33 5741 32 1
Yices2 0 4924 50873.51 51487.19 4924 4924 0 38 5741 37 1
cvc5 0 4790 109431.02 110037.61 4790 4790 0 172 5741 157 11
bv_decide-nokernel 0 4713 210107.19 210776.11 4713 4713 0 249 5741 244 4
bv_decide 0 4627 290823.50 291487.41 4627 4627 0 335 5741 331 3
Z3-alpha 0 4592
(base +125) 		681224.03 176140.63 4592 4592 0 370 5741 361 9
Z3-Owl 0 4501
(base +220) 		161409.09 162001.11 4501 4501 0 461 5741 454 4
z3siri 0 4435
(base -32) 		209098.46 209677.25 4435 4435 0 527 5741 425 9
SMTInterpol 0 596 127475.21 116503.29 596 596 0 4366 5741 3684 0
Bitwuzla-MachBV-base n 0 4928 53134.81 53747.05 4928 4928 0 34 5741 29 5
Z3-alpha-base n 0 4467 199624.27 200203.84 4467 4467 0 495 5741 489 6
z3siri-base n 0 4467 201216.42 201797.38 4467 4467 0 495 5741 489 6
Z3-Owl-base n 0 4281 326455.94 327025.02 4281 4281 0 681 5741 675 6
(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-MachBV 0 5594
(base +37) 		47355.28 48057.82 5594 0 5594 52 5057 52 0
Bitwuzla 0 5567 55644.53 56343.49 5567 0 5567 79 5057 79 0
Yices2 0 5567 69681.89 70377.17 5567 0 5567 79 5057 79 0
cvc5 0 5148 192661.24 193325.38 5148 0 5148 498 5057 481 15
z3siri 0 4873
(base +396) 		219982.99 220618.78 4873 0 4873 773 5057 686 2
Z3-alpha 0 4778
(base +300) 		850810.48 216909.89 4778 0 4778 868 5057 829 36
Z3-Owl 0 4155
(base -105) 		184203.06 184753.39 4155 0 4155 1491 5057 1488 0
bv_decide-nokernel 0 4149 216055.61 216707.80 4149 0 4149 1497 5057 1464 32
bv_decide 0 4011 347234.96 347900.11 4011 0 4011 1635 5057 1599 34
SMTInterpol 0 2329 219579.43 195923.30 2329 0 2329 3317 5057 3051 0
Bitwuzla-MachBV-base n 0 5557 60530.55 61222.50 5557 0 5557 89 5057 89 0
Z3-alpha-base n 0 4478 190177.61 190759.06 4478 0 4478 1168 5057 1164 2
z3siri-base n 0 4477 190650.72 191230.23 4477 0 4477 1169 5057 1165 2
Z3-Owl-base n 0 4260 261312.56 261871.64 4260 0 4260 1386 5057 1383 1
(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-MachBV 0 10101
(base +118) 		17784.17 19040.53 10101 4743 5358 0 602 0 0
Bitwuzla 0 10019 14109.70 15349.90 10019 4728 5291 0 684 0 0
Yices2 0 9909 11127.29 12349.05 9909 4589 5320 0 794 0 0
cvc5 0 8498 24252.34 25300.07 8498 4005 4493 1 2204 0 0
Z3-alpha 0 7734
(base +383) 		70113.72 21374.05 7734 3795 3939 0 2969 0 0
z3siri 0 7387
(base +43) 		19789.88 20708.35 7387 3487 3900 8 3308 0 0
Z3-Owl 0 6983
(base +512) 		33022.68 33910.41 6983 3519 3464 0 3720 0 0
bv_decide-nokernel 0 6049 34413.15 35348.33 6049 3181 2868 1 4653 0 0
bv_decide 0 5694 37930.67 38815.86 5694 3010 2684 1 5008 0 0
SMTInterpol 0 1965 21583.01 9183.17 1965 287 1678 423 8315 0 0
Bitwuzla-MachBV-base n 0 9983 16027.77 17255.32 9983 4716 5267 0 720 0 0
Z3-alpha-base n 0 7351 17648.29 18560.45 7351 3615 3736 0 3352 0 0
z3siri-base n 0 7344 17741.41 18651.46 7344 3612 3732 0 3359 0 0
Z3-Owl-base n 0 6471 22159.50 22960.32 6471 3169 3302 0 4232 0 0
(base +/- n): for derived solvers: increment over base solver
n: non-competing solver