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)
void __VERIFIER_error() { abort(); }

int __VERIFIER_nondet_int() { int val; return val; }
--- 
+++ 
@@ -1,3 +1,19 @@
 void __VERIFIER_error() { abort(); }
 
-int __VERIFIER_nondet_int() { int val; return val; }
+// 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
