An SMT solver for the theories of bit-vectors, floating-points, arrays and uninterpreted functions.
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”.
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} }