This module implements an encoder for bitvector formulae to propositional logic. It is described in more detail in [20].