FromInt.pvs 659 Bytes