Slight refactoring, introduces a number of different ways to pass the
information to the SMT solver.

Also introduces a few more examples.

The unit test suite gets broken with this change.