13511 tmp___0 = __VERIFIER_nondet_int();
13512 }
13513#line 3102
13514 if (tmp___0 != 0) {
13515#line 3104
13516 goto ldv_28294;
13517 } else
13518#line 3102
13519 if (ldv_s_quatech_device_usb_serial_driver != 0) {
13520#line 3104
13521 goto ldv_28294;
13522 } else {
13523#line 3106
13524 goto ldv_28296;
13525 }
13526 ldv_28296: ;
13527 ldv_module_exit: ;
13528 {
13529#line 4710
13530 ldv_check_final_state();
13531 }
13532#line 4713
13533 return;
13534}
13535}
13536#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/6284/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
13537void ldv_blast_assert(void)
13538{
13539
13540 {
13541 ERROR: ;
13542#line 6
13543 goto ERROR;
13544}
13545}
13546#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/6284/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
13547extern int __VERIFIER_nondet_int(void) ;
13548#line 4734 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/6284/dscv_tempdir/dscv/ri/43_1a/drivers/staging/serqt_usb2/serqt_usb2.c.p"
13549int ldv_spin = 0;
13550#line 4738 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/6284/dscv_tempdir/dscv/ri/43_1a/drivers/staging/serqt_usb2/serqt_usb2.c.p"
13551void ldv_check_alloc_flags(gfp_t flags )