enforce idempotency

bug reported by Clemens
Z3Prover · Sep 15, 2021 · 50375df · 50375df
1 parent c58b2f4
commit 50375df
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/util/zstring.cpp b/src/util/zstring.cpp
@@ -150,7 +150,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 && i + 1 < m_buffer.size() && 'u' == m_buffer[i+1])) {
             _flush();
             strm << "\\u{" << std::hex << ch << std::dec << "}";
         }