addToAssertion addVarTypes applyFunc axiomatizedOps banner binding2SMT cAssertion checkImplicationWithSMT emptyTransState freshVar getAssertion getFreshVar getFreshVarIndex getFreshVarsForTypes getVarTypes ilog incFreshVarIndex loadAnalysisWithImports main makeTransState missingConsInBranch nonfailCondExpOf nonfailPreCondExpOf normalizeArgs postCondExpOf preCondExpOf pred2SMT proveNonFailingFunc proveNonFailingFuncs proveNonFailingRule renameFreeVars renameLetVars renamePatternVars setAssertion setFreshVarIndex showWithLineNums simpExpr tconsOfTypeExpr test testBoolCase testcv testv typedVar2SMT varTypes verifyNonFailingMod verifyNonFailingModules