Bitwuzla

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

About Bitwuzla

Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, floating-point arithmetic, 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 is now available on GitHub
Bitwuzla won 17 out of 26 (participated) divisions at SMT-COMP 2020
Bitwuzla participating at SMT-COMP 2020 (submitted binary)