7401 tmp___0 = __VERIFIER_nondet_int();
7402 }
7403#line 627
7404 if (tmp___0 != 0) {
7405#line 629
7406 goto ldv_27934;
7407 } else
7408#line 627
7409 if (ldv_s_metrousb_device_usb_serial_driver != 0) {
7410#line 629
7411 goto ldv_27934;
7412 } else {
7413#line 631
7414 goto ldv_27936;
7415 }
7416 ldv_27936: ;
7417 ldv_module_exit: ;
7418 {
7419#line 906
7420 ldv_check_final_state();
7421 }
7422#line 909
7423 return;
7424}
7425}
7426#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1817/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
7427void ldv_blast_assert(void)
7428{
7429
7430 {
7431 ERROR: ;
7432#line 6
7433 goto ERROR;
7434}
7435}
7436#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1817/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
7437extern int __VERIFIER_nondet_int(void) ;
7438#line 930 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1817/dscv_tempdir/dscv/ri/43_1a/drivers/usb/serial/metro-usb.c.p"
7439int ldv_spin = 0;
7440#line 934 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1817/dscv_tempdir/dscv/ri/43_1a/drivers/usb/serial/metro-usb.c.p"
7441void ldv_check_alloc_flags(gfp_t flags )