3266 switch_default:
3267#line 352
3268 goto switch_break;
3269 } else {
3270 switch_break: ;
3271 }
3272 }
3273 }
3274 }
3275 while_break: ;
3276 }
3277 ldv_module_exit:
3278 {
3279#line 367
3280 fujitsu_exit();
3281 }
3282 ldv_final:
3283 {
3284#line 370
3285 ldv_check_final_state();
3286 }
3287#line 373
3288 return;
3289}
3290}
3291#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4175/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
3292void ldv_blast_assert(void)
3293{
3294
3295 {
3296 ERROR:
3297#line 6
3298 goto ERROR;
3299}
3300}
3301#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4175/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
3302extern int __VERIFIER_nondet_int(void) ;
3303#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4175/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3304int ldv_mutex = 1;
3305#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4175/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3306int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )