SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
BVModule

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