941 ldv_16164: ;
942 ldv_16170:
943 {
944#line 336
945 tmp___1 = __VERIFIER_nondet_int();
946 }
947#line 336
948 if (tmp___1 != 0) {
949#line 337
950 goto ldv_16169;
951 } else {
952#line 339
953 goto ldv_16171;
954 }
955 ldv_16171: ;
956
957 ldv_final:
958 {
959#line 438
960 ldv_check_final_state();
961 }
962#line 441
963 return;
964}
965}
966#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11167/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
967void ldv_blast_assert(void)
968{
969
970 {
971 ERROR: ;
972#line 6
973 goto ERROR;
974}
975}
976#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11167/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
977extern int __VERIFIER_nondet_int(void) ;
978#line 462 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11167/dscv_tempdir/dscv/ri/43_1a/drivers/clocksource/cs5535-clockevt.c.p"
979int ldv_spin = 0;
980#line 466 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11167/dscv_tempdir/dscv/ri/43_1a/drivers/clocksource/cs5535-clockevt.c.p"
981void ldv_check_alloc_flags(gfp_t flags )