zapato: Automatic theorem proving for predicate abstraction refinement. Counterexample-driven abstraction refinement is an automatic process that produces abstract models of finite and infinite-state systems. When this process is applied to software, an automatic theorem prover for quantifier-free first-order logic helps to determine the feasibility of program paths and to refine the abstraction. In this paper we report on a fast, lightweight, and automatic theorem prover called Zapato which we have built specifically to solve the queries produced during the abstraction refinement process.