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