Abstract Bit-vector operations are ubiquitous in programming languages and formal verification, but their complex semantics pose challenges for SMT solvers. Although bit-blasting—translating bit-vectors to Boolean variables—is widely used, it struggles with arithmetic bit-vector operations on large bit-widths (e. g. , 64-bit or 256-bit variables) due to exponential blowup. Int-blasting, which maps bit-vectors to integer arithmetic, offers a scalable alternative for arithmetic bit-vector operations, but introduces many modulo operations of which some are redundant. This article presents a modular three-step translation from bit-vector formulas to integer formulas, designed to keep the amount of modulo operations low, while preserving correctness. In the first step, we translate bit-vector operations to integer operations. Thereby, we introduce the two functions bv2nat and nat2bvₖ as explicit operators in the SMT-LIB theory of bit-vectors. Each integer operation is wrapped by bv2nat and nat2bvₖ. Hence, the sort of all bit-vector terms is preserved. Therefore, the first translation step is an equivalence transformation. In the second step, we simplify the formula by replacing the composition bv2nat nat2bvₖ with a modulo operation. These modulo operations are added lazily, i. e. , if the modulo does not change the result of the operation, it is omitted. In our experiments this reduced the average amount of modulo operations by 51%. In the third step, we introduce lemmas to precisely capture the meaning of bv2nat and nat2bvₖ. We prove that these lemmas suffice to solve bit-vector formulas. Furthermore, we illustrate that these lemmas are also sufficient for bit-vector formulas with quantifiers, arrays and uninterpreted functions. We implement our translation in SMTInterpol and evaluate it on 19570 SMT-LIB benchmarks. Results show that our lazy int-blasting solves 15% more tasks than an eager int-blasting, with 35% faster average runtime and 12% lower memory usage.
Barth et al. (Fri,) studied this question.