don't bail out from SMT simplification on encountering the built-in boolean enum

Rather interesting screw up there. We were bailing out of SMT simplification
when encountering an enum, as we don't support it yet. However, every model
begins with the implicit definition of the built-in type boolean. So SMT
simplification was previously useless as it would bail out on every single
model.

We still don't handle full enums, but we can at least cope with boolean now.

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