11829 __cil_tmp79 = & dev->mode_config.mutex;
11830#line 651
11831 mutex_lock_nested(__cil_tmp79, 0U);
11832#line 652
11833 drm_helper_resume_force_mode(dev);
11834#line 653
11835 __cil_tmp80 = & dev->mode_config.mutex;
11836#line 653
11837 mutex_unlock(__cil_tmp80);
11838 }
11839 } else {
11840
11841 }
11842#line 656
11843 return (0);
11844}
11845}
11846#line 886
11847void ldv_check_final_state(void) ;
11848#line 892
11849extern void ldv_initialize(void) ;
11850#line 895
11851extern int nondet_int(void) ;
11852#line 898 "/anthill/stuff/tacas-comp/work/current--X--drivers/gpu/drm/i915/i915.ko--X--safe-main18linux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/46/dscv_tempdir/dscv/ri/08_1/drivers/gpu/drm/i915/i915_drv.c.p"
11853int LDV_IN_INTERRUPT ;
11854#line 5 "/anthill/stuff/tacas-comp/work/current--X--drivers/gpu/drm/i915/i915.ko--X--safe-main18linux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/46/dscv_tempdir/dscv/ri/08_1/kernel-rules/files/engine-blast-assert.h"
11855void ldv_blast_assert(void)
11856{
11857
11858 {
11859 ERROR: ;
11860#line 6
11861 goto ERROR;
11862}
11863}
11864#line 6 "/anthill/stuff/tacas-comp/work/current--X--drivers/gpu/drm/i915/i915.ko--X--safe-main18linux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/46/dscv_tempdir/dscv/ri/08_1/kernel-rules/files/engine-blast.h"
11865extern int ldv_undefined_int(void) ;
11866#line 1654 "/anthill/stuff/tacas-comp/work/current--X--drivers/gpu/drm/i915/i915.ko--X--safe-main18linux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/46/dscv_tempdir/dscv/ri/08_1/drivers/gpu/drm/i915/i915_drv.c.p"
11867int ldv_module_refcounter = 1;
11868#line 1657 "/anthill/stuff/tacas-comp/work/current--X--drivers/gpu/drm/i915/i915.ko--X--safe-main18linux-3.0.1--X--08_1/linux-3.0.1/csd_deg_dscv/46/dscv_tempdir/dscv/ri/08_1/drivers/gpu/drm/i915/i915_drv.c.p"
11869void ldv_module_get(struct module *module )