The non-printable delete control character (Unicode code point U+007F or 127 in decimal) is printed directly to output in string literals instead of producing `"\u{7f}".
For example:
(declare-const x String)
(assert (= x "\u{7e}\u{7f}\u{80}"))
(check-sat)
(get-model)
produces the model
(
(define-fun x () String
"~�\u{80}")
)
I think the problem is in the following line
|
if (ch < 32 || ch >= 128 || ('\\' == ch && i + 1 < m_buffer.size() && 'u' == m_buffer[i+1])) { |
The test should be
ch < 32 || ch >= 127 || ...
The non-printable delete control character (Unicode code point U+007F or 127 in decimal) is printed directly to output in string literals instead of producing `"\u{7f}".
For example:
produces the model
I think the problem is in the following line
z3/src/util/zstring.cpp
Line 153 in 77cb70a
The test should be
ch < 32 || ch >= 127 || ...