The Model-Constructing Satisfiability Calculus (mcSAT) is a recently
proposed generalization of propositional DPLL/CDCL for reasoning
modulo theories. In contrast to most DPLL(T)-based SMT solvers, which
carry out conflict-driven learning only on the propositional level,
mcSAT calculi can also synthesise new theory literals during
learning, resulting in a simple yet very flexible framework for
designing efficient decision procedures. We present an mcSAT calculus
for the theory of fixed-size bit-vectors, based on tailor-made
conflict-driven learning that exploits both propositional and
arithmetic properties of bit-vector operations. Our procedure avoids
unnecessary bit-blasting and performs well on problems from domains
like software verification, and on constraints over large bit-vectors.