4570#line 394
4571 tmp___1 = __VERIFIER_nondet_int();
4572 }
4573#line 394
4574 if (tmp___1 != 0) {
4575#line 395
4576 goto ldv_24597;
4577 } else {
4578#line 397
4579 goto ldv_24599;
4580 }
4581 ldv_24599: ;
4582 {
4583#line 464
4584 acpi_container_exit();
4585 }
4586 ldv_final:
4587 {
4588#line 467
4589 ldv_check_final_state();
4590 }
4591#line 470
4592 return;
4593}
4594}
4595#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4603/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
4596void ldv_blast_assert(void)
4597{
4598
4599 {
4600 ERROR: ;
4601#line 6
4602 goto ERROR;
4603}
4604}
4605#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4603/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
4606extern int __VERIFIER_nondet_int(void) ;
4607#line 491 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4603/dscv_tempdir/dscv/ri/43_1a/drivers/acpi/container.c.p"
4608int ldv_spin = 0;
4609#line 495 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4603/dscv_tempdir/dscv/ri/43_1a/drivers/acpi/container.c.p"
4610void ldv_check_alloc_flags(gfp_t flags )