3378 } else {
3379
3380 }
3381#line 236
3382 goto switch_break;
3383 switch_default:
3384#line 237
3385 goto switch_break;
3386 } else {
3387 switch_break: ;
3388 }
3389 }
3390 }
3391 }
3392 while_break: ;
3393 }
3394 ldv_module_exit:
3395 {
3396#line 246
3397 ldv_check_final_state();
3398 }
3399#line 249
3400 return;
3401}
3402}
3403#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1862/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
3404void ldv_blast_assert(void)
3405{
3406
3407 {
3408 ERROR:
3409#line 6
3410 goto ERROR;
3411}
3412}
3413#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1862/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
3414extern int __VERIFIER_nondet_int(void) ;
3415#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1862/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3416int ldv_mutex = 1;
3417#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1862/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3418int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )