5902 goto ldv_36024;
5903 } else
5904#line 344
5905 if (ldv_s_opti_pci_driver_pci_driver != 0) {
5906#line 346
5907 goto ldv_36024;
5908 } else {
5909#line 348
5910 goto ldv_36026;
5911 }
5912 ldv_36026: ;
5913 ldv_module_exit:
5914 {
5915#line 439
5916 opti_exit();
5917 }
5918 ldv_final:
5919 {
5920#line 442
5921 ldv_check_final_state();
5922 }
5923#line 445
5924 return;
5925}
5926}
5927#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17126/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
5928void ldv_blast_assert(void)
5929{
5930
5931 {
5932 ERROR: ;
5933#line 6
5934 goto ERROR;
5935}
5936}
5937#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17126/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
5938extern int __VERIFIER_nondet_int(void) ;
5939#line 466 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17126/dscv_tempdir/dscv/ri/43_1a/drivers/ata/pata_opti.c.p"
5940int ldv_spin = 0;
5941#line 470 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17126/dscv_tempdir/dscv/ri/43_1a/drivers/ata/pata_opti.c.p"
5942void ldv_check_alloc_flags(gfp_t flags )