FromInt.pvs 731 Bytes