3602 switch_default:
3603#line 579
3604 goto switch_break;
3605 } else {
3606 switch_break: ;
3607 }
3608 }
3609 }
3610 }
3611 while_break: ;
3612 }
3613 ldv_module_exit:
3614 {
3615#line 603
3616 cpu5wdt_exit_module();
3617 }
3618 ldv_final:
3619 {
3620#line 606
3621 ldv_check_final_state();
3622 }
3623#line 609
3624 return;
3625}
3626}
3627#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16397/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
3628void ldv_blast_assert(void)
3629{
3630
3631 {
3632 ERROR:
3633#line 6
3634 goto ERROR;
3635}
3636}
3637#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16397/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
3638extern int __VERIFIER_nondet_int(void) ;
3639#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16397/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3640int ldv_mutex = 1;
3641#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16397/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3642int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )