20161 {
20162#line 2812
20163 cfi_intelext_destroy(var_group1);
20164 }
20165#line 2819
20166 goto switch_break;
20167 switch_default:
20168#line 2820
20169 goto switch_break;
20170 } else {
20171 switch_break: ;
20172 }
20173 }
20174 }
20175 }
20176 while_break: ;
20177 }
20178 {
20179#line 2829
20180 ldv_check_final_state();
20181 }
20182#line 2832
20183 return;
20184}
20185}
20186#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5348/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
20187void ldv_blast_assert(void)
20188{
20189
20190 {
20191 ERROR:
20192#line 6
20193 goto ERROR;
20194}
20195}
20196#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5348/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
20197extern int __VERIFIER_nondet_int(void) ;
20198#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5348/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
20199int ldv_mutex = 1;
20200#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5348/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
20201int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )