nNonNegativeRule: FAIL
nNonNegative: FAIL
mInvariantParamInPreserved: FAIL
mCurrentContractNonNegative: FAIL
