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