7946 } else {
7947
7948 }
7949#line 1124
7950 goto switch_break;
7951 switch_default:
7952#line 1125
7953 goto switch_break;
7954 } else {
7955 switch_break: ;
7956 }
7957 }
7958 }
7959 }
7960 while_break: ;
7961 }
7962 ldv_module_exit:
7963 {
7964#line 1134
7965 ldv_check_final_state();
7966 }
7967#line 1137
7968 return;
7969}
7970}
7971#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4048/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
7972void ldv_blast_assert(void)
7973{
7974
7975 {
7976 ERROR:
7977#line 6
7978 goto ERROR;
7979}
7980}
7981#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4048/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
7982extern int __VERIFIER_nondet_int(void) ;
7983#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4048/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
7984int ldv_mutex = 1;
7985#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4048/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
7986int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )