7624#line 475
7625 tmp___1 = __VERIFIER_nondet_int();
7626 }
7627#line 475
7628 if (tmp___1 != 0) {
7629#line 476
7630 goto ldv_34846;
7631 } else {
7632#line 478
7633 goto ldv_34848;
7634 }
7635 ldv_34848: ;
7636 {
7637#line 525
7638 com20020_module_exit();
7639 }
7640 ldv_final:
7641 {
7642#line 531
7643 ldv_check_final_state();
7644 }
7645#line 534
7646 return;
7647}
7648}
7649#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/13847/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
7650void ldv_blast_assert(void)
7651{
7652
7653 {
7654 ERROR: ;
7655#line 6
7656 goto ERROR;
7657}
7658}
7659#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/13847/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
7660extern int __VERIFIER_nondet_int(void) ;
7661#line 555 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/13847/dscv_tempdir/dscv/ri/43_1a/drivers/net/arcnet/com20020.c.p"
7662int ldv_spin = 0;
7663#line 559 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/13847/dscv_tempdir/dscv/ri/43_1a/drivers/net/arcnet/com20020.c.p"
7664void ldv_check_alloc_flags(gfp_t flags )