6436 tmp___0 = __VERIFIER_nondet_int();
6437 }
6438#line 676
6439 if (tmp___0 != 0) {
6440#line 678
6441 goto ldv_30798;
6442 } else
6443#line 676
6444 if (ldv_s_freecom_driver_usb_driver != 0) {
6445#line 678
6446 goto ldv_30798;
6447 } else {
6448#line 680
6449 goto ldv_30800;
6450 }
6451 ldv_30800: ;
6452 ldv_module_exit: ;
6453 {
6454#line 744
6455 ldv_check_final_state();
6456 }
6457#line 747
6458 return;
6459}
6460}
6461#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2016/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
6462void ldv_blast_assert(void)
6463{
6464
6465 {
6466 ERROR: ;
6467#line 6
6468 goto ERROR;
6469}
6470}
6471#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2016/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
6472extern int __VERIFIER_nondet_int(void) ;
6473#line 768 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2016/dscv_tempdir/dscv/ri/43_1a/drivers/usb/storage/freecom.c.p"
6474int ldv_spin = 0;
6475#line 772 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2016/dscv_tempdir/dscv/ri/43_1a/drivers/usb/storage/freecom.c.p"
6476void ldv_check_alloc_flags(gfp_t flags )