The quantifier-free extensional theory of arrays 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 is combined with a decidable quantifier-free first-order theory . Unlike traditional lazy SMT approaches, where lemmas are added on the boolean abstraction layer, our decision procedure adds lemmas in . 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.