2948#line 252
2949 tmp___1 = __VERIFIER_nondet_int();
2950 }
2951#line 252
2952 if (tmp___1 != 0) {
2953#line 253
2954 goto ldv_18554;
2955 } else {
2956#line 255
2957 goto ldv_18556;
2958 }
2959 ldv_18556: ;
2960 {
2961#line 269
2962 switch_class_exit();
2963 }
2964 ldv_final:
2965 {
2966#line 272
2967 ldv_check_final_state();
2968 }
2969#line 275
2970 return;
2971}
2972}
2973#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5574/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
2974void ldv_blast_assert(void)
2975{
2976
2977 {
2978 ERROR: ;
2979#line 6
2980 goto ERROR;
2981}
2982}
2983#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5574/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
2984extern int __VERIFIER_nondet_int(void) ;
2985#line 296 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5574/dscv_tempdir/dscv/ri/43_1a/drivers/staging/android/switch/switch_class.c.p"
2986int ldv_spin = 0;
2987#line 300 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5574/dscv_tempdir/dscv/ri/43_1a/drivers/staging/android/switch/switch_class.c.p"
2988void ldv_check_alloc_flags(gfp_t flags )