4611 goto switch_break;
4612 switch_default:
4613#line 780
4614 goto switch_break;
4615 } else {
4616 switch_break: ;
4617 }
4618 }
4619 }
4620 }
4621 while_break: ;
4622 }
4623 {
4624#line 798
4625 mc13xxx_rtc_exit();
4626 }
4627 ldv_final:
4628 {
4629#line 801
4630 ldv_check_final_state();
4631 }
4632#line 804
4633 return;
4634}
4635}
4636#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6246/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
4637void ldv_blast_assert(void)
4638{
4639
4640 {
4641 ERROR:
4642#line 6
4643 goto ERROR;
4644}
4645}
4646#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6246/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
4647extern int __VERIFIER_nondet_int(void) ;
4648#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6246/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4649int ldv_mutex = 1;
4650#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6246/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4651int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )