#5140

Z3Prover · May 22, 2021 · a10de2e · a10de2e
1 parent c230d89
commit a10de2e
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 5 deletions.
diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp
@@ -1188,7 +1188,7 @@ namespace smt2 {
 
         void parse_string_const() {
             SASSERT(curr() == scanner::STRING_TOKEN);
-            zstring zs(m_scanner.get_string());
+            zstring zs(m_scanner.get_string(), true);
             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
@@ -73,10 +73,10 @@ bool zstring::is_escape_char(char const *& s, unsigned& result) {
     return false;
 }
 
-zstring::zstring(char const* s) {
+zstring::zstring(char const* s, bool from_input) {
     while (*s) {
         unsigned ch = 0;
-        if (is_escape_char(s, ch)) {
+        if (from_input && is_escape_char(s, ch)) {
             m_buffer.push_back(ch);
         }
         else {

diff --git a/src/util/zstring.h b/src/util/zstring.h
@@ -32,8 +32,8 @@ class zstring {
     static unsigned ascii_max_char() { return 255; }
     static unsigned ascii_num_bits() { return 8; }
     zstring() {}
-    zstring(char const* s);
-    zstring(const std::string &str) : zstring(str.c_str()) {}
+    zstring(char const* s, bool from_input);
+    zstring(const std::string &str) : zstring(str.c_str(), false) {}
     zstring(unsigned sz, unsigned const* s) { m_buffer.append(sz, s); SASSERT(well_formed()); }
     zstring(unsigned ch);
     zstring replace(zstring const& src, zstring const& dst) const;