7170 } else {
7171
7172 }
7173#line 1116
7174 goto switch_break;
7175 switch_default:
7176#line 1117
7177 goto switch_break;
7178 } else {
7179 switch_break: ;
7180 }
7181 }
7182 }
7183 }
7184 while_break: ;
7185 }
7186 ldv_module_exit:
7187 {
7188#line 1126
7189 ldv_check_final_state();
7190 }
7191#line 1129
7192 return;
7193}
7194}
7195#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12601/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
7196void ldv_blast_assert(void)
7197{
7198
7199 {
7200 ERROR:
7201#line 6
7202 goto ERROR;
7203}
7204}
7205#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12601/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
7206extern int __VERIFIER_nondet_int(void) ;
7207#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12601/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
7208int ldv_mutex = 1;
7209#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12601/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
7210int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )