3932#line 537
3933 LDV_IN_INTERRUPT = 1;
3934 }
3935#line 543
3936 goto switch_break;
3937 switch_default:
3938#line 544
3939 goto switch_break;
3940 } else {
3941 switch_break: ;
3942 }
3943 }
3944 }
3945 }
3946 while_break: ;
3947 }
3948 ldv_module_exit:
3949 {
3950#line 553
3951 ldv_check_final_state();
3952 }
3953#line 556
3954 return;
3955}
3956}
3957#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1053/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
3958void ldv_blast_assert(void)
3959{
3960
3961 {
3962 ERROR:
3963#line 6
3964 goto ERROR;
3965}
3966}
3967#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1053/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
3968extern int __VERIFIER_nondet_int(void) ;
3969#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1053/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3970int ldv_mutex = 1;
3971#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1053/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3972int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )