Efficient SMT Solving for Bit-Vectors and the Extensional Theory of Arrays

The Satisfiability Modulo Theories (SMT) problem is to decide the satisfiability of a formula expressed in a (decidable) first-order background theory. In this thesis we address the problem of designing, implementing, testing, and debugging an efficient SMT solver for the quantifier-free extensional theory of arrays, combined with bit-vectors. This thesis consists of three main parts. After an introduction into the problem and its domain, the first part considers the design of an efficient decision procedure for the quantifier-free extensional theory of arrays. We discuss the decision procedure in detail. In particular, we prove correctness, provide a complexity analysis, and discuss implementation and optimization details. The second part focuses on the design and implementation details of our SMT solver, called Boolector. In the SMT competitions 2008 and 2009, Boolector clearly won the division of the quantifier-free theory of bit-vectors, arrays and uninterpreted functions QF AUFBV. Moreover, it won the division of the quantifier-free theory of bit-vectors QF BV in 2008 and achieved the second place in 2009. We discuss selected optimization techniques and features such as symbolic overflow detection, propagating unconstrained variables, and under-approximation techniques for bit-vectors. In the last part, this thesis addresses engineering aspects such as testing and debugging techniques optimized for SMT solver development. We show that fuzzing and debugging techniques can be successfully applied to SMT solvers. We report on critical defects, such as segmentation faults and incorrect results, which we have found for state-of-the-art SMT solvers. Finally, we demonstrate the effectiveness of delta-debugging techniques in minimizing failure-inducing SMT formulas.