def METHOD_NAME(self, left: z3.ExprRef, op: str, right: z3.ExprRef) -> z3.ExprRef:
    """Given left, right, op, apply the binary operation."""
    try:
        if op == "+":
            return left + right
        elif op == "-":
            return left - right
        elif op == "*":
            return left * right
        elif op == "/":
            return left / right
        elif op == "**":
            return left**right
        elif op == "==":
            return left == right
        elif op == "<=":
            return left <= right
        elif op == ">=":
            return left >= right
        elif op == "<":
            return left < right
        elif op == ">":
            return left > right
        else:
            raise Z3ParseException(f"Unhandled binary operation {op}.")
    except TypeError:
        raise Z3ParseException(f"Operation {op} incompatible with types {left} and {right}.")