addFailedFuncToStats addFunsToVerifyInfo' addFunsToVerifyInfo addNFCsToProgs addPostCondToStats addPreCondToStats addProgsToState allFuncs checkProgs currTAProgs evalOption failedFuncs getOption incFailTestInStats incNumAllInStats incNumNFCInStats incPatTestInStats inferNFCs initVState initVerifyInfo isContractOp isProperty isVerifiedContracts isVerifiedFailfree lookupProg modifyOptions nfConds numAllFuncs numFailTests numNFCFuncs numPatTests postConds preConds printCP printWhenAll printWhenIntermediate printWhenStatus showContractStats showFailfreeStats showStats tdeclOf toolOpts trInfo uPostCond uPreCond vPostCond vPreCond whenOption