Bitwuzla Documentation
======================

**Bitwuzla** is a Satisfiability Modulo Theories (SMT) solver for bit-vectors,
floating-points, arrays, uninterpreted functions and their combinations.

How do I pronounce **Bitwuzla**?
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Bitwuzla's name is derived from an Austrian dialect expression that can be
translated as "someone who tinkers with bits".
It is **pronounced** as "``bitvootslah``".

- **Bit** ...
- **w** as ``v`` in ``vector``
- **u** as ``oo`` in ``good`` (but short)
- **z** as ``ts`` in ``tsunami``
- **l** just an ``l`` as in ``lion``
- **a** as ``u`` in ``cut``

Table of Contents
^^^^^^^^^^^^^^^^^
.. toctree::
  :maxdepth: 2

  install

  binary
  api

.. toctree::
  :maxdepth: 1

  references