2797 goto ldv_23576;
2798 } else
2799#line 216
2800 if (ldv_s_vmic_driver_pci_driver != 0) {
2801#line 218
2802 goto ldv_23576;
2803 } else {
2804#line 220
2805 goto ldv_23578;
2806 }
2807 ldv_23578: ;
2808 ldv_module_exit:
2809 {
2810#line 269
2811 vmic_exit();
2812 }
2813 ldv_final:
2814 {
2815#line 272
2816 ldv_check_final_state();
2817 }
2818#line 275
2819 return;
2820}
2821}
2822#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5074/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
2823void ldv_blast_assert(void)
2824{
2825
2826 {
2827 ERROR: ;
2828#line 6
2829 goto ERROR;
2830}
2831}
2832#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5074/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
2833extern int __VERIFIER_nondet_int(void) ;
2834#line 296 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5074/dscv_tempdir/dscv/ri/43_1a/drivers/staging/vme/boards/vme_vmivme7805.c.p"
2835int ldv_spin = 0;
2836#line 300 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5074/dscv_tempdir/dscv/ri/43_1a/drivers/staging/vme/boards/vme_vmivme7805.c.p"
2837void ldv_check_alloc_flags(gfp_t flags )