825 switch_default:
826#line 271
827 goto switch_break;
828 } else {
829 switch_break: ;
830 }
831 }
832 }
833 }
834 while_break: ;
835 }
836 ldv_module_exit:
837 {
838#line 286
839 acntsa_exit();
840 }
841 ldv_final:
842 {
843#line 289
844 ldv_check_final_state();
845 }
846#line 292
847 return;
848}
849}
850#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1166/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
851void ldv_blast_assert(void)
852{
853
854 {
855 ERROR:
856#line 6
857 goto ERROR;
858}
859}
860#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1166/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
861extern int __VERIFIER_nondet_int(void) ;
862#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1166/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
863int ldv_mutex = 1;
864#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1166/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
865int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )