Lemmas on Demand for the Extensional Theory of Arrays
Robert Brummayer, Armin Biere · Journal on Satisfiability Boolean Modeling and Computation · 2009
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 wh