let check_error (node : tree_node) error_at_node =
    let r_path = path_to_root node in

    List.iter (fun n -> print_node Format.std_formatter n; fprintf "@.") r_path;
    let _ = Message.msg_string Message.Error ("counterex. size:"^(string_of_int (List.length r_path))) in
    print_string "Expanding....\n";
    let r_path = expand_path_with_old r_path in
    print_string "Done expanding.\n";

    List.iter (fun n -> print_node Format.std_formatter (Tree.get_node_label n); fprintf "@.") r_path;

    (*print_string ";
    List.iter (print_node Format.std_formatter) r_path;*)
let  _ = Message.msg_string Message.Error ("counterex. size:"^(string_of_int (List.length r_path))) in
  
    match Options.getValueOfBool "block" with
        true -> 
          begin
            let r_path_flat = List.map Tree.get_node_label r_path in

            let reg_l = ((List.map (get_region) (Misc.chop_last r_path_flat))@[error_at_node] )
            in

            let id_l = List.map get_id r_path_flat in 

            let rec get_ops ns acc =
              match ns with
                [] -> List.rev acc
              |        [n] -> List.rev (get_op n :: acc)
              |        n1::((n2::rest) as rest') ->
                  match Operation.get_info (get_op n2) with
                    Operation.Call _ ->
                      let caller_region = get_region (Tree.get_node_label n1) in
                      let call_op = List.hd (Abstraction.enabled_ops caller_region) in
                      get_ops rest (call_op :: get_op n1 :: acc)
                  | _ -> get_ops rest' (get_op n1 :: acc) in

            Format.printf "r_path =@.";
            List.iter (fun n -> (print_node Format.std_formatter (Tree.get_node_label n);
                                 Format.printf "@.")) r_path;

            let op_l = get_ops (List.tl r_path) [] in
            Format.printf "op_l =@.";
            List.iter (fun op -> (Operation.print Format.std_formatter op;
                                  Format.printf "@.")) op_l;

            let index = !Abstraction.predIndex in

              match (Stats.time "block_analyze_trace" (Abstraction.block_analyze_trace reg_l op_l) id_l) with
                  (-1,a) -> 
                    (* the assumption is that -1 indicates it goes all the way to the top *)
                    let (root::path) = r_path_flat in (* should never fail ! *)
                      NonEmptyErrorAtRoot(a,root,path)
                | (i,a) ->
                    (* " is the number of hops from the root the falsehood comes *)
                    if index = !Abstraction.predIndex then
                      failwith "No new predicates found.";
                    let (err_path,n',path) = Misc.list_cut' i (r_path_flat) in
                      EmptyErrorAtNode(a,n',path,err_path)
          end
      | false ->
          (*begin
            let rec backward_pre n (err_n,subs_err_n) path =
              match (Tree.get_parent_edge n) with
                  Some(e) ->
                    (* f is n's father and op labels the edge f --> n *)
                    let f = Tree.get_source e
                    and op = Tree.get_edge_label e in
                    let f_reg = get_region f in
                      (* the error subregion at f *)
                      (* JHALA: this subregion business is rubbish. It only blows up the
                          formulas. Not required *)
                      (* JHALA: MAJOR CHANGE! dropping the " in the recursive call *)
        
                    (* JHALA: temporarily comment out!::  let _ = Abstraction.setWPCapRegion f_reg in *)
                    let pre_err_f = (Abstraction.pre err_n op global_variable_table) in
                    let err_f = Region.cap f_reg pre_err_f in
                    let pre_subs_err_f = (Abstraction.spre subs_err_n op global_variable_table) 
                    in

                    let subs_err_f = Region.cap f_reg pre_subs_err_f in
                    (* JHALA: temporarily comment out!:: let _ = Abstraction.resetWPCapRegion () in *)
                      (*let check_emptiness_flag = Abstraction.check_emptiness op in*)
                      if ((*check_emptiness_flag &&*) Stats.time " Region.is_empty subs_err_f)   
                      then
                        begin
                          (*Message.msg_printer Message.Error print_tree_node f;*)
                        EmptyErrorAtNode(err_f, f, n::path, n::path)
                        end
                      else
                        backward_pre f (pre_err_f,pre_subs_err_f) (n::path)
                | None ->
                    (* n is the root *)
                    NonEmptyErrorAtRoot(err_n, n, path)
            in
            let prec_err_n = Abstraction.precise error_at_node in
            let rv = backward_pre node (prec_err_n,prec_err_n) [] in
              (* double checking *)
              (*
            let _ = 
              begin
                let reg_l = 
                  ((List.map (get_region)(Misc.chop_last r_path))@[error_at_node] )
                in
                let op_l = List.map (get_op) ( List.tl r_path) in
                  match (Stats.time " (Abstraction.block_analyze_trace reg_l) op_l) with
                      (-1,a) -> 
                        (* the assumption is that -1 indicates it goes all the way to the top *)
                        let (root::path) = r_path in (* should never fail ! *)
                          NonEmptyErrorAtRoot(a,root,path)
                    | (i,a) ->
                        (* " is the number of hops from the root the falsehood comes *)                     
                        let (n',path) = Misc.list_cut i (r_path) in
                        let _ = Message.msg_printer Message.Error print_tree_node n' in
                          EmptyErrorAtNode(a,n',path,path)
              end
            in *)
              rv
          end*) failwith "block = false not implemented"