1629 goto switch_break;
1630 switch_default:
1631#line 257
1632 goto switch_break;
1633 } else {
1634 switch_break: ;
1635 }
1636 }
1637 }
1638 }
1639 while_break: ;
1640 }
1641 {
1642#line 269
1643 mtdblock_exit();
1644 }
1645 ldv_final:
1646 {
1647#line 272
1648 ldv_check_final_state();
1649 }
1650#line 275
1651 return;
1652}
1653}
1654#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5640/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
1655void ldv_blast_assert(void)
1656{
1657
1658 {
1659 ERROR:
1660#line 6
1661 goto ERROR;
1662}
1663}
1664#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5640/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
1665extern int __VERIFIER_nondet_int(void) ;
1666#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5640/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1667int ldv_mutex = 1;
1668#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5640/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1669int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )