Use prenex normal form when using cegqi-nested-qe (#4522)

Use prenex normal form when using cegqi-nested-qe (#4522)

Previously, we used a specialized variant of prenex normal form that allowed top level disjunctions. However, the method to put quantifiers into this form led to variable shadowing on some benchmarks in SMT-LIB LRA.

This simplifies the code so that we use standard prenex normal form when cegqi-nested-qe is used and deletes the old variant (DISJ_NORMAL).