24508#line 1607
24509 __cil_tmp11 = *((unsigned long *)__cil_tmp10);
24510#line 1607
24511 __cil_tmp12 = (unsigned long )vq;
24512#line 1607
24513 __cil_tmp13 = __cil_tmp12 + 16952;
24514#line 1607
24515 __cil_tmp14 = *((struct vring_used_elem **)__cil_tmp13);
24516#line 1607
24517 __cil_tmp15 = __cil_tmp14 + __cil_tmp11;
24518#line 1607
24519 __cil_tmp16 = (unsigned long )__cil_tmp15;
24520#line 1607
24521 __cil_tmp17 = __cil_tmp16 + 4;
24522#line 1607
24523 *((__u32 *)__cil_tmp17) = (__u32 )1;
24524#line 1608
24525 __cil_tmp18 = (struct kref *)ubufs;
24526#line 1608
24527 kref_put(__cil_tmp18, & vhost_zerocopy_done_signal);
24528 }
24529#line 1609
24530 return;
24531}
24532}
24533#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/51/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
24534void ldv_blast_assert(void)
24535{
24536
24537 {
24538 ERROR:
24539#line 6
24540 goto ERROR;
24541}
24542}
24543#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/51/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
24544extern int __VERIFIER_nondet_int(void) ;
24545#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/51/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
24546int ldv_mutex = 1;
24547#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/51/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
24548int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )