5263 }
5264 ldv_18977: ;
5265 ldv_18981:
5266 {
5267#line 681
5268 tmp___0 = __VERIFIER_nondet_int();
5269 }
5270#line 681
5271 if (tmp___0 != 0) {
5272#line 682
5273 goto ldv_18980;
5274 } else {
5275#line 684
5276 goto ldv_18982;
5277 }
5278 ldv_18982: ;
5279
5280 {
5281#line 757
5282 ldv_check_final_state();
5283 }
5284#line 760
5285 return;
5286}
5287}
5288#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11328/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
5289void ldv_blast_assert(void)
5290{
5291
5292 {
5293 ERROR: ;
5294#line 6
5295 goto ERROR;
5296}
5297}
5298#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11328/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
5299extern int __VERIFIER_nondet_int(void) ;
5300#line 781 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11328/dscv_tempdir/dscv/ri/43_1a/drivers/i2c/algos/i2c-algo-pca.c.p"
5301int ldv_spin = 0;
5302#line 785 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11328/dscv_tempdir/dscv/ri/43_1a/drivers/i2c/algos/i2c-algo-pca.c.p"
5303void ldv_check_alloc_flags(gfp_t flags )