function wfWitnessSmall()

in impl/src/tooling/verifier/smt_workflows.ts [365:471]
96 lines of code
26 McCabe index (conditional complexity)

function wfWitnessSmall(usercode: CodeFileInfo[], timeout: number, errorTrgtPos: { file: string, line: number, pos: number }, entrypoint: MIRInvokeKey, printprogress: boolean, smallopsonly: boolean): {result: CheckerResult, time: number, input?: any} | undefined {
    const SMALL_MODEL = smallopsonly 
    ? [
        { EnableCollection_SmallHavoc: true, EnableCollection_LargeHavoc: false, EnableCollection_SmallOps: true, EnableCollection_LargeOps: false, StringOpt: "ASCII" }
    ]
    : [
        { EnableCollection_SmallHavoc: true, EnableCollection_LargeHavoc: false, EnableCollection_SmallOps: true, EnableCollection_LargeOps: true, StringOpt: "ASCII" },
        { EnableCollection_SmallHavoc: false, EnableCollection_LargeHavoc: true, EnableCollection_SmallOps: true, EnableCollection_LargeOps: true, StringOpt: "ASCII" },
    ];

    const BV_SIZES = [
        3,
        5, 
        8, 
        12, 
        16
    ];

    const start = Date.now();

    for(let i = 0; i < BV_SIZES.length; ++i) {
        if(printprogress) {
            process.stderr.write(`    Looking for small (${BV_SIZES[i]}) bit width witnesses...\n`);
        }

        try {
            const { masm } = generateMASM(usercode, entrypoint, AssemblyFlavor.UFOverApproximate, true /*EnableCollection_SmallOps always true*/);
            if(masm === undefined) {
                if(printprogress) {
                    process.stderr.write(`    compile errors\n`);
                }
                return undefined;
            }
            else {
                const numgen = computeNumGen(masm, BV_SIZES[i]);
                const hashgen = BVEmitter.create(BigInt(16));
                if(numgen === undefined) {
                    if(printprogress) {
                        process.stderr.write(`    constants larger than specified bitvector size -- continuing checks...\n`);
                    }
                }
                else {
                    for (let j = 0; j < SMALL_MODEL.length; ++j) {
                        const vopts = { ISize: BV_SIZES[i], ...SMALL_MODEL[j] } as VerifierOptions;
                        if(printprogress) {
                            process.stderr.write(`      Checking *${vopts.EnableCollection_LargeHavoc ? "mixed" : "small"}* inputs with *${vopts.EnableCollection_LargeOps ? "mixed" : "small"}* operations...\n`);
                        }

                        const res = generateSMTPayload(masm, "witness", timeout, {int: numgen, hash: hashgen}, vopts, errorTrgtPos, entrypoint);
                        if (res === undefined) {
                            if (printprogress) {
                                process.stderr.write(`      payload generation errors\n`);
                            }
                            return undefined;
                        }

                        const cres = runVEvaluator(res, "witness");
                        const jres = JSON.parse(cres);
                        const rr = jres["result"];
                        if (rr === "unreachable") {
                            if (printprogress) {
                                process.stderr.write(`      unreachable -- continuing checks...\n`);
                            }
                        }
                        else if (rr === "witness") {
                            const end = Date.now();
                            const witness = jres["input"];

                            //
                            //Witness may be unreachable for some reason (Float <-> Real approx), depends on NAT_MAX not being 2^64, etc.
                            //May want to try executing it here to validate -- if it fails then we can return undefined?
                            //

                            if (printprogress) {
                                process.stderr.write(`      witness\n`);
                            }

                            return { result: "witness", time: (end - start) / 1000, input: witness };
                        }
                        else if (rr === "timeout") {
                            if (printprogress) {
                                process.stderr.write(`      timeout -- moving on\n`);
                            }

                            const end = Date.now();
                            return { result: "timeout", time: (end - start) / 1000 };
                        }
                        else {
                            if (printprogress) {
                                process.stderr.write(`      error -- moving on\n`);
                            }
                            return undefined;
                        }
                    }
                }
            }
        } catch(e) {
            if(printprogress) {
                process.stderr.write(`    failure: ${e}\n`);
            }
            return undefined;
        }   
    }

    const end = Date.now();
    return {result: "unreachable", time: (end - start) / 1000};
}