issue with isize for enum discriminants

[tjhance]

This is a follow-up to #2767

I think there is still a discrepancy in handling of isize, as the conversion uses isize for whatever platform Verus is compiled on, not necessarily the target architecture of the user code