ClabureDB: Classified Bug-Reports Database

      value = nondet_int();
#line 108
      enqueue(& queue, value);
#line 109
      __cil_tmp8 = i + 1;
#line 109
      __cil_tmp9 = __cil_tmp8 * 4U;
#line 109
      __cil_tmp10 = (unsigned int )(stored_elements) + __cil_tmp9;
#line 109
      *((int *)__cil_tmp10) = value;
#line 110
      enqueue_flag = (_Bool)0;
#line 111
      dequeue_flag = (_Bool)1;
      }
    } else {

    }
    {
#line 113
    pthread_mutex_unlock(& m);
#line 102
    i = i + 1;
    }
  }
  while_0_break: /* CIL Label */ ;
  }
#line 116
  return ((void *)0);
  ERROR: ;
#line 120
  return ((void *)0);
}
}
#line 122 "queue_bad.c"
void *t2(void *arg ) 
{ int i ;
  int tmp ;
  int tmp___0 ;
  unsigned int __cil_tmp5 ;