let rec refine_path anc path =
    match path with
        []   -> ()
      | n::p ->
          stats_nb_refined_nodes := !stats_nb_refined_nodes + 1 ;

          Message.msg_string Message.Debug "Refining node:" ;
          Message.msg_printer Message.Debug print_tree_node n ;
          Message.msg_string Message.Debug "whose ancestor is:" ;
          Message.msg_printer Message.Debug print_tree_node anc ;

          let anc_reg = get_region anc
          and n_marking_data = get_marking_data n in

            Message.msg_string Message.Debug "calling Abstraction.post with region:" ;
            Message.msg_string Message.Debug ("    region    : " ^ (Region.to_string anc_reg)) ;
            Message.msg_string Message.Debug ("    operation : " ^ (Operation.to_string (get_op n))) ;

            n_marking_data.region <- Abstraction.post anc_reg (get_op n) global_variable_table;

            Message.msg_string Message.Debug "The refined node looks like:" ;
            Message.msg_printer Message.Debug print_tree_node n ;

            refine_path n p