3847 goto switch_break;
3848 switch_default:
3849#line 771
3850 goto switch_break;
3851 } else {
3852 switch_break: ;
3853 }
3854 }
3855 }
3856 }
3857 while_break: ;
3858 }
3859 {
3860#line 799
3861 unioxx5_driver_cleanup_module();
3862 }
3863 ldv_final:
3864 {
3865#line 806
3866 ldv_check_final_state();
3867 }
3868#line 809
3869 return;
3870}
3871}
3872#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1483/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
3873void ldv_blast_assert(void)
3874{
3875
3876 {
3877 ERROR:
3878#line 6
3879 goto ERROR;
3880}
3881}
3882#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1483/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
3883extern int __VERIFIER_nondet_int(void) ;
3884#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1483/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3885int ldv_mutex = 1;
3886#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1483/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3887int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )