9024 goto switch_break;
9025 switch_default:
9026#line 613
9027 goto switch_break;
9028 } else {
9029 switch_break: ;
9030 }
9031 }
9032 }
9033 }
9034 while_break: ;
9035 }
9036 {
9037#line 634
9038 dstr_exit();
9039 }
9040 ldv_final:
9041 {
9042#line 637
9043 ldv_check_final_state();
9044 }
9045#line 640
9046 return;
9047}
9048}
9049#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16799/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
9050void ldv_blast_assert(void)
9051{
9052
9053 {
9054 ERROR:
9055#line 6
9056 goto ERROR;
9057}
9058}
9059#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16799/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
9060extern int __VERIFIER_nondet_int(void) ;
9061#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16799/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
9062int ldv_mutex = 1;
9063#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16799/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
9064int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )