6315 } else {
6316
6317 }
6318#line 603
6319 goto switch_break;
6320 switch_default:
6321#line 604
6322 goto switch_break;
6323 } else {
6324 switch_break: ;
6325 }
6326 }
6327 }
6328 }
6329 while_break: ;
6330 }
6331 ldv_module_exit:
6332 {
6333#line 613
6334 ldv_check_final_state();
6335 }
6336#line 616
6337 return;
6338}
6339}
6340#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7712/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
6341void ldv_blast_assert(void)
6342{
6343
6344 {
6345 ERROR:
6346#line 6
6347 goto ERROR;
6348}
6349}
6350#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7712/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
6351extern int __VERIFIER_nondet_int(void) ;
6352#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7712/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6353int ldv_mutex = 1;
6354#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7712/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6355int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )