Deciding Bit-Vector Formulas with mcSAT

The Model-Constructing Satisfiability Calculus (mcSAT) is a recently proposed generalisation of propositional DPLL/CDCL for reasoning modulo theories. In contrast to most DPLL(T)-based SMT solvers, which carry out con ict-driven learning only on the propositional level, mcSAT calculi can also synthesise new theory literals during learning, resulting in a simple yet very exible framework for designing efficient decision procedures. We present an mcSAT calculus for the theory of bounded-length bit-vectors, based on tailor-made con ict-driven learning that can exploit both propositional and arithmetic properties of bit-vector operations. Our procedure can in particular avoid full bitblasting for constraints that are mainly arithmetic in nature, and therefore performs well on problems from domains like software verification.