5806 }
5807 ldv_36134: ;
5808 ldv_36137:
5809 {
5810#line 248
5811 tmp___0 = __VERIFIER_nondet_int();
5812 }
5813#line 248
5814 if (tmp___0 != 0) {
5815#line 249
5816 goto ldv_36136;
5817 } else {
5818#line 251
5819 goto ldv_36138;
5820 }
5821 ldv_36138: ;
5822
5823 {
5824#line 286
5825 ldv_check_final_state();
5826 }
5827#line 289
5828 return;
5829}
5830}
5831#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12747/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
5832void ldv_blast_assert(void)
5833{
5834
5835 {
5836 ERROR: ;
5837#line 6
5838 goto ERROR;
5839}
5840}
5841#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12747/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
5842extern int __VERIFIER_nondet_int(void) ;
5843#line 310 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12747/dscv_tempdir/dscv/ri/43_1a/drivers/net/usb/plusb.c.p"
5844int ldv_spin = 0;
5845#line 314 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12747/dscv_tempdir/dscv/ri/43_1a/drivers/net/usb/plusb.c.p"
5846void ldv_check_alloc_flags(gfp_t flags )