Int casts (Odr_int stuff)