Handle slicing operation with non-unit step length and indeterminant upper bound in ExprWrapper

[Raine-Yang-UofT]

Currently, the parse_index_op method in ExprWrapper does not properly handle cases where a string slicing operation has a step length greater than 1 and the ending index is the end of the string. For example, x[1::2].

Since z3.SubString does not support a "step length" argument, the current approach converts a slicing with step into a list of SubString connected with z3.Concat. This method fails when we have an unknown upper bound.

As shown in the code below, the current approach handles this case by raising a Z3ParseError and skipping the parsing for this expression. An alternative algorithm may be required to cover all slicing operations correctly.

# in `parse_index_op`

if step == 1:
    return z3.SubString(value, lower, upper - lower)

# unhandled case: the upper bound is indeterminant
if step != 1 and upper == z3.Length(value):
    raise Z3ParseException(
         "Unable to convert a slicing operation with a non-unit step length and an indeterminant upper bound"
    )

return z3.Concat(*(z3.SubString(value, i, 1) for i in range(lower, upper, step)))