975#line 474
976 tmp___1 = __VERIFIER_nondet_int();
977 }
978#line 474
979 if (tmp___1 != 0) {
980#line 475
981 goto ldv_14343;
982 } else {
983#line 477
984 goto ldv_14345;
985 }
986 ldv_14345: ;
987 {
988#line 511
989 iTCO_vendor_exit_module();
990 }
991 ldv_final:
992 {
993#line 514
994 ldv_check_final_state();
995 }
996#line 517
997 return;
998}
999}
1000#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17345/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
1001void ldv_blast_assert(void)
1002{
1003
1004 {
1005 ERROR: ;
1006#line 6
1007 goto ERROR;
1008}
1009}
1010#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17345/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
1011extern int __VERIFIER_nondet_int(void) ;
1012#line 538 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17345/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/iTCO_vendor_support.c.p"
1013int ldv_spin = 0;
1014#line 542 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17345/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/iTCO_vendor_support.c.p"
1015void ldv_check_alloc_flags(gfp_t flags )