proc addAsgnFact(m: var TModel; key, value: PNode) {.
    ...raises: [Exception, OSError, KeyError, ValueError, IOError], tags: [
    RootEffect, WriteIOEffect, ReadEnvEffect, ReadIOEffect, ReadDirEffect],
    forbids: [].}

proc addCaseBranchFacts(m: var TModel; n: PNode; i: int) {....raises: [Exception,
    OSError, KeyError, ValueError, IOError, ERecoverableError], tags: [
    RootEffect, WriteIOEffect, ReadEnvEffect, ReadIOEffect, ReadDirEffect],
    forbids: [].}

proc addDiscriminantFact(m: var TModel; n: PNode) {.
    ...raises: [Exception, OSError, KeyError, ValueError, IOError], tags: [
    RootEffect, WriteIOEffect, ReadEnvEffect, ReadIOEffect, ReadDirEffect],
    forbids: [].}

proc addFact(m: var TModel; nn: PNode) {....raises: [Exception, OSError, KeyError,
    ValueError, IOError, ERecoverableError], tags: [RootEffect, WriteIOEffect,
    ReadEnvEffect, ReadIOEffect, ReadDirEffect], forbids: [].}

proc addFactLe(m: var TModel; a, b: PNode) {.
    ...raises: [Exception, OSError, KeyError, ValueError, IOError], tags: [
    RootEffect, WriteIOEffect, ReadEnvEffect, ReadIOEffect, ReadDirEffect],
    forbids: [].}

proc addFactLt(m: var TModel; a, b: PNode) {.
    ...raises: [Exception, OSError, KeyError, ValueError, IOError], tags: [
    RootEffect, WriteIOEffect, ReadEnvEffect, ReadIOEffect, ReadDirEffect],
    forbids: [].}

proc addFactNeg(m: var TModel; n: PNode) {....raises: [Exception, OSError,
    KeyError, ValueError, IOError, ERecoverableError], tags: [RootEffect,
    WriteIOEffect, ReadEnvEffect, ReadIOEffect, ReadDirEffect], forbids: [].}

proc buildAdd(a: PNode; b: BiggestInt; o: Operators): PNode {.
    ...raises: [Exception, OSError, KeyError, ValueError, IOError], tags: [
    RootEffect, WriteIOEffect, ReadEnvEffect, ReadIOEffect, ReadDirEffect],
    forbids: [].}

proc buildCall(op: PSym; a, b: PNode): PNode {.
    ...raises: [Exception, OSError, KeyError, ValueError, IOError], tags: [
    RootEffect, WriteIOEffect, ReadEnvEffect, ReadIOEffect, ReadDirEffect],
    forbids: [].}

proc buildCall(op: PSym; a: PNode): PNode {.
    ...raises: [Exception, OSError, KeyError, ValueError, IOError], tags: [
    RootEffect, WriteIOEffect, ReadEnvEffect, ReadIOEffect, ReadDirEffect],
    forbids: [].}

proc buildLe(o: Operators; a, b: PNode): PNode {.
    ...raises: [Exception, OSError, KeyError, ValueError, IOError], tags: [
    RootEffect, WriteIOEffect, ReadEnvEffect, ReadIOEffect, ReadDirEffect],
    forbids: [].}

proc canon(n: PNode; o: Operators): PNode {.
    ...raises: [Exception, OSError, KeyError, ValueError, IOError], tags: [
    RootEffect, WriteIOEffect, ReadEnvEffect, ReadIOEffect, ReadDirEffect],
    forbids: [].}

proc checkFieldAccess(m: TModel; n: PNode; conf: ConfigRef; produceError: bool) {....raises: [
    Exception, OSError, KeyError, ValueError, IOError, ERecoverableError], tags: [
    RootEffect, WriteIOEffect, ReadEnvEffect, ReadIOEffect, ReadDirEffect],
    forbids: [].}

proc doesImply(facts: TModel; prop: PNode): TImplication {....raises: [Exception,
    OSError, KeyError, ValueError, IOError, ERecoverableError], tags: [
    RootEffect, WriteIOEffect, ReadEnvEffect, ReadIOEffect, ReadDirEffect],
    forbids: [].}

proc highBound(conf: ConfigRef; x: PNode; o: Operators): PNode {....raises: [
    Exception, OSError, KeyError, ValueError, IOError, ERecoverableError], tags: [
    RootEffect, WriteIOEffect, ReadEnvEffect, ReadIOEffect, ReadDirEffect],
    forbids: [].}

proc impliesNotNil(m: TModel; arg: PNode): TImplication {....raises: [Exception,
    OSError, KeyError, ValueError, IOError, ERecoverableError], tags: [
    RootEffect, WriteIOEffect, ReadEnvEffect, ReadIOEffect, ReadDirEffect],
    forbids: [].}

proc interestingCaseExpr(m: PNode): bool {.
    ...raises: [Exception, OSError, KeyError, ValueError, IOError], tags: [
    RootEffect, WriteIOEffect, ReadEnvEffect, ReadIOEffect, ReadDirEffect],
    forbids: [].}

proc invalidateFacts(m: var TModel; n: PNode) {.
    ...raises: [Exception, OSError, KeyError, ValueError, IOError], tags: [
    RootEffect, WriteIOEffect, ReadEnvEffect, ReadIOEffect, ReadDirEffect],
    forbids: [].}

proc invalidateFacts(s: var seq[PNode]; n: PNode) {.
    ...raises: [Exception, OSError, KeyError, ValueError, IOError], tags: [
    RootEffect, WriteIOEffect, ReadEnvEffect, ReadIOEffect, ReadDirEffect],
    forbids: [].}

proc lowBound(conf: ConfigRef; x: PNode): PNode {....raises: [Exception, OSError,
    KeyError, ValueError, IOError, ERecoverableError], tags: [RootEffect,
    WriteIOEffect, ReadEnvEffect, ReadIOEffect, ReadDirEffect], forbids: [].}

proc proveLe(m: TModel; a, b: PNode): TImplication {....raises: [Exception,
    OSError, KeyError, ValueError, IOError, ERecoverableError], tags: [
    RootEffect, WriteIOEffect, ReadEnvEffect, ReadIOEffect, ReadDirEffect],
    forbids: [].}

proc sameSubexprs(m: TModel; a, b: PNode): bool {....raises: [Exception, OSError,
    KeyError, ValueError, IOError, ERecoverableError], tags: [RootEffect,
    WriteIOEffect, ReadEnvEffect, ReadIOEffect, ReadDirEffect], forbids: [].}

proc sameTree(a, b: PNode): bool {....raises: [Exception, OSError, KeyError,
    ValueError, IOError], tags: [RootEffect, WriteIOEffect, ReadEnvEffect,
                                 ReadIOEffect, ReadDirEffect], forbids: [].}

proc simpleSlice(a, b: PNode): BiggestInt {.
    ...raises: [Exception, OSError, KeyError, ValueError, IOError], tags: [
    RootEffect, WriteIOEffect, ReadEnvEffect, ReadIOEffect, ReadDirEffect],
    forbids: [].}