3740 tmp___0 = __VERIFIER_nondet_int();
3741 }
3742#line 395
3743 if (tmp___0 != 0) {
3744#line 397
3745 goto ldv_21135;
3746 } else
3747#line 395
3748 if (ldv_s_rotary_encoder_driver_platform_driver != 0) {
3749#line 397
3750 goto ldv_21135;
3751 } else {
3752#line 399
3753 goto ldv_21137;
3754 }
3755 ldv_21137: ;
3756 ldv_module_exit: ;
3757 {
3758#line 467
3759 ldv_check_final_state();
3760 }
3761#line 470
3762 return;
3763}
3764}
3765#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3037/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
3766void ldv_blast_assert(void)
3767{
3768
3769 {
3770 ERROR: ;
3771#line 6
3772 goto ERROR;
3773}
3774}
3775#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3037/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
3776extern int __VERIFIER_nondet_int(void) ;
3777#line 491 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3037/dscv_tempdir/dscv/ri/43_1a/drivers/input/misc/rotary_encoder.c.p"
3778int ldv_spin = 0;
3779#line 495 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3037/dscv_tempdir/dscv/ri/43_1a/drivers/input/misc/rotary_encoder.c.p"
3780void ldv_check_alloc_flags(gfp_t flags )