aCallType2Bool
addCallTypeRestriction
addConditionRestriction
addConjunct
addEquVarCondition
addFailedFunc
addMissingCase
addSingleCase
addVarAnyType
addVarExps
addVarType
addVarTypes
anyTypes
banner
checkPredefinedOp
currentFuncDecls
enforceNormalForm
funcDecls2Usage
getBranchState
getCallType
getCondition
getConsInfos
getCurrentFuncName
getExpandedCondition
getExpandedConditionWithConj
getFuncType
getNonFailConditionOf
getToolOptions
getVarExps
getVarType
getVarTypeOf
getVarTypes
incrIncompleteCases
incrNonTrivialCall
incrUnsatSMT
inferCallTypes
inferIOTypes
initVerifyState
isUnsatisfiable
main
newFreshVarIndex
noVerifyFunctions
printIOTypes
printIOTypesIfDemanded
printIfVerb
printVerifyResult
printVerifyResults
removeVarAnyType
restoreBranchState
setCallCondition
setCondition
setCurrentFunc
setFreshVarIndex
setNewFunCondition
setToolError
setVarExpTypeOf
setVarExps
setVarTypes
showFunctionInfo
showIncompleteBranch
showSimpExp
showVarExpTypes
tryVerifyProg
unionFDecls
usedFuncsInFunc
usedFuncsInRule
verifyBranch
verifyExpr
verifyFunc
verifyFuncCall
verifyFuncRule
verifyMissingBranches
verifyModule
verifyModuleIfNew
verifyNonTrivFuncCall
verifyVarExpr
vstCallTypes
vstCondition
vstConsInfos
vstCurrFunc
vstCurrModule
vstError
vstFailedFuncs
vstFreshVar
vstFunConds
vstIOTypes
vstImpCallTypes
vstImpFunConds
vstModules
vstNewFailed
vstNewFunConds
vstPartialBranches
vstStats
vstToolOpts
vstVarExp
vstVarTypes