Scalable Bit-Blasting with Abstractions

The dominant state-of-the-art approach for solving bit-vector formulas in Satisfiability Modulo Theories (SMT) is bit-blasting, an eager reduction to propositional logic. Bit-blasting is surprisingly efficient in practice but does not generally scale well with increasing bit-widths, especially when bit-vector arithmetic is present. In this paper, we present a novel CEGAR-style abstraction-refinement procedure for the theory of fixed-size bit-vectors that significantly improves the scalability of bitblasting. We provide lemma schemes for various arithmetic bit-vector operators and an abduction-based framework for synthesizing refinement lemmas. We extended the state-of-the-art SMT solver Bitwuzla with our abstraction-refinement approach and show that it significantly improves solver performance on a variety of benchmark sets, including industrial benchmarks that arise from smart contract verification.

-We present a modular and configurable CEGAR-style abstraction-refinement framework for the theory of fixed-size bit-vectors, based on bit-blasting. -We provide a set of refinement lemmas for a restricted but sufficient set of arithmetic bit-vector operators (bvmul, bvudiv, bvurem). This set of lemmas consists of a set of basic, hand-crafted lemmas (encoding core properties of abstracted operators) and a set of lemmas synthesized via abduction. -We provide a lemma scoring scheme and an abduction-based framework for synthesizing lemmas, utilizing the syntax-restricted abduction reasoning capabilities of the SMT solver cvc5 [7]. -We extend the open-source SMT solver Bitwuzla [29] with our approach and show that it significantly improves performance on a wide range of benchmarks, including industrial benchmarks from smart contract verification.

Developing scalable approaches for solving bit-vector formulas with large bit-widths is a long-standing challenge. Previous efforts to tackle this challenge can be mainly divided into two categories: alternative approaches to bit-blasting that primarily rely on word-level reasoning, and techniques based on bit-blasting that try to reduce the size of the original problem on the bit-level.

Alternative approaches to bit-blasting include: translations to linear integer arithmetic [11] and non-linear integer arithmetic (in combination with CEGARstyle handling of bit-wise operators) [36]; layered CDCL(T )-style approaches that rely on encoding fragments of the input problem into other theories before resorting to bit-blasting [13,21]; instances of the model-constructing satisfiability (mcSAT) calculus [20,35], a generalization of propositional conflict-driven clause learning (CDCL) to SMT; and incomplete techniques such as local search [19,28,30], which are only able to determine satisfiability. All of these approaches are generally not competitive with bit-blasting.