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.