3037 goto ldv_20663;
3038 } else
3039#line 374
3040 if (ldv_s_epx_c3_fops_file_operations != 0) {
3041#line 376
3042 goto ldv_20663;
3043 } else {
3044#line 378
3045 goto ldv_20665;
3046 }
3047 ldv_20665: ;
3048 ldv_module_exit:
3049 {
3050#line 508
3051 watchdog_exit();
3052 }
3053 ldv_final:
3054 {
3055#line 511
3056 ldv_check_final_state();
3057 }
3058#line 514
3059 return;
3060}
3061}
3062#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17358/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
3063void ldv_blast_assert(void)
3064{
3065
3066 {
3067 ERROR: ;
3068#line 6
3069 goto ERROR;
3070}
3071}
3072#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17358/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
3073extern int __VERIFIER_nondet_int(void) ;
3074#line 535 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17358/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sbc_epx_c3.c.p"
3075int ldv_spin = 0;
3076#line 539 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17358/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sbc_epx_c3.c.p"
3077void ldv_check_alloc_flags(gfp_t flags )