5961 tmp___0 = __VERIFIER_nondet_int();
5962 }
5963#line 543
5964 if (tmp___0 != 0) {
5965#line 545
5966 goto ldv_24073;
5967 } else
5968#line 543
5969 if (ldv_s_cytherm_driver_usb_driver != 0) {
5970#line 545
5971 goto ldv_24073;
5972 } else {
5973#line 547
5974 goto ldv_24075;
5975 }
5976 ldv_24075: ;
5977 ldv_module_exit: ;
5978 {
5979#line 627
5980 ldv_check_final_state();
5981 }
5982#line 630
5983 return;
5984}
5985}
5986#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1911/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
5987void ldv_blast_assert(void)
5988{
5989
5990 {
5991 ERROR: ;
5992#line 6
5993 goto ERROR;
5994}
5995}
5996#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1911/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
5997extern int __VERIFIER_nondet_int(void) ;
5998#line 651 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1911/dscv_tempdir/dscv/ri/43_1a/drivers/usb/misc/cytherm.c.p"
5999int ldv_spin = 0;
6000#line 655 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1911/dscv_tempdir/dscv/ri/43_1a/drivers/usb/misc/cytherm.c.p"
6001void ldv_check_alloc_flags(gfp_t flags )