5853#line 255
5854 if (0) {
5855 switch_default:
5856#line 257
5857 goto switch_break;
5858 } else {
5859 switch_break: ;
5860 }
5861 }
5862 }
5863 while_break: ;
5864 }
5865 {
5866#line 289
5867 cicada_exit();
5868 }
5869 ldv_final:
5870 {
5871#line 292
5872 ldv_check_final_state();
5873 }
5874#line 295
5875 return;
5876}
5877}
5878#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9658/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
5879void ldv_blast_assert(void)
5880{
5881
5882 {
5883 ERROR:
5884#line 6
5885 goto ERROR;
5886}
5887}
5888#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9658/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
5889extern int __VERIFIER_nondet_int(void) ;
5890#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9658/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5891int ldv_mutex = 1;
5892#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9658/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5893int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )