def METHOD_NAME(self, node: astroid.BinOp) -> z3.ExprRef:
    """Convert an astroid BinOp node to a z3 expression."""
    left, op, right = node.left, node.op, node.right
    left = self.reduce(left)
    right = self.reduce(right)
    return self.apply_bin_op(left, op, right)