5909#line 349
5910 uv_mmtimer_ioctl(var_group1, var_uv_mmtimer_ioctl_0_p1, var_uv_mmtimer_ioctl_0_p2);
5911 }
5912#line 356
5913 goto switch_break;
5914 switch_default:
5915#line 357
5916 goto switch_break;
5917 } else {
5918 switch_break: ;
5919 }
5920 }
5921 }
5922 }
5923 while_break: ;
5924 }
5925 ldv_module_exit:
5926 {
5927#line 366
5928 ldv_check_final_state();
5929 }
5930#line 369
5931 return;
5932}
5933}
5934#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16707/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
5935void ldv_blast_assert(void)
5936{
5937
5938 {
5939 ERROR:
5940#line 6
5941 goto ERROR;
5942}
5943}
5944#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16707/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
5945extern int __VERIFIER_nondet_int(void) ;
5946#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16707/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5947int ldv_mutex = 1;
5948#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16707/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
5949int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )