4440#line 340
4441 tmp___1 = __VERIFIER_nondet_int();
4442 }
4443#line 340
4444 if (tmp___1 != 0) {
4445#line 341
4446 goto ldv_18885;
4447 } else {
4448#line 343
4449 goto ldv_18887;
4450 }
4451 ldv_18887: ;
4452 {
4453#line 407
4454 i2c_stub_exit();
4455 }
4456 ldv_final:
4457 {
4458#line 410
4459 ldv_check_final_state();
4460 }
4461#line 413
4462 return;
4463}
4464}
4465#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11392/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
4466void ldv_blast_assert(void)
4467{
4468
4469 {
4470 ERROR: ;
4471#line 6
4472 goto ERROR;
4473}
4474}
4475#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11392/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
4476extern int __VERIFIER_nondet_int(void) ;
4477#line 434 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11392/dscv_tempdir/dscv/ri/43_1a/drivers/i2c/busses/i2c-stub.c.p"
4478int ldv_spin = 0;
4479#line 438 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11392/dscv_tempdir/dscv/ri/43_1a/drivers/i2c/busses/i2c-stub.c.p"
4480void ldv_check_alloc_flags(gfp_t flags )