8330 tmp___0 = __VERIFIER_nondet_int();
8331 }
8332#line 1599
8333 if (tmp___0 != 0) {
8334#line 1601
8335 goto ldv_27962;
8336 } else
8337#line 1599
8338 if (ldv_s_spcp8x5_device_usb_serial_driver != 0) {
8339#line 1601
8340 goto ldv_27962;
8341 } else {
8342#line 1603
8343 goto ldv_27964;
8344 }
8345 ldv_27964: ;
8346 ldv_module_exit: ;
8347 {
8348#line 2596
8349 ldv_check_final_state();
8350 }
8351#line 2599
8352 return;
8353}
8354}
8355#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1832/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
8356void ldv_blast_assert(void)
8357{
8358
8359 {
8360 ERROR: ;
8361#line 6
8362 goto ERROR;
8363}
8364}
8365#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1832/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
8366extern int __VERIFIER_nondet_int(void) ;
8367#line 2620 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1832/dscv_tempdir/dscv/ri/43_1a/drivers/usb/serial/spcp8x5.c.p"
8368int ldv_spin = 0;
8369#line 2624 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1832/dscv_tempdir/dscv/ri/43_1a/drivers/usb/serial/spcp8x5.c.p"
8370void ldv_check_alloc_flags(gfp_t flags )