2953#line 328
2954 tmp___1 = __VERIFIER_nondet_int();
2955 }
2956#line 328
2957 if (tmp___1 != 0) {
2958#line 329
2959 goto ldv_20882;
2960 } else {
2961#line 331
2962 goto ldv_20884;
2963 }
2964 ldv_20884: ;
2965 {
2966#line 398
2967 driver_adl_pci7296_cleanup_module();
2968 }
2969 ldv_final:
2970 {
2971#line 401
2972 ldv_check_final_state();
2973 }
2974#line 404
2975 return;
2976}
2977}
2978#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5898/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
2979void ldv_blast_assert(void)
2980{
2981
2982 {
2983 ERROR: ;
2984#line 6
2985 goto ERROR;
2986}
2987}
2988#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5898/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
2989extern int __VERIFIER_nondet_int(void) ;
2990#line 425 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5898/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/adl_pci7296.c.p"
2991int ldv_spin = 0;
2992#line 429 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5898/dscv_tempdir/dscv/ri/43_1a/drivers/staging/comedi/drivers/adl_pci7296.c.p"
2993void ldv_check_alloc_flags(gfp_t flags )