avoid SMT simplification of "true" and "false"

These literals are already as simple as they can be. Any attempt to ask the SMT
solver to simplify them just produces themselves. So avoid calling the solver
altogether in these cases.

Github: closes #139 "avoid calling SMT solver for "true" and "false""