3753 switch_default:
3754#line 277
3755 goto switch_break;
3756 } else {
3757 switch_break: ;
3758 }
3759 }
3760 }
3761 }
3762 while_break: ;
3763 }
3764 ldv_module_exit:
3765 {
3766#line 289
3767 gen_74x164_exit();
3768 }
3769 ldv_final:
3770 {
3771#line 292
3772 ldv_check_final_state();
3773 }
3774#line 295
3775 return;
3776}
3777}
3778#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5840/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
3779void ldv_blast_assert(void)
3780{
3781
3782 {
3783 ERROR:
3784#line 6
3785 goto ERROR;
3786}
3787}
3788#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5840/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
3789extern int __VERIFIER_nondet_int(void) ;
3790#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5840/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3791int ldv_mutex = 1;
3792#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5840/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3793int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )