#include <stdio.h>

#include "cbmcLLRBContext.h"

/* cbmc built in functions */
int nondet_int();

void verifySpecification_stub(struct Context* context) {
    verifySpecification(context);
}

void verifySpecification(struct Context* context, struct Node* node) {
    for (int i = 0; i < 10; i++) {
        int hoge      = nodet_int();
        node->key     = hoge;
        node->value   = node->key;
        context->next = VerifySpecification;

        assert(&context->data[Tree]->tree.root->key == hoge);
        meta(context, Put);
    }
    meta(context, Exit);
}


int main(int argc, char const* argv[]) {
    startCode(VerifySpecification);
    return 0;
}