# dead code eliminated (only tracks what's needed, so sensible to changes in annotations)

type List = {
  bool next_ge,next_le; /* automatically generated */
  data next:List;
}

pred inorder_ge(pointer p:List) = 
  allpos t of List: p<next*>t & t.next!=null => t.next_ge=true;

pred inorder_le(pointer p:List) = 
  allpos t of List: p<next*>t & t.next!=null => t.next_le=true;

proc reverse(data list:List):List
[inorder_ge(list)]
{
  data res:List;
  pointer temp:List;
  bool list_ge_res,temp_ge_list,temp_ge_res; /* automatically generated */
  while [inorder_ge(list) & inorder_le(res) & (res!=null & list!=null => list_ge_res=true)]
        (list!=null) {
    temp = list.next, 
      temp_ge_list = list.next_ge; /* automatically generated */
    list.next = res, 
      list.next_le = list_ge_res; /* automatically generated */
    res = list, 
      temp_ge_res = temp_ge_list; /* automatically generated */
    list = temp, 
      list_ge_res = temp_ge_res; /* automatically generated */
  }
  return res;
}
[inorder_le(return)]