902#line 291
903 tmp___1 = __VERIFIER_nondet_int();
904 }
905#line 291
906 if (tmp___1 != 0) {
907#line 292
908 goto ldv_14605;
909 } else {
910#line 294
911 goto ldv_14607;
912 }
913 ldv_14607: ;
914 {
915#line 418
916 duramar2150_c2port_exit();
917 }
918 ldv_final:
919 {
920#line 421
921 ldv_check_final_state();
922 }
923#line 424
924 return;
925}
926}
927#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12478/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
928void ldv_blast_assert(void)
929{
930
931 {
932 ERROR: ;
933#line 6
934 goto ERROR;
935}
936}
937#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12478/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
938extern int __VERIFIER_nondet_int(void) ;
939#line 445 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12478/dscv_tempdir/dscv/ri/43_1a/drivers/misc/c2port/c2port-duramar2150.c.p"
940int ldv_spin = 0;
941#line 449 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12478/dscv_tempdir/dscv/ri/43_1a/drivers/misc/c2port/c2port-duramar2150.c.p"
942void ldv_check_alloc_flags(gfp_t flags )