10540 goto switch_break;
10541 switch_default:
10542#line 1682
10543 goto switch_break;
10544 } else {
10545 switch_break: ;
10546 }
10547 }
10548 }
10549 }
10550 while_break: ;
10551 }
10552 {
10553#line 1721
10554 cleanup_ftl();
10555 }
10556 ldv_final:
10557 {
10558#line 1724
10559 ldv_check_final_state();
10560 }
10561#line 1727
10562 return;
10563}
10564}
10565#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5616/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
10566void ldv_blast_assert(void)
10567{
10568
10569 {
10570 ERROR:
10571#line 6
10572 goto ERROR;
10573}
10574}
10575#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5616/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
10576extern int __VERIFIER_nondet_int(void) ;
10577#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5616/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
10578int ldv_mutex = 1;
10579#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5616/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
10580int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )