Counterexample Guided Abstraction Refinement (CEGAR) has been a powerful paradigm in formal verification. The basic step in CEGAR is to refine the abstraction used in formal verification based on spurious counterexamples–counterexamples that are an artifact of the coarseness of the abstraction and do not correspond to “real” counterexamples. The initial paper on CEGAR was published in CAV 2000, and thus…