8321 tmp___0 = __VERIFIER_nondet_int();
8322 }
8323#line 421
8324 if (tmp___0 != 0) {
8325#line 423
8326 goto ldv_38919;
8327 } else
8328#line 421
8329 if (ldv_s_vp7045_usb_driver_usb_driver != 0) {
8330#line 423
8331 goto ldv_38919;
8332 } else {
8333#line 425
8334 goto ldv_38921;
8335 }
8336 ldv_38921: ;
8337 ldv_module_exit: ;
8338 {
8339#line 519
8340 ldv_check_final_state();
8341 }
8342#line 522
8343 return;
8344}
8345}
8346#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/8567/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
8347void ldv_blast_assert(void)
8348{
8349
8350 {
8351 ERROR: ;
8352#line 6
8353 goto ERROR;
8354}
8355}
8356#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/8567/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
8357extern int __VERIFIER_nondet_int(void) ;
8358#line 543 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/8567/dscv_tempdir/dscv/ri/43_1a/drivers/media/dvb/dvb-usb/vp7045.c.p"
8359int ldv_spin = 0;
8360#line 547 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/8567/dscv_tempdir/dscv/ri/43_1a/drivers/media/dvb/dvb-usb/vp7045.c.p"
8361void ldv_check_alloc_flags(gfp_t flags )