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