void __VERIFIER_error() { abort(); }

int __VERIFIER_nondet_int() { int val; return val; }
void __VERIFIER_error() { abort(); }

// Some files define __VERIFIER_assume, some declare as extern. What happens when redefined?
void __VERIFIER_assume(int expression) { if (!expression) { LOOP: goto LOOP; }; return; }

// #define __VERIFIER_nondet(X) X __VERIFIER_nondet_##X() { X val; return val; }
#define __VERIFIER_nondet2(X, Y) X __VERIFIER_nondet_##Y() { X val; return val; }
#define __VERIFIER_nondet(X) __VERIFIER_nondet2(X, X)

__VERIFIER_nondet2(_Bool, bool)
__VERIFIER_nondet(char)
__VERIFIER_nondet2(unsigned char, uchar)
// int __VERIFIER_nondet_int() { int val; return val; }
__VERIFIER_nondet(int)
__VERIFIER_nondet2(unsigned int, uint)
__VERIFIER_nondet(long)
__VERIFIER_nondet2(unsigned long, ulong)
// void* __VERIFIER_nondet_pointer() { void* val; return val; }
__VERIFIER_nondet2(void*, pointer)
Add more common __VERIFIER functions
Add more common __VERIFIER functions
