3799 goto ldv_18275;
3800 } else
3801#line 831
3802 if (ldv_s_wb_smsc_wdt_fops_file_operations != 0) {
3803#line 833
3804 goto ldv_18275;
3805 } else {
3806#line 835
3807 goto ldv_18277;
3808 }
3809 ldv_18277: ;
3810 ldv_module_exit:
3811 {
3812#line 1021
3813 wb_smsc_wdt_exit();
3814 }
3815 ldv_final:
3816 {
3817#line 1028
3818 ldv_check_final_state();
3819 }
3820#line 1031
3821 return;
3822}
3823}
3824#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
3825void ldv_blast_assert(void)
3826{
3827
3828 {
3829 ERROR: ;
3830#line 6
3831 goto ERROR;
3832}
3833}
3834#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
3835extern int __VERIFIER_nondet_int(void) ;
3836#line 1052 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
3837int ldv_spin = 0;
3838#line 1056 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17363/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/smsc37b787_wdt.c.p"
3839void ldv_check_alloc_flags(gfp_t flags )