4261 goto ldv_22894;
4262 } else
4263#line 461
4264 if (ldv_s_max1586_pmic_driver_i2c_driver != 0) {
4265#line 463
4266 goto ldv_22894;
4267 } else {
4268#line 465
4269 goto ldv_22896;
4270 }
4271 ldv_22896: ;
4272 ldv_module_exit:
4273 {
4274#line 616
4275 max1586_pmic_exit();
4276 }
4277 ldv_final:
4278 {
4279#line 619
4280 ldv_check_final_state();
4281 }
4282#line 622
4283 return;
4284}
4285}
4286#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12235/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
4287void ldv_blast_assert(void)
4288{
4289
4290 {
4291 ERROR: ;
4292#line 6
4293 goto ERROR;
4294}
4295}
4296#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12235/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
4297extern int __VERIFIER_nondet_int(void) ;
4298#line 643 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12235/dscv_tempdir/dscv/ri/43_1a/drivers/regulator/max1586.c.p"
4299int ldv_spin = 0;
4300#line 647 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12235/dscv_tempdir/dscv/ri/43_1a/drivers/regulator/max1586.c.p"
4301void ldv_check_alloc_flags(gfp_t flags )