Fix issue involving dropped purification lemmas for transcendental functions (#8198)

Fix issue involving dropped purification lemmas for transcendental functions (#8198)

Fixes #4693.
Fixes #8181 (which now times out).

The issue was caused by purification lemmas being dropped, often in incremental mode. This meant that we were replacing sin(t) by sin(k) when checking models, but not having any information about sin(k).

We now are more robust and send the purification lemmas for transcendental functions based on checking whether it is necessary to do so.