6939 switch_default:
6940#line 704
6941 goto switch_break;
6942 } else {
6943 switch_break: ;
6944 }
6945 }
6946 }
6947 }
6948 while_break: ;
6949 }
6950 ldv_module_exit:
6951 {
6952#line 720
6953 ir_exit();
6954 }
6955 ldv_final:
6956 {
6957#line 723
6958 ldv_check_final_state();
6959 }
6960#line 726
6961 return;
6962}
6963}
6964#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7536/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
6965void ldv_blast_assert(void)
6966{
6967
6968 {
6969 ERROR:
6970#line 6
6971 goto ERROR;
6972}
6973}
6974#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7536/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
6975extern int __VERIFIER_nondet_int(void) ;
6976#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7536/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6977int ldv_mutex = 1;
6978#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/7536/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
6979int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )