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