4091 goto ldv_20246;
4092 } else
4093#line 367
4094 if (ldv_s_smbalert_driver_i2c_driver != 0) {
4095#line 369
4096 goto ldv_20246;
4097 } else {
4098#line 371
4099 goto ldv_20248;
4100 }
4101 ldv_20248: ;
4102 ldv_module_exit:
4103 {
4104#line 439
4105 i2c_smbus_exit();
4106 }
4107 ldv_final:
4108 {
4109#line 442
4110 ldv_check_final_state();
4111 }
4112#line 445
4113 return;
4114}
4115}
4116#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11475/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
4117void ldv_blast_assert(void)
4118{
4119
4120 {
4121 ERROR: ;
4122#line 6
4123 goto ERROR;
4124}
4125}
4126#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11475/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
4127extern int __VERIFIER_nondet_int(void) ;
4128#line 466 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11475/dscv_tempdir/dscv/ri/43_1a/drivers/i2c/i2c-smbus.c.p"
4129int ldv_spin = 0;
4130#line 470 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11475/dscv_tempdir/dscv/ri/43_1a/drivers/i2c/i2c-smbus.c.p"
4131void ldv_check_alloc_flags(gfp_t flags )