addPostConditionCheck addPostConditionTo addPreConditionCheck addPreConditions addToAssertion addVarTypes applyFunc axiomatizedOps banner binding2SMT cAssertion callSMT checkImplication checkImplicationWithSMT emptyTransState extractPostConditionProofObligation fileInPath freshVar fromNoCheckQName genSMTTypes getAssertion getContractCheckerModulePath getFreshVar getFreshVarIndex getIncludePath getVarTypes ilog main makeTransState nondetTrans nondetTransL normalizeArgs optPreConditionInRule postCondExpOf preCondExpOf pred2smt proveContracts proveContractsInProg provePostCondition provePreCondition renamePatternVars setAssertion setFreshVarIndex showDictOf showDictTypeOf showQNameNoDots showWithLineNums tconsOfTypeExpr toNoCheckQName typedVar2SMT unzipBranches varTypes verifyPostConditions verifyPreConditions writeTransformedFCY writeTransformedTAFCY