[hwayne]

...Whoops. Yup, SMT solvers can famously return `unknown` on top of `sat` and `unsat`. Just added a post addendum about the mistake.