11073 goto switch_break;
11074 switch_default:
11075#line 700
11076 goto switch_break;
11077 } else {
11078 switch_break: ;
11079 }
11080 }
11081 }
11082 }
11083 while_break: ;
11084 }
11085 {
11086#line 718
11087 frpw_exit();
11088 }
11089 ldv_final:
11090 {
11091#line 721
11092 ldv_check_final_state();
11093 }
11094#line 724
11095 return;
11096}
11097}
11098#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16805/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
11099void ldv_blast_assert(void)
11100{
11101
11102 {
11103 ERROR:
11104#line 6
11105 goto ERROR;
11106}
11107}
11108#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16805/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
11109extern int __VERIFIER_nondet_int(void) ;
11110#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16805/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
11111int ldv_mutex = 1;
11112#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16805/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
11113int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )