5283 tmp___0 = __VERIFIER_nondet_int();
5284 }
5285#line 414
5286 if (tmp___0 != 0) {
5287#line 416
5288 goto ldv_24366;
5289 } else
5290#line 414
5291 if (ldv_s_i2c_tiny_usb_driver_usb_driver != 0) {
5292#line 416
5293 goto ldv_24366;
5294 } else {
5295#line 418
5296 goto ldv_24368;
5297 }
5298 ldv_24368: ;
5299 ldv_module_exit: ;
5300 {
5301#line 540
5302 ldv_check_final_state();
5303 }
5304#line 543
5305 return;
5306}
5307}
5308#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11394/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
5309void ldv_blast_assert(void)
5310{
5311
5312 {
5313 ERROR: ;
5314#line 6
5315 goto ERROR;
5316}
5317}
5318#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11394/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
5319extern int __VERIFIER_nondet_int(void) ;
5320#line 564 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11394/dscv_tempdir/dscv/ri/43_1a/drivers/i2c/busses/i2c-tiny-usb.c.p"
5321int ldv_spin = 0;
5322#line 568 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11394/dscv_tempdir/dscv/ri/43_1a/drivers/i2c/busses/i2c-tiny-usb.c.p"
5323void ldv_check_alloc_flags(gfp_t flags )