2891 tmp___0 = __VERIFIER_nondet_int();
2892 }
2893#line 639
2894 if (tmp___0 != 0) {
2895#line 641
2896 goto ldv_14634;
2897 } else
2898#line 639
2899 if (ldv_s_iscsi_boot_ktype_kobj_type != 0) {
2900#line 641
2901 goto ldv_14634;
2902 } else {
2903#line 643
2904 goto ldv_14636;
2905 }
2906 ldv_14636: ;
2907
2908 {
2909#line 766
2910 ldv_check_final_state();
2911 }
2912#line 769
2913 return;
2914}
2915}
2916#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3997/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
2917void ldv_blast_assert(void)
2918{
2919
2920 {
2921 ERROR: ;
2922#line 6
2923 goto ERROR;
2924}
2925}
2926#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3997/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
2927extern int __VERIFIER_nondet_int(void) ;
2928#line 790 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3997/dscv_tempdir/dscv/ri/43_1a/drivers/scsi/iscsi_boot_sysfs.c.p"
2929int ldv_spin = 0;
2930#line 794 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/3997/dscv_tempdir/dscv/ri/43_1a/drivers/scsi/iscsi_boot_sysfs.c.p"
2931void ldv_check_alloc_flags(gfp_t flags )