BinaryOp bvSMulNoUnderflow(Expr x, Expr y) => BinaryOp(BinaryOpKind.bvSMulNoUnderflow, x, y).declare();