7354 goto switch_break;
7355 switch_default:
7356#line 530
7357 goto switch_break;
7358 } else {
7359 switch_break: ;
7360 }
7361 }
7362 }
7363 }
7364 while_break: ;
7365 }
7366 {
7367#line 547
7368 comm_exit();
7369 }
7370 ldv_final:
7371 {
7372#line 550
7373 ldv_check_final_state();
7374 }
7375#line 553
7376 return;
7377}
7378}
7379#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16798/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
7380void ldv_blast_assert(void)
7381{
7382
7383 {
7384 ERROR:
7385#line 6
7386 goto ERROR;
7387}
7388}
7389#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16798/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
7390extern int __VERIFIER_nondet_int(void) ;
7391#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16798/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
7392int ldv_mutex = 1;
7393#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16798/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
7394int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )