2640#line 163
2641 tmp___1 = __VERIFIER_nondet_int();
2642 }
2643#line 163
2644 if (tmp___1 != 0) {
2645#line 164
2646 goto ldv_19753;
2647 } else {
2648#line 166
2649 goto ldv_19755;
2650 }
2651 ldv_19755: ;
2652 {
2653#line 200
2654 ks_exit();
2655 }
2656 ldv_final:
2657 {
2658#line 203
2659 ldv_check_final_state();
2660 }
2661#line 206
2662 return;
2663}
2664}
2665#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4831/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
2666void ldv_blast_assert(void)
2667{
2668
2669 {
2670 ERROR: ;
2671#line 6
2672 goto ERROR;
2673}
2674}
2675#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4831/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
2676extern int __VERIFIER_nondet_int(void) ;
2677#line 227 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4831/dscv_tempdir/dscv/ri/43_1a/drivers/hid/hid-kensington.c.p"
2678int ldv_spin = 0;
2679#line 231 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4831/dscv_tempdir/dscv/ri/43_1a/drivers/hid/hid-kensington.c.p"
2680void ldv_check_alloc_flags(gfp_t flags )