5974 goto switch_break;
5975 switch_default:
5976#line 410
5977 goto switch_break;
5978 } else {
5979 switch_break: ;
5980 }
5981 }
5982 }
5983 }
5984 while_break: ;
5985 }
5986 {
5987#line 428
5988 ste10Xp_exit();
5989 }
5990 ldv_final:
5991 {
5992#line 431
5993 ldv_check_final_state();
5994 }
5995#line 434
5996 return;
5997}
5998}
5999#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9673/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
6000void ldv_blast_assert(void)
6001{
6002
6003 {
6004 ERROR:
6005#line 6
6006 goto ERROR;
6007}
6008}
6009#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9673/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
6010extern int __VERIFIER_nondet_int(void) ;
6011#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9673/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6012int ldv_mutex = 1;
6013#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9673/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6014int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )