7753 {
7754#line 999
7755 target_alloc(var_group4);
7756 }
7757#line 1014
7758 goto switch_break;
7759 switch_default:
7760#line 1015
7761 goto switch_break;
7762 } else {
7763 switch_break: ;
7764 }
7765 }
7766 }
7767 }
7768 while_break: ;
7769 }
7770 {
7771#line 1024
7772 ldv_check_final_state();
7773 }
7774#line 1027
7775 return;
7776}
7777}
7778#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7655/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
7779void ldv_blast_assert(void)
7780{
7781
7782 {
7783 ERROR:
7784#line 6
7785 goto ERROR;
7786}
7787}
7788#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7655/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
7789extern int __VERIFIER_nondet_int(void) ;
7790#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7655/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
7791int ldv_mutex = 1;
7792#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7655/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
7793int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )