Mathias Preiner

Bit-Precise Interpolation in Bitwuzla

2026 · Lecture notes in computer science

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, …