Satisfiability Modulo Theories (SMT) solvers rely on extensive theory lemma generation in order to find proofs in quantified theories, like the theory of arrays. This means that the solver instantiates thousands of quantifiers during proof search. In practice, abundant quantifier instantiation can lead to divergence. Counterexample guided abstraction refinement (CEGAR) is a common technique for handling complex theory reasoning in software model checking by removing quantified, theory specific facts and selectively reintroducing them to help guide the SMT solver to a proof. We present Yardbird, a CEGAR framework that uses egg, an off-the-shelf e-graph implementation, to find useful quantifier instantiations for bounded model checking of array programs. Yardbird is an extensible framework where domain-specific instantiation strategies can be implemented as simple cost functions without modifying the underlying solver. We evaluate our technique on 187 SV-COMP array benchmarks and compare against Z3’s built-in array theory solver. We show that Yardbird solves 20 benchmarks that Z3’s array theory solver cannot in the time provided. Additionally, in benchmarks where both Z3 and Yardbird succeed, Yardbird reduces array axiom instantiations in 88% of benchmarks by 95% on average.