4910#line 165
4911 tmp___1 = __VERIFIER_nondet_int();
4912 }
4913#line 165
4914 if (tmp___1 != 0) {
4915#line 166
4916 goto ldv_35148;
4917 } else {
4918#line 168
4919 goto ldv_35150;
4920 }
4921 ldv_35150: ;
4922 {
4923#line 182
4924 tdfx_exit();
4925 }
4926 ldv_final:
4927 {
4928#line 185
4929 ldv_check_final_state();
4930 }
4931#line 188
4932 return;
4933}
4934}
4935#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
4936void ldv_blast_assert(void)
4937{
4938
4939 {
4940 ERROR: ;
4941#line 6
4942 goto ERROR;
4943}
4944}
4945#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
4946extern int __VERIFIER_nondet_int(void) ;
4947#line 209 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12/dscv_tempdir/dscv/ri/43_1a/drivers/gpu/drm/tdfx/tdfx_drv.c.p"
4948int ldv_spin = 0;
4949#line 213 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12/dscv_tempdir/dscv/ri/43_1a/drivers/gpu/drm/tdfx/tdfx_drv.c.p"
4950void ldv_check_alloc_flags(gfp_t flags )