We have been working on using equalities and uninterpreted functions as an abstract layer inside Spacer. A bi-product of this research was a version of model based projection centered around the theory of EUF that layers the different theory reasoning on top of an an e-graph. We wrote a paper solely on quantifier elimination and model based projection using e-graphs. It received a distinguished paper award at CAV 2023. You can read the full paper here. The code has been merged with Z3.