3347 } else {
3348
3349 }
3350#line 272
3351 goto switch_break;
3352 switch_default:
3353#line 273
3354 goto switch_break;
3355 } else {
3356 switch_break: ;
3357 }
3358 }
3359 }
3360 }
3361 while_break: ;
3362 }
3363 ldv_module_exit:
3364 {
3365#line 282
3366 ldv_check_final_state();
3367 }
3368#line 285
3369 return;
3370}
3371}
3372#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7680/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
3373void ldv_blast_assert(void)
3374{
3375
3376 {
3377 ERROR:
3378#line 6
3379 goto ERROR;
3380}
3381}
3382#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7680/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
3383extern int __VERIFIER_nondet_int(void) ;
3384#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7680/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3385int ldv_mutex = 1;
3386#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7680/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3387int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )