bv2epr: a tool for polynomially translating quantifier-free bit-vector formulas into EPR Bit-precise reasoning is essential in many applications of satisfiability modulo theories (SMT). In recent years, efficient approaches for solving fixed-size bit-vector formulas have been developed. Most of these approaches rely on bit-blasting. In [1], we argued that bit-blasting is not polynomial in general, and then showed that solving quantifier-free bit-vector formulas (QF_BV) is NExpTime-complete. In this paper, we present a tool based on a new polynomial translation from QF_BV into effectively propositional logic (EPR). This allows us to solve QF_BV problems using EPR solvers and avoids the exponential growth that comes with bit-blasting. Additionally, our tool allows us to easily generate new challenging benchmarks for EPR solvers.