def _comparison_helper(
    a: "BitVecFunc",
    b: Union[BitVec, int],
    operation: Callable,
    default_value: bool,
    inputs_equal: bool,
) -> Bool:
    """
    Helper function for comparison operations with BitVecFuncs.

    :param a: The BitVecFunc to compare.
    :param b: A BitVec or int to compare to.
    :param operation: The comparison operation to perform.
    :return: The resulting Bool
    """
    # Is there some hack for gt/lt comparisons?
    if isinstance(b, int):
        b = BitVec(z3.BitVecVal(b, a.size()))

    union = a.annotations + b.annotations

    if not a.symbolic and not b.symbolic:
        return Bool(z3.BoolVal(operation(a.value, b.value)), annotations=union)

    if (
        not isinstance(b, BitVecFunc)
        or not a.func_name
        or not a.input_
        or not a.func_name == b.func_name
    ):
        return Bool(z3.BoolVal(default_value), annotations=union)

    return And(
        Bool(cast(z3.BoolRef, operation(a.raw, b.raw)), annotations=union),
        a.input_ == b.input_ if inputs_equal else a.input_ != b.input_,
    )
Helper function for comparison operations with BitVecFuncs.

    :param a: The BitVecFunc to compare.
    :param b: A BitVec or int to compare to.
    :param operation: The comparison operation to perform.
    :return: The resulting Bool