3077 switch_default:
3078#line 477
3079 goto switch_break;
3080 } else {
3081 switch_break: ;
3082 }
3083 }
3084 }
3085 }
3086 while_break: ;
3087 }
3088 ldv_module_exit:
3089 {
3090#line 494
3091 watchdog_exit();
3092 }
3093 ldv_final:
3094 {
3095#line 497
3096 ldv_check_final_state();
3097 }
3098#line 500
3099 return;
3100}
3101}
3102#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16416/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
3103void ldv_blast_assert(void)
3104{
3105
3106 {
3107 ERROR:
3108#line 6
3109 goto ERROR;
3110}
3111}
3112#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16416/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
3113extern int __VERIFIER_nondet_int(void) ;
3114#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16416/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3115int ldv_mutex = 1;
3116#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16416/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3117int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )