6970 }
6971 ldv_22613: ;
6972 ldv_22625:
6973 {
6974#line 1159
6975 tmp___0 = __VERIFIER_nondet_int();
6976 }
6977#line 1159
6978 if (tmp___0 != 0) {
6979#line 1160
6980 goto ldv_22624;
6981 } else {
6982#line 1162
6983 goto ldv_22626;
6984 }
6985 ldv_22626: ;
6986
6987 {
6988#line 1637
6989 ldv_check_final_state();
6990 }
6991#line 1640
6992 return;
6993}
6994}
6995#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5690/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
6996void ldv_blast_assert(void)
6997{
6998
6999 {
7000 ERROR: ;
7001#line 6
7002 goto ERROR;
7003}
7004}
7005#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5690/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
7006extern int __VERIFIER_nondet_int(void) ;
7007#line 1661 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5690/dscv_tempdir/dscv/ri/43_1a/drivers/staging/media/cxd2099/cxd2099.c.p"
7008int ldv_spin = 0;
7009#line 1665 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/5690/dscv_tempdir/dscv/ri/43_1a/drivers/staging/media/cxd2099/cxd2099.c.p"
7010void ldv_check_alloc_flags(gfp_t flags )