Applying Light Quantifier Elimination Works Only for 1 Solver Silently

[baierd]

Applying light quantifier elimination applyQELightImpl() is only implemented for Z3. While returning the original formula is valid, we should tell users that this only works for Z3.
Otherwise they expect that a feature works and it does nothing.