Bit-Precise Interpolation in Bitwuzla

Bitwuzla is a state-of-the-art SMT solver specialized in theories relevant to bit-precise reasoning. The main bit-vector solving procedure of Bitwuzla is based on bit-blasting, a reduction of bit-vector constraints to propositional logic (SAT). Until now, Bitwuzla did not support interpolant generation, which is a key requirement for many verification applications that rely on bit-precise reasoning. We present an extension of Bitwuzla with the capability to produce interpolants and interpolation sequences for quantifier-free bit-vector formulas. Our interpolation workflow extracts bit-level interpolants from proofs produced by the back-end SAT solver, which are lifted to the word-level and post-processed to recover and simplify word-level structure. We evaluate our new bit-vector interpolation engine in the context of various interpolation-based algorithms for symbolic model checking.