About Bitwuzla

Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the theories of bit-vectors, floating-points, arrays and uninterpreted functions and their combinations. Its name is derived from an Austrian dialect expression that can be translated as “someone who tinkers with bits”.

Pronunciation of Bitwuzla

• Bit…
• ‘w’ as ‘v’ in ‘vector’,
• ‘u’ as ‘oo’ in ‘good’ (but short),
• ‘z’ as ‘ts’ in ‘tsunami’,
• ‘l’ just an ‘l’,
• ‘a’ as ‘u’ in ‘cut’

Citing Bitwuzla

If you are citing Bitwuzla, please use the following BibTex entry:

@article{DBLP:journals/corr/abs-2006-01621,
  author    = {Aina Niemetz and
               Mathias Preiner},
  title     = {Bitwuzla at the {SMT-COMP} 2020},
  journal   = {CoRR},
  volume    = {abs/2006.01621},
  year      = {2020},
  url       = {https://arxiv.org/abs/2006.01621},
  archivePrefix = {arXiv},
  eprint    = {2006.01621},
  biburl    = {https://dblp.org/rec/journals/corr/abs-2006-01621.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

News

• Bitwuzla won 17 out of 26 (participated) divisions at SMT-COMP 2020
• Bitwuzla participating at SMT-COMP 2020 (submitted binary)