12965 } else {
12966
12967 }
12968#line 1979
12969 goto switch_break;
12970 switch_default:
12971#line 1980
12972 goto switch_break;
12973 } else {
12974 switch_break: ;
12975 }
12976 }
12977 }
12978 }
12979 while_break: ;
12980 }
12981 ldv_module_exit:
12982 {
12983#line 1989
12984 ldv_check_final_state();
12985 }
12986#line 1992
12987 return;
12988}
12989}
12990#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13522/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
12991void ldv_blast_assert(void)
12992{
12993
12994 {
12995 ERROR:
12996#line 6
12997 goto ERROR;
12998}
12999}
13000#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13522/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
13001extern int __VERIFIER_nondet_int(void) ;
13002#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13522/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
13003int ldv_mutex = 1;
13004#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/13522/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
13005int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )