4166 goto ldv_29000;
4167 } else
4168#line 217
4169 if (ldv_s_ioapic_driver_pci_driver != 0) {
4170#line 219
4171 goto ldv_29000;
4172 } else {
4173#line 221
4174 goto ldv_29002;
4175 }
4176 ldv_29002: ;
4177 ldv_module_exit:
4178 {
4179#line 254
4180 ioapic_exit();
4181 }
4182 ldv_final:
4183 {
4184#line 257
4185 ldv_check_final_state();
4186 }
4187#line 260
4188 return;
4189}
4190}
4191#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2505/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
4192void ldv_blast_assert(void)
4193{
4194
4195 {
4196 ERROR: ;
4197#line 6
4198 goto ERROR;
4199}
4200}
4201#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2505/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
4202extern int __VERIFIER_nondet_int(void) ;
4203#line 281 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2505/dscv_tempdir/dscv/ri/43_1a/drivers/pci/ioapic.c.p"
4204int ldv_spin = 0;
4205#line 285 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2505/dscv_tempdir/dscv/ri/43_1a/drivers/pci/ioapic.c.p"
4206void ldv_check_alloc_flags(gfp_t flags )