From 706a037bf4bc20e37f85978b6ae8912cb9f32e67 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Mon, 16 Nov 2015 15:16:50 +0100
Subject: [PATCH] Python 3.x string decoding fix

---
 scripts/update_api.py       | 2 +-
 src/api/python/z3printer.py | 8 +++++++-
 2 files changed, 8 insertions(+), 2 deletions(-)

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