3864 goto ldv_19257;
3865 } else
3866#line 496
3867 if (ldv_s_acquirewdt_driver_platform_driver != 0) {
3868#line 499
3869 goto ldv_19257;
3870 } else {
3871#line 501
3872 goto ldv_19259;
3873 }
3874 ldv_19259: ;
3875 ldv_module_exit:
3876 {
3877#line 655
3878 acq_exit();
3879 }
3880 ldv_final:
3881 {
3882#line 658
3883 ldv_check_final_state();
3884 }
3885#line 661
3886 return;
3887}
3888}
3889#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17335/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
3890void ldv_blast_assert(void)
3891{
3892
3893 {
3894 ERROR: ;
3895#line 6
3896 goto ERROR;
3897}
3898}
3899#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17335/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
3900extern int __VERIFIER_nondet_int(void) ;
3901#line 682 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17335/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/acquirewdt.c.p"
3902int ldv_spin = 0;
3903#line 686 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17335/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/acquirewdt.c.p"
3904void ldv_check_alloc_flags(gfp_t flags )