FromInt.pvs 682 Bytes