Enable new implementation of CEGQI based on nested quantifier elimination (#5477)

Enable new implementation of CEGQI based on nested quantifier elimination (#5477)

This replaces the old implementation of CEGQI based on nested quantifier elimination (--cegqi-nested-qe) with the new implementation.

The previous implementation used some convoluted internal attributes to manage dependencies between quantified formulas, the new implementation is much simpler: it simply eliminates nested quantification eagerly.

Fixes #5365, fixes #5279, fixes #4849, fixes #4433.

This PR also required fixes related to how quantifier elimination is computed.