Do not eliminate variables that are equal to unevaluatable terms (#4267)

Do not eliminate variables that are equal to unevaluatable terms (#4267)

When we eliminate a variable x -> v during simplification, it may be the case that v contains "unevaluated" operators like forall, choice, etc. Thus, we do not produce correct models for such inputs unless simplification is disabled.

This PR ensures we only eliminate variables when v contains only evaluated operators.

Additionally, the kinds registered as unevaluated were slightly modified so that when we are in a logic like QF_LIA, there are no registered unevaluated operators, hence the check above is unnecessary. This is to minimize the performance impact of this change.

Fixes #4500.