From a10de2e975deaecdbc41498fe7d138cc8be5ce5f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 22 May 2021 10:15:06 -0700
Subject: [PATCH] #5140

---
 src/parsers/smt2/smt2parser.cpp | 2 +-
 src/util/zstring.cpp            | 4 ++--
 src/util/zstring.h              | 4 ++--
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp
index 344c61283f9..596cb8af90e 100644
--- 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
index 8508b9790ba..aa5bdd665f7 100644
--- 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
index 83679225230..6181240caad 100644
--- 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;