1 files changed, 29 insertions, 4 deletions
diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp
index 93178b948..8d68d4e86 100644
--- a/src/util/regexp.cpp
+++ b/src/util/regexp.cpp
@@ -58,13 +58,25 @@ unsigned String::convertUnsignedIntToCode(unsigned i)
   return (i + start_code()) % num_codes();
 }
 
+String::String(const std::vector<unsigned> &s) : d_str(s)
+{
+#ifdef CVC4_ASSERTIONS
+  for (unsigned u : d_str)
+  {
+    Assert(convertUnsignedIntToCode(u) < num_codes());
+  }
+#endif
+}
+
 int String::cmp(const String &y) const {
   if (size() != y.size()) {
     return size() < y.size() ? -1 : 1;
   }
   for (unsigned int i = 0; i < size(); ++i) {
     if (d_str[i] != y.d_str[i]) {
-      return getUnsignedCharAt(i) < y.getUnsignedCharAt(i) ? -1 : 1;
+      unsigned cp = convertUnsignedIntToCode(d_str[i]);
+      unsigned cpy = convertUnsignedIntToCode(y.d_str[i]);
+      return cp < cpy ? -1 : 1;
     }
   }
   return 0;
@@ -207,12 +219,25 @@ std::vector<unsigned> String::toInternal(const std::string &s,
       i++;
     }
   }
+#ifdef CVC4_ASSERTIONS
+  for (unsigned u : str)
+  {
+    Assert(convertUnsignedIntToCode(u) < num_codes());
+  }
+#endif
   return str;
 }
 
-unsigned char String::getUnsignedCharAt(size_t pos) const {
-  Assert(pos < size());
-  return convertUnsignedIntToChar(d_str[pos]);
+unsigned String::front() const
+{
+  Assert(!d_str.empty());
+  return d_str.front();
+}
+
+unsigned String::back() const
+{
+  Assert(!d_str.empty());
+  return d_str.back();
 }
 
 std::size_t String::overlap(const String &y) const {