assume           4571 arch/x86/events/intel/core.c 		int assume = 3 * !boot_cpu_has(X86_FEATURE_HYPERVISOR);
assume           4574 arch/x86/events/intel/core.c 			max((int)edx.split.num_counters_fixed, assume);
assume             85 tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/locks.h 	assume(lock_impl_trylock(lock));
assume            194 tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/locks.h 	assume(prev_count);
assume             25 tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/misc.h #define udelay(x) assume(0)
assume             66 tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/preempt.c 	assume(thread_cpu_id >= 0);
assume             67 tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/preempt.c 	assume(thread_cpu_id < NR_CPUS);
assume             46 tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/simple_sync_srcu.c 	assume(try_check_zero(sp, idx, trycount));
assume             50 tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/simple_sync_srcu.c 	assume(try_check_zero(sp, idx^1, trycount));