diff --git a/scripts/update_api.py b/scripts/update_api.py
index bb5935a1e..6e7b6d5f7 100644
--- a/scripts/update_api.py
+++ b/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 ""
 
diff --git a/src/api/python/z3printer.py b/src/api/python/z3printer.py
index 5116046dd..2a242865e 100644
--- a/src/api/python/z3printer.py
+++ b/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