Add trascendental function kinds to list of unevaluated operators (#4640)

Add trascendental function kinds to list of unevaluated operators (#4640)

Fixes #4636.

This adds transcendental function kinds to the list of unevaluated operators (operators that don't necessarily rewrite to constants when applied to constant children). One consequence of this is that when models are enabled, we cannot solve for equations like (= a (cos b)), since the value of (cos b) is not necessarily evaluable, and hence must be approximated. As a result, we answer the benchmark on #4636 instead of generating an incorrect model (when models are enabled). When models are disabled, we answer "sat". A regression had a similar issue which happened to be succeeding. I've added --no-check-models to this regression (or otherwise we would answer unknown for this benchmark).