Fix remove term formula policy for terms beneath quantifiers (#5497)

Fix remove term formula policy for terms beneath quantifiers (#5497)

Now that extended arithmetic symbols are not eliminated during expandDefinitions, this allowed for a chain of events that would not apply theory preprocessing on certain terms.

In particular, a term t would not have theory preprocessing applied to it if it was a strict subterm of ITE-term s that occurred in a term position in a quantified formula body, and s did not have free variables. In this case, term formula removal would add a lemma corresponding to the ITE skolem definition, whose subterms did not have theory preprocessing applied. This meant that a (div a d) term was not being preprocessed in #5482, leading to solution unsoundness.

This changes the policy in term formula removal to be in sync with theory preprocessing: term formula removal and theory preprocessing only apply to terms that are not beneath quantifiers. In particular, this means that ground terms in quantifier bodies are left untouched until they are introduced e.g. by instantiation.

This fixes the solution soundness issue (fixes #5482).