precondition: the expression BinOp(op,Intx,Int y) shall be well-typed.
@after 2.5.0 if x and y have different widths then they are extended to the same width, which is the width of the largest operand. If an operator is signed, then it will be correctly sign-extended.