Fix policy for purifying arguments of exp (#8416)

Fix policy for purifying arguments of exp (#8416)

This corrects the policy for when to purify exp. It ensures we purify exp whenever the kind is not a variable or constant, instead of when the kind is a transcendental function app. The latter permits problematic terms like (exp (* (exp 1.0) (exp 1.0)).

This also corrects an issue where information for ordering on variables would be skipped if we failed to produce a model value for a single variable, which was the original source of the error on #8415.

It furthermore fixes the PfRule ARITH_TRANS_EXP_APPROX_BELOW, which did not handle non-constant arguments of exp.

Fixes #8415.