converts a symbolic char to a number in the given base
        returns expression, result
        expression is a symbolic boolean indicating whether or not it was a valid number
        result is the value

def _char_to_val(char, base):
        """
        converts a symbolic char to a number in the given base
        returns expression, result
        expression is a symbolic boolean indicating whether or not it was a valid number
        result is the value
        """
        cases = []
        # 0-9
        max_digit = claripy.BVV(b"9")
        min_digit = claripy.BVV(b"0")
        if base < 10:
            max_digit = claripy.BVV(ord("0") + base, 8)
        is_digit = claripy.And(char >= min_digit, char <= max_digit)
        # return early here so we don't add unnecessary statements
        if base <= 10:
            return is_digit, char - min_digit

        # handle alphabetic chars
        max_char_lower = claripy.BVV(ord("a") + base-10 - 1, 8)
        max_char_upper = claripy.BVV(ord("A") + base-10 - 1, 8)
        min_char_lower = claripy.BVV(ord("a"), 8)
        min_char_upper = claripy.BVV(ord("A"), 8)

        cases.append((is_digit, char - min_digit))
        is_alpha_lower = claripy.And(char >= min_char_lower, char <= max_char_lower)
        cases.append((is_alpha_lower, char - min_char_lower + 10))
        is_alpha_upper = claripy.And(char >= min_char_upper, char <= max_char_upper)
        cases.append((is_alpha_upper, char - min_char_upper + 10))

        expression = claripy.Or(is_digit, is_alpha_lower, is_alpha_upper)
        # use the last case as the default, the expression will encode whether or not it's satisfiable
        result = claripy.ite_cases(cases[:-1], cases[-1][1])

        return expression, result