Python 3.x string decoding fix

scripts/update_api.py

@@ -99,7 +99,7 @@ else:
      if s != None:
         enc = sys.stdout.encoding
         if enc != None: return s.decode(enc)
-        else: return s
+        else: return s.decode('ascii')
      else:
         return ""
 

src/api/python/z3printer.py

@@ -1157,7 +1157,13 @@ def set_pp_option(k, v):
 def obj_to_string(a):
     out = io.StringIO()
     _PP(out, _Formatter(a))
-    return out.getvalue()
+    r = out.getvalue()
+    if sys.version < '3':
+        return r
+    else:
+        enc = sys.stdout.encoding
+        if enc != None: return r.decode(enc)
+        return r
 
 _html_out = None