2863 goto switch_break;
2864 switch_default:
2865#line 201
2866 goto switch_break;
2867 } else {
2868 switch_break: ;
2869 }
2870 }
2871 }
2872 }
2873 while_break: ;
2874 }
2875 {
2876#line 217
2877 tivo_exit();
2878 }
2879 ldv_final:
2880 {
2881#line 220
2882 ldv_check_final_state();
2883 }
2884#line 223
2885 return;
2886}
2887}
2888#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/230/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
2889void ldv_blast_assert(void)
2890{
2891
2892 {
2893 ERROR:
2894#line 6
2895 goto ERROR;
2896}
2897}
2898#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/230/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
2899extern int __VERIFIER_nondet_int(void) ;
2900#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/230/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2901int ldv_mutex = 1;
2902#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/230/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2903int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )