#include <stdio.h>

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

int main(int argc, char const* argv[]) {
    for (int i = 0; i < 10; i++) {
        put(nondet_int());
        verifySpefication();
    }
    return 0;
}