4514#line 384
4515 tmp___1 = __VERIFIER_nondet_int();
4516 }
4517#line 384
4518 if (tmp___1 != 0) {
4519#line 385
4520 goto ldv_24954;
4521 } else {
4522#line 387
4523 goto ldv_24956;
4524 }
4525 ldv_24956: ;
4526 {
4527#line 553
4528 acpi_fan_exit();
4529 }
4530 ldv_final:
4531 {
4532#line 556
4533 ldv_check_final_state();
4534 }
4535#line 559
4536 return;
4537}
4538}
4539#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4606/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
4540void ldv_blast_assert(void)
4541{
4542
4543 {
4544 ERROR: ;
4545#line 6
4546 goto ERROR;
4547}
4548}
4549#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4606/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
4550extern int __VERIFIER_nondet_int(void) ;
4551#line 580 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4606/dscv_tempdir/dscv/ri/43_1a/drivers/acpi/fan.c.p"
4552int ldv_spin = 0;
4553#line 584 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4606/dscv_tempdir/dscv/ri/43_1a/drivers/acpi/fan.c.p"
4554void ldv_check_alloc_flags(gfp_t flags )