4657 switch_default:
4658#line 805
4659 goto switch_break;
4660 } else {
4661 switch_break: ;
4662 }
4663 }
4664 }
4665 }
4666 while_break: ;
4667 }
4668 ldv_module_exit:
4669 {
4670#line 817
4671 wm8400_regulator_exit();
4672 }
4673 ldv_final:
4674 {
4675#line 820
4676 ldv_check_final_state();
4677 }
4678#line 823
4679 return;
4680}
4681}
4682#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4595/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
4683void ldv_blast_assert(void)
4684{
4685
4686 {
4687 ERROR:
4688#line 6
4689 goto ERROR;
4690}
4691}
4692#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4595/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
4693extern int __VERIFIER_nondet_int(void) ;
4694#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4595/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4695int ldv_mutex = 1;
4696#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/4595/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4697int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )