9867 } else {
9868
9869 }
9870#line 1017
9871 goto switch_break;
9872 switch_default:
9873#line 1018
9874 goto switch_break;
9875 } else {
9876 switch_break: ;
9877 }
9878 }
9879 }
9880 }
9881 while_break: ;
9882 }
9883 ldv_module_exit:
9884 {
9885#line 1027
9886 ldv_check_final_state();
9887 }
9888#line 1030
9889 return;
9890}
9891}
9892#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1133/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
9893void ldv_blast_assert(void)
9894{
9895
9896 {
9897 ERROR:
9898#line 6
9899 goto ERROR;
9900}
9901}
9902#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1133/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
9903extern int __VERIFIER_nondet_int(void) ;
9904#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1133/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
9905int ldv_mutex = 1;
9906#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1133/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
9907int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )