6599 tmp___0 = __VERIFIER_nondet_int();
6600 }
6601#line 1290
6602 if (tmp___0 != 0) {
6603#line 1292
6604 goto ldv_24335;
6605 } else
6606#line 1290
6607 if (ldv_s_ds_driver_usb_driver != 0) {
6608#line 1292
6609 goto ldv_24335;
6610 } else {
6611#line 1294
6612 goto ldv_24337;
6613 }
6614 ldv_24337: ;
6615 ldv_module_exit: ;
6616 {
6617#line 1536
6618 ldv_check_final_state();
6619 }
6620#line 1539
6621 return;
6622}
6623}
6624#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4894/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
6625void ldv_blast_assert(void)
6626{
6627
6628 {
6629 ERROR: ;
6630#line 6
6631 goto ERROR;
6632}
6633}
6634#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4894/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
6635extern int __VERIFIER_nondet_int(void) ;
6636#line 1560 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4894/dscv_tempdir/dscv/ri/43_1a/drivers/w1/masters/ds2490.c.p"
6637int ldv_spin = 0;
6638#line 1564 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4894/dscv_tempdir/dscv/ri/43_1a/drivers/w1/masters/ds2490.c.p"
6639void ldv_check_alloc_flags(gfp_t flags )