Lemmas on Demand for the Extensional Theory of Arrays

The quantifier-free extensional theory of arrays T A plays an important role in hardware and software verification. In this article we present a novel decision procedure that refines formula abstractions with lemmas on demand. We consider the case where T A is combined with a decidable quantifier-free first-order theory T B . Unlike traditional lazy SMT approaches, where lemmas are added on the boolean abstraction layer, our decision procedure adds lemmas in T B . We discuss our decision procedure in detail. In particular, we prove soundness and completeness, and discuss complexity. We present our decision procedure in a generic context and provide implementation details and optimizations, in particular for bit-vectors. Finally, we report on experiments and discuss related work.