mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
fix for #975, add mask to ensure character encoding is unique within range of bits used for encoding
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
7bb5e72e07
commit
48638c6f1e
|
@ -1435,6 +1435,7 @@ bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_
|
|||
zstring s;
|
||||
bool lchange = false;
|
||||
SASSERT(lhs.empty());
|
||||
TRACE("seq", tout << ls << "\n"; tout << rs << "\n";);
|
||||
// solve from back
|
||||
while (true) {
|
||||
while (!rs.empty() && m_util.str.is_empty(rs.back())) {
|
||||
|
@ -1552,9 +1553,11 @@ bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_
|
|||
head2 < rs.size() &&
|
||||
m_util.str.is_string(ls[head1].get(), s1) &&
|
||||
m_util.str.is_string(rs[head2].get(), s2)) {
|
||||
TRACE("seq", tout << s1 << " - " << s2 << " " << s1.length() << " " << s2.length() << "\n";);
|
||||
unsigned l = std::min(s1.length(), s2.length());
|
||||
for (unsigned i = 0; i < l; ++i) {
|
||||
if (s1[i] != s2[i]) {
|
||||
TRACE("seq", tout << "different at position " << i << " " << s1[i] << " " << s2[i] << "\n";);
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
|
|
@ -126,13 +126,14 @@ static bool is_escape_char(char const *& s, unsigned& result) {
|
|||
zstring::zstring(encoding enc): m_encoding(enc) {}
|
||||
|
||||
zstring::zstring(char const* s, encoding enc): m_encoding(enc) {
|
||||
unsigned mask = 0xFF; // TBD for UTF
|
||||
while (*s) {
|
||||
unsigned ch;
|
||||
if (is_escape_char(s, ch)) {
|
||||
m_buffer.push_back(ch);
|
||||
m_buffer.push_back(ch & mask);
|
||||
}
|
||||
else {
|
||||
m_buffer.push_back(*s);
|
||||
m_buffer.push_back(*s & mask);
|
||||
++s;
|
||||
}
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue