12979 goto ldv_29714;
12980 } else
12981#line 2659
12982 if (ldv_s_hsu_pci_driver_pci_driver != 0) {
12983#line 2663
12984 goto ldv_29714;
12985 } else {
12986#line 2665
12987 goto ldv_29716;
12988 }
12989 ldv_29716: ;
12990 ldv_module_exit:
12991 {
12992#line 4078
12993 hsu_pci_exit();
12994 }
12995 ldv_final:
12996 {
12997#line 4081
12998 ldv_check_final_state();
12999 }
13000#line 4084
13001 return;
13002}
13003}
13004#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17428/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
13005void ldv_blast_assert(void)
13006{
13007
13008 {
13009 ERROR: ;
13010#line 6
13011 goto ERROR;
13012}
13013}
13014#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17428/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
13015extern int __VERIFIER_nondet_int(void) ;
13016#line 4105 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17428/dscv_tempdir/dscv/ri/43_1a/drivers/tty/serial/mfd.c.p"
13017int ldv_spin = 0;
13018#line 4109 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17428/dscv_tempdir/dscv/ri/43_1a/drivers/tty/serial/mfd.c.p"
13019void ldv_check_alloc_flags(gfp_t flags )