4533#line 2096
4534 tmp___1 = __VERIFIER_nondet_int();
4535 }
4536#line 2096
4537 if (tmp___1 != 0) {
4538#line 2097
4539 goto ldv_14618;
4540 } else {
4541#line 2099
4542 goto ldv_14620;
4543 }
4544 ldv_14620: ;
4545 {
4546#line 3029
4547 bsdcomp_cleanup();
4548 }
4549 ldv_final:
4550 {
4551#line 3032
4552 ldv_check_final_state();
4553 }
4554#line 3035
4555 return;
4556}
4557}
4558#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
4559void ldv_blast_assert(void)
4560{
4561
4562 {
4563 ERROR: ;
4564#line 6
4565 goto ERROR;
4566}
4567}
4568#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
4569extern int __VERIFIER_nondet_int(void) ;
4570#line 3056 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
4571int ldv_spin = 0;
4572#line 3060 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/15261/dscv_tempdir/dscv/ri/43_1a/drivers/net/ppp/bsd_comp.c.p"
4573void ldv_check_alloc_flags(gfp_t flags )