1904 goto ldv_19904;
1905 } else
1906#line 187
1907 if (ldv_s_stub_driver_pci_driver != 0) {
1908#line 189
1909 goto ldv_19904;
1910 } else {
1911#line 191
1912 goto ldv_19906;
1913 }
1914 ldv_19906: ;
1915 ldv_module_exit:
1916 {
1917#line 224
1918 pci_stub_exit();
1919 }
1920 ldv_final:
1921 {
1922#line 227
1923 ldv_check_final_state();
1924 }
1925#line 230
1926 return;
1927}
1928}
1929#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2506/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
1930void ldv_blast_assert(void)
1931{
1932
1933 {
1934 ERROR: ;
1935#line 6
1936 goto ERROR;
1937}
1938}
1939#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2506/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
1940extern int __VERIFIER_nondet_int(void) ;
1941#line 251 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2506/dscv_tempdir/dscv/ri/43_1a/drivers/pci/pci-stub.c.p"
1942int ldv_spin = 0;
1943#line 255 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2506/dscv_tempdir/dscv/ri/43_1a/drivers/pci/pci-stub.c.p"
1944void ldv_check_alloc_flags(gfp_t flags )