5846 goto switch_break;
5847 switch_default:
5848#line 380
5849 goto switch_break;
5850 } else {
5851 switch_break: ;
5852 }
5853 }
5854 }
5855 }
5856 while_break: ;
5857 }
5858 {
5859#line 407
5860 qs6612_exit();
5861 }
5862 ldv_final:
5863 {
5864#line 410
5865 ldv_check_final_state();
5866 }
5867#line 413
5868 return;
5869}
5870}
5871#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9669/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
5872void ldv_blast_assert(void)
5873{
5874
5875 {
5876 ERROR:
5877#line 6
5878 goto ERROR;
5879}
5880}
5881#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9669/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
5882extern int __VERIFIER_nondet_int(void) ;
5883#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9669/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5884int ldv_mutex = 1;
5885#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/9669/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5886int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )