Bitwuzla

An SMT solver for bit-vectors, floating-points, arrays and uninterpreted functions.

Awards

Mathias Preiner, Aina Niemetz, Clark Barrett. Satisfiability Modulo Extensional Constant Arrays. CAV: 27-49. (2026)
CAV Distinguished Paper Award

Dominik Schreiber, Aina Niemetz, Mathias Preiner. Massively Parallel Bit-Precise Verification with Bitwuzla and Mallob. TACAS: 170-191. (2026)
TACAS Distinguished Paper Award
TACAS Distinguished Artifact Award
ETAPS Best Tool Paper Award

Aina Niemetz, Mathias Preiner. Bitwuzla. CAV: 3-17. (2023)
CAV Distinguished Paper Award

SMT-COMP 2024 (details)

entered: 22 divisions
overall: 43 gold medals , 3 silver medals , 15 bronze medals
division awards: 42 gold medals (out of 82)
competition-wide awards:
- 1 gold medal (out of 30)
- 3 silver medals (out of 30)
- 15 bronze medals (out of 30)

SMT-COMP 2023 (details)

entered: 21 divisions
overall: 27 gold medals , 7 silver medals , 4 bronze medals
division awards: 26 gold medals (out of 54)
competition-wide awards:
- 1 gold medal (out of 20)
- 7 silver medals (out of 20)
- 4 bronze medals (out of 20)

SMT-COMP 2022 (details)

entered: 18 divisions
overall: 32 gold medals , 8 silver medals , 4 bronze medals
division awards: 32 gold medals (out of 48)
competition-wide awards:
- 7 silver medals (out of 20)
- 4 bronze medals (out of 20)
FLOC Olympic Games: 1 silver medal

SMT-COMP 2021 (details)

entered: 11 divisions
overall: 17 gold medals , 2 silver medals , 5 bronze medals
division awards: 17 gold medals (out of 28)
competition-wide awards:
- 2 silver medals (out of 20)
- 5 bronze medals (out of 20)

SMT-COMP 2020 (details)

entered: 26 divisions
overall: 45 gold medals , 6 bronze medals
division awards: 43 gold medals (out of 71)
competition-wide awards:
- 2 gold medals (out of 20)
- 6 bronze medals (out of 20)