skip SMT simplification of unsupported expressions, and continue

We were aborting SMT simplification whenever we hit an unsupported expression.
This was unnecessarily conservative as one unsupported expression does not mean
that every later expression in the model will be unsupported. Note that we still
*do* need to abort on unsupported definitions and similar constructs while
traversing the model because skipping these can affect the correctness of later
simplification decisions.

Github: related to #130 "interact with SMT solver"