From f0689546f3419a791e3f2531118d964c20383661 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 26 Feb 2020 09:16:23 -0800
Subject: [PATCH] return non-escaped string value for Python #3080

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 scripts/update_api.py   |  2 +-
 src/api/api_context.h   |  2 ++
 src/api/api_seq.cpp     | 11 +++++++----
 src/api/python/z3/z3.py |  5 ++++-
 src/api/z3_api.h        |  4 ++--
 5 files changed, 16 insertions(+), 8 deletions(-)

diff --git a/scripts/update_api.py b/scripts/update_api.py
index ec3fe4903..3e6c6001f 100755
--- a/scripts/update_api.py
+++ b/scripts/update_api.py
@@ -70,7 +70,7 @@ Type2Str = { VOID : 'void', VOID_PTR : 'void*', INT : 'int', UINT : 'unsigned',
 Type2PyStr = { VOID_PTR : 'ctypes.c_void_p', INT : 'ctypes.c_int', UINT : 'ctypes.c_uint', INT64 : 'ctypes.c_longlong',
                UINT64 : 'ctypes.c_ulonglong', DOUBLE : 'ctypes.c_double', FLOAT : 'ctypes.c_float',
                STRING : 'ctypes.c_char_p', STRING_PTR : 'ctypes.POINTER(ctypes.c_char_p)', BOOL : 'ctypes.c_bool', SYMBOL : 'Symbol',
-               PRINT_MODE : 'ctypes.c_uint', ERROR_CODE : 'ctypes.c_uint', CHAR : 'ctypes.c_char', CHAR_PTR: 'ctypes.c_char_p'
+               PRINT_MODE : 'ctypes.c_uint', ERROR_CODE : 'ctypes.c_uint', CHAR : 'ctypes.c_char', CHAR_PTR: 'ctypes.POINTER(ctypes.c_char)'
                }
 
 # Mapping to .NET types
diff --git a/src/api/api_context.h b/src/api/api_context.h
index e81c3ba02..28fee34b3 100644
--- a/src/api/api_context.h
+++ b/src/api/api_context.h
@@ -187,6 +187,8 @@ namespace api {
         char * mk_external_string(char const * str, unsigned n);
         char * mk_external_string(char const * str);
         char * mk_external_string(std::string && str);
+        sbuffer<char>              m_char_buffer;
+
 
         // Create a numeral of the given sort
         expr * mk_numeral_core(rational const & n, sort * s);
diff --git a/src/api/api_seq.cpp b/src/api/api_seq.cpp
index 00136c021..dd8524ba0 100644
--- a/src/api/api_seq.cpp
+++ b/src/api/api_seq.cpp
@@ -150,7 +150,7 @@ extern "C" {
         Z3_CATCH_RETURN("");
     }
 
-    Z3_string Z3_API Z3_get_lstring(Z3_context c, Z3_ast s, unsigned* length) {
+    Z3_char_ptr Z3_API Z3_get_lstring(Z3_context c, Z3_ast s, unsigned* length) {
         Z3_TRY;
         LOG_Z3_get_lstring(c, s, length);
         RESET_ERROR_CODE();
@@ -163,9 +163,12 @@ extern "C" {
             SET_ERROR_CODE(Z3_INVALID_ARG, "expression is not a string literal");
             return "";
         }
-        std::string s = str.as_string();        
-        *length = (unsigned)(s.size());
-        return mk_c(c)->mk_external_string(s.c_str(), *length);
+        mk_c(c)->m_char_buffer.reset();
+        for (unsigned i = 0; i < str.length(); ++i) {
+            mk_c(c)->m_char_buffer.push_back((char)str[i]);
+        }
+        *length = str.length();
+        return mk_c(c)->m_char_buffer.c_ptr();
         Z3_CATCH_RETURN("");
     }
 
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 4792c2ab5..4c143f3ff 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -10032,10 +10032,13 @@ class SeqRef(ExprRef):
     def is_string_value(self):
         return Z3_is_string(self.ctx_ref(), self.as_ast())
 
+
     def as_string(self):
         """Return a string representation of sequence expression."""
         if self.is_string_value():
-           return Z3_get_string(self.ctx_ref(), self.as_ast())
+            string_length = ctypes.c_uint()
+            chars = Z3_get_lstring(self.ctx_ref(), self.as_ast(), byref(string_length))
+            return string_at(chars, size=string_length.value).decode('ascii')
         return Z3_ast_to_string(self.ctx_ref(), self.as_ast())
 
     def __le__(self, other):
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 60059e460..920665ca5 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -3474,9 +3474,9 @@ extern "C" {
 
        \pre  Z3_is_string(c, s)
 
-       def_API('Z3_get_lstring' ,STRING ,(_in(CONTEXT), _in(AST), _out(UINT)))
+       def_API('Z3_get_lstring' ,CHAR_PTR ,(_in(CONTEXT), _in(AST), _out(UINT)))
      */
-    Z3_string Z3_API Z3_get_lstring(Z3_context c, Z3_ast s, unsigned* length);
+    Z3_char_ptr Z3_API Z3_get_lstring(Z3_context c, Z3_ast s, unsigned* length);
 
     /**
        \brief Create an empty sequence of the sequence sort \c seq.