6454#line 367
6455 tmp___1 = __VERIFIER_nondet_int();
6456 }
6457#line 367
6458 if (tmp___1 != 0) {
6459#line 368
6460 goto ldv_35717;
6461 } else {
6462#line 370
6463 goto ldv_35719;
6464 }
6465 ldv_35719: ;
6466 {
6467#line 440
6468 arcnet_rfc1051_exit();
6469 }
6470 ldv_final:
6471 {
6472#line 443
6473 ldv_check_final_state();
6474 }
6475#line 446
6476 return;
6477}
6478}
6479#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/13851/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
6480void ldv_blast_assert(void)
6481{
6482
6483 {
6484 ERROR: ;
6485#line 6
6486 goto ERROR;
6487}
6488}
6489#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/13851/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
6490extern int __VERIFIER_nondet_int(void) ;
6491#line 467 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/13851/dscv_tempdir/dscv/ri/43_1a/drivers/net/arcnet/rfc1051.c.p"
6492int ldv_spin = 0;
6493#line 471 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/13851/dscv_tempdir/dscv/ri/43_1a/drivers/net/arcnet/rfc1051.c.p"
6494void ldv_check_alloc_flags(gfp_t flags )