4973 } else {
4974
4975 }
4976#line 420
4977 goto switch_break;
4978 switch_default:
4979#line 421
4980 goto switch_break;
4981 } else {
4982 switch_break: ;
4983 }
4984 }
4985 }
4986 }
4987 while_break: ;
4988 }
4989 ldv_module_exit:
4990 {
4991#line 430
4992 ldv_check_final_state();
4993 }
4994#line 433
4995 return;
4996}
4997}
4998#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6253/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
4999void ldv_blast_assert(void)
5000{
5001
5002 {
5003 ERROR:
5004#line 6
5005 goto ERROR;
5006}
5007}
5008#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6253/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
5009extern int __VERIFIER_nondet_int(void) ;
5010#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6253/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5011int ldv_mutex = 1;
5012#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6253/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5013int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )