7002#line 541
7003 tmp___1 = __VERIFIER_nondet_int();
7004 }
7005#line 541
7006 if (tmp___1 != 0) {
7007#line 542
7008 goto ldv_35000;
7009 } else {
7010#line 544
7011 goto ldv_35002;
7012 }
7013 ldv_35002: ;
7014 {
7015#line 588
7016 com90io_exit();
7017 }
7018 ldv_final:
7019 {
7020#line 591
7021 ldv_check_final_state();
7022 }
7023#line 594
7024 return;
7025}
7026}
7027#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/13849/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
7028void ldv_blast_assert(void)
7029{
7030
7031 {
7032 ERROR: ;
7033#line 6
7034 goto ERROR;
7035}
7036}
7037#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/13849/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
7038extern int __VERIFIER_nondet_int(void) ;
7039#line 615 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/13849/dscv_tempdir/dscv/ri/43_1a/drivers/net/arcnet/com90io.c.p"
7040int ldv_spin = 0;
7041#line 619 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/13849/dscv_tempdir/dscv/ri/43_1a/drivers/net/arcnet/com90io.c.p"
7042void ldv_check_alloc_flags(gfp_t flags )