mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 08:28:44 +00:00
Code Activity

enforce idempotency

Browse source 
bug reported by Clemens
This commit is contained in:
Nikolaj Bjorner 2021-09-15 15:36:07 +01:00
parent c58b2f4a9c
commit 50375df8dc
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/util/zstring.cpp
View file

@ -150,7 +150,7 @@ std::string zstring::encode() const {
#define _flush() if (offset > 0) { buffer[offset] = 0; strm << buffer; offset = 0; } #define _flush() if (offset > 0) { buffer[offset] = 0; strm << buffer; offset = 0; }
for (unsigned i = 0; i < m_buffer.size(); ++i) { for (unsigned i = 0; i < m_buffer.size(); ++i) {
unsigned ch = m_buffer[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(); _flush();
strm << "\\u{" << std::hex << ch << std::dec << "}"; strm << "\\u{" << std::hex << ch << std::dec << "}";
} }