2966 tmp___0 = __VERIFIER_nondet_int();
2967 }
2968#line 245
2969 if (tmp___0 != 0) {
2970#line 247
2971 goto ldv_21098;
2972 } else
2973#line 245
2974 if (ldv_s_wm831x_on_driver_platform_driver != 0) {
2975#line 247
2976 goto ldv_21098;
2977 } else {
2978#line 249
2979 goto ldv_21100;
2980 }
2981 ldv_21100: ;
2982 ldv_module_exit: ;
2983 {
2984#line 295
2985 ldv_check_final_state();
2986 }
2987#line 298
2988 return;
2989}
2990}
2991#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3039/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
2992void ldv_blast_assert(void)
2993{
2994
2995 {
2996 ERROR: ;
2997#line 6
2998 goto ERROR;
2999}
3000}
3001#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3039/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
3002extern int __VERIFIER_nondet_int(void) ;
3003#line 319 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3039/dscv_tempdir/dscv/ri/43_1a/drivers/input/misc/wm831x-on.c.p"
3004int ldv_spin = 0;
3005#line 323 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3039/dscv_tempdir/dscv/ri/43_1a/drivers/input/misc/wm831x-on.c.p"
3006void ldv_check_alloc_flags(gfp_t flags )