mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
#4939 escape character
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
f48fb8d3e8
commit
5414030875
|
@ -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));
|
||||
|
|
|
@ -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;
|
||||
}
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue