2725#line 525
2726 tmp___1 = __VERIFIER_nondet_int();
2727 }
2728#line 525
2729 if (tmp___1 != 0) {
2730#line 526
2731 goto ldv_19754;
2732 } else {
2733#line 528
2734 goto ldv_19756;
2735 }
2736 ldv_19756: ;
2737 {
2738#line 566
2739 uclogic_exit();
2740 }
2741 ldv_final:
2742 {
2743#line 569
2744 ldv_check_final_state();
2745 }
2746#line 572
2747 return;
2748}
2749}
2750#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4865/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
2751void ldv_blast_assert(void)
2752{
2753
2754 {
2755 ERROR: ;
2756#line 6
2757 goto ERROR;
2758}
2759}
2760#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4865/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
2761extern int __VERIFIER_nondet_int(void) ;
2762#line 593 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4865/dscv_tempdir/dscv/ri/43_1a/drivers/hid/hid-uclogic.c.p"
2763int ldv_spin = 0;
2764#line 597 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4865/dscv_tempdir/dscv/ri/43_1a/drivers/hid/hid-uclogic.c.p"
2765void ldv_check_alloc_flags(gfp_t flags )