5664 }
5665 ldv_36126: ;
5666 ldv_36131:
5667 {
5668#line 205
5669 tmp___0 = __VERIFIER_nondet_int();
5670 }
5671#line 205
5672 if (tmp___0 != 0) {
5673#line 206
5674 goto ldv_36130;
5675 } else {
5676#line 208
5677 goto ldv_36132;
5678 }
5679 ldv_36132: ;
5680
5681 {
5682#line 267
5683 ldv_check_final_state();
5684 }
5685#line 270
5686 return;
5687}
5688}
5689#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/704/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
5690void ldv_blast_assert(void)
5691{
5692
5693 {
5694 ERROR: ;
5695#line 6
5696 goto ERROR;
5697}
5698}
5699#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/704/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
5700extern int __VERIFIER_nondet_int(void) ;
5701#line 291 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/704/dscv_tempdir/dscv/ri/43_1a/drivers/gpu/drm/drm_usb.c.p"
5702int ldv_spin = 0;
5703#line 295 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/704/dscv_tempdir/dscv/ri/43_1a/drivers/gpu/drm/drm_usb.c.p"
5704void ldv_check_alloc_flags(gfp_t flags )