[quantifiers] Fix prenex computation (#5879)

[quantifiers] Fix prenex computation (#5879)

Previously our prenex computation could generate quantifiers of the form forall x y y. F, which would lead to an assertion failure in getFreeVariablesScope, as it assumes that no shadowing occurs. This commit makes the prenex computation take a set rather than a vector, thus avoiding duplications of prenexed variables. It also changes mkForall to take a constant vector, since it does not modify the given vector.

Fixes #5693