Haramonize the characer set used to talk to Z3.

There is no need to use ISO-8859-1 when we can use UTF-8 for talking to Z3,
so use that for both input/output.  Also move the UTF-8 string constant to
a constant, allowing for easy changing later.