Satisfiability Modulo Theories (SMT) solvers struggle with quantifier reasoning over common data types such as arrays. Counterexample guided abstraction refinement (CEGAR) is a common technique for dealing with complex theory reasoning in software model checking by abstracting away quantified, theory specific facts and selectively reintroducing them to help guide SMT solvers to a proof. We present our work-in-progress, Yardbird, a CEGAR framework that uses egg, an off-the-shelf e-graph implementation, to find useful theory refinements for bounded model checking of array programs. We generate refinements by using theory axioms as rewrite rules in the equality saturation engine. We find theory conflicts by detecting when two e-classes should be merged, and then selecting refinement terms using a custom property-directed cost function. We evaluate our technique on 193 SV-COMP array benchmarks and compare against Z3. We show that Yardbird outperforms Z3 for 26% of benchmarks on verification time and reduces quantifier instantiations in 49% of benchmarks.