9523 tmp___0 = __VERIFIER_nondet_int();
9524 }
9525#line 1232
9526 if (tmp___0 != 0) {
9527#line 1234
9528 goto ldv_19711;
9529 } else
9530#line 1232
9531 if (ldv_s_bd2802_i2c_driver_i2c_driver != 0) {
9532#line 1234
9533 goto ldv_19711;
9534 } else {
9535#line 1236
9536 goto ldv_19713;
9537 }
9538 ldv_19713: ;
9539 ldv_module_exit: ;
9540 {
9541#line 1610
9542 ldv_check_final_state();
9543 }
9544#line 1613
9545 return;
9546}
9547}
9548#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12440/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
9549void ldv_blast_assert(void)
9550{
9551
9552 {
9553 ERROR: ;
9554#line 6
9555 goto ERROR;
9556}
9557}
9558#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12440/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
9559extern int __VERIFIER_nondet_int(void) ;
9560#line 1634 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12440/dscv_tempdir/dscv/ri/43_1a/drivers/leds/leds-bd2802.c.p"
9561int ldv_spin = 0;
9562#line 1638 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12440/dscv_tempdir/dscv/ri/43_1a/drivers/leds/leds-bd2802.c.p"
9563void ldv_check_alloc_flags(gfp_t flags )