fix: fix type checking for slicing upper bound

Including z3.ArithRef (type of Length()) as valid slicing upper bound

python_ta/transforms/ExprWrapper.py

@@ -246,7 +246,11 @@ def parse_index_op(self, node: nodes.Subscript) -> z3.ExprRef:
                 )
                 step = 1 if slice.step is None else self._parse_number_literal(slice.step)
 
-                if isinstance(lower, int) and isinstance(upper, int) and isinstance(step, int):
+                if (
+                    isinstance(lower, int)
+                    and isinstance(upper, (int, z3.ArithRef))
+                    and isinstance(step, int)
+                ):
 
                     if step == 1:
                         return z3.SubString(value, lower, upper)