4044 goto ldv_24996;
4045 } else
4046#line 358
4047 if (ldv_s_sercos3_pci_driver_pci_driver != 0) {
4048#line 360
4049 goto ldv_24996;
4050 } else {
4051#line 362
4052 goto ldv_24998;
4053 }
4054 ldv_24998: ;
4055 ldv_module_exit:
4056 {
4057#line 432
4058 sercos3_exit_module();
4059 }
4060 ldv_final:
4061 {
4062#line 435
4063 ldv_check_final_state();
4064 }
4065#line 438
4066 return;
4067}
4068}
4069#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11183/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
4070void ldv_blast_assert(void)
4071{
4072
4073 {
4074 ERROR: ;
4075#line 6
4076 goto ERROR;
4077}
4078}
4079#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11183/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
4080extern int __VERIFIER_nondet_int(void) ;
4081#line 459 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11183/dscv_tempdir/dscv/ri/43_1a/drivers/uio/uio_sercos3.c.p"
4082int ldv_spin = 0;
4083#line 463 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11183/dscv_tempdir/dscv/ri/43_1a/drivers/uio/uio_sercos3.c.p"
4084void ldv_check_alloc_flags(gfp_t flags )