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