8314 tmp___0 = __VERIFIER_nondet_int();
8315 }
8316#line 784
8317 if (tmp___0 != 0) {
8318#line 786
8319 goto ldv_30830;
8320 } else
8321#line 784
8322 if (ldv_s_jumpshot_driver_usb_driver != 0) {
8323#line 786
8324 goto ldv_30830;
8325 } else {
8326#line 788
8327 goto ldv_30832;
8328 }
8329 ldv_30832: ;
8330 ldv_module_exit: ;
8331 {
8332#line 836
8333 ldv_check_final_state();
8334 }
8335#line 839
8336 return;
8337}
8338}
8339#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2018/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
8340void ldv_blast_assert(void)
8341{
8342
8343 {
8344 ERROR: ;
8345#line 6
8346 goto ERROR;
8347}
8348}
8349#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2018/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
8350extern int __VERIFIER_nondet_int(void) ;
8351#line 860 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2018/dscv_tempdir/dscv/ri/43_1a/drivers/usb/storage/jumpshot.c.p"
8352int ldv_spin = 0;
8353#line 864 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2018/dscv_tempdir/dscv/ri/43_1a/drivers/usb/storage/jumpshot.c.p"
8354void ldv_check_alloc_flags(gfp_t flags )