From 520b24aab419dfe6acbdf573d74273a125589334 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 30 Jan 2021 04:58:58 -0800
Subject: [PATCH] string escaping
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/ast/seq_decl_plugin.cpp | 4 +---
src/parsers/smt2/smt2parser.cpp | 3 ++-
src/util/zstring.cpp | 2 +-
3 files changed, 4 insertions(+), 5 deletions(-)
diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index 0c690f3f5..f1ef304e2 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -629,9 +629,7 @@ void seq_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol
}
app* seq_decl_plugin::mk_string(symbol const& s) {
- zstring canonStr(s.bare_str());
- symbol canonSym(canonStr.encode());
- parameter param(canonSym);
+ parameter param(s);
func_decl* f = m_manager->mk_const_decl(m_stringc_sym, m_string,
func_decl_info(m_family_id, OP_STRING_CONST, 1, ¶m));
return m_manager->mk_const(f);
diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp
index 85990c871..266cb4420 100644
--- a/src/parsers/smt2/smt2parser.cpp
+++ b/src/parsers/smt2/smt2parser.cpp
@@ -1188,7 +1188,8 @@ namespace smt2 {
void parse_string_const() {
SASSERT(curr() == scanner::STRING_TOKEN);
- expr_stack().push_back(sutil().str.mk_string(symbol(m_scanner.get_string())));
+ zstring zs(m_scanner.get_string());
+ expr_stack().push_back(sutil().str.mk_string(zs));
TRACE("smt2parser", tout << "new string: " << mk_pp(expr_stack().back(), m()) << "\n";);
next();
}
diff --git a/src/util/zstring.cpp b/src/util/zstring.cpp
index 0df1f3dcd..941a05f4a 100644
--- a/src/util/zstring.cpp
+++ b/src/util/zstring.cpp
@@ -137,7 +137,7 @@ std::string zstring::encode() const {
#define _flush() if (offset > 0) { buffer[offset] = 0; strm << buffer; offset = 0; }
for (unsigned i = 0; i < m_buffer.size(); ++i) {
unsigned ch = m_buffer[i];
- if (ch < 32 || ch >= 128) {
+ if (ch < 32 || ch >= 128 || ch == '\\') {
_flush();
strm << "\\u{" << std::hex << ch << std::dec << "}";
}