when encountering an SMT-unsupported expression, include it in the debug message

When diagnosing why a model you expect to be SMT-simplified is not getting
simplified, it is helpful for Rumur to actually tell you the reason it gave up.

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