Avoid defining let-bound variables on SMT level

[marcoeilers]

When evaluating an expression let x == (e1) in e2, Silicon emits an (assert (= x e1)) for a fresh variable x on the SMT level to make sure that e1 is available as a triggering term even when does not occur in e2; this is done to fix viperproject/silver#688.

However, these additional variables and equalities can slow down verification significantly (see attached file
floats.txt).

This PR implements a compromise and emits these definitions only when e1 might be triggering and only during function and predicate verification, since in those, let-bound function calls and similar expressions are commonly used e.g. to call lemmas or trigger quantifiers (as in the original issue).