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’

News

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