nondet_int         13 tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/locks.h int nondet_int(void);
nondet_int         65 tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/preempt.c 	thread_cpu_id = nondet_int();