From 54140308754fad26c29b80791b4d71c222f2d5a8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 28 Jan 2021 11:57:00 -0800 Subject: [PATCH] #4939 escape character Signed-off-by: Nikolaj Bjorner --- src/api/api_seq.cpp | 1 + src/util/zstring.cpp | 7 +------ 2 files changed, 2 insertions(+), 6 deletions(-) diff --git a/src/api/api_seq.cpp b/src/api/api_seq.cpp index 462c2da2e..9657befd9 100644 --- a/src/api/api_seq.cpp +++ b/src/api/api_seq.cpp @@ -49,6 +49,7 @@ extern "C" { LOG_Z3_mk_string(c, str); RESET_ERROR_CODE(); zstring s(str); + std::cout << "mk-string " << str << "\n"; app* a = mk_c(c)->sutil().str.mk_string(s); mk_c(c)->save_ast_trail(a); RETURN_Z3(of_ast(a)); diff --git a/src/util/zstring.cpp b/src/util/zstring.cpp index 73e195a3c..86ce2b42c 100644 --- a/src/util/zstring.cpp +++ b/src/util/zstring.cpp @@ -235,10 +235,6 @@ std::string zstring::encode() const { _flush(); strm << esc_table[ch]; } - else if (ch == '\\') { - _flush(); - strm << "\\\\"; - } else if (ch >= 256) { _flush(); strm << "\\u{" << std::hex << ch << std::dec << "}"; @@ -248,9 +244,8 @@ std::string zstring::encode() const { strm << "\\x" << std::hex << ch << std::dec; } else { - if (offset == 99) { + if (offset == 99) _flush(); - } buffer[offset++] = (char)ch; } }