841#line 168
842 tmp___1 = __VERIFIER_nondet_int();
843 }
844#line 168
845 if (tmp___1 != 0) {
846#line 169
847 goto ldv_14375;
848 } else {
849#line 171
850 goto ldv_14377;
851 }
852 ldv_14377: ;
853 {
854#line 211
855 cpufreq_gov_powersave_exit();
856 }
857 ldv_final:
858 {
859#line 219
860 ldv_check_final_state();
861 }
862#line 222
863 return;
864}
865}
866#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11153/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
867void ldv_blast_assert(void)
868{
869
870 {
871 ERROR: ;
872#line 6
873 goto ERROR;
874}
875}
876#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11153/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
877extern int __VERIFIER_nondet_int(void) ;
878#line 243 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11153/dscv_tempdir/dscv/ri/43_1a/drivers/cpufreq/cpufreq_powersave.c.p"
879int ldv_spin = 0;
880#line 247 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11153/dscv_tempdir/dscv/ri/43_1a/drivers/cpufreq/cpufreq_powersave.c.p"
881void ldv_check_alloc_flags(gfp_t flags )