A scalable decision procedure for fixed-width bit-vectors

Efficient decision procedures for bit-vectors are essential for modern verification frameworks. This paper describes a new decision procedure for the core theory of bit-vectors that exploits a reduction to equality reasoning. The procedure is embedded in a congruence closure algorithm, whose data structures are extended in order to efficiently manage the relations between bit-vector slicings, modulo equivalence classes. The resulting procedure is incremental, backtrack-able, and proof producing: it can be used as a theory-solver for a lazy SMT schema. Experiments show that our approach is comparable and often superior to bit-blasting on the core fragment, and that it also helps as a theory layer when applied over the full bit-vector theory.