4848 goto switch_break;
4849 switch_default:
4850#line 431
4851 goto switch_break;
4852 } else {
4853 switch_break: ;
4854 }
4855 }
4856 }
4857 }
4858 while_break: ;
4859 }
4860 {
4861#line 450
4862 acpi_container_exit();
4863 }
4864 ldv_final:
4865 {
4866#line 453
4867 ldv_check_final_state();
4868 }
4869#line 456
4870 return;
4871}
4872}
4873#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/91/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
4874void ldv_blast_assert(void)
4875{
4876
4877 {
4878 ERROR:
4879#line 6
4880 goto ERROR;
4881}
4882}
4883#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/91/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
4884extern int __VERIFIER_nondet_int(void) ;
4885#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/91/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4886int ldv_mutex = 1;
4887#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/91/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4888int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )