let update_tree_after_refinment entry_pts unprocessed_nodes ts coverers =
    let rec update_and_compute n =
      Format.printf "@.Found node:@.";
      print_node Format.std_formatter n;
      Format.printf "@.with %d children@." (List.length (Tree.get_children n));
      let n_data = get_node_data n in
      (match n_data.mark with
        Unprocessed -> 
          assert (not (Tree.has_child n)) ;
          begin
            match (Options.getValueOfString "comp") with
              "path" -> ();
            | _ ->         
                unprocessed_nodes#add_element n ;
                Message.msg_string Message.Debug "Adding to unprocessed#nodes";
                Message.msg_printer Message.Debug print_tree_node n ;
          end            
      | Processed_Was_Covered_To_Reprocess md ->
              (* --- for debugging --- *)
          assert (not (Tree.has_child n)) ;
          begin
            match (Options.getValueOfString "comp") with
              "path" -> ()
            | _ ->         
                Message.msg_string Message.Debug "Adding to unprocessed#nodes";
                Message.msg_printer Message.Debug print_tree_node n ;
                unprocessed_nodes#add_element n ;
                Region.addCoverer coverers md.region n
          end
      | Processed_Covered md ->
              (* --- for debugging --- *)
          assert (not (Tree.has_child n)) ;
          if md.time_stamp >= ts || called_after md ts then
            begin
              print_string "Redo covered node!\n";
              n_data.mark <- Processed_Was_Covered_To_Reprocess md ;
              Message.msg_string Message.Debug "Adding to unprocessed#nodes";
              Message.msg_printer Message.Debug print_tree_node n ;
              unprocessed_nodes#add_element n
            end
          else
            Region.addCoverer coverers md.region n
      | Processed_Uncovered md ->
          (*Format.printf " md.call_time_stamp;*)
          if called_after md ts then
            begin
              print_string "Redo uncovered node because of call!\n";
              Tree.delete_children n;
              n_data.mark <- Processed_Was_Covered_To_Reprocess md ;
              Message.msg_string Message.Debug "Adding to unprocessed#nodes";
              Message.msg_printer Message.Debug print_tree_node n ;
              unprocessed_nodes#add_element n
            end
          else
            begin
              Format.printf "This node's function target was called early enough: %d vs. " ts;
              (match md.call_time_stamp with
                None -> Format.printf "NONE@."
              | Some t -> Format.printf "%d@." t);
              Region.addCoverer coverers md.region n
            end)
    (*in List.iter update_and_compute (get_children n)*)
    in let funcs fname entries =
      let update_entry entry =
        let stamp = get_time_stamp entry in
        Format.printf "Entry for %s: %d vs. %d@." fname stamp ts;
        if stamp >= ts then
          remove_pt entry_pts fname entry
        else
          update_and_compute entry
      in nset_iter update_entry entries
    in
      Format.print_string "Updating tree after refinement....\n";
      Region.clearCoverers coverers;
      if ts = 0 then
        begin
          (* We must start all over again. We can't do this the normal way, since that
           * would remove the main program entry point for being in the error time range. *)
          Format.printf "Start over again!@.";
          let mainfn = List.hd (Options.getValueOfStringList "main") in
          let tree_root = !(Hashtbl.find tree_node_table 0) in
          clear_pts entry_pts;
          add_pt entry_pts mainfn tree_root;
          Tree.delete_children tree_root;
          (get_node_data tree_root).mark <-
            Processed_Was_Covered_To_Reprocess (get_marking_data tree_root);
          unprocessed_nodes#add_element tree_root
        end
      else
        Hashtbl.iter funcs entry_pts