From 50375df8dc6e8b60b6c3306fdba0e4ccb296a4d5 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 15 Sep 2021 15:36:07 +0100
Subject: [PATCH] enforce idempotency

bug reported by Clemens
---
 src/util/zstring.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/util/zstring.cpp b/src/util/zstring.cpp
index 9f61be171..534999606 100644
--- 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 << "}";
         }