code: def StrIndexOf(input_string, substring, startIndex, bitlength):
      
      try:
          s = input_string.value
          t = substring.value
          i = startIndex.value
          return BVV(i + s[i:].index(t), bitlength)
      except ValueError:
          return BVV(-1, bitlength)
docs: Return True if the concrete value of the input_string ends with suffix
      otherwise false.
  
      :param input_string: the string we want to check
      :param substring: the substring we want to find the index
      :param startIndex: the index to start searching at
      :param bitlength: bitlength of the bitvector representing the index of the substring
  
      :return BVV: index of the substring in bit-vector representation or -1 in bitvector representation