bdd_ptr bddpaths[10];

/* function that updates BDD pointers floating around in user's code;
the remaining ones are kept in the sub_results list below */

void update_bddpaths(unsigned (*new_place) (unsigned node)) {
  int j;
  
  /* update the pointers in bddpaths */

  for (j = 0; j < exp_count; j++) 
    bddpaths[j] = new_place(bddpaths[j]);
}

/* we can only update pointers that are not stored as local
   variables, so values of local variables are thrown onto a stack */

DECLARE_SEQUENTIAL_LIST(sub_results, unsigned);

bdd_ptr makepath(bdd_manager *bddm, ..., 
                  void (*update_bddpaths) 
                     (unsigned (*new_place) (unsigned node))) {

...
  bdd_ptr res, sub_res, default_state_ptr;
 
  sub_res = makepath(bddm, n+1, leaf_value, update_bddpaths);

  /* push BDD pointer sub_res on list sub_results */

  PUSH_SEQUENTIAL_LIST(sub_results, unsigned, sub_res);
  
  /* insert a new hashed node; thus potentially changing the pointer
  to the node known as sub_res above, and also potentially changing
  the pointers in bddpaths[10].  But bdd_find_leaf_hashed automatically
  updates all pointers in the sub_results list, since it was provided
  as an argument.  Also, the function update_bddpaths is called when a
  doubling of the table takes place and an appropriate renaming function
  new_place is supplied by bdd_find_leaf_hashed */

  default_state_ptr = 
    bdd_find_leaf_hashed(bddm, 
                         default_state, 
                         SEQUENTIAL_LIST(sub_results), 
                         update_bddpaths);

  /* restore the value of sub_res */

  POP_SEQUENTIAL_LIST(sub_results, unsigned, sub_res);
  ...
}