From 57d430b3fdc9c25171a227104482150d9ac01cf0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Apr 2020 06:38:14 -0700 Subject: [PATCH] fix #3700 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 2 +- src/ast/seq_decl_plugin.cpp | 16 ++++++++-------- src/ast/seq_decl_plugin.h | 4 ++-- 3 files changed, 11 insertions(+), 11 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 2cf1f0814..2ef7ea69d 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -1125,7 +1125,7 @@ br_status seq_rewriter::mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result bool isc2 = m_util.str.is_string(b, s2); if (isc1 && isc2 && m_autil.is_numeral(c, r) && r.is_unsigned()) { - int idx = s1.indexof(s2, r.get_unsigned()); + int idx = s1.indexofu(s2, r.get_unsigned()); result = m_autil.mk_numeral(rational(idx), true); return BR_DONE; } diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 3bfe25877..78e685426 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -280,13 +280,13 @@ bool zstring::contains(zstring const& other) const { return cont; } -int zstring::indexof(zstring const& other, int offset) const { - SASSERT(offset >= 0); - if (static_cast(offset) <= length() && other.length() == 0) return offset; - if (static_cast(offset) == length()) return -1; +int zstring::indexofu(zstring const& other, unsigned offset) const { + if (offset <= length() && other.length() == 0) return offset; + if (offset == length()) return -1; + if (offset < other.length() + offset) return -1; if (other.length() + offset > length()) return -1; unsigned last = length() - other.length(); - for (unsigned i = static_cast(offset); i <= last; ++i) { + for (unsigned i = offset; i <= last; ++i) { bool prefix = true; for (unsigned j = 0; prefix && j < other.length(); ++j) { prefix = m_buffer[i + j] == other[j]; @@ -313,10 +313,10 @@ int zstring::last_indexof(zstring const& other) const { return -1; } -zstring zstring::extract(int offset, int len) const { +zstring zstring::extract(unsigned offset, unsigned len) const { zstring result(m_encoding); - SASSERT(0 <= offset && 0 <= len); - int last = std::min(offset+len, static_cast(length())); + if (offset + len < offset) return result; + int last = std::min(offset+len, length()); for (int i = offset; i < last; ++i) { result.m_buffer.push_back(m_buffer[i]); } diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 8f124c617..653f46afe 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -119,9 +119,9 @@ public: bool suffixof(zstring const& other) const; bool prefixof(zstring const& other) const; bool contains(zstring const& other) const; - int indexof(zstring const& other, int offset) const; + int indexofu(zstring const& other, unsigned offset) const; int last_indexof(zstring const& other) const; - zstring extract(int lo, int hi) const; + zstring extract(unsigned lo, unsigned hi) const; zstring operator+(zstring const& other) const; bool operator==(const zstring& other) const; bool operator!=(const zstring& other) const;