8811 goto switch_break;
8812 switch_default:
8813#line 1123
8814 goto switch_break;
8815 } else {
8816 switch_break: ;
8817 }
8818 }
8819 }
8820 }
8821 while_break: ;
8822 }
8823 {
8824#line 1144
8825 cleanup_nftl();
8826 }
8827 ldv_final:
8828 {
8829#line 1147
8830 ldv_check_final_state();
8831 }
8832#line 1150
8833 return;
8834}
8835}
8836#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5495/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
8837void ldv_blast_assert(void)
8838{
8839
8840 {
8841 ERROR:
8842#line 6
8843 goto ERROR;
8844}
8845}
8846#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5495/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
8847extern int __VERIFIER_nondet_int(void) ;
8848#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5495/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
8849int ldv_mutex = 1;
8850#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5495/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
8851int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )