void partition(Listp hd , int v ) 
{ Listp next ;
  Listp prev ;
  int tmp ;
  Listp curr ;
  Listp less ;
  Listp more ;
  int k ;
  int V308 ;
  int V954 ;
  int V1670 ;
  int V2475 ;
  int V2449 ;
  int V3236 ;
  int V4092 ;
  int V4046 ;
  int V4357 ;
  int V5205 ;
  int V11258 ;
  int V12186 ;
  int V12136 ;
  int V21229 ;
  int V22157 ;
  int V22107 ;
  int V11279 ;
  int V22434 ;
  int V25829 ;
  int V25803 ;
  int V36330 ;
  int V37153 ;
  int V37107 ;
  int V69345 ;
  int V70168 ;
  int V70122 ;
  int V70469 ;
  int V76553 ;
  int V76507 ;
  int V87793 ;
  int V88308 ;
  int V89282 ;
  int V89236 ;
  int V100522 ;
  int V101005 ;
  int V101506 ;
  int V101626 ;
  int V101771 ;
  int V102523 ;
  int V102497 ;
  int V113751 ;
  int V165991 ;
  int V167041 ;
  int V172423 ;
  int V1691 ;
  int V172451 ;
  int V172576 ;
  int V172787 ;
  int V172968 ;
  int V173075 ;
  int V173230 ;
  int V173631 ;
  int V173750 ;
  int V174365 ;
  int V175551 ;
  int V176260 ;
  int V182850 ;
  int V182878 ;
  int V175572 ;
  int V183003 ;
  int V183214 ;
  int V186040 ;
  int V186052 ;
  int V186159 ;
  int V186363 ;
  int V187134 ;
  int V187108 ;
  int V188315 ;
  int V188940 ;
  int V205645 ;
  int V205813 ;
  int V213935 ;
  int V214067 ;
  int V214912 ;
  int V214866 ;
  int V215157 ;
  int V215964 ;
  int V216187 ;
  int V216266 ;
  int V216385 ;

  {
  []
  tassume(" dll(?k,null,hd,?end,null)");
  next = (Listp )0;
  prev = (Listp )0;
  curr = hd;
  less = (Listp )0;
  more = (Listp )0;
  hd = (List *)0;
  (hd = 0) * (more = 0) * (less = 0) * (prev = 0) * (next = 0) * Dll(k,0,curr,end,0)
  {
  (hd = 0) * (more = 0) * (less = 0) * (prev = 0) * (next = 0) * Dll(k,0,curr,end,0)
  while (1) {
while_0_continue: /* CIL Label */ 
    (hd = 0) * (more = 0) * (less = 0) * (prev = 0) * (next = 0) * Dll(k,0,curr,end,0)
    Dll(V2475,next,V2326,end,0) * (hd = 0) * (less = 0) * (prev = 0) * (curr = next) * curr -> [n: V2326, b: 0, V2327] * (~(V1998 = 0)) * (~(more = 0)) * (~(next = 0)) * (~(V2449 = 0)) * Dll(V2449,0,more,V1998,0)
    Dll(V4357,0,more,V1998,0) * (~(V4357 = 0)) * (curr = next) * (curr = 0) * Dll(V2475,more,next,end,0) * (~(V1998 = 0)) * (~(more = 0)) * (hd = 0) * (less = 0) * (prev = 0)
    Dll(V37153,next,V36975,end,0) * (hd = 0) * (prev = 0) * (curr = next) * curr -> [n: V36975, b: 0, V36976] * Dll(V25803,0,less,V25384,0) * (~(V25803 = 0)) * (~(V36346 >= v)) * (~(more = 0)) * (~(V1998 = 0)) * (~(V25384 = 0)) * (~(less = 0)) * (~(V11279 >= v)) * (~(next = 0)) * (~(V37107 = 0)) * Dll(V37107,0,more,V1998,0)
    Dll(V70469,0,more,V1998,0) * (~(V70469 = 0)) * (curr = next) * (curr = 0) * Dll(V37153,more,next,end,0) * Dll(V25803,0,less,V25384,0) * (~(V25803 = 0)) * (~(V36346 >= v)) * (~(V1998 = 0)) * (~(V25384 = 0)) * (~(less = 0)) * (~(V11279 >= v)) * (~(more = 0)) * (hd = 0) * (prev = 0)
    (curr = 0) * (curr = next) * less -> [n: 0, data: tmp, b: 0, V3237] * (hd = 0) * (prev = 0) * (~(tmp >= v)) * Dll(V2475,less,next,end,0) * Dll(V2449,0,more,V1998,0) * (~(V2449 = 0)) * (~(less = 0)) * (~(more = 0)) * (~(V1998 = 0))
    Dll(V187134,next,V187005,end,0) * (hd = 0) * (more = 0) * (prev = 0) * (curr = next) * curr -> [n: V187005, b: 0, V187006] * (~(V186677 = 0)) * (~(V175572 >= v)) * (~(less = 0)) * (~(next = 0)) * (~(tmp >= v)) * (~(V187108 = 0)) * Dll(V187108,0,less,V186677,0)
    Dll(V215157,0,less,V186677,0) * (~(V215157 = 0)) * (curr = next) * (curr = 0) * (~(tmp >= v)) * Dll(V187134,less,next,end,0) * (~(V186677 = 0)) * (~(V175572 >= v)) * (~(less = 0)) * (~(V188331 >= v)) * (hd = 0) * (more = 0) * (prev = 0)
    ;
    (hd = 0) * (more = 0) * (less = 0) * (prev = 0) * (next = 0) * Dll(k,0,curr,end,0)
    Dll(V2475,next,V2326,end,0) * (hd = 0) * (less = 0) * (prev = 0) * (curr = next) * curr -> [n: V2326, b: 0, V2327] * (~(V1998 = 0)) * (~(more = 0)) * (~(next = 0)) * (~(V2449 = 0)) * Dll(V2449,0,more,V1998,0)
    Dll(V4357,0,more,V1998,0) * (~(V4357 = 0)) * (curr = next) * (curr = 0) * Dll(V2475,more,next,end,0) * (~(V1998 = 0)) * (~(more = 0)) * (hd = 0) * (less = 0) * (prev = 0)
    Dll(V37153,next,V36975,end,0) * (hd = 0) * (prev = 0) * (curr = next) * curr -> [n: V36975, b: 0, V36976] * Dll(V25803,0,less,V25384,0) * (~(V25803 = 0)) * (~(V36346 >= v)) * (~(more = 0)) * (~(V1998 = 0)) * (~(V25384 = 0)) * (~(less = 0)) * (~(V11279 >= v)) * (~(next = 0)) * (~(V37107 = 0)) * Dll(V37107,0,more,V1998,0)
    Dll(V70469,0,more,V1998,0) * (~(V70469 = 0)) * (curr = next) * (curr = 0) * Dll(V37153,more,next,end,0) * Dll(V25803,0,less,V25384,0) * (~(V25803 = 0)) * (~(V36346 >= v)) * (~(V1998 = 0)) * (~(V25384 = 0)) * (~(less = 0)) * (~(V11279 >= v)) * (~(more = 0)) * (hd = 0) * (prev = 0)
    (curr = 0) * (curr = next) * less -> [n: 0, data: tmp, b: 0, V3237] * (hd = 0) * (prev = 0) * (~(tmp >= v)) * Dll(V2475,less,next,end,0) * Dll(V2449,0,more,V1998,0) * (~(V2449 = 0)) * (~(less = 0)) * (~(more = 0)) * (~(V1998 = 0))
    Dll(V187134,next,V187005,end,0) * (hd = 0) * (more = 0) * (prev = 0) * (curr = next) * curr -> [n: V187005, b: 0, V187006] * (~(V186677 = 0)) * (~(V175572 >= v)) * (~(less = 0)) * (~(next = 0)) * (~(tmp >= v)) * (~(V187108 = 0)) * Dll(V187108,0,less,V186677,0)
    Dll(V215157,0,less,V186677,0) * (~(V215157 = 0)) * (curr = next) * (curr = 0) * (~(tmp >= v)) * Dll(V187134,less,next,end,0) * (~(V186677 = 0)) * (~(V175572 >= v)) * (~(less = 0)) * (~(V188331 >= v)) * (hd = 0) * (more = 0) * (prev = 0)
    if ((unsigned int )curr != (unsigned int )((Listp )0)) {

    } else {
      Dll(V4357,0,more,V1998,0) * (~(V4357 = 0)) * (curr = next) * (curr = 0) * Dll(V2475,more,next,end,0) * (~(V1998 = 0)) * (~(more = 0)) * (hd = 0) * (less = 0) * (prev = 0)
      Dll(V70469,0,more,V1998,0) * (~(V70469 = 0)) * (curr = next) * (curr = 0) * Dll(V37153,more,next,end,0) * Dll(V25803,0,less,V25384,0) * (~(V25803 = 0)) * (~(V36346 >= v)) * (~(V1998 = 0)) * (~(V25384 = 0)) * (~(less = 0)) * (~(V11279 >= v)) * (~(more = 0)) * (hd = 0) * (prev = 0)
      (curr = 0) * (curr = next) * less -> [n: 0, data: tmp, b: 0, V3237] * (hd = 0) * (prev = 0) * (~(tmp >= v)) * Dll(V2475,less,next,end,0) * Dll(V2449,0,more,V1998,0) * (~(V2449 = 0)) * (~(less = 0)) * (~(more = 0)) * (~(V1998 = 0))
      Dll(V215157,0,less,V186677,0) * (~(V215157 = 0)) * (curr = next) * (curr = 0) * (~(tmp >= v)) * Dll(V187134,less,next,end,0) * (~(V186677 = 0)) * (~(V175572 >= v)) * (~(less = 0)) * (~(V188331 >= v)) * (hd = 0) * (more = 0) * (prev = 0)
      (curr = 0) * (hd = 0) * (more = 0) * (less = 0) * (prev = 0) * (next = 0) * Dll(k,0,curr,end,0)
      goto while_0_break;
    }
    curr -> [n: V279, data: V308, b: 0, V309] * (hd = 0) * (more = 0) * (less = 0) * (prev = 0) * (next = 0) * Dll((k - 1),curr,V279,end,0) * (~(curr = 0))
    curr -> [n: V2326, data: V3236, b: 0, V3237] * (hd = 0) * (less = 0) * (prev = 0) * (curr = next) * (~(V1998 = 0)) * (~(more = 0)) * (~(next = 0)) * (~(V2449 = 0)) * Dll(V2449,0,more,V1998,0) * Dll(V2475,next,V2326,end,0)
    curr -> [n: V36975, data: V69345, b: 0, V69346] * (hd = 0) * (prev = 0) * (curr = next) * Dll(V25803,0,less,V25384,0) * (~(V25803 = 0)) * (~(V36346 >= v)) * (~(more = 0)) * (~(V1998 = 0)) * (~(V25384 = 0)) * (~(less = 0)) * (~(V11279 >= v)) * (~(next = 0)) * (~(V37107 = 0)) * Dll(V37107,0,more,V1998,0) * Dll(V37153,next,V36975,end,0)
    curr -> [n: V187005, data: V188315, b: 0, V188316] * (hd = 0) * (more = 0) * (prev = 0) * (curr = next) * (~(V186677 = 0)) * (~(V175572 >= v)) * (~(less = 0)) * (~(next = 0)) * (~(tmp >= v)) * (~(V187108 = 0)) * Dll(V187108,0,less,V186677,0) * Dll(V187134,next,V187005,end,0)
    tmp = curr->data;
    curr -> [n: V279, data: tmp, b: 0, V309] * (hd = 0) * (more = 0) * (less = 0) * (prev = 0) * (next = 0) * Dll((k - 1),curr,V279,end,0) * (~(curr = 0))
    curr -> [n: V2326, data: tmp, b: 0, V3237] * (hd = 0) * (less = 0) * (prev = 0) * (curr = next) * (~(V1998 = 0)) * (~(more = 0)) * (~(next = 0)) * (~(V2449 = 0)) * Dll(V2449,0,more,V1998,0) * Dll(V2475,next,V2326,end,0)
    curr -> [n: V25700, data: tmp, b: 0, V36331] * (prev = 0) * (hd = 0) * (curr = next) * (~(V11279 >= v)) * Dll(V12136,0,more,V1998,0) * (~(V12136 = 0)) * (~(less = 0)) * (~(V25384 = 0)) * (~(V1998 = 0)) * (~(more = 0)) * (~(next = 0)) * (~(V36346 >= v)) * (~(V25803 = 0)) * Dll(V25803,0,less,V25384,0) * Dll(V25829,next,V25700,end,0)
    curr -> [n: V187005, data: tmp, b: 0, V188316] * (hd = 0) * (more = 0) * (prev = 0) * (curr = next) * (~(V186677 = 0)) * (~(V175572 >= v)) * (~(less = 0)) * (~(next = 0)) * (~(V188331 >= v)) * (~(V187108 = 0)) * Dll(V187108,0,less,V186677,0) * Dll(V187134,next,V187005,end,0)
    if (tmp >= v) {
      curr -> [n: V279, data: tmp, b: 0, V309] * (hd = 0) * (more = 0) * (less = 0) * (prev = 0) * (next = 0) * (tmp >= v) * (~(curr = 0)) * Dll((k - 1),curr,V279,end,0)
      curr -> [n: V2326, data: tmp, b: 0, V3237] * (hd = 0) * (less = 0) * (prev = 0) * (curr = next) * (tmp >= v) * Dll(V2475,next,V2326,end,0) * Dll(V2449,0,more,V1998,0) * (~(V2449 = 0)) * (~(next = 0)) * (~(more = 0)) * (~(V1998 = 0))
      curr -> [n: V25700, data: tmp, b: 0, V36331] * (prev = 0) * (hd = 0) * (curr = next) * (tmp >= v) * Dll(V25829,next,V25700,end,0) * Dll(V25803,0,less,V25384,0) * (~(V25803 = 0)) * (~(V36346 >= v)) * (~(next = 0)) * (~(more = 0)) * (~(V1998 = 0)) * (~(V25384 = 0)) * (~(less = 0)) * (~(V12136 = 0)) * Dll(V12136,0,more,V1998,0) * (~(V11279 >= v))
      curr -> [n: V187005, data: tmp, b: 0, V188316] * (hd = 0) * (more = 0) * (prev = 0) * (curr = next) * (tmp >= v) * Dll(V187134,next,V187005,end,0) * Dll(V187108,0,less,V186677,0) * (~(V187108 = 0)) * (~(V188331 >= v)) * (~(next = 0)) * (~(less = 0)) * (~(V175572 >= v)) * (~(V186677 = 0))
      next = curr->n;
      curr->n = more;
      curr -> [n: more, data: tmp, b: 0, V309] * (hd = 0) * (more = 0) * (less = 0) * (prev = 0) * Dll((k - 1),curr,next,end,0) * (~(curr = 0)) * (tmp >= v)
      curr -> [n: more, data: tmp, b: 0, V3237] * (hd = 0) * (less = 0) * (prev = 0) * (~(V1998 = 0)) * (~(more = 0)) * (~(curr = 0)) * (~(V2449 = 0)) * Dll(V2449,0,more,V1998,0) * Dll(V2475,curr,next,end,0) * (tmp >= v)
      curr -> [n: more, data: tmp, b: 0, V36331] * (prev = 0) * (hd = 0) * (~(V11279 >= v)) * Dll(V12136,0,more,V1998,0) * (~(V12136 = 0)) * (~(less = 0)) * (~(V25384 = 0)) * (~(V1998 = 0)) * (~(more = 0)) * (~(curr = 0)) * (~(V36346 >= v)) * (~(V25803 = 0)) * Dll(V25803,0,less,V25384,0) * Dll(V25829,curr,next,end,0) * (tmp >= v)
      curr -> [n: more, data: tmp, b: 0, V188316] * (hd = 0) * (more = 0) * (prev = 0) * (~(V186677 = 0)) * (~(V175572 >= v)) * (~(less = 0)) * (~(curr = 0)) * (~(V188331 >= v)) * (~(V187108 = 0)) * Dll(V187108,0,less,V186677,0) * Dll(V187134,curr,next,end,0) * (tmp >= v)
      if ((unsigned int )more != (unsigned int )((Listp )0)) {
        more -> [n: V3547, b: 0, V3548] * (hd = 0) * (less = 0) * (prev = 0) * Dll((V2449 - 1),more,V3547,V1998,0) * (~(V2449 = 0)) * (~(curr = 0)) * (~(more = 0)) * (~(V1998 = 0)) * Dll(V2475,curr,next,end,0) * (tmp >= v) * curr -> [n: more, data: tmp, b: 0, V3237]
        more -> [n: V36620, b: 0, V36621] * (prev = 0) * (hd = 0) * Dll((V12136 - 1),more,V36620,V1998,0) * (~(V11279 >= v)) * (~(V12136 = 0)) * (~(less = 0)) * (~(V25384 = 0)) * (~(V1998 = 0)) * (~(more = 0)) * (~(curr = 0)) * (~(V36346 >= v)) * (~(V25803 = 0)) * Dll(V25803,0,less,V25384,0) * Dll(V25829,curr,next,end,0) * (tmp >= v) * curr -> [n: more, data: tmp, b: 0, V36331]
        more->b = curr;
      } else {

      }
      curr -> [n: more, data: tmp, b: 0, V309] * (hd = 0) * (more = 0) * (less = 0) * (prev = 0) * Dll((k - 1),curr,next,end,0) * (~(curr = 0)) * (tmp >= v)
      more -> [n: V3547, b: curr, V3548] * (hd = 0) * (less = 0) * (prev = 0) * Dll((V2449 - 1),more,V3547,V1998,0) * (~(V2449 = 0)) * (~(curr = 0)) * (~(more = 0)) * (~(V1998 = 0)) * Dll(V2475,curr,next,end,0) * (tmp >= v) * curr -> [n: more, data: tmp, b: 0, V3237]
      more -> [n: V36620, b: curr, V36621] * (prev = 0) * (hd = 0) * Dll((V12136 - 1),more,V36620,V1998,0) * (~(V11279 >= v)) * (~(V12136 = 0)) * (~(less = 0)) * (~(V25384 = 0)) * (~(V1998 = 0)) * (~(more = 0)) * (~(curr = 0)) * (~(V36346 >= v)) * (~(V25803 = 0)) * Dll(V25803,0,less,V25384,0) * Dll(V25829,curr,next,end,0) * (tmp >= v) * curr -> [n: more, data: tmp, b: 0, V36331]
      curr -> [n: more, data: tmp, b: 0, V188316] * (hd = 0) * (more = 0) * (prev = 0) * (~(V186677 = 0)) * (~(V175572 >= v)) * (~(less = 0)) * (~(curr = 0)) * (~(V188331 >= v)) * (~(V187108 = 0)) * Dll(V187108,0,less,V186677,0) * Dll(V187134,curr,next,end,0) * (tmp >= v)
      more = curr;
      more->b = (struct list *)0;
      curr = next;
    } else {
      curr -> [n: V2326, data: tmp, b: 0, V3237] * (hd = 0) * (less = 0) * (prev = 0) * (curr = next) * (~(tmp >= v)) * Dll(V2475,next,V2326,end,0) * Dll(V2449,0,more,V1998,0) * (~(V2449 = 0)) * (~(next = 0)) * (~(more = 0)) * (~(V1998 = 0))
      curr -> [n: V36975, data: tmp, b: 0, V69346] * (hd = 0) * (prev = 0) * (curr = next) * (~(tmp >= v)) * Dll(V37153,next,V36975,end,0) * Dll(V37107,0,more,V1998,0) * (~(V37107 = 0)) * (~(next = 0)) * (~(V11279 >= v)) * (~(less = 0)) * (~(V25384 = 0)) * (~(V1998 = 0)) * (~(more = 0)) * (~(V36346 >= v)) * (~(V25803 = 0)) * Dll(V25803,0,less,V25384,0)
      curr -> [n: V279, data: tmp, b: 0, V309] * (hd = 0) * (more = 0) * (less = 0) * (prev = 0) * (next = 0) * (~(tmp >= v)) * (~(curr = 0)) * Dll((k - 1),curr,V279,end,0)
      curr -> [n: V187005, data: tmp, b: 0, V188316] * (hd = 0) * (more = 0) * (prev = 0) * (curr = next) * (~(tmp >= v)) * Dll(V187134,next,V187005,end,0) * Dll(V187108,0,less,V186677,0) * (~(V187108 = 0)) * (~(V188331 >= v)) * (~(next = 0)) * (~(less = 0)) * (~(V175572 >= v)) * (~(V186677 = 0))
      next = curr->n;
      curr->n = less;
      curr -> [n: less, data: tmp, b: 0, V3237] * (hd = 0) * (less = 0) * (prev = 0) * (~(V1998 = 0)) * (~(more = 0)) * (~(curr = 0)) * (~(V2449 = 0)) * Dll(V2449,0,more,V1998,0) * Dll(V2475,curr,next,end,0) * (~(tmp >= v))
      curr -> [n: less, data: tmp, b: 0, V69346] * (hd = 0) * (prev = 0) * Dll(V25803,0,less,V25384,0) * (~(V25803 = 0)) * (~(V36346 >= v)) * (~(more = 0)) * (~(V1998 = 0)) * (~(V25384 = 0)) * (~(less = 0)) * (~(V11279 >= v)) * (~(curr = 0)) * (~(V37107 = 0)) * Dll(V37107,0,more,V1998,0) * Dll(V37153,curr,next,end,0) * (~(tmp >= v))
      curr -> [n: less, data: tmp, b: 0, V309] * (hd = 0) * (more = 0) * (less = 0) * (prev = 0) * Dll((k - 1),curr,next,end,0) * (~(curr = 0)) * (~(tmp >= v))
      curr -> [n: less, data: tmp, b: 0, V188316] * (hd = 0) * (more = 0) * (prev = 0) * (~(V186677 = 0)) * (~(V175572 >= v)) * (~(less = 0)) * (~(curr = 0)) * (~(V188331 >= v)) * (~(V187108 = 0)) * Dll(V187108,0,less,V186677,0) * Dll(V187134,curr,next,end,0) * (~(tmp >= v))
      if ((unsigned int )less != (unsigned int )((Listp )0)) {
        less -> [n: V76040, b: 0, V76041] * (hd = 0) * (prev = 0) * Dll((V25803 - 1),less,V76040,V25384,0) * (~(V25803 = 0)) * (~(V36346 >= v)) * (~(more = 0)) * (~(V1998 = 0)) * (~(V25384 = 0)) * (~(less = 0)) * (~(V11279 >= v)) * (~(curr = 0)) * (~(V37107 = 0)) * Dll(V37107,0,more,V1998,0) * Dll(V37153,curr,next,end,0) * (~(tmp >= v)) * curr -> [n: less, data: tmp, b: 0, V69346]
        less -> [n: V214387, b: 0, V214388] * (hd = 0) * (more = 0) * (prev = 0) * Dll((V187108 - 1),less,V214387,V186677,0) * (~(V187108 = 0)) * (~(V188331 >= v)) * (~(curr = 0)) * (~(less = 0)) * (~(V175572 >= v)) * (~(V186677 = 0)) * Dll(V187134,curr,next,end,0) * (~(tmp >= v)) * curr -> [n: less, data: tmp, b: 0, V188316]
        less->b = curr;
      } else {

      }
      curr -> [n: less, data: tmp, b: 0, V3237] * (hd = 0) * (less = 0) * (prev = 0) * (~(V1998 = 0)) * (~(more = 0)) * (~(curr = 0)) * (~(V2449 = 0)) * Dll(V2449,0,more,V1998,0) * Dll(V2475,curr,next,end,0) * (~(tmp >= v))
      less -> [n: V76040, b: curr, V76041] * (hd = 0) * (prev = 0) * Dll((V25803 - 1),less,V76040,V25384,0) * (~(V25803 = 0)) * (~(V36346 >= v)) * (~(more = 0)) * (~(V1998 = 0)) * (~(V25384 = 0)) * (~(less = 0)) * (~(V11279 >= v)) * (~(curr = 0)) * (~(V37107 = 0)) * Dll(V37107,0,more,V1998,0) * Dll(V37153,curr,next,end,0) * (~(tmp >= v)) * curr -> [n: less, data: tmp, b: 0, V69346]
      curr -> [n: less, data: tmp, b: 0, V309] * (hd = 0) * (more = 0) * (less = 0) * (prev = 0) * Dll((k - 1),curr,next,end,0) * (~(curr = 0)) * (~(tmp >= v))
      less -> [n: V214387, b: curr, V214388] * (hd = 0) * (more = 0) * (prev = 0) * Dll((V187108 - 1),less,V214387,V186677,0) * (~(V187108 = 0)) * (~(V188331 >= v)) * (~(curr = 0)) * (~(less = 0)) * (~(V175572 >= v)) * (~(V186677 = 0)) * Dll(V187134,curr,next,end,0) * (~(tmp >= v)) * curr -> [n: less, data: tmp, b: 0, V188316]
      less = curr;
      less->b = (struct list *)0;
      curr = next;
    }
    (curr = next) * more -> [n: 0, data: tmp, b: 0, V309] * (hd = 0) * (less = 0) * (prev = 0) * (tmp >= v) * (~(more = 0)) * Dll((k - 1),more,next,end,0)
    (curr = next) * more -> [n: V3594, data: tmp, b: 0, V3237] * (hd = 0) * (less = 0) * (prev = 0) * V3594 -> [n: V3547, b: more, V3548] * (tmp >= v) * Dll(V2475,more,next,end,0) * (~(V1998 = 0)) * (~(V3594 = 0)) * (~(more = 0)) * (~(V2449 = 0)) * Dll((V2449 - 1),V3594,V3547,V1998,0)
    (curr = next) * less -> [n: 0, data: tmp, b: 0, V3237] * (hd = 0) * (prev = 0) * (~(tmp >= v)) * Dll(V2475,less,next,end,0) * Dll(V2449,0,more,V1998,0) * (~(V2449 = 0)) * (~(less = 0)) * (~(more = 0)) * (~(V1998 = 0))
    (curr = next) * more -> [n: V36667, data: tmp, b: 0, V36331] * (prev = 0) * (hd = 0) * V36667 -> [n: V36620, b: more, V36621] * (tmp >= v) * Dll(V25829,more,next,end,0) * Dll(V25803,0,less,V25384,0) * (~(V25803 = 0)) * (~(V36346 >= v)) * (~(more = 0)) * (~(V36667 = 0)) * (~(V1998 = 0)) * (~(V25384 = 0)) * (~(less = 0)) * (~(V12136 = 0)) * (~(V11279 >= v)) * Dll((V12136 - 1),V36667,V36620,V1998,0)
    (curr = next) * less -> [n: V76087, data: tmp, b: 0, V69346] * (hd = 0) * (prev = 0) * V76087 -> [n: V76040, b: less, V76041] * (~(tmp >= v)) * Dll(V37153,less,next,end,0) * Dll(V37107,0,more,V1998,0) * (~(V37107 = 0)) * (~(less = 0)) * (~(V11279 >= v)) * (~(V76087 = 0)) * (~(V25384 = 0)) * (~(V1998 = 0)) * (~(more = 0)) * (~(V36346 >= v)) * (~(V25803 = 0)) * Dll((V25803 - 1),V76087,V76040,V25384,0)
    (curr = next) * less -> [n: 0, data: tmp, b: 0, V309] * (hd = 0) * (more = 0) * (prev = 0) * (~(tmp >= v)) * (~(less = 0)) * Dll((k - 1),less,next,end,0)
    (curr = next) * more -> [n: 0, data: tmp, b: 0, V188316] * (hd = 0) * (prev = 0) * (tmp >= v) * Dll(V187134,more,next,end,0) * Dll(V187108,0,less,V186677,0) * (~(V187108 = 0)) * (~(V188331 >= v)) * (~(more = 0)) * (~(less = 0)) * (~(V175572 >= v)) * (~(V186677 = 0))
    (curr = next) * less -> [n: V214434, data: tmp, b: 0, V188316] * (hd = 0) * (more = 0) * (prev = 0) * V214434 -> [n: V214387, b: less, V214388] * (~(tmp >= v)) * Dll(V187134,less,next,end,0) * (~(V186677 = 0)) * (~(V175572 >= v)) * (~(V214434 = 0)) * (~(less = 0)) * (~(V188331 >= v)) * (~(V187108 = 0)) * Dll((V187108 - 1),V214434,V214387,V186677,0)
    if ((unsigned int )curr != (unsigned int )((Listp )0)) {
      curr -> [n: V861, b: more, V862] * (curr = next) * (hd = 0) * (less = 0) * (prev = 0) * Dll(((k - 1) - 1),next,V861,end,0) * (~(more = 0)) * (tmp >= v) * (~(next = 0)) * more -> [n: 0, data: tmp, b: 0, V309]
      curr -> [n: V3914, b: more, V3915] * (curr = next) * (hd = 0) * (less = 0) * (prev = 0) * Dll((V2475 - 1),next,V3914,end,0) * (tmp >= v) * V3594 -> [n: V3547, b: more, V3548] * (~(V1998 = 0)) * (~(V3594 = 0)) * (~(more = 0)) * (~(V2449 = 0)) * Dll((V2449 - 1),V3594,V3547,V1998,0) * (~(next = 0)) * more -> [n: V3594, data: tmp, b: 0, V3237]
      curr -> [n: V5131, b: less, V5132] * (curr = next) * (hd = 0) * (prev = 0) * Dll((V2475 - 1),next,V5131,end,0) * (~(tmp >= v)) * Dll(V2449,0,more,V1998,0) * (~(V2449 = 0)) * (~(less = 0)) * (~(more = 0)) * (~(V1998 = 0)) * (~(next = 0)) * less -> [n: 0, data: tmp, b: 0, V3237]
      curr -> [n: V36975, b: more, V36976] * (curr = next) * (prev = 0) * (hd = 0) * Dll((V25829 - 1),next,V36975,end,0) * (tmp >= v) * V36667 -> [n: V36620, b: more, V36621] * Dll(V25803,0,less,V25384,0) * (~(V25803 = 0)) * (~(V36346 >= v)) * (~(more = 0)) * (~(V36667 = 0)) * (~(V1998 = 0)) * (~(V25384 = 0)) * (~(less = 0)) * (~(V12136 = 0)) * (~(V11279 >= v)) * Dll((V12136 - 1),V36667,V36620,V1998,0) * (~(next = 0)) * more -> [n: V36667, data: tmp, b: 0, V36331]
      curr -> [n: V76395, b: less, V76396] * (curr = next) * (hd = 0) * (prev = 0) * Dll((V37153 - 1),next,V76395,end,0) * (~(tmp >= v)) * V76087 -> [n: V76040, b: less, V76041] * Dll(V37107,0,more,V1998,0) * (~(V37107 = 0)) * (~(less = 0)) * (~(V11279 >= v)) * (~(V76087 = 0)) * (~(V25384 = 0)) * (~(V1998 = 0)) * (~(more = 0)) * (~(V36346 >= v)) * (~(V25803 = 0)) * Dll((V25803 - 1),V76087,V76040,V25384,0) * (~(next = 0)) * less -> [n: V76087, data: tmp, b: 0, V69346]
      curr -> [n: V174294, b: less, V174295] * (curr = next) * (hd = 0) * (more = 0) * (prev = 0) * Dll(((k - 1) - 1),next,V174294,end,0) * (~(less = 0)) * (~(tmp >= v)) * (~(next = 0)) * less -> [n: 0, data: tmp, b: 0, V309]
      curr -> [n: V188844, b: more, V188845] * (curr = next) * (hd = 0) * (prev = 0) * Dll((V187134 - 1),next,V188844,end,0) * (tmp >= v) * Dll(V187108,0,less,V186677,0) * (~(V187108 = 0)) * (~(V188331 >= v)) * (~(more = 0)) * (~(less = 0)) * (~(V175572 >= v)) * (~(V186677 = 0)) * (~(next = 0)) * more -> [n: 0, data: tmp, b: 0, V188316]
      curr -> [n: V214754, b: less, V214755] * (curr = next) * (hd = 0) * (more = 0) * (prev = 0) * Dll((V187134 - 1),next,V214754,end,0) * (~(tmp >= v)) * V214434 -> [n: V214387, b: less, V214388] * (~(V186677 = 0)) * (~(V175572 >= v)) * (~(V214434 = 0)) * (~(less = 0)) * (~(V188331 >= v)) * (~(V187108 = 0)) * Dll((V187108 - 1),V214434,V214387,V186677,0) * (~(next = 0)) * less -> [n: V214434, data: tmp, b: 0, V188316]
      curr->b = (struct list *)0;
    } else {

    }
  }
while_0_break: /* CIL Label */ 
  Dll(V4357,0,more,V1998,0) * (~(V4357 = 0)) * (curr = next) * (curr = 0) * Dll(V2475,more,next,end,0) * (~(V1998 = 0)) * (~(more = 0)) * (hd = 0) * (less = 0) * (prev = 0)
  Dll(V70469,0,more,V1998,0) * (~(V70469 = 0)) * (curr = next) * (curr = 0) * Dll(V37153,more,next,end,0) * Dll(V25803,0,less,V25384,0) * (~(V25803 = 0)) * (~(V36346 >= v)) * (~(V1998 = 0)) * (~(V25384 = 0)) * (~(less = 0)) * (~(V11279 >= v)) * (~(more = 0)) * (hd = 0) * (prev = 0)
  (curr = 0) * (curr = next) * less -> [n: 0, data: tmp, b: 0, V3237] * (hd = 0) * (prev = 0) * (~(tmp >= v)) * Dll(V2475,less,next,end,0) * Dll(V2449,0,more,V1998,0) * (~(V2449 = 0)) * (~(less = 0)) * (~(more = 0)) * (~(V1998 = 0))
  Dll(V215157,0,less,V186677,0) * (~(V215157 = 0)) * (curr = next) * (curr = 0) * (~(tmp >= v)) * Dll(V187134,less,next,end,0) * (~(V186677 = 0)) * (~(V175572 >= v)) * (~(less = 0)) * (~(V188331 >= v)) * (hd = 0) * (more = 0) * (prev = 0)
  (curr = 0) * (hd = 0) * (more = 0) * (less = 0) * (prev = 0) * (next = 0) * Dll(k,0,curr,end,0)
  ;
  }
  return;
}
}