#ifndef STL_STRING
#define STL_STRING

#include "definitions.h"
#include "cstring"
#include "cstdio"
#include "cassert"
#include "iostream"
#include "cstdlib"
#include "memory"

extern "C" void itoa(int value, char *str, int base);

namespace std
{
template <class charT>
struct char_traits
{
  using char_type = charT;
  using int_type = int;
  using off_type = std::ptrdiff_t;
  using pos_type = std::size_t;

  static void assign(char_type &c1, const char_type &c2) noexcept
  {
    c1 = c2;
  }

  static char_type *assign(char_type *s, std::size_t n, char_type a)
  {
    for (std::size_t i = 0; i < n; ++i)
      s[i] = a;
    return s;
  }

  static bool eq(char_type c1, char_type c2) noexcept
  {
    return c1 == c2;
  }

  static bool lt(char_type c1, char_type c2) noexcept
  {
    return c1 < c2;
  }

  static int compare(const char_type *s1, const char_type *s2, std::size_t n)
  {
    for (std::size_t i = 0; i < n; ++i)
    {
      if (lt(s1[i], s2[i]))
        return -1;
      if (lt(s2[i], s1[i]))
        return 1;
    }
    return 0;
  }

  static std::size_t length(const char_type *s)
  {
    std::size_t i = 0;
    while (!eq(s[i], char_type(0)))
      ++i;
    return i;
  }

  static const char_type *
  find(const char_type *s, std::size_t n, const char_type &a)
  {
    for (std::size_t i = 0; i < n; ++i)
      if (eq(s[i], a))
        return s + i;
    return nullptr;
  }

  static char_type *move(char_type *dest, const char_type *src, std::size_t n)
  {
    return static_cast<char_type *>(memmove(dest, src, n * sizeof(charT)));
  }

  static char_type *copy(char_type *dest, const char_type *src, std::size_t n)
  {
    return static_cast<char_type *>(memcpy(dest, src, n * sizeof(charT)));
  }

  static int_type eof() noexcept
  {
    return EOF;
  }

  static int_type to_int_type(char_type c) noexcept
  {
    return static_cast<unsigned char>(c);
  }

  static char_type to_char_type(int_type c) noexcept
  {
    return static_cast<char_type>(c);
  }

  static bool eq_int_type(int_type c1, int_type c2) noexcept
  {
    return c1 == c2;
  }

  static int_type not_eof(int_type c) noexcept
  {
    return (c == eof()) ? 0 : c;
  }
};

template <
  class CharT,
  class Traits = char_traits<CharT>,
  class Alloc = allocator<CharT>>
class basic_string
{
public:
  static const size_t npos = static_cast<size_t>(-1);
  char *str;
  int _size;

  class const_iterator;
  class iterator
  {
  public:
    char *pointer;
    char *it_str;
    int pos;

    iterator(const iterator &i)
    {
      pointer = i.pointer;
      pos = i.pos;
      it_str = i.it_str;
    }

    iterator()
    {
      pointer = NULL;
      pos = 0;
      it_str = NULL;
    }

    iterator(char *p_pointer)
    {
      pointer = p_pointer;
      pos = 0;
      it_str = p_pointer;
    }

    iterator &operator=(const const_iterator &right)
    {
      this->pointer = right.pointer;
      this->pos = right.pos;
      return *this;
    }

    iterator &operator=(const iterator &right)
    {
      this->pointer = right.pointer;
      this->pos = right.pos;
      this->it_str = right.it_str;
      return *this;
    }

    char *operator->()
    {
      return pointer;
    }

    char &operator*()
    {
      return *pointer;
    }

    CC_DIAGNOSTIC_PUSH()
    DO_PRAGMA(GCC diagnostic ignored "-Wreturn-stack-address")

    iterator operator-(int n) const
    {
      iterator buffer;
      buffer.pointer = pointer - sizeof(char) * n;
      buffer.pos = pos - n;
      buffer.it_str = it_str;
      __ESBMC_assert(buffer.pos >= 0, "underflow");
      return buffer;
    }

    iterator operator+(int n) const
    {
      iterator buffer;
      buffer.pointer = pointer + sizeof(char) * n;
      buffer.pos = pos + n;
      buffer.it_str = it_str;
      return buffer;
    }

    //operator increases pointer address, but returns old value.
    //It's like "++c"
    iterator &operator++()
    {
      pointer = pointer + sizeof(char);
      pos++;
      return *this;
    }

    //operator increases pointer address and returns new value
    //It's like "c++"
    iterator operator++(int _b)
    {
      iterator buffer = *this;
      pointer = pointer + sizeof(char);
      pos++;
      return buffer;
    }
    //operator decreases pointer address, but returns old value.
    //It's like "--c"
    iterator &operator--()
    {
      pointer = pointer - sizeof(char);
      pos--;
      return *this;
    }

    CC_DIAGNOSTIC_POP()

    //operator decreases pointer address and returns new value
    //It's like "c--"
    iterator operator--(int _b)
    {
      iterator buffer = *this;
      pointer = pointer - sizeof(char);
      pos--;
      return buffer;
    }

    //operator returns true if both members point to the same address
    //returns false if not happen

    bool operator==(const iterator &right) const
    {
      return (pointer == right.pointer && pos == right.pos);
    }

    bool operator==(const const_iterator &right) const
    {
      return (pointer == right.pointer && pos == right.pos);
    }

    bool operator!=(const iterator &right) const
    {
      return !(pos == right.pos);
    }

    bool operator!=(const const_iterator &right) const
    {
      return !(pos == right.pos);
    }

    bool operator<(const iterator &right) const
    {
      return (pos < right.pos);
    }

    bool operator<(const const_iterator &right) const
    {
      return (pos < right.pos);
    }

    //operator returns true if pointer address of right is lower than this

    bool operator>(const iterator &right) const
    {
      return (pos > right.pos);
    }

    bool operator>(const const_iterator &right) const
    {
      return (pos > right.pos);
    }

    //operator returns true if pointer address of right is higher or equal than this

    bool operator<=(const iterator &right) const
    {
      return !(pos > right.pos);
    }

    bool operator<=(const const_iterator &right) const
    {
      return !(pos > right.pos);
    }

    //operator returns true if pointer address of right is lower or equal than this

    bool operator>=(const iterator &right) const
    {
      return !(pos < right.pos);
    }

    bool operator>=(const const_iterator &right) const
    {
      return !(pos < right.pos);
    }

    CC_DIAGNOSTIC_PUSH()
    DO_PRAGMA(GCC diagnostic ignored "-Wreturn-stack-address")

    //operator adds n positions on pointer address, and returns its address value

    iterator &operator+=(int n)
    {
      pointer = pointer + sizeof(char) * n;
      pos += n;
      return *this;
    }

    //operator subtracts n positions on pointer address, and returns its address value

    iterator operator-=(int n)
    {
      pointer = pointer - sizeof(char) * n;
      pos -= n;
      return *this;
    }

    CC_DIAGNOSTIC_POP()
  };

  class const_iterator
  {
  public:
    char *pointer;
    int pos;

    const_iterator(const iterator &i)
    {
      pointer = i.pointer;
      pos = i.pos;
    }

    const_iterator(const const_iterator &i)
    {
      pointer = i.pointer;
      pos = i.pos;
    }

    const_iterator()
    {
      pointer = NULL;
    }

    //This creates an iterator that points to the value pointed to by p_pointer.
    const_iterator(char *p_pointer)
    {
      pointer = p_pointer;
    }

    char *operator->()
    { //operator returns memo address pointer
      return pointer;
    }

    char &operator*()
    {
      return *pointer;
    }

    CC_DIAGNOSTIC_PUSH()
    DO_PRAGMA(GCC diagnostic ignored "-Wreturn-stack-address")

    //operator subtracts n positions on pointer address of this
    const_iterator operator-(int n) const
    {
      const_iterator buffer;
      buffer.pointer = pointer - sizeof(char) * n;
      buffer.pos = pos - n;
      return buffer;
    }

    const_iterator operator+(int n) const
    {
      const_iterator buffer;
      buffer.pointer = pointer + sizeof(char) * n;
      buffer.pos = pos + n;
      return buffer;
    }

    CC_DIAGNOSTIC_POP()

    const_iterator &operator++()
    {
      pointer = pointer + sizeof(char);
      pos++;
      return *this;
    }
    const_iterator operator++(int)
    {
      const_iterator buffer = *this;
      pointer = pointer + sizeof(char);
      pos++;
      return buffer;
    }

    //operator returns true if both members point to the same address
    //returns false if not happen

    bool operator==(const iterator &right) const
    {
      return (pointer == right.pointer);
    }

    bool operator==(const const_iterator &right) const
    {
      return (pointer == right.pointer);
    }

    //just the complement of "=="

    bool operator!=(const const_iterator &right) const
    {
      return !(pointer == right.pointer);
    }

    bool operator!=(const iterator &right) const
    {
      return !(pointer == right.pointer);
    }

    bool operator!=(iterator right)
    {
      return !(pointer == right.pointer);
    }

    //operator returns true if pointer address of right is higher than this

    bool operator<(const iterator &right) const
    {
      return (pointer < right.pointer);
    }

    bool operator<(const const_iterator &right) const
    {
      return (pointer < right.pointer);
    }

    //operator returns true if pointer address of right is lower than this

    bool operator>(const iterator &right) const
    {
      return (pointer > right.pointer);
    }

    bool operator>(const const_iterator &right) const
    {
      return (pointer > right.pointer);
    }

    //operator returns true if pointer address of right is higher or equal than this

    bool operator<=(const iterator &right) const
    {
      return !(pointer > right.pointer);
    }

    bool operator<=(const const_iterator &right) const
    {
      return !(pointer > right.pointer);
    }

    //operator returns true if pointer address of right is lower or equal than this

    bool operator>=(const iterator &right) const
    {
      return !(pointer < right.pointer);
    }

    bool operator>=(const const_iterator &right) const
    {
      return !(pointer < right.pointer);
    }
    const_iterator(iterator &i)
    {
      pointer = i.pointer;
      pos = i.pos;
    }

    //operator adds n positions on pointer address, and returns its address value
  };

  basic_string();
  basic_string(const CharT *);
  basic_string(const CharT *s, size_t n);
  basic_string(
    const basic_string<CharT, Traits, Alloc> &str,
    size_t pos,
    size_t n);
  basic_string(basic_string<CharT, Traits, Alloc> &s, size_t n);
  basic_string(char c, size_t n);
  explicit basic_string(int len);
  basic_string(const_iterator begin, const_iterator end);
  char *c_str() const;
  bool operator>(basic_string<CharT, Traits, Alloc> &a);
  bool operator>(const char *a);
  friend bool
  operator>(const char *lhs, basic_string<CharT, Traits, Alloc> &rhs);
  friend bool
  operator>(basic_string<CharT, Traits, Alloc> &lhs, const char *rhs);
  bool operator<(basic_string<CharT, Traits, Alloc> &a);
  bool operator<(const char *a);
  friend bool
  operator<(const char *lhs, basic_string<CharT, Traits, Alloc> &rhs);
  friend bool
  operator<(basic_string<CharT, Traits, Alloc> &lhs, const char *rhs);
  bool operator>=(basic_string<CharT, Traits, Alloc> &a);
  bool operator>=(const char *lhs);
  bool operator<=(basic_string<CharT, Traits, Alloc> &a);
  bool operator<=(const char *lhs);
  basic_string<CharT, Traits, Alloc> &
  operator=(basic_string<CharT, Traits, Alloc> &str);
  basic_string<CharT, Traits, Alloc> &operator=(const char *s);
  basic_string<CharT, Traits, Alloc> &operator=(char c);
  basic_string<CharT, Traits, Alloc> &
  operator=(const basic_string<CharT, Traits, Alloc> &str);
  basic_string<CharT, Traits, Alloc> &
  operator+=(const basic_string<CharT, Traits, Alloc> &s);
  basic_string<CharT, Traits, Alloc> &operator+=(const char *s);
  basic_string<CharT, Traits, Alloc> &operator+=(char s);
  //TODO: operator+

  char &operator[](size_t pos);
  char at(size_t pos) const;
  char front() const;
  char back() const;
  bool empty() const;
  size_t length() const;
  int compare(const basic_string<CharT, Traits, Alloc> &s) const;
  int compare(const char *s) const;
  int compare(int pos1, size_t n1, basic_string<CharT, Traits, Alloc> &s) const;
  int compare(int pos1, size_t n1, const char *s) const;
  int compare(
    size_t pos1,
    size_t n1,
    basic_string<CharT, Traits, Alloc> &s,
    size_t pos2,
    size_t n2) const;
  size_t find_first_of(
    const basic_string<CharT, Traits, Alloc> &s,
    size_t pos = 0) const;
  size_t find_first_of(const char *s, size_t pos = 0) const;
  size_t find_first_of(char c, size_t pos = 0) const;
  size_t find(basic_string<CharT, Traits, Alloc> &s, size_t pos = 0) const;
  size_t find(const char *s, size_t pos = 0) const;
  size_t find(const char *s, size_t pos, size_t n) const;
  size_t find(char c, size_t pos = 0) const;
  basic_string<CharT, Traits, Alloc> &
  assign(basic_string<CharT, Traits, Alloc> &s);
  basic_string<CharT, Traits, Alloc> &assign(const char *s, size_t n);
  basic_string<CharT, Traits, Alloc> &
  assign(basic_string<CharT, Traits, Alloc> &s, size_t pos, size_t n);
  basic_string<CharT, Traits, Alloc> &assign(const char *s);
  basic_string<CharT, Traits, Alloc> &assign(size_t n, char c);
  basic_string<CharT, Traits, Alloc> &assign(iterator one, iterator two)
  {
  __ESBMC_HIDE:
    char *s = one.it_str;
    int pos = one.pos;
    int n = two.pos, i, k;
    __ESBMC_assert(s != NULL, "The parameter must be different than NULL");
    this->_size = n - pos + 1;
    this->str = new char[this->_size + 1];
    for (k = 0, i = pos; i <= n; i++, k++)
      this->str[k] = s[i];
    this->str[k] = '\0';
    return *this;
  }
  basic_string<CharT, Traits, Alloc> &
  append(basic_string<CharT, Traits, Alloc> &s);
  basic_string<CharT, Traits, Alloc> &append(const char *s, size_t n);
  basic_string<CharT, Traits, Alloc> &
  append(basic_string<CharT, Traits, Alloc> &s, size_t pos, size_t n);
  basic_string<CharT, Traits, Alloc> &append(const char *s);
  basic_string<CharT, Traits, Alloc> &append(size_t n, char c);
  basic_string<CharT, Traits, Alloc> &append(iterator one, iterator two)
  {
  __ESBMC_HIDE:
    char *s = one.it_str;
    int sLen = strlen(s);
    int pos = one.pos;
    int n = two.pos;
    __ESBMC_assert(pos >= 0, "basic_string overflow");
    __ESBMC_assert(pos < sLen, "basic_string overflow");
    __ESBMC_assert(n <= sLen, "basic_string overflow");
    __ESBMC_assert(n > 0, "basic_string overflow");
    __ESBMC_assert(s != NULL, "The parameter must be different than NULL");
    if ((pos > sLen) || (pos > n))
    {
      // TODO: when we support try-catch, replace the assert with the throw statement below
      //throw out_of_range();
      __ESBMC_assert(0, "basic_string append failed, out_of_range");
    }

    int totalLength = this->size();
    totalLength += (n - pos + 1);
    int i, j, k;
    basic_string<CharT, Traits, Alloc> result;
    result.str = new char[totalLength + 1];
    for (i = 0; i < this->_size; i++)
    {
      result.str[i] = this->str[i];
    }
    for (j = i, k = pos; j < totalLength; j++, k++)
    {
      result.str[j] = s[k];
    }
    result.str[j] = '\0';
    this->_size = totalLength;
    this->str = result.str;
    return *this;
  }
  void swap(basic_string<CharT, Traits, Alloc> &s);
  void resize(size_t n, char c);
  void resize(size_t n);
  size_t capacity() const;
  size_t max_size() const;
  int size() const;
  size_t rfind(basic_string<CharT, Traits, Alloc> &s, size_t pos = npos) const;
  size_t rfind(const char *s, size_t pos = npos) const;
  size_t rfind(char *s) const;
  size_t rfind(char c, size_t pos = npos) const;
  size_t rfind(const char *s, size_t pos, size_t n) const;
  size_t find_last_of(
    const basic_string<CharT, Traits, Alloc> &s,
    size_t pos = npos) const;
  size_t find_last_of(const char *s, size_t pos = npos) const;
  size_t find_last_of(char *s) const;
  size_t find_last_of(char c, size_t pos = npos) const;
  size_t find_first_not_of(
    const basic_string<CharT, Traits, Alloc> &s,
    size_t pos = 0) const;
  size_t find_first_not_of(const char *s, size_t pos = 0) const;
  size_t find_first_not_of(char c, size_t pos = 0) const;
  basic_string<CharT, Traits, Alloc> &erase(size_t pos, size_t n);
  basic_string<CharT, Traits, Alloc> &erase(size_t pos, size_t n, char *tmp);
  basic_string<CharT, Traits, Alloc> &erase(size_t pos = 0);
  basic_string<CharT, Traits, Alloc> &erase(iterator it)
  {
    __ESBMC_assert(it.pos >= 0, "The parameter must be greater than zero");
    int pos = it.pos;
    int n = 1;
    int i, k, len = this->length();
    __ESBMC_assert(pos < len, "overflow");
    int lenOne = pos + 1;
    char *one = new char[lenOne];
    for (i = 0; i < pos; i++)
    {
      one[i] = this->str[i];
    }
    int lenTwo = (len - (pos + n)) + 1;
    char *two = new char[lenTwo];
    for (k = 0, i = pos + n; i < len; i++, k++)
    {
      two[k] = this->str[i];
    }
    int totalLen = len - n;
    this->str = new char[totalLen + 1];
    this->_size = totalLen;
    for (i = 0; i < lenOne - 1; i++)
    {
      this->str[i] = one[i];
    }
    for (k = 0; k < lenTwo - 1; k++, i++)
    {
      this->str[i] = two[k];
    }
    this->str[i] = '\0';
    return *this;
  }

  basic_string<CharT, Traits, Alloc> &erase(iterator begin, iterator end)
  {
    __ESBMC_assert(
      begin.pos >= 0, "The first parameter must be greater than zero");
    __ESBMC_assert(
      end.pos >= 0, "The second parameter must be greater than zero");
    int pos = begin.pos;
    int i, k, len = this->length();
    __ESBMC_assert(
      end.pos <= len, "The second parameter must be less than zero");
    int n = (end.pos - begin.pos) + 1;
    __ESBMC_assert(pos < len, "overflow");
    int lenOne = pos + 1;
    char *one = new char[lenOne];
    for (i = 0; i < pos; i++)
    {
      one[i] = this->str[i];
    }
    int lenTwo = (len - (pos + n)) + 1;
    char *two = new char[lenTwo];
    for (k = 0, i = pos + n; i < len; i++, k++)
    {
      two[k] = this->str[i];
    }
    int totalLen = len - n;
    this->str = new char[totalLen + 1];
    this->_size = totalLen;
    for (i = 0; i < lenOne - 1; i++)
    {
      this->str[i] = one[i];
    }
    for (k = 0; k < lenTwo - 1; k++, i++)
    {
      this->str[i] = two[k];
    }
    this->str[i] = '\0';
    return *this;
  }

  basic_string<CharT, Traits, Alloc> &
  replace(size_t pos1, size_t n1, const basic_string<CharT, Traits, Alloc> &s);
  basic_string<CharT, Traits, Alloc> &replace(
    size_t pos1,
    size_t n1,
    basic_string<CharT, Traits, Alloc> &s,
    size_t pos2,
    size_t n2);
  basic_string<CharT, Traits, Alloc> &
  replace(size_t pos1, size_t n1, char *s, size_t pos2, size_t n2);
  basic_string<CharT, Traits, Alloc> &
  replace(size_t pos1, size_t n1, const char *s, size_t n2);
  basic_string<CharT, Traits, Alloc> &
  replace(size_t pos1, size_t n1, const char *s);
  basic_string<CharT, Traits, Alloc> &
  replace(size_t pos1, size_t n1, size_t n2, char c);

  //new add
  basic_string<CharT, Traits, Alloc> &replace(
    basic_string<CharT, Traits, Alloc>::iterator i1,
    basic_string<CharT, Traits, Alloc>::iterator i2,
    basic_string<CharT, Traits, Alloc> &str);
  basic_string<CharT, Traits, Alloc> &replace(
    basic_string<CharT, Traits, Alloc>::iterator i1,
    basic_string<CharT, Traits, Alloc>::iterator i2,
    char *s,
    size_t n2);
  basic_string<CharT, Traits, Alloc> &replace(
    basic_string<CharT, Traits, Alloc>::iterator i1,
    basic_string<CharT, Traits, Alloc>::iterator i2,
    char *s);
  basic_string<CharT, Traits, Alloc> &replace(
    basic_string<CharT, Traits, Alloc>::iterator i1,
    basic_string<CharT, Traits, Alloc>::iterator i2,
    size_t n2,
    char c);
  basic_string<CharT, Traits, Alloc> &replace(
    basic_string<CharT, Traits, Alloc>::iterator i1,
    basic_string<CharT, Traits, Alloc>::iterator i2,
    basic_string<CharT, Traits, Alloc>::iterator i3,
    basic_string<CharT, Traits, Alloc>::iterator i4);

  basic_string<CharT, Traits, Alloc> &
  insert(size_t pos1, basic_string<CharT, Traits, Alloc> &s);
  basic_string<CharT, Traits, Alloc> &insert(
    size_t pos1,
    basic_string<CharT, Traits, Alloc> &s,
    size_t pos2,
    size_t n);
  basic_string<CharT, Traits, Alloc> &
  insert(size_t pos1, const char *s, size_t n);
  basic_string<CharT, Traits, Alloc> &insert(size_t pos1, const char *s);
  basic_string<CharT, Traits, Alloc> &insert(size_t pos1, size_t n, char c);
  basic_string<CharT, Traits, Alloc> &
  insert(iterator it_one, iterator it_two, iterator it_three)
  {
  __ESBMC_HIDE:
    int pos1 = it_one.pos;
    char *s = it_two.pointer;
    int n = it_three.pos;
    int len = this->length(), i, k;
    int lim = n;
    int sLen = strlen(s);
    __ESBMC_assert((pos1 >= 0) && (pos1 < len), "basic_string overflow");
    __ESBMC_assert(n > 0, "basic_string overflow");
    __ESBMC_assert(s != NULL, "The parameter must be different than NULL");
    __ESBMC_assert(lim < sLen, "basic_string overflow");
    int lenOne = pos1 + 1;
    char *one = new char[lenOne];
    for (i = 0; i < pos1; i++)
    {
      one[i] = this->str[i];
    }
    int lenTwo = (len - pos1) + 1;
    char *two = new char[lenTwo];
    for (k = 0, i = pos1; i < len; i++, k++)
    {
      two[k] = this->str[i];
    }
    int totalLen = n + len;
    this->str = new char[totalLen + 1];
    this->_size = totalLen;

    for (i = 0; i < lenOne - 1; i++)
    {
      this->str[i] = one[i];
    }
    for (k = 0; k < lim; k++, i++)
    {
      this->str[i] = s[k];
    }
    for (k = 0; k < lenTwo - 1; k++, i++)
    {
      this->str[i] = two[k];
    }
    this->str[i] = '\0';
    return *this;
  }
  iterator insert(iterator p, char c)
  {
    __ESBMC_assert(p.pos >= 0, "The first parameter must be greater than zero");
    int pos1 = p.pos;
    int n = 1;
    char *s = new char[n + 1];
    for (int i = 0; i < n; i++)
    {
      s[i] = c;
    }
    int len = this->length(), i, k;
    int sLen = n;
    __ESBMC_assert(pos1 < len, "overflow");
    int lenOne = pos1 + 1;
    char *one = new char[lenOne];
    for (i = 0; i < pos1; i++)
    {
      one[i] = this->str[i];
    }
    int lenTwo = (len - pos1) + 1;
    char *two = new char[lenTwo];
    for (k = 0, i = pos1; i < len; i++, k++)
    {
      two[k] = this->str[i];
    }
    int totalLen = len + n;
    this->str = new char[totalLen + 1];
    this->_size = totalLen;

    for (i = 0; i < lenOne - 1; i++)
    {
      this->str[i] = one[i];
    }
    for (k = 0; k < sLen; k++, i++)
    {
      this->str[i] = s[k];
    }
    for (k = 0; k < lenTwo - 1; k++, i++)
    {
      this->str[i] = two[k];
    }
    this->str[i] = '\0';
    basic_string<CharT, Traits, Alloc>::iterator it(this->str);
    it.pos = p.pos;
    return it;
  }

  basic_string &insert(iterator p, size_t n, char c)
  {
    __ESBMC_assert(p.pos >= 0, "The first parameter must be greater than zero");
    __ESBMC_assert(n >= 0, "The second parameter must be greater than zero");
    int pos1 = p.pos;
    char *s = new char[n + 1];
    for (int i = 0; i < n; i++)
    {
      s[i] = c;
    }
    int len = this->length(), i, k;
    int sLen = n;
    __ESBMC_assert(pos1 < len, "overflow");
    if (pos1 == (len - 1))
    {
      char *one = new char[len];
      for (i = 0; i < len; i++)
      {
        one[i] = this->str[i];
      }
      int totalLen = len + n;
      this->str = new char[totalLen + 1];
      this->_size = totalLen;
      for (i = 0; i < len; i++)
      {
        this->str[i] = one[i];
      }
      for (; i < totalLen; i++)
      {
        this->str[i] = c;
      }
      this->str[i] = '\0';
      return *this;
    }
    int lenOne = pos1 + 1;
    char *one = new char[lenOne];
    for (i = 0; i < pos1; i++)
    {
      one[i] = this->str[i];
    }
    int lenTwo = (len - pos1) + 1;
    char *two = new char[lenTwo];
    for (k = 0, i = pos1; i < len; i++, k++)
    {
      two[k] = this->str[i];
    }
    int totalLen = len + n;
    this->str = new char[totalLen + 1];
    this->_size = totalLen;

    for (i = 0; i < lenOne - 1; i++)
    {
      this->str[i] = one[i];
    }
    for (k = 0; k < sLen; k++, i++)
    {
      this->str[i] = s[k];
    }
    for (k = 0; k < lenTwo - 1; k++, i++)
    {
      this->str[i] = two[k];
    }
    this->str[i] = '\0';
    return *this;
  }

  basic_string<CharT, Traits, Alloc> &insert(const_iterator p, size_t n, char c)
  {
    __ESBMC_assert(p.pos >= 0, "The first parameter must be greater than zero");
    __ESBMC_assert(n >= 0, "The second parameter must be greater than zero");
    int pos1 = p.pos;
    char *s = new char[n + 1];
    for (int i = 0; i < n; i++)
    {
      s[i] = c;
    }
    int len = this->length(), i, k;
    int sLen = n;
    __ESBMC_assert(pos1 < len, "overflow");
    if (pos1 == (len - 1))
    {
      char *one = new char[len];
      for (i = 0; i < len; i++)
      {
        one[i] = this->str[i];
      }
      int totalLen = len + n;
      this->str = new char[totalLen + 1];
      this->_size = totalLen;
      for (i = 0; i < len; i++)
      {
        this->str[i] = one[i];
      }
      for (; i < totalLen; i++)
      {
        this->str[i] = c;
      }
      this->str[i] = '\0';
      return *this;
    }
    int lenOne = pos1 + 1;
    char *one = new char[lenOne];
    for (i = 0; i < pos1; i++)
    {
      one[i] = this->str[i];
    }
    int lenTwo = (len - pos1) + 1;
    char *two = new char[lenTwo];
    for (k = 0, i = pos1; i < len; i++, k++)
    {
      two[k] = this->str[i];
    }
    int totalLen = len + n;
    this->str = new char[totalLen + 1];
    this->_size = totalLen;

    for (i = 0; i < lenOne - 1; i++)
    {
      this->str[i] = one[i];
    }
    for (k = 0; k < sLen; k++, i++)
    {
      this->str[i] = s[k];
    }
    for (k = 0; k < lenTwo - 1; k++, i++)
    {
      this->str[i] = two[k];
    }
    this->str[i] = '\0';
    return *this;
  }
  template <class InputIterator>
  void insert(iterator p, InputIterator first, InputIterator last);
  size_t copy(char *s, size_t n, size_t pos = 0) const;
  const char *data() const;

  basic_string<CharT, Traits, Alloc> substr(size_t pos, size_t n)
  {
  __ESBMC_HIDE:
    __ESBMC_assert(pos >= 0, "The first parameter must be greater than zero");
    __ESBMC_assert(n >= 0, "The second parameter must be greater than zero");
    int len = this->length();
    __ESBMC_assert((pos < len) && ((pos + n) <= len), "basic_string overflow");
    int i, k;
    int lenOne = n + 1;
    char *one = new char[lenOne];
    for (k = 0, i = pos; i < (pos + n); k++, i++)
    {
      one[k] = this->str[i];
    }
    one[k] = '\0';
    basic_string<CharT, Traits, Alloc> tmp(one);
    delete[] one; // Freeing dynamically allocated memory
    return tmp;
  }

  basic_string<CharT, Traits, Alloc> substr(size_t pos) const
  {
  __ESBMC_HIDE:
    __ESBMC_assert(pos >= 0, "The first parameter must be greater than zero");
    int i, k;
    int len = this->length();
    __ESBMC_assert(pos < len, "basic_string overflow");
    int lenOne = len + 1;
    char *one = new char[lenOne];
    for (k = 0, i = pos; i < len; k++, i++)
    {
      one[k] = this->str[i];
    }
    one[k] = '\0';
    basic_string<CharT, Traits, Alloc> tmp(one);
    delete[] one; // Freeing dynamically allocated memory
    return tmp;
  }

  basic_string<CharT, Traits, Alloc>::iterator begin() const
  {
    return basic_string<CharT, Traits, Alloc>::iterator(this->str);
  }

  basic_string<CharT, Traits, Alloc>::iterator end() const
  {
    basic_string<CharT, Traits, Alloc>::iterator end(this->str);
    end.pos = this->length() - 1;
    return end;
  }
  template <class T>
  basic_string<CharT, Traits, Alloc> &assign(T first, T last)
  {
    __ESBMC_assert(
      first != NULL, "The first parameter must be different than NULL");
    __ESBMC_assert(
      last != NULL, "The second parameter must be different than NULL");
    __ESBMC_assert(first >= 0, "The first parameter must be greater than zero");
    __ESBMC_assert(last >= 0, "The second parameter must be greater than zero");
    int i;
    this->_size = first;
    this->str = new char[first + 1];
    for (i = 0; i < first; i++)
    {
      this->str[i] = last;
    }
    this->str[i] = '\0';
    return *this;
  }

  template <class InputIterator>
  basic_string<CharT, Traits, Alloc> &
  append(InputIterator first, InputIterator last)
  {
    __ESBMC_assert(first >= 0, "The first parameter must be greater than zero");
    __ESBMC_assert(last >= 0, "The second parameter must be greater than zero");
    int rhsLen = first;
    char c = last;
    int totalLen = this->_size + rhsLen;
    basic_string<CharT, Traits, Alloc> temp(totalLen);
    int i, j;
    for (i = 0; i < this->_size; i++)
      temp.str[i] = this->str[i];
    for (j = i; j < totalLen; j++)
      temp.str[j] = c;
    temp.str[totalLen] = '\0';
    *this = temp;
    return *this;
  }

private:
};

typedef basic_string<char> string;
} // namespace std

namespace std
{
template <typename CharT, typename Traits, typename Alloc>
basic_string<CharT, Traits, Alloc>::basic_string()
{
  str = new char[1];
  str[0] =
    '\0'; // Assign the null terminator to represent an empty basic_string
  _size = 0;
}

template <typename CharT, typename Traits, typename Alloc>
basic_string<CharT, Traits, Alloc>::basic_string(const CharT *s)
{
__ESBMC_HIDE:
  __ESBMC_assert(s != NULL, "basic_string<CharT, Traits, Alloc> invalid");
  _size = strlen(s);
  str = new char[_size + 1];

  strcpy(str, s);
}

template <typename CharT, typename Traits, typename Alloc>
basic_string<CharT, Traits, Alloc>::basic_string(const CharT *s, size_t n)
{
__ESBMC_HIDE:
  __ESBMC_assert(n < strlen(s), "basic_string overflow");
  __ESBMC_assert(s != NULL, "invalid basic_string");

  int i;
  str = new char[n + 1];
  _size = n;
  for (i = 0; (i < _size) && (s[i] != '\0'); i++)
    str[i] = s[i];
  str[i] = '\0';
}

template <typename CharT, typename Traits, typename Alloc>
basic_string<CharT, Traits, Alloc>::basic_string(
  basic_string<CharT, Traits, Alloc> &s,
  size_t n)
{
__ESBMC_HIDE:
  __ESBMC_assert(n < s.length(), "basic_string overflow");
  __ESBMC_assert(s.str != NULL, "invalid basic_string");
  int i, j;

  // Avoid allocating a negative amount.
  int sz = s._size - n + 1;
  if (sz < 0)
    sz = 0;
  this->str = new char[sz];
  this->_size = s._size - n;
  for (i = n, j = 0; s.str[i] != '\0'; i++, j++)
    this->str[j] = s.str[i];
  str[j] = '\0';
}

template <typename CharT, typename Traits, typename Alloc>
basic_string<CharT, Traits, Alloc>::basic_string(int len)
{
  __ESBMC_assert(len >= 0, "the parameter must be greater or equal than zero");
  str = new char[len + 1];
  _size = len;
}

template <typename CharT, typename Traits, typename Alloc>
basic_string<CharT, Traits, Alloc>::basic_string(char c, size_t n)
{
  __ESBMC_assert(n > 0, "the second parameter must be different than zero");
  str = new char[n + 1];
  for (int i = 0; i < n; i++)
    str[i] = c;
  str[n] = '\0';
  _size = n;
}

template <typename CharT, typename Traits, typename Alloc>
char *basic_string<CharT, Traits, Alloc>::c_str() const
{
__ESBMC_HIDE:
  return str;
}

template <typename CharT, typename Traits, typename Alloc>
inline ostream &operator<<(ostream &o, basic_string<CharT, Traits, Alloc>)
{
  return o;
}

template <typename CharT, typename Traits, typename Alloc>
inline ostream &
operator<<(ostream &o, typename basic_string<CharT, Traits, Alloc>::iterator &)
{
  return o;
}

template <typename CharT, typename Traits, typename Alloc>
inline istream &operator>>(istream &is, basic_string<CharT, Traits, Alloc>)
{
  return is;
}

template <typename CharT, typename Traits, typename Alloc>
bool basic_string<CharT, Traits, Alloc>::operator>(
  basic_string<CharT, Traits, Alloc> &a)
{
__ESBMC_HIDE:
  __ESBMC_assert(a.str != NULL, "The parameter must be different than NULL");
  int i;
  for (i = 0; (this->str[i] != '\0') && (a.str[i] != '\0'); i++)
  {
    if (this->str[i] > a.str[i])
      return true;
  }
  return false;
}

template <typename CharT, typename Traits, typename Alloc>
bool basic_string<CharT, Traits, Alloc>::operator>(const char *a)
{
__ESBMC_HIDE:
  __ESBMC_assert(a != NULL, "The parameter must be different than NULL");
  int i;
  for (i = 0; (this->str[i] != '\0') && (a[i] != '\0'); i++)
  {
    if (this->str[i] > a[i])
      return true;
  }
  return false;
}

template <typename CharT, typename Traits, typename Alloc>
bool operator>(
  const basic_string<CharT, Traits, Alloc> &lhs,
  const basic_string<CharT, Traits, Alloc> &rhs)
{
__ESBMC_HIDE:
  __ESBMC_assert(
    lhs.str != NULL, "The first parameter must be different than NULL");
  __ESBMC_assert(
    rhs.str != NULL, "The second parameter must be different than NULL");
  int i;
  for (i = 0; (lhs.str[i] != '\0') && (rhs.str[i] != '\0'); i++)
  {
    if (lhs.str[i] > rhs.str[i])
      return true;
  }
  return false;
}

template <typename CharT, typename Traits, typename Alloc>
bool operator<(
  const basic_string<CharT, Traits, Alloc> &lhs,
  const basic_string<CharT, Traits, Alloc> &rhs)
{
__ESBMC_HIDE:
  __ESBMC_assert(
    lhs.str != NULL, "The first parameter must be different than NULL");
  __ESBMC_assert(
    rhs.str != NULL, "The second parameter must be different than NULL");
  int i;
  for (i = 0; (lhs.str[i] != '\0') && (rhs.str[i] != '\0'); i++)
  {
    if (lhs.str[i] < rhs.str[i])
      return true;
  }
  return false;
}

template <typename CharT, typename Traits, typename Alloc>
bool operator>(const char *lhs, basic_string<CharT, Traits, Alloc> &rhs)
{
__ESBMC_HIDE:
  __ESBMC_assert(
    lhs != NULL, "The first parameter must be different than NULL");
  __ESBMC_assert(
    rhs.str != NULL, "The second parameter must be different than NULL");
  int i;
  for (i = 0; (lhs[i] != '\0') && (rhs.str[i] != '\0'); i++)
  {
    if (lhs[i] > rhs.str[i])
      return true;
  }
  return false;
}

template <typename CharT, typename Traits, typename Alloc>
bool operator>(basic_string<CharT, Traits, Alloc> &lhs, const char *rhs)
{
__ESBMC_HIDE:
  __ESBMC_assert(
    lhs.str != NULL, "The first parameter must be different than NULL");
  __ESBMC_assert(
    rhs != NULL, "The second parameter must be different than NULL");
  int i;
  for (i = 0; (lhs.str[i] != '\0') && (rhs[i] != '\0'); i++)
  {
    if (lhs.str[i] > rhs[i])
      return true;
  }
  return false;
}

template <typename CharT, typename Traits, typename Alloc>
bool basic_string<CharT, Traits, Alloc>::operator<(
  basic_string<CharT, Traits, Alloc> &a)
{
__ESBMC_HIDE:
  __ESBMC_assert(a.str != NULL, "The parameter must be different than NULL");
  int i;
  for (i = 0; (this->str[i] != '\0') && (a.str[i] != '\0'); i++)
  {
    if (this->str[i] < a.str[i])
      return true;
  }
  return false;
}

template <typename CharT, typename Traits, typename Alloc>
bool basic_string<CharT, Traits, Alloc>::operator<(const char *a)
{
__ESBMC_HIDE:
  __ESBMC_assert(a != NULL, "The parameter must be different than NULL");
  int i;
  for (i = 0; (this->str[i] != '\0') && (a[i] != '\0'); i++)
  {
    if (this->str[i] < a[i])
      return true;
  }
  return false;
}

template <typename CharT, typename Traits, typename Alloc>
bool operator<(const char *lhs, basic_string<CharT, Traits, Alloc> &rhs)
{
__ESBMC_HIDE:
  __ESBMC_assert(
    lhs != NULL, "The first parameter must be different than NULL");
  __ESBMC_assert(
    rhs.str != NULL, "The second parameter must be different than NULL");
  int i;
  for (i = 0; (lhs[i] != '\0') && (rhs.str[i] != '\0'); i++)
  {
    if (lhs[i] < rhs.str[i])
      return true;
  }
  return false;
}

template <typename CharT, typename Traits, typename Alloc>
bool operator<(basic_string<CharT, Traits, Alloc> &lhs, const char *rhs)
{
__ESBMC_HIDE:
  __ESBMC_assert(
    lhs.str != NULL, "The first parameter must be different than NULL");
  __ESBMC_assert(
    rhs != NULL, "The second parameter must be different than NULL");
  int i;
  for (i = 0; (lhs.str[i] != '\0') && (rhs[i] != '\0'); i++)
  {
    if (lhs.str[i] < rhs[i])
      return true;
  }
  return false;
}

template <typename CharT, typename Traits, typename Alloc>
bool basic_string<CharT, Traits, Alloc>::operator>=(
  basic_string<CharT, Traits, Alloc> &a)
{
__ESBMC_HIDE:
  __ESBMC_assert(a.str != NULL, "The parameter must be different than NULL");
  int tmp = strcmp(this->str, a.str);
  if (tmp > 0 || tmp == 0)
  {
    return true;
  }
  else
  {
    return false;
  }
}

template <typename CharT, typename Traits, typename Alloc>
bool basic_string<CharT, Traits, Alloc>::operator>=(const char *lhs)
{
__ESBMC_HIDE:
  __ESBMC_assert(lhs != NULL, "The parameter must be different than NULL");
  int tmp = strcmp(this->str, lhs);
  if (tmp > 0 || tmp == 0)
  {
    return true;
  }
  else
  {
    return false;
  }
}

template <typename CharT, typename Traits, typename Alloc>
bool basic_string<CharT, Traits, Alloc>::operator<=(
  basic_string<CharT, Traits, Alloc> &a)
{
__ESBMC_HIDE:
  __ESBMC_assert(a.str != NULL, "The parameter must be different than NULL");
  int tmp = strcmp(this->str, a.str);
  if (tmp < 0 || tmp == 0)
  {
    return true;
  }
  else
  {
    return false;
  }
}

template <typename CharT, typename Traits, typename Alloc>
bool basic_string<CharT, Traits, Alloc>::operator<=(const char *lhs)
{
__ESBMC_HIDE:
  __ESBMC_assert(lhs != NULL, "The parameter must be different than NULL");
  int tmp = strcmp(this->str, lhs);
  if (tmp < 0 || tmp == 0)
  {
    return true;
  }
  else
  {
    return false;
  }
}

template <typename CharT, typename Traits, typename Alloc>
size_t basic_string<CharT, Traits, Alloc>::length() const
{
  return this->_size;
}

template <typename CharT, typename Traits, typename Alloc>
char &basic_string<CharT, Traits, Alloc>::operator[](size_t pos)
{
  __ESBMC_assert(
    (pos >= 0) && (pos < this->_size), "Error! Invalid access memory area");
  if (pos > this->_size)
    return this->str[this->_size - 1];
  else
    return this->str[pos];
}

template <typename CharT, typename Traits, typename Alloc>
char basic_string<CharT, Traits, Alloc>::at(size_t pos) const
{
  if (pos >= this->length())
  {
    // TODO: when we support try-catch, replace the assert with the throw statement below
    //throw out_of_range();
    __ESBMC_assert(0, "basic_string append failed, out_of_range");
  }

  return this->str[pos];
}

template <typename CharT, typename Traits, typename Alloc>
char basic_string<CharT, Traits, Alloc>::front() const
{
  __ESBMC_assert(
    this->length() > 0, "basic_string::front() failed: basic_string is empty");

  return this->str[0];
}

template <typename CharT, typename Traits, typename Alloc>
char basic_string<CharT, Traits, Alloc>::back() const
{
  __ESBMC_assert(
    this->length() > 0, "basic_string::back() failed: basic_string is empty");

  return this->str[this->length() - 1];
}

template <typename CharT, typename Traits, typename Alloc>
bool basic_string<CharT, Traits, Alloc>::empty() const
{
  if (this->_size == 0)
    return true;
  return false;
}

template <typename CharT, typename Traits, typename Alloc>
basic_string<CharT, Traits, Alloc> &
basic_string<CharT, Traits, Alloc>::operator=(
  const basic_string<CharT, Traits, Alloc> &str)
{
__ESBMC_HIDE:
  this->_size = str.length();
  this->str = new char[this->_size + 1];
  strcpy(this->str, str.str);
  return *this;
}

template <typename CharT, typename Traits, typename Alloc>
basic_string<CharT, Traits, Alloc> &
basic_string<CharT, Traits, Alloc>::operator=(
  basic_string<CharT, Traits, Alloc> &str)
{
__ESBMC_HIDE:
  if (this == &str)
    return *this;
  this->_size = str.length();
  this->str = new char[this->_size + 1];
  strcpy(this->str, str.str);
  return *this;
}

template <typename CharT, typename Traits, typename Alloc>
basic_string<CharT, Traits, Alloc> &
basic_string<CharT, Traits, Alloc>::operator=(const char *s)
{
__ESBMC_HIDE:
  __ESBMC_assert(s != NULL, "The parameter must be different than NULL");
  this->_size = strlen(s);
  this->str = new char[this->_size + 1];
  strcpy(this->str, s); // Copy the contents of s to str
  return *this; // Return a reference to the modified basic_string object
}

template <typename CharT, typename Traits, typename Alloc>
basic_string<CharT, Traits, Alloc> &
basic_string<CharT, Traits, Alloc>::operator=(char s)
{
__ESBMC_HIDE:
  this->_size = 1;
  this->str = new char[this->_size + 1];
  this->str[0] = s;
  this->str[1] = '\0';
  return *this;
}

template <typename CharT, typename Traits, typename Alloc>
basic_string<CharT, Traits, Alloc> &
basic_string<CharT, Traits, Alloc>::operator+=(
  const basic_string<CharT, Traits, Alloc> &s)
{
__ESBMC_HIDE:
  __ESBMC_assert(s.str != NULL, "The parameter must be different than NULL");
  int rhsLen = s._size;
  int lhsLen = this->_size;
  int totalLen = lhsLen + rhsLen;
  char temp[totalLen + 1];
  int i, j, k;
  for (i = 0; i < lhsLen; i++)
    temp[i] = this->str[i];
  temp[i] = '\0';
  for (j = i, k = 0; j < totalLen; j++, k++)
    temp[j] = s.str[k];
  temp[j] = '\0';
  this->str = new char[totalLen + 1];
  this->_size = totalLen;
  strcpy(this->str, temp);
  return *this;
}

template <typename CharT, typename Traits, typename Alloc>
basic_string<CharT, Traits, Alloc> &
basic_string<CharT, Traits, Alloc>::operator+=(const char *s)
{
__ESBMC_HIDE:
  __ESBMC_assert(s != NULL, "The parameter must be different than NULL");
  int rhsLen = strlen(s);
  int lhsLen = this->_size;
  int totalLen = lhsLen + rhsLen;
  char temp[totalLen + 1];
  int i, j, k;
  for (i = 0; i < lhsLen; i++)
    temp[i] = this->str[i];
  temp[i] = '\0';
  for (j = i, k = 0; j < totalLen; j++, k++)
    temp[j] = s[k];
  temp[j] = '\0';
  this->str = new char[totalLen + 1];
  this->_size = totalLen;
  strcpy(this->str, temp);
  return *this;
}

template <typename CharT, typename Traits, typename Alloc>
basic_string<CharT, Traits, Alloc> &
basic_string<CharT, Traits, Alloc>::operator+=(char s)
{
__ESBMC_HIDE:
  int totalLen = this->_size + 1;
  char temp[totalLen + 1];
  int i = 0;
  if (this->_size != 0)
  {
    for (i = 0; i < this->_size; i++)
    {
      temp[i] = this->str[i];
    }
  }
  temp[i] = s;
  i++;
  temp[i] = '\0';
  this->str = new char[totalLen + 1];
  this->_size = totalLen;
  strcpy(this->str, temp);
  return *this;
}

template <typename CharT, typename Traits, typename Alloc>
void basic_string<CharT, Traits, Alloc>::swap(
  basic_string<CharT, Traits, Alloc> &s)
{
__ESBMC_HIDE:
  __ESBMC_assert(s.str != NULL, "The parameter must be different than NULL");
  basic_string<CharT, Traits, Alloc> aux(s.str);
  s.str = this->str;
  s._size = this->_size;
  this->str = aux.str;
  this->_size = aux._size;
}

template <typename CharT, typename Traits, typename Alloc>
size_t basic_string<CharT, Traits, Alloc>::capacity() const
{
  return this->_size;
}

template <typename CharT, typename Traits, typename Alloc>
size_t basic_string<CharT, Traits, Alloc>::max_size() const
{
  int nondet;
  return nondet;
}

template <typename CharT, typename Traits, typename Alloc>
int basic_string<CharT, Traits, Alloc>::size() const
{
  return this->_size;
}

template <typename CharT, typename Traits, typename Alloc>
void basic_string<CharT, Traits, Alloc>::resize(size_t n)
{
__ESBMC_HIDE:
  __ESBMC_assert(n > 0, "The parameter must be greater than zero");
  int num = this->_size, i;
  char *tmp = new char[n + 1];
  for (i = 0; i < n; i++)
  {
    tmp[i] = this->str[i];
  }
  tmp[i] = '\0';
  this->_size = n;
  this->str = new char[n + 1];
  for (i = 0; i < n; i++)
    this->str[i] = tmp[i];
  this->str[i] = '\0';
}

template <typename CharT, typename Traits, typename Alloc>
void basic_string<CharT, Traits, Alloc>::resize(size_t n, char c)
{
__ESBMC_HIDE:
  __ESBMC_assert(n > 0, "The parameter must be greater than zero");
  int num, i;
  num = this->length();
  basic_string<CharT, Traits, Alloc> tmp(this->str);
  this->_size = n;
  this->str = new char[n + 1];
  for (i = 0; i < num; i++)
    this->str[i] = tmp.str[i];
  for (i = num; i < (this->_size); i++)
    this->str[i] = c;
  this->str[i] = '\0';
}

template <typename CharT, typename Traits, typename Alloc>
basic_string<CharT, Traits, Alloc> &basic_string<CharT, Traits, Alloc>::assign(
  basic_string<CharT, Traits, Alloc> &s)
{
__ESBMC_HIDE:
  __ESBMC_assert(s.str != NULL, "The parameter must be different than NULL");
  *this = s;
  return *this;
}

template <typename CharT, typename Traits, typename Alloc>
basic_string<CharT, Traits, Alloc> &basic_string<CharT, Traits, Alloc>::assign(
  basic_string<CharT, Traits, Alloc> &s,
  size_t pos,
  size_t n)
{
__ESBMC_HIDE:
  __ESBMC_assert(
    (pos >= 0) && (pos < s.length()) && ((pos + n) < s.length()) && (n > 0),
    "basic_string overflow");
  __ESBMC_assert(s.str != NULL, "The parameter must be different than NULL");
  this->_size = (n);
  this->str = new char[this->_size + 1];
  strncpy(this->str, s.str + pos, n);
  return *this;
}

template <typename CharT, typename Traits, typename Alloc>
basic_string<CharT, Traits, Alloc> &
basic_string<CharT, Traits, Alloc>::assign(const char *s, size_t n)
{
__ESBMC_HIDE:
  __ESBMC_assert((n < strlen(s)) && (n >= 0), "basic_string overflow");
  __ESBMC_assert(s != NULL, "The parameter must be different than NULL");
  this->_size = (n);
  this->str = new char[this->_size];
  strncpy(this->str, s, n);
  return *this;
}

template <typename CharT, typename Traits, typename Alloc>
basic_string<CharT, Traits, Alloc> &
basic_string<CharT, Traits, Alloc>::assign(const char *s)
{
__ESBMC_HIDE:
  __ESBMC_assert(s != NULL, "The parameter must be different than NULL");
  *this = s;
  return *this;
}

template <typename CharT, typename Traits, typename Alloc>
basic_string<CharT, Traits, Alloc> &
basic_string<CharT, Traits, Alloc>::assign(size_t n, char c)
{
__ESBMC_HIDE:
  __ESBMC_assert(n > 0, "basic_string overflow");
  int i;
  this->_size = n;
  this->str = new char[n + 1];
  for (i = 0; i < n; i++)
  {
    this->str[i] = c;
  }
  this->str[i] = '\0';
  return *this;
}

template <typename CharT, typename Traits, typename Alloc>
size_t
basic_string<CharT, Traits, Alloc>::copy(char *s, size_t n, size_t pos) const
{
__ESBMC_HIDE:
  __ESBMC_assert(pos >= 0, "basic_string overflow");
  __ESBMC_assert(pos < this->length(), "basic_string overflow");
  __ESBMC_assert(n <= this->length(), "basic_string overflow");
  __ESBMC_assert(n > 0, "basic_string overflow");
  __ESBMC_assert(s != NULL, "The parameter must be different than NULL");
  size_t aux = n + pos;
  if (pos > this->size())
  {
    // TODO: when we support try-catch, replace the assert with the throw statement below
    //throw out_of_range();
    __ESBMC_assert(0, "basic_string append failed, out_of_range");
  }
  if (s == NULL)
  {
    s = new char[n];
  }
  strncpy(s, this->c_str() + pos, aux);
  return n;
}

template <typename CharT, typename Traits, typename Alloc>
const char *basic_string<CharT, Traits, Alloc>::data() const
{
  return this->str;
}

template <typename CharT, typename Traits, typename Alloc>
basic_string<CharT, Traits, Alloc> &basic_string<CharT, Traits, Alloc>::append(
  basic_string<CharT, Traits, Alloc> &s)
{
__ESBMC_HIDE:
  __ESBMC_assert(s.str != NULL, "The parameter must be different than NULL");
  *this += s;
  return *this;
}

template <typename CharT, typename Traits, typename Alloc>
basic_string<CharT, Traits, Alloc> &
basic_string<CharT, Traits, Alloc>::append(const char *s, size_t n)
{
__ESBMC_HIDE:
  __ESBMC_assert(n >= 0, "basic_string overflow");
  __ESBMC_assert(s != NULL, "The parameter must be different than NULL");
  if (n > 1)
    if (n > strlen(s))
    {
      // TODO: when we support try-catch, replace the assert with the throw statement below
      //throw out_of_range();
      __ESBMC_assert(0, "basic_string append failed, out_of_range");
    }

  int rhsLen = n;
  int totalLen = this->_size + rhsLen;
  basic_string<CharT, Traits, Alloc> temp(totalLen);
  int i, j, k;
  for (i = 0; i < this->_size; i++)
    temp.str[i] = this->str[i];
  for (j = i, k = 0; j < totalLen; j++, k++)
    temp.str[j] = s[k];
  temp.str[totalLen] = '\0';
  *this = temp;
  return *this;
}

template <typename CharT, typename Traits, typename Alloc>
basic_string<CharT, Traits, Alloc> &basic_string<CharT, Traits, Alloc>::append(
  basic_string<CharT, Traits, Alloc> &s,
  size_t pos,
  size_t n)
{
__ESBMC_HIDE:
  __ESBMC_assert(pos >= 0, "basic_string overflow");
  __ESBMC_assert(pos < s.length(), "basic_string overflow");
  __ESBMC_assert(n <= s.length(), "basic_string overflow");
  __ESBMC_assert(n > 0, "basic_string overflow");
  __ESBMC_assert(s.str != NULL, "The parameter must be different than NULL");
  if ((pos > s._size) || (n > (s._size - pos)))
  {
    // TODO: when we support try-catch, replace the assert with the throw statement below
    //throw out_of_range();
    __ESBMC_assert(0, "basic_string append failed, out_of_range");
  }

  int rhsLen = n;
  int totalLen = this->_size + rhsLen;
  basic_string<CharT, Traits, Alloc> temp(totalLen);
  int i, j, k;
  for (i = 0; i < this->_size; i++)
    temp.str[i] = this->str[i];
  for (j = i, k = pos; j < totalLen; j++, k++)
    temp.str[j] = s.str[k];
  temp.str[totalLen] = '\0';
  *this = temp;
  return *this;
}

template <typename CharT, typename Traits, typename Alloc>
basic_string<CharT, Traits, Alloc> &
basic_string<CharT, Traits, Alloc>::append(const char *s)
{
__ESBMC_HIDE:
  __ESBMC_assert(s != NULL, "The parameter must be different than NULL");
  int rhsLen = strlen(s);
  int totalLen = this->_size + rhsLen;
  basic_string<CharT, Traits, Alloc> temp(totalLen);
  int i, j, k;
  for (i = 0; i < this->_size; i++)
    temp.str[i] = this->str[i];
  for (j = i, k = 0; j < totalLen; j++, k++)
    temp.str[j] = s[k];
  temp.str[totalLen] = '\0';
  *this = temp;
  return *this;
}

template <typename CharT, typename Traits, typename Alloc>
basic_string<CharT, Traits, Alloc> &
basic_string<CharT, Traits, Alloc>::append(size_t n, char c)
{
__ESBMC_HIDE:
  __ESBMC_assert(n > 0, "basic_string overflow");
  int rhsLen = n;
  int totalLen = this->_size + rhsLen;
  char *temp = new char[totalLen + 1];
  int i, j, k;

  for (i = 0; i < this->_size; i++)
    temp[i] = this->str[i];

  for (k = 0; i < totalLen; i++, k++)
    temp[i] = c;
  temp[i] = '\0';

  basic_string<CharT, Traits, Alloc> tmp(temp);
  *this = tmp;
  return *this;
}

template <typename CharT, typename Traits, typename Alloc>
size_t basic_string<CharT, Traits, Alloc>::find(char c, size_t pos) const
{
__ESBMC_HIDE:
  __ESBMC_assert(pos < this->length(), "basic_string overflow");

  for (size_t i = pos; i < this->length(); i++)
    if (this->str[i] == c)
      return i; // Return the index if character found

  return npos; // Return npos if character not found
}

template <typename CharT, typename Traits, typename Alloc>
size_t basic_string<CharT, Traits, Alloc>::find(
  basic_string<CharT, Traits, Alloc> &s,
  size_t pos) const
{
__ESBMC_HIDE:
  __ESBMC_assert((pos >= 0) && (pos < this->length()), "basic_string overflow");
  __ESBMC_assert(s.str != NULL, "The parameter must be different than NULL");
  int len = this->length();
  int lim = pos;
  char *s1 = new char[len + 1];
  strcpy(s1, this->str);
  int slen = s.length();
  char *s2 = new char[slen + 1];
  strcpy(s2, s.str);
  pos = -1;
  size_t i, j;

  for (i = lim; i < len; i++)
  {
    for (j = 0; (j < slen) && ((i + j) < len); j++)
    {
      if (s1[i + j] != s2[j])
      {
        break;
      }
      else
      {
        if (pos == -1)
        {
          pos = i + j;
        }
      }
    }
    if (s2[j] == '\0')
    {
      return pos;
    }
  }

  return -1;
}

template <typename CharT, typename Traits, typename Alloc>
size_t
basic_string<CharT, Traits, Alloc>::find(const char *s, size_t pos, size_t n)
  const
{
__ESBMC_HIDE:
  __ESBMC_assert(
    (pos >= 0) && (pos < this->length()) && ((pos + n) < this->length()) &&
      (n > 0),
    "basic_string overflow");
  __ESBMC_assert(s != NULL, "The parameter must be different than NULL");
  size_t i, j;

  int len = this->length();
  int lim = pos;
  char *s1 = new char[len + 1];
  strcpy(s1, this->str);

  int slen = n;
  char *s2 = new char[slen + 1];
  for (i = 0; i < slen; i++)
  {
    s2[i] = s[i];
  }
  s2[i] = '\0';

  pos = -1;

  for (i = lim; i < len; i++)
  {
    for (j = 0; (j < slen) && ((i + j) < len); j++)
    {
      if (s1[i + j] != s2[j])
      {
        break;
      }
      else
      {
        if (pos == -1)
        {
          pos = i + j;
        }
      }
    }
    if (s2[j] == '\0')
    {
      return pos;
    }
  }

  return -1;
}

template <typename CharT, typename Traits, typename Alloc>
size_t basic_string<CharT, Traits, Alloc>::find(const char *s, size_t pos) const
{
__ESBMC_HIDE:
  __ESBMC_assert((pos >= 0) && (pos < this->length()), "basic_string overflow");
  __ESBMC_assert(s != NULL, "The parameter must be different than NULL");
  int len = this->length();
  int lim = pos;
  char *s1 = new char[len + 1];
  strcpy(s1, this->str);
  int slen = strlen(s);
  char *s2 = new char[slen + 1];
  strcpy(s2, s);
  pos = -1;
  size_t i, j;

  for (i = lim; i < len; i++)
  {
    for (j = 0; (j < slen) && ((i + j) < len); j++)
    {
      if (s1[i + j] != s2[j])
      {
        break;
      }
      else
      {
        if (pos == -1)
        {
          pos = i + j;
        }
      }
    }
    if (s2[j] == '\0')
    {
      return pos;
    }
  }

  return -1;
}

template <typename CharT, typename Traits, typename Alloc>
basic_string<CharT, Traits, Alloc> &basic_string<CharT, Traits, Alloc>::insert(
  size_t pos1,
  basic_string<CharT, Traits, Alloc> &s)
{
__ESBMC_HIDE:
  int len = this->length(), i, k;
  __ESBMC_assert((pos1 >= 0) && (pos1 < len), "basic_string overflow");
  __ESBMC_assert(s.str != NULL, "The parameter must be different than NULL");
  int lenOne = pos1 + 1;
  char *one = new char[lenOne];
  for (i = 0; i < pos1; i++)
  {
    one[i] = this->str[i];
  }
  int lenTwo = (len - pos1) + 1;
  char *two = new char[lenTwo];
  for (k = 0, i = pos1; i < len; i++, k++)
  {
    two[k] = this->str[i];
  }
  int totalLen = s.length() + len;
  this->str = new char[totalLen + 1];
  this->_size = totalLen;

  for (i = 0; i < lenOne - 1; i++)
  {
    this->str[i] = one[i];
  }
  for (k = 0; k < s.length(); k++, i++)
  {
    this->str[i] = s.str[k];
  }
  for (k = 0; k < lenTwo - 1; k++, i++)
  {
    this->str[i] = two[k];
  }
  this->str[i] = '\0';
  return *this;
}

template <typename CharT, typename Traits, typename Alloc>
basic_string<CharT, Traits, Alloc> &basic_string<CharT, Traits, Alloc>::insert(
  size_t pos1,
  basic_string<CharT, Traits, Alloc> &s,
  size_t pos2,
  size_t n)
{
__ESBMC_HIDE:
  int len = this->length(), i, k;
  int sLen = s.length();
  __ESBMC_assert((pos1 >= 0) && (pos1 < len), "basic_string overflow");
  __ESBMC_assert(
    (pos2 >= 0) && (pos2 < s.length()) && ((pos2 + n) < sLen) && (n > 0),
    "basic_string overflow");
  __ESBMC_assert(s.str != NULL, "The parameter must be different than NULL");
  int lim = n + pos2;
  int lenOne = pos1 + 1;
  char *one = new char[lenOne];
  for (i = 0; i < pos1; i++)
  {
    one[i] = this->str[i];
  }
  int lenTwo = (len - pos1) + 1;
  char *two = new char[lenTwo];
  for (k = 0, i = pos1; i < len; i++, k++)
  {
    two[k] = this->str[i];
  }
  int totalLen = n + len;
  this->str = new char[totalLen + 1];
  this->_size = totalLen;

  for (i = 0; i < lenOne - 1; i++)
  {
    this->str[i] = one[i];
  }
  for (k = pos2; k < lim; k++, i++)
  {
    this->str[i] = s.str[k];
  }
  for (k = 0; k < lenTwo - 1; k++, i++)
  {
    this->str[i] = two[k];
  }
  this->str[i] = '\0';
  return *this;
}

template <typename CharT, typename Traits, typename Alloc>
basic_string<CharT, Traits, Alloc> &
basic_string<CharT, Traits, Alloc>::insert(size_t pos1, const char *s, size_t n)
{
__ESBMC_HIDE:
  int len = this->length(), i, k;
  int lim = n;
  int sLen = strlen(s);
  __ESBMC_assert((pos1 >= 0) && (pos1 < len), "basic_string overflow");
  __ESBMC_assert(n > 0, "basic_string overflow");
  __ESBMC_assert(s != NULL, "The parameter must be different than NULL");
  __ESBMC_assert(lim < sLen, "basic_string overflow");
  int lenOne = pos1 + 1;
  char *one = new char[lenOne];
  for (i = 0; i < pos1; i++)
  {
    one[i] = this->str[i];
  }
  int lenTwo = (len - pos1) + 1;
  char *two = new char[lenTwo];
  for (k = 0, i = pos1; i < len; i++, k++)
  {
    two[k] = this->str[i];
  }
  int totalLen = n + len;
  this->str = new char[totalLen + 1];
  this->_size = totalLen;

  for (i = 0; i < lenOne - 1; i++)
  {
    this->str[i] = one[i];
  }
  for (k = 0; k < lim; k++, i++)
  {
    this->str[i] = s[k];
  }
  for (k = 0; k < lenTwo - 1; k++, i++)
  {
    this->str[i] = two[k];
  }
  this->str[i] = '\0';
  return *this;
}

template <typename CharT, typename Traits, typename Alloc>
basic_string<CharT, Traits, Alloc> &
basic_string<CharT, Traits, Alloc>::insert(size_t pos1, const char *s)
{
__ESBMC_HIDE:
  int len = this->length(), i, k;
  __ESBMC_assert(pos1 >= 0, "basic_string overflow");
  __ESBMC_assert(s != NULL, "The parameter must be different than NULL");
  int sLen = strlen(s);
  int lenOne = pos1 + 1;
  char *one = new char[lenOne];
  for (i = 0; i < pos1; i++)
  {
    one[i] = this->str[i];
  }
  int lenTwo = (len - pos1) + 1;
  char *two = new char[lenTwo];
  for (k = 0, i = pos1; i < len; i++, k++)
  {
    two[k] = this->str[i];
  }
  int totalLen = len + strlen(s);
  this->str = new char[totalLen + 1];
  this->_size = totalLen;

  for (i = 0; i < lenOne - 1; i++)
  {
    this->str[i] = one[i];
  }
  for (k = 0; k < sLen; k++, i++)
  {
    this->str[i] = s[k];
  }
  for (k = 0; k < lenTwo - 1; k++, i++)
  {
    this->str[i] = two[k];
  }
  this->str[i] = '\0';
  return *this;
}

template <typename CharT, typename Traits, typename Alloc>
basic_string<CharT, Traits, Alloc> &
basic_string<CharT, Traits, Alloc>::insert(size_t pos1, size_t n, char c)
{
__ESBMC_HIDE:
  int len = this->length(), i, k;
  int sLen = n;
  __ESBMC_assert(
    (pos1 >= 0) && (pos1 < len) && ((pos1 + n) < len) && (n > 0),
    "basic_string overflow");
  char *s = new char[n + 1];
  for (i = 0; i < n; i++)
  {
    s[i] = c;
  }
  int lenOne = pos1 + 1;
  char *one = new char[lenOne];
  for (i = 0; i < pos1; i++)
  {
    one[i] = this->str[i];
  }
  int lenTwo = (len - pos1) + 1;
  char *two = new char[lenTwo];
  for (k = 0, i = pos1; i < len; i++, k++)
  {
    two[k] = this->str[i];
  }
  int totalLen = len + n;
  this->str = new char[totalLen + 1];
  this->_size = totalLen;

  for (i = 0; i < lenOne - 1; i++)
  {
    this->str[i] = one[i];
  }
  for (k = 0; k < sLen; k++, i++)
  {
    this->str[i] = s[k];
  }
  for (k = 0; k < lenTwo - 1; k++, i++)
  {
    this->str[i] = two[k];
  }
  this->str[i] = '\0';
  return *this;
}

template <typename CharT, typename Traits, typename Alloc>
basic_string<CharT, Traits, Alloc> &
basic_string<CharT, Traits, Alloc>::erase(size_t pos, size_t n)
{
__ESBMC_HIDE:
  __ESBMC_assert(
    (pos < this->length()) && ((pos + n) <= this->length()), "overflow");
  int i, k, len = this->length();
  int lenOne = pos + 1;
  char *one = new char[lenOne];
  for (i = 0; i < pos; i++)
  {
    one[i] = this->str[i];
  }
  int lenTwo = (len - (pos + n)) + 1;
  char *two = new char[lenTwo];
  for (k = 0, i = pos + n; i < len; i++, k++)
  {
    two[k] = this->str[i];
  }
  int totalLen = len - n;
  this->str = new char[totalLen + 1];
  this->_size = totalLen;
  for (i = 0; i < lenOne - 1; i++)
  {
    this->str[i] = one[i];
  }
  for (k = 0; k < lenTwo - 1; k++, i++)
  {
    this->str[i] = two[k];
  }
  this->str[i] = '\0';
  return *this;
}

template <typename CharT, typename Traits, typename Alloc>
basic_string<CharT, Traits, Alloc> &
basic_string<CharT, Traits, Alloc>::erase(size_t pos)
{
__ESBMC_HIDE:
  int n = this->length() - 1;
  __ESBMC_assert(
    (pos < this->length()) && ((pos + n) <= this->length()), "overflow");
  int i, k, len = this->length();
  int lenOne = pos + 1;
  char *one = new char[lenOne];
  for (i = 0; i < pos; i++)
  {
    one[i] = this->str[i];
  }
  int lenTwo = (len - (pos + n)) + 1;
  char *two = new char[lenTwo];
  for (k = 0, i = pos + n; i < len; i++, k++)
  {
    two[k] = this->str[i];
  }
  int totalLen = len - n;
  this->str = new char[totalLen + 1];
  this->_size = totalLen;
  for (i = 0; i < lenOne - 1; i++)
  {
    this->str[i] = one[i];
  }
  for (k = 0; k < lenTwo - 1; k++, i++)
  {
    this->str[i] = two[k];
  }
  this->str[i] = '\0';
  return *this;
}

template <typename CharT, typename Traits, typename Alloc>
basic_string<CharT, Traits, Alloc> &basic_string<CharT, Traits, Alloc>::replace(
  size_t pos1,
  size_t n1,
  const basic_string<CharT, Traits, Alloc> &s)
{
__ESBMC_HIDE:
  __ESBMC_assert(
    (pos1 < this->length()) && ((pos1 + n1) <= this->length()), "overflow");
  __ESBMC_assert(s.str != NULL, "The parameter must be different than NULL");
  this->erase(pos1, n1);
  this->insert(pos1, s.str);
  return *this;
}

template <typename CharT, typename Traits, typename Alloc>
basic_string<CharT, Traits, Alloc> &basic_string<CharT, Traits, Alloc>::replace(
  size_t pos1,
  size_t n1,
  basic_string<CharT, Traits, Alloc> &s,
  size_t pos2,
  size_t n2)
{
__ESBMC_HIDE:
  __ESBMC_assert(
    (pos1 < this->length()) && ((pos1 + n1) <= this->length()), "overflow");
  __ESBMC_assert(
    (pos2 < s.length()) && ((pos2 + n2) <= s.length()) && (n2 > 0), "overflow");
  __ESBMC_assert(s.str != NULL, "The parameter must be different than NULL");
  this->erase(pos1, n1);
  int i, k;
  char *tmp = new char[n2 + 1];
  for (k = 0, i = pos2; i < (n2 + pos2); i++, k++)
    tmp[k] = s.str[i];
  tmp[k] = '\0';
  this->insert(pos1, tmp);
  return *this;
}

template <typename CharT, typename Traits, typename Alloc>
basic_string<CharT, Traits, Alloc> &basic_string<CharT, Traits, Alloc>::replace(
  size_t pos1,
  size_t n1,
  const char *s,
  size_t n2)
{
__ESBMC_HIDE:
  __ESBMC_assert(
    (pos1 < this->length()) && ((pos1 + n1) <= this->length()), "overflow");
  __ESBMC_assert(n2 > 0, "overflow");
  __ESBMC_assert(s != NULL, "The parameter must be different than NULL");
  this->erase(pos1, n1);
  int i, k;
  char *tmp = new char[n2 + 1];
  for (k = 0, i = 0; i < n2; i++, k++)
    tmp[k] = s[i];
  tmp[k] = '\0';
  this->insert(pos1, tmp);
  return *this;
}

template <typename CharT, typename Traits, typename Alloc>
basic_string<CharT, Traits, Alloc> &basic_string<CharT, Traits, Alloc>::replace(
  size_t pos1,
  size_t n1,
  const char *s)
{
__ESBMC_HIDE:
  __ESBMC_assert(
    (pos1 < this->length()) && ((pos1 + n1) <= this->length()), "overflow");
  __ESBMC_assert(s != NULL, "The parameter must be different than NULL");
  this->erase(pos1, n1);
  int i, k, n2;
  n2 = strlen(s);
  char *tmp = new char[n2 + 1];
  for (k = 0, i = 0; i < n2; i++, k++)
    tmp[k] = s[i];
  tmp[k] = '\0';
  this->insert(pos1, tmp);
  return *this;
}

template <typename CharT, typename Traits, typename Alloc>
basic_string<CharT, Traits, Alloc> &basic_string<CharT, Traits, Alloc>::replace(
  size_t pos1,
  size_t n1,
  size_t n2,
  char c)
{
__ESBMC_HIDE:
  __ESBMC_assert(
    (pos1 < this->length()) && ((pos1 + n1) <= this->length()), "overflow");
  __ESBMC_assert(n2 > 0, "overflow");
  this->erase(pos1, n1);
  int k;
  char *tmp = new char[n2 + 1];
  for (k = 0; k < n2; k++)
    tmp[k] = c;
  tmp[k] = '\0';
  this->insert(pos1, tmp);
  return *this;
}
//new add

template <typename CharT, typename Traits, typename Alloc>
basic_string<CharT, Traits, Alloc> &basic_string<CharT, Traits, Alloc>::replace(
  basic_string<CharT, Traits, Alloc>::iterator i1,
  basic_string<CharT, Traits, Alloc>::iterator i2,
  basic_string<CharT, Traits, Alloc> &str)
{
__ESBMC_HIDE:
  __ESBMC_assert(str.str != NULL, "The parameter must be different than NULL");
  int tmp_one = i1.pos;
  int tmp_two = i2.pos + 1;
  int tmp = tmp_two - tmp_one;
  this->erase(tmp_one, tmp);
  this->insert(tmp_one, str.str);
  return *this;
}

template <typename CharT, typename Traits, typename Alloc>
basic_string<CharT, Traits, Alloc> &basic_string<CharT, Traits, Alloc>::replace(
  basic_string<CharT, Traits, Alloc>::iterator i1,
  basic_string<CharT, Traits, Alloc>::iterator i2,
  char *s,
  size_t n2)
{
__ESBMC_HIDE:
  __ESBMC_assert(s != NULL, "The parameter must be different than NULL");
  int tmp_one = i1.pos;
  int tmp_two = i2.pos;
  int tmpx = tmp_two - tmp_one;
  this->replace(tmp_one, tmpx, s, n2);
  return *this;
}

template <typename CharT, typename Traits, typename Alloc>
basic_string<CharT, Traits, Alloc> &basic_string<CharT, Traits, Alloc>::replace(
  basic_string<CharT, Traits, Alloc>::iterator i1,
  basic_string<CharT, Traits, Alloc>::iterator i2,
  char *s)
{
__ESBMC_HIDE:
  __ESBMC_assert(s != NULL, "The parameter must be different than NULL");
  int tmp_one = i1.pos;
  int tmp_two = i2.pos;
  int tmpx = tmp_two - tmp_one;
  this->erase(tmp_one, tmpx);
  this->insert(tmp_one, s);
  return *this;
}

template <typename CharT, typename Traits, typename Alloc>
basic_string<CharT, Traits, Alloc> &basic_string<CharT, Traits, Alloc>::replace(
  basic_string<CharT, Traits, Alloc>::iterator i1,
  basic_string<CharT, Traits, Alloc>::iterator i2,
  size_t n2,
  char c)
{
__ESBMC_HIDE:
  int tmp_one = i1.pos;
  int tmp_two = i2.pos + 1;
  int tmpk = tmp_two - tmp_one;
  this->erase(tmp_one, tmpk);
  int k;
  char *tmp = new char[n2 + 1];
  for (k = 0; k < n2; k++)
    tmp[k] = c;
  tmp[k] = '\0';
  this->insert(tmp_one, tmp);
  return *this;
}

template <typename CharT, typename Traits, typename Alloc>
basic_string<CharT, Traits, Alloc> &basic_string<CharT, Traits, Alloc>::replace(
  basic_string<CharT, Traits, Alloc>::iterator i1,
  basic_string<CharT, Traits, Alloc>::iterator i2,
  basic_string<CharT, Traits, Alloc>::iterator i3,
  basic_string<CharT, Traits, Alloc>::iterator i4)
{
  return *this;
}

template <typename CharT, typename Traits, typename Alloc>
int basic_string<CharT, Traits, Alloc>::compare(const char *s) const
{
__ESBMC_HIDE:
  __ESBMC_assert(s != NULL, "The parameter must be different than NULL");
  int i;
  int sLen = strlen(s);
  int len = this->length();
  if (len < sLen)
    return -1;
  if (len > sLen)
    return 1;
  for (i = 0; i < sLen; i++)
  {
    if (this->str[i] != s[i])
    {
      return 2;
    }
  }
  return 0;
}

template <typename CharT, typename Traits, typename Alloc>
int basic_string<CharT, Traits, Alloc>::compare(
  const basic_string<CharT, Traits, Alloc> &s) const
{
__ESBMC_HIDE:
  __ESBMC_assert(s.str != NULL, "The parameter must be different than NULL");
  int i;
  int sLen = s.length();
  int len = this->length();
  if (len < sLen)
    return -1;
  if (len > sLen)
    return 1;
  for (i = 0; i < sLen; i++)
  {
    if (this->str[i] != s.str[i])
    {
      return 2;
    }
  }
  return 0;
}

template <typename CharT, typename Traits, typename Alloc>
int basic_string<CharT, Traits, Alloc>::compare(
  int pos1,
  size_t n1,
  const char *s) const
{
__ESBMC_HIDE:
  __ESBMC_assert(
    (pos1 < this->length()) && ((pos1 + n1) <= this->length()), "overflow");
  __ESBMC_assert(s != NULL, "The parameter must be different than NULL");
  int i, k;
  char *tmp = new char[n1 + 1];
  for (k = 0, i = pos1; i < (pos1 + n1); i++, k++)
  {
    tmp[k] = this->str[i];
  }
  tmp[k] = '\0';
  int sLen = strlen(s);
  int len = strlen(tmp);
  if (len < sLen)
    return -1;
  if (len > sLen)
    return 1;
  for (i = 0; i < sLen; i++)
  {
    if (tmp[i] != s[i])
    {
      return 2;
    }
  }
  return 0;
}

template <typename CharT, typename Traits, typename Alloc>
int basic_string<CharT, Traits, Alloc>::compare(
  int pos1,
  size_t n1,
  basic_string<CharT, Traits, Alloc> &s) const
{
__ESBMC_HIDE:
  __ESBMC_assert(
    (pos1 < this->length()) && ((pos1 + n1) <= this->length()), "overflow");
  __ESBMC_assert(s.str != NULL, "The parameter must be different than NULL");
  int i, k;
  char *tmp = new char[n1 + 1];
  for (k = 0, i = pos1; i < (pos1 + n1); i++, k++)
  {
    tmp[k] = this->str[i];
  }
  tmp[k] = '\0';
  int sLen = s.length();
  int len = strlen(tmp);
  if (len < sLen)
    return -1;
  if (len > sLen)
    return 1;
  for (i = 0; i < sLen; i++)
  {
    if (tmp[i] != s.str[i])
    {
      return 2;
    }
  }
  return 0;
}

template <typename CharT, typename Traits, typename Alloc>
int basic_string<CharT, Traits, Alloc>::compare(
  size_t pos1,
  size_t n1,
  basic_string<CharT, Traits, Alloc> &s,
  size_t pos2,
  size_t n2) const
{
__ESBMC_HIDE:
  __ESBMC_assert(
    (pos1 < this->length()) && ((pos1 + n1) <= this->length()), "overflow");
  __ESBMC_assert(
    (pos2 < s.length()) && ((pos2 + n2) <= s.length()) && (n2 > 0), "overflow");
  __ESBMC_assert(s.str != NULL, "The parameter must be different than NULL");
  int i, k;

  char *tmp = new char[n1 + 1];
  for (k = 0, i = pos1; i < (pos1 + n1); i++, k++)
  {
    tmp[k] = this->str[i];
  }
  tmp[k] = '\0';

  char *tmp2 = new char[n2 + 1];
  for (k = 0, i = pos2; i < (pos2 + n2); i++, k++)
  {
    tmp2[k] = s.str[i];
  }
  tmp2[k] = '\0';

  int sLen = strlen(tmp2);
  int len = strlen(tmp);

  if (len < sLen)
    return -1;
  if (len > sLen)
    return 1;

  for (i = 0; i < sLen; i++)
  {
    if (tmp[i] != tmp2[i])
    {
      return 2;
    }
  }

  return 0;
}

template <typename CharT, typename Traits, typename Alloc>
size_t basic_string<CharT, Traits, Alloc>::find_first_of(
  const char *s,
  size_t pos) const
{
__ESBMC_HIDE:
  __ESBMC_assert(s != NULL, "The parameter must be different than NULL");
  size_t len = this->length();
  size_t slen = strlen(s);
  if (pos >= len || slen == 0)
    return npos;
  for (size_t i = pos; i < len; i++)
    for (size_t j = 0; j < slen; j++)
      if (this->str[i] == s[j])
        return i;
  return npos;
}

template <typename CharT, typename Traits, typename Alloc>
size_t basic_string<CharT, Traits, Alloc>::find_first_of(
  const basic_string<CharT, Traits, Alloc> &s,
  size_t pos) const
{
__ESBMC_HIDE:
  __ESBMC_assert(s.str != NULL, "The parameter must be different than NULL");
  size_t len = this->length();
  size_t slen = s.length();
  if (pos >= len || slen == 0)
    return npos;
  for (size_t i = pos; i < len; i++)
    for (size_t j = 0; j < slen; j++)
      if (this->str[i] == s.str[j])
        return i;
  return npos;
}

template <typename CharT, typename Traits, typename Alloc>
size_t
basic_string<CharT, Traits, Alloc>::find_first_of(char c, size_t pos) const
{
__ESBMC_HIDE:
  size_t len = this->length();
  if (pos >= len)
    return npos;
  for (size_t i = pos; i < len; i++)
    if (this->str[i] == c)
      return i;
  return npos;
}

template <typename CharT, typename Traits, typename Alloc>
size_t basic_string<CharT, Traits, Alloc>::find_first_not_of(
  const basic_string<CharT, Traits, Alloc> &s,
  size_t pos) const
{
__ESBMC_HIDE:
  __ESBMC_assert(s.str != NULL, "The parameter must be different than NULL");
  size_t len = this->length();
  size_t slen = s.length();
  if (pos >= len)
    return npos;
  for (size_t i = pos; i < len; i++)
  {
    bool found = false;
    for (size_t j = 0; j < slen; j++)
      if (this->str[i] == s.str[j])
      {
        found = true;
        break;
      }
    if (!found)
      return i;
  }
  return npos;
}

template <typename CharT, typename Traits, typename Alloc>
size_t basic_string<CharT, Traits, Alloc>::find_first_not_of(
  const char *s,
  size_t pos) const
{
__ESBMC_HIDE:
  __ESBMC_assert(s != NULL, "The parameter must be different than NULL");
  size_t len = this->length();
  size_t slen = strlen(s);
  if (pos >= len)
    return npos;
  for (size_t i = pos; i < len; i++)
  {
    bool found = false;
    for (size_t j = 0; j < slen; j++)
      if (this->str[i] == s[j])
      {
        found = true;
        break;
      }
    if (!found)
      return i;
  }
  return npos;
}

template <typename CharT, typename Traits, typename Alloc>
size_t
basic_string<CharT, Traits, Alloc>::find_first_not_of(char c, size_t pos) const
{
__ESBMC_HIDE:
  size_t len = this->length();
  if (pos >= len)
    return npos;
  for (size_t i = pos; i < len; i++)
    if (this->str[i] != c)
      return i;
  return npos;
}

template <typename CharT, typename Traits, typename Alloc>
size_t basic_string<CharT, Traits, Alloc>::find_last_of(
  const basic_string<CharT, Traits, Alloc> &s,
  size_t pos) const
{
__ESBMC_HIDE:
  __ESBMC_assert(s.str != NULL, "The parameter must be different than NULL");
  size_t len = this->length();
  size_t slen = s.length();
  if (len == 0 || slen == 0)
    return npos;
  size_t start = (pos >= len) ? len - 1 : pos;
  for (size_t i = start + 1; i-- > 0;)
    for (size_t j = 0; j < slen; j++)
      if (this->str[i] == s.str[j])
        return i;
  return npos;
}

template <typename CharT, typename Traits, typename Alloc>
size_t basic_string<CharT, Traits, Alloc>::find_last_of(
  const char *s,
  size_t pos) const
{
__ESBMC_HIDE:
  __ESBMC_assert(s != NULL, "The parameter must be different than NULL");
  size_t len = this->length();
  size_t slen = strlen(s);
  if (len == 0 || slen == 0)
    return npos;
  size_t start = (pos >= len) ? len - 1 : pos;
  for (size_t i = start + 1; i-- > 0;)
    for (size_t j = 0; j < slen; j++)
      if (this->str[i] == s[j])
        return i;
  return npos;
}

template <typename CharT, typename Traits, typename Alloc>
size_t basic_string<CharT, Traits, Alloc>::find_last_of(char *s) const
{
  return find_last_of(static_cast<const char *>(s), npos);
}

template <typename CharT, typename Traits, typename Alloc>
size_t
basic_string<CharT, Traits, Alloc>::find_last_of(char c, size_t pos) const
{
__ESBMC_HIDE:
  size_t len = this->length();
  if (len == 0)
    return npos;
  size_t start = (pos >= len) ? len - 1 : pos;
  for (size_t i = start + 1; i-- > 0;)
    if (this->str[i] == c)
      return i;
  return npos;
}

template <typename CharT, typename Traits, typename Alloc>
size_t basic_string<CharT, Traits, Alloc>::rfind(char c, size_t pos) const
{
__ESBMC_HIDE:
  int i;
  int len = this->length();
  for (i = len; i > 0; i--)
    if (this->str[i] == c)
      return i;
  return npos; // Return npos when the character is not found
}

template <typename CharT, typename Traits, typename Alloc>
size_t basic_string<CharT, Traits, Alloc>::rfind(
  basic_string<CharT, Traits, Alloc> &s,
  size_t pos) const
{
__ESBMC_HIDE:
  // Early returns for edge cases
  if (s._size == 0)
    return (pos < this->_size) ? pos : this->_size;
  if (s._size > this->_size)
    return npos;

  __ESBMC_assert(s.str != NULL, "The parameter must be different than NULL");

  size_t len = this->_size;
  size_t slen = s._size;

  // Calculate the rightmost valid starting position
  size_t max_start;
  if (pos >= len)
    max_start = len - slen;
  else if (pos + 1 >= slen)
    max_start = pos - slen + 1;
  else
    return npos;

  // Search backward from rightmost valid position
  for (size_t start = max_start + 1; start > 0; start--)
  {
    size_t i = start - 1;
    bool match = true;

    // Simple forward comparison at position i
    for (size_t j = 0; j < slen; j++)
    {
      if (this->str[i + j] != s.str[j])
      {
        match = false;
        break;
      }
    }

    if (match)
      return i;
  }

  return npos;
}

template <typename CharT, typename Traits, typename Alloc>
size_t
basic_string<CharT, Traits, Alloc>::rfind(const char *s, size_t pos, size_t n)
  const
{
__ESBMC_HIDE:
  __ESBMC_assert(s != NULL, "The parameter must be different than NULL");
  size_t len = this->length();
  if (n == 0)
    return (pos < len) ? pos : len;
  if (n > len)
    return npos;
  size_t max_start = len - n;
  size_t start = (pos > max_start) ? max_start : pos;
  for (size_t i = start + 1; i-- > 0;)
  {
    bool match = true;
    for (size_t j = 0; j < n; j++)
      if (this->str[i + j] != s[j])
      {
        match = false;
        break;
      }
    if (match)
      return i;
  }
  return npos;
}

template <typename CharT, typename Traits, typename Alloc>
size_t
basic_string<CharT, Traits, Alloc>::rfind(const char *s, size_t pos) const
{
__ESBMC_HIDE:
  __ESBMC_assert(s != NULL, "The parameter must be different than NULL");
  return rfind(s, pos, strlen(s));
}

template <typename CharT, typename Traits, typename Alloc>
size_t basic_string<CharT, Traits, Alloc>::rfind(char *s) const
{
__ESBMC_HIDE:
  int pos = 0;
  //__ESBMC_assert((pos < this->length()) && (pos >= 0),
  //"overflow");
  __ESBMC_assert(s != NULL, "The parameter must be different than NULL");
  size_t i, j, k;
  int num = 0;
  int lim = pos;

  int len = this->length();
  char *s1 = new char[len + 1];
  strcpy(s1, this->str);

  int slen = strlen(s);
  char *s2 = new char[slen + 1];
  strcpy(s2, s);

  for (i = len - 1; i >= lim; i--)
  {
    for (k = i, j = slen - 1; j >= 0; j--)
    {
      if (s1[k] != s2[j])
      {
        break;
      }
      else
      {
        num++;
        if (num == slen)
        {
          return k;
        }
        k--;
      }
    }
  }
  return -1;
}

template <typename CharT, typename Traits, typename Alloc>
basic_string<CharT, Traits, Alloc> operator+(
  basic_string<CharT, Traits, Alloc> lhs,
  basic_string<CharT, Traits, Alloc> rhs)
{
  int totalLength = lhs.size();
  totalLength += rhs.size();
  int i, j, k;
  basic_string<CharT, Traits, Alloc> result;
  result.str = new char[totalLength + 1];
  for (i = 0; i < lhs.size(); i++)
  {
    result.str[i] = lhs.str[i];
  }
  for (j = i, k = 0; j < totalLength; j++, k++)
  {
    result.str[j] = rhs.str[k];
  }
  result.str[j] = '\0';
  result._size = totalLength;
  return result;
}

template <typename CharT, typename Traits, typename Alloc>
basic_string<CharT, Traits, Alloc>
operator+(basic_string<CharT, Traits, Alloc> lhs, char *rhs)
{
  int totalLength = lhs.size();
  totalLength += strlen(rhs);
  int i, j, k;
  basic_string<CharT, Traits, Alloc> result;
  result.str = new char[totalLength + 1];
  for (i = 0; i < lhs.size(); i++)
  {
    result.str[i] = lhs.str[i];
  }
  for (j = i, k = 0; j < totalLength; j++, k++)
  {
    result.str[j] = rhs[k];
  }
  result.str[j] = '\0';
  result._size = totalLength;
  return result;
}

template <typename CharT, typename Traits, typename Alloc>
basic_string<CharT, Traits, Alloc>
operator+(basic_string<CharT, Traits, Alloc> lhs, char rhc)
{
  int totalLength = lhs.size();
  totalLength += 1;
  int i;
  basic_string<CharT, Traits, Alloc> result;
  result.str = new char[totalLength + 1];
  for (i = 0; i < lhs.size(); i++)
  {
    result.str[i] = lhs.str[i];
  }
  result.str[i] = rhc;
  result.str[i + 1] = '\0';
  result._size = totalLength;
  return result;
}

template <typename CharT, typename Traits, typename Alloc>
basic_string<CharT, Traits, Alloc>
operator+(char *lhs, basic_string<CharT, Traits, Alloc> rhs)
{
  int lhsLen = strlen(lhs);
  int totalLength = lhsLen;
  totalLength += rhs.size();
  int i, j, k;
  basic_string<CharT, Traits, Alloc> result;
  result.str = new char[totalLength + 1];
  for (i = 0; i < lhsLen; i++)
  {
    result.str[i] = lhs[i];
  }
  for (j = i, k = 0; j < totalLength; j++, k++)
  {
    result.str[j] = rhs.str[k];
  }
  result.str[j] = '\0';
  result._size = totalLength;
  return result;
}

/*
 * The following operator overloading is really obfuscating on standard types (char*, char).
 * Clang would generate parse error for such thing. For the time being, let's just
 * comment them to avoid the parse error so that we can progress further.
 * The purpose of such overloading may become clear when we run benchmarks.
 * Remove them if they are not affecting the pass rate in our benchmarks
 */
#if 0
basic_string operator+(char * lhs, char rhc) {
	int lhsLen = strlen(lhs);
	int totalLength = lhsLen;
	totalLength += 1;
	int i;
	basic_string result;
	result.str = new char[totalLength + 1];
	for(i = 0; i < lhsLen; i++){
		result.str[i] = lhs[i];
	}
	result.str[i] = rhc;
	result.str[i+1] = '\0';
	result._size = totalLength;
	return result;
}
#endif
template <typename CharT, typename Traits, typename Alloc>
basic_string<CharT, Traits, Alloc>
operator+(char lhc, basic_string<CharT, Traits, Alloc> rhs)
{
  int totalLength = 1;
  totalLength += rhs.size();
  int i, j, k;
  basic_string<CharT, Traits, Alloc> result;
  result.str = new char[totalLength + 1];
  result.str[0] = lhc;
  for (j = 1, k = 0; j < totalLength; j++, k++)
  {
    result.str[j] = rhs.str[k];
  }
  result.str[j] = '\0';
  result._size = totalLength;
  return result;
}

template <typename CharT, typename Traits, typename Alloc>
bool operator==(
  const basic_string<CharT, Traits, Alloc> &a,
  const basic_string<CharT, Traits, Alloc> &b)
{
__ESBMC_HIDE:
  __ESBMC_assert(
    a.str != NULL, "The first parameter must be different than NULL");
  __ESBMC_assert(
    b.str != NULL, "The second parameter must be different than NULL");
  if (a._size != b._size)
    return false;
  int aux;
  aux = strcmp(b.c_str(), a.c_str());
  if (aux == 0)
  {
    return true;
  }
  else
  {
    return false;
  }
}

template <typename CharT, typename Traits, typename Alloc>
bool operator==(const char *lhs, const basic_string<CharT, Traits, Alloc> &rhs)
{
__ESBMC_HIDE:
  __ESBMC_assert(
    lhs != NULL, "The first parameter must be different than NULL");
  __ESBMC_assert(
    rhs.str != NULL, "The second parameter must be different than NULL");
  if (strlen(lhs) != rhs._size)
    return false;
  int aux;
  aux = strcmp((char *)lhs, rhs.c_str());
  if (aux == 0)
  {
    return true;
  }
  else
  {
    return false;
  }
}

template <typename CharT, typename Traits, typename Alloc>
bool operator==(const basic_string<CharT, Traits, Alloc> &lhs, const char *rhs)
{
__ESBMC_HIDE:
  __ESBMC_assert(
    lhs.str != NULL, "The first parameter must be different than NULL");
  __ESBMC_assert(
    rhs != NULL, "The second parameter must be different than NULL");
  if (lhs._size != strlen(rhs))
    return false;
  int aux;
  aux = strcmp(lhs.c_str(), (char *)rhs);
  if (aux == 0)
  {
    return true;
  }
  else
  {
    return false;
  }
}
template <typename CharT, typename Traits, typename Alloc>
bool operator!=(
  const basic_string<CharT, Traits, Alloc> &a,
  const basic_string<CharT, Traits, Alloc> &b)
{
__ESBMC_HIDE:
  __ESBMC_assert(a.str != NULL, "The parameter must be different than NULL");
  __ESBMC_assert(b.str != NULL, "The parameter must be different than NULL");
  if (a._size != b._size)
    return true;
  int aux;
  aux = strcmp(a.c_str(), b.c_str());
  if (aux == 0)
  {
    return false;
  }
  else
  {
    return true;
  }
}

template <typename CharT, typename Traits, typename Alloc>
bool operator!=(const CharT *lhs, const basic_string<CharT, Traits, Alloc> &rhs)
{
__ESBMC_HIDE:
  __ESBMC_assert(
    lhs != NULL, "The first parameter must be different than NULL");
  __ESBMC_assert(
    rhs.str != NULL, "The second parameter must be different than NULL");
  if (strlen(lhs) != rhs._size)
    return true;
  int aux;
  aux = strcmp((char *)lhs, rhs.c_str());
  if (aux == 0)
  {
    return false;
  }
  else
  {
    return true;
  }
}

template <typename CharT, typename Traits, typename Alloc>
bool operator!=(const basic_string<CharT, Traits, Alloc> &lhs, const CharT *rhs)
{
__ESBMC_HIDE:
  __ESBMC_assert(
    lhs.str != NULL, "The first parameter must be different than NULL");
  __ESBMC_assert(
    rhs != NULL, "The second parameter must be different than NULL");
  if (lhs._size != strlen(rhs))
    return true;
  int aux;
  aux = strcmp(lhs.c_str(), (char *)rhs);
  if (aux == 0)
  {
    return false;
  }
  else
  {
    return true;
  }
}

template <typename CharT, typename Traits, typename Alloc>
istream &
getline(istream &is, basic_string<CharT, Traits, Alloc> &str, char delim);
template <typename CharT, typename Traits, typename Alloc>
istream &getline(istream &is, basic_string<CharT, Traits, Alloc> &str);

std::string to_string(int value)
{
  char buffer[50];
  itoa(value, buffer, 10);
  return string(buffer);
}

std::string to_string(long value)
{
  char buffer[50];
  itoa(value, buffer, 10);
  return string(buffer);
}

std::string to_string(long long value)
{
  char buffer[50];
  itoa(value, buffer, 10);
  return string(buffer);
}

std::string to_string(unsigned value)
{
  char buffer[50];
  itoa(value, buffer, 10);
  return string(buffer);
}

std::string to_string(unsigned long value)
{
  char buffer[50];
  itoa(value, buffer, 10);
  return string(buffer);
}

std::string to_string(unsigned long long value)
{
  char buffer[50];
  itoa(value, buffer, 10);
  return string(buffer);
}

std::string to_string(float value)
{
  char buffer[50];
  itoa(value, buffer, 10);
  return string(buffer);
}

std::string to_string(double value)
{
  char buffer[50];
  itoa(value, buffer, 10);
  return string(buffer);
}

std::string to_string(long double value)
{
  char buffer[50];
  itoa(value, buffer, 10);
  return string(buffer);
}

int stoi(const std::string &str, size_t *pos = 0, int base = 10)
{
  const char *c_str = str.c_str();

  char *endptr;
  long result = std::strtol(c_str, &endptr, base);

  __ESBMC_assert(endptr != c_str, "No digits in input string");

  return static_cast<int>(result);
}

float stof(const std::string &str, size_t *pos = 0)
{
  const char *c_str = str.c_str();

  char *endptr;
  float result = std::strtof(c_str, &endptr);

  __ESBMC_assert(endptr != c_str, "No digits in input string");

  return result;
}

} // namespace std
#endif
