Efficiently Solving Bit-Vector Problems Using Model Checkers

Bit-precise reasoning is essential in many applications of Satisfiability Modulo Theories (SMT). Most approaches for solving quantifier-free fixed-size bit-vector logics (QF BV) rely on bit-blasting. In previous work, we have shown that bit-blasting is not polynomial in general [19], and later proposed QF BV<<1 , a class of bit-vector problems that is PSpace-complete [15]. In this paper, we give examples of how to create (polynomial) SMV specifications out of QF BV<<1 formulas. We then use various model checkers to solve those problems and give detailed experimental results. Our results show that BDD-based model checkers outperform current SMT solvers by several orders of magnitude on our benchmarks. Unrolling and using SAT-based model checking turns out to be the same as bit-blasting and gives worse results. In addition to this, our approach allows us to easily generate new challenging benchmarks for SMT solvers as well as for model checkers.