4715 goto switch_break;
4716 switch_default:
4717#line 1139
4718 goto switch_break;
4719 } else {
4720 switch_break: ;
4721 }
4722 }
4723 }
4724 }
4725 while_break: ;
4726 }
4727 {
4728#line 1168
4729 ksphy_exit();
4730 }
4731 ldv_final:
4732 {
4733#line 1171
4734 ldv_check_final_state();
4735 }
4736#line 1174
4737 return;
4738}
4739}
4740#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9667/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
4741void ldv_blast_assert(void)
4742{
4743
4744 {
4745 ERROR:
4746#line 6
4747 goto ERROR;
4748}
4749}
4750#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9667/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
4751extern int __VERIFIER_nondet_int(void) ;
4752#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9667/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4753int ldv_mutex = 1;
4754#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9667/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4755int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )