let model_check init o_err =
    let interface = Options.getValueOfString "interface" in
    let component = Options.getValueOfString "component" in

    Message.msg_string Message.Debug "Entering parallel_model_check" ;
    Message.msg_string Message.Debug ("   init region: " ^ (Region.to_string init)) ;
    Message.msg_string Message.Debug 
      (match o_err with None -> "No error region" | Some e -> "   error region: " ^ (Region.to_string e)) ;
    let err = 
      match o_err with
        None -> failwith "parallel_model_check: error region not specified."
      | Some e -> e
    in 
    (* the final result of the search will be stored here *)
    let resulting_error_path = ref None
    and offending_error_node = ref None
      
    (* this boolean variable allows to stop the while-loop *)
    and continue = ref true

    (* The structure to look up which node covers another begins as empty *)
    and coverers = Region.emptyCoverers ()

    (* Record of which entry points a function has *)
    and entry_pts : (string, node_set) Hashtbl.t = Hashtbl.create 100

    (* Record of which exit points a function has *)
    and exit_pts : (string, node_set) Hashtbl.t = Hashtbl.create 100

    (* helper object to create nodes *)
    and tnc = new tree_node_creator

   
    (* the set of pending nodes to be processed *)
    and unprocessed_nodes = 
      if Options.getValueOfBool "bfs" then new Search.bfsiterator
      else new Search.dfsiterator

    (* the global time used for time stamps *)
    and time = ref 0 in

    let summary_edges_enode n =
      match get_kind n with
        Entry en -> List.map (fun (n_out, path) -> (n, n_out, path)) (nmap_to_list en.exit_pts)
      |        _ -> raise (Failure "Entry node expected in summary_edges_enode") in

    let summary_edges fname =
      let epts = get_pts entry_pts fname in
      List.fold_left (@) [] (List.map summary_edges_enode
                               (nset_to_list epts)) in

    let lift_and_propagate sum_es call_n reg_in =
      (*let reg = get_region call_n in
      let op =
        match Abstraction.enabled_ops reg with
          [op] -> op
        | _ -> failwith " in
      let reg_in = Abstraction.post reg op global_variable_table in*)
      print_string "lift_and_propagate\n";
      let lift_one (n_in, n_out, (path : summary_path)) =
        (*fprintf ";
        (*Region.print Format.std_formatter reg_in;*)
        print_node Format.std_formatter call_n;
        fprintf ";
        (*Region.print Format.std_formatter (get_region n_in);*)
        print_node Format.std_formatter n_in;
        fprintf ";*)
        if Region.leq reg_in (get_region n_in) then
          (match get_kind n_in with
            Entry en ->
              fprintf "A call site matched in lift_and_propagate.@.";
              print_node Format.std_formatter call_n;
              fprintf "@.";
              let summary_already_exists n_child =
                let edge = get_parent_edge n_child in
                match edge with
                  SummaryEdge {n_out = n_out'} -> node_equal n_out n_out'
                | _ -> false in
              if List.exists summary_already_exists (Tree.get_children call_n) then
                fprintf "I would have propagated this edge, but it already exists!@."
              else
                (update_caller call_n (Some (get_time_stamp n_out));
                 let retOp = SummaryEdge {path = path; n_in = n_in; n_out = n_out} in
                 let child = tnc#create_child Node Unprocessed retOp call_n in
                 Format.printf "Now caller has %d children.@." (List.length (Tree.get_children call_n));
                 unprocessed_nodes#add_element child)
          | _ -> failwith "Entry node expected in lift_and_propagate")
        (*else
          print_string "*)
      in List.iter lift_one sum_es in

    let new_summary_edge (n_in, path_in) (n_out, path_out) =
      (*fprintf ";
      print_node Format.std_formatter n_in;
      fprintf ";
      print_node Format.std_formatter n_out;
      fprintf ";
      let print_path_node n =
        print_node Format.std_formatter n;
        fprintf " in
      List.iter print_path_node path_in;
      fprintf ";
      List.iter print_path_node path_out;
      fprintf ";*)

      let path = ConsPath (path_in, path_out) in

      (match (get_kind n_in, get_kind n_out) with
        (Entry en, Exit ex) ->
          en.exit_pts <- nmap_add en.exit_pts n_out path;
          ex.entry_pts <- nmap_add ex.entry_pts n_in path;
          (*Format.fprintf Format.std_formatter "
            (nset_size en.call_sites);
          print_node Format.std_formatter n_in;
          fprintf ";*)
          nmap_iter (lift_and_propagate [(n_in, n_out, path)])
            en.call_sites
      | _ ->
          (match (get_kind n_in, get_kind n_out) with
            (Exit _, _) -> print_string "Came from Exit\n";
          | (_, Entry _) -> print_string "Went to Entry\n";
          | (Node, _) -> print_string "Came from Node\n";
          | (_, Node) -> print_string "Went to Node\n";
          | _ -> print_string "Huh?\n");
          failwith "Expecting edge from Entry to Exit in new_summary_edge");
    print_string "Summary edge added\n" in
          
    let new_summary_edges ns n_out =
      List.iter (fun n_in -> new_summary_edge n_in n_out) ns in
      
    (* The function for constructing children .. and adding them to the tree *)
    let construct_children node accu op =
      (tnc#create_child Node Unprocessed op node)::accu
    in                                 
                                                 
 (* the root of the reachability tree *)
    let tree_root =
      tnc#create_root (Processed_Was_Covered_To_Reprocess { time_stamp = !time ;
                                                            region = init ;
                                                            call_time_stamp = Some 0 }) in
    add_pt entry_pts (Abstraction.reg_function_name init) tree_root;

    let new_entry mark n op fname =
      let n_region = get_region n in
      let n_root = tnc#create_root Unprocessed in

      let entry_region = Abstraction.post n_region op global_variable_table in

      let call_sites = nmap_add nmap_empty n entry_region in
      let entry = Entry {call_sites = call_sites;
                         exit_pts = nset_empty} in

      let md = { time_stamp = (time := !time + 1; !time);
                 region = entry_region;
                 call_time_stamp = Some 0} in
      let n_entry = tnc#create_child entry (mark md) (PathEdge op) n_root in

      update_caller n None; (* None indicates an in-progress function call.
                             * The stamp will be updated with an exit node's time
                             * stamp if the call terminates. *)
      (*unprocessed_nodes#add_element n_entry;*)

      n_entry in

    let new_exit n op =
      let n_region = get_region n in
      let exit = Exit {entry_pts = nset_empty} in
      let region = n_region (*Abstraction.post n_region op global_variable_table*) in
      let marking_data = { region = region;
                           time_stamp = (time := !time + 1 ; !time);
                           call_time_stamp = Some 0 } in
      let child = tnc#create_child exit
          (Processed_Uncovered marking_data)
          (PathEdge op) n in
      
      let fname = Abstraction.reg_function_name n_region in
      print_string "It's a new exit point for ";
      print_string fname;
      print_string "!\n";
      add_pt exit_pts fname child;
      child in

    let do_subtree_cut_refinement anc new_anc_region err_path err_n =
      let use_bfs = Options.getValueOfBool "bfs" in

      fprintf "Subtree cut refinement starting at:@.";
      print_node Format.std_formatter anc;
      fprintf "@.";
      
      let new_anc_region =
        match get_kind anc with
          Entry en ->
            print_string "Entry found!\n";
            (* We must treat Entry nodes specially to assure that new predicates are
             * inferred correctly. *)
            Format.fprintf Format.std_formatter "Choose 1 of %d call sites.@." (nset_size en.call_sites);
            let reg = get_region anc in
            (match nmap_choose (fun r -> Region.leq r reg) en.call_sites with
              None -> new_anc_region
            | Some caller ->
                let caller = get_region caller in
                let caller = Abstraction.focus_stamp caller in
                Abstraction.post caller (List.hd (Abstraction.enabled_ops caller))
                  global_variable_table)
        | Exit ex -> failwith "Exit found!"
        | _ -> new_anc_region in

      Message.msg_string Message.Debug "This ancestor now looks like:" ;
      (*Message.msg_printer Message.Debug print_tree_node anc ;*)
        (* Note that here there is no path to update as the entire subtree is going to be chopped off... *)

      Message.msg_string Message.Debug "Now deleting subtree:" ;

      (*let old_children = Tree.get_children anc in*)

      (* Invalidate summary edges for error nodes, finding the earliest timestamp along
       * the path in the process *)

      iter_pts (fun fname pts ->
        Format.fprintf Format.std_formatter "@.Entry points to %s:@." fname;
        nset_iter (fun n -> print_node Format.std_formatter n; fprintf "@.") pts)
        entry_pts;

      let clear_summary n_in en =
        en.exit_pts <- nmap_empty;
        fprintf "clear_summary ";
        print_node Format.std_formatter n_in;
        fprintf "@." in

      let rec backup n stamp =
        fprintf "backup: ";
        print_node Format.std_formatter n;
        fprintf "@.";
        if node_equal n anc then
          (min stamp (get_time_stamp n), true)
        else
          (match get_kind n with
            Entry en ->
              clear_summary n en;
              (min stamp (get_time_stamp n), false)
          | _ ->
              let (stamp, stop) =
                (match get_parent_edge n with
                  SummaryEdge {n_in = n_in; n_out = n_out} ->
                    (*let stamp = clear_summary n_in (get_entry n_in) stamp in*)
                    fprintf "<RETURN>@.";
                    let ret = backup n_out stamp in
                    fprintf "<CALL>@.";
                    ret
                | _ -> (stamp, false)) in
              if stop then
                (stamp, true)
              else
                backup (Tree.get_parent n) stamp) in

      let invalidate stamp n =
        let parent = Tree.get_parent n in
        (match get_region_opt parent with
          None -> ()
        | Some reg ->
            (match Abstraction.enabled_ops reg with
              [op] ->
                (match Operation.get_info op with
                  Operation.Call (_, fname, _) ->
                    let checkEntry n_in =
                      Format.printf "checkEntry@.";
                      let en = get_entry n_in in
                      if nset_mem en.call_sites parent then
                        clear_summary n_in en
                    in nset_iter checkEntry (get_pts entry_pts fname)
                | _ -> ())
            | _ -> ()));
        min stamp (get_time_stamp n)

      in let first_stamp = List.fold_left invalidate (get_time_stamp err_n) err_path in
      let (first_stamp, _) = backup err_n first_stamp in
      let first_stamp = 0 in
      Printf.printf "first_stamp = %d\n" first_stamp;

      (* Jhala: I'm assuming that its ok to just empty this out and fill it back up when we are traversing the tree later ... this whole traversal business is not good by the way, there should be a much more incremental way to do it *)
      unprocessed_nodes#empty_out ();

      let data = Tree.get_node_label anc in
      let marking_data = get_marking_data anc in
      (* update the ancestor region *)
      Message.msg_string Message.Debug "Updating the ancestor's region..." ;
      marking_data.region <- new_anc_region ;

      fprintf "Delete children of ";
      print_node Format.std_formatter anc;
      fprintf "@.";
      tnc#delete_children anc;

      Message.msg_string Message.Debug "Now re-adding children:" ;

      let add_children ops =
        print_string "add_children\n";
        List.fold_left (construct_children anc) [] 
          (List.map (fun s -> PathEdge s) ops) in

      let children =
        match Abstraction.enabled_ops new_anc_region with
          [op] as ops ->
            (match Operation.get_info op with
              Operation.Call (_, fname, _) -> [(*new_entry (fun s -> Processed_Covered s)
                                                 anc op fname*)]
            | Operation.Ret _ ->
                print_string "Anchor is a return\n";
                let n_out = new_exit anc op in

                (* Just adding an unprocessed node for a particular return point is not
                 * good enough, because its parent may have been deleted due to summary
                 * edges that appear in the " part of the trace having been deleted
                 * because they also appear in the " part. *)
                let entries = entry_pts_node (Tree.get_parent n_out) in
                let entries =
                  List.fold_left (fun m (n, p) -> nmap_add m n p) nmap_empty entries in
                let lift n_in path =
                  let en = get_entry n_in in
                  let create_summary call_n _ =
                    fprintf "Refining summary edge for:@.";
                    print_node Format.std_formatter call_n;
                    fprintf "@.";
                    let retOp = SummaryEdge {path = path; n_in = n_in; n_out = n_out} in
                    let _ = tnc#create_child Node Unprocessed retOp call_n in
                    () in
                  nmap_iter create_summary en.call_sites in
                nmap_iter lift entries;
                [n_out]
            | _ -> add_children ops)
        | ops -> add_children ops in

      fprintf "The children are:@." ;
      List.iter (fun ch -> (print_tree_node Format.std_formatter ch; fprintf "@.")) children;

      fprintf "@.Anc:@.";
      print_node Format.std_formatter anc;
      fprintf "@.";
      (*fprintf ";
      List.iter (fun s -> print_node Format.std_formatter s; fprintf ") old_children;*)
      
      
      (* add the children to the set of pending nodes *)
      (* Jhala: This should all be done by the the subtree cut 
         Message.msg_string Message.Debug " ;
         unprocessed_nodes#add_list children ;
       *)

      (* Recalculate reached region from all entry points that remain valid *)
      Message.msg_string Message.Debug "Updating the currently reached region" ;
      Stats.time "update_tree_after_refinement[CUT]" 
        (update_tree_after_refinment entry_pts unprocessed_nodes
           first_stamp) coverers;
      print_string "Refinement complete.\n"
    in


    (* the refinment process *)
    let do_refinment anc path new_anc_region =
      let anc_data = Tree.get_node_label anc in
      let anc_marking_data = get_marking_data anc in
        (* update the ancestor region *)
      Message.msg_string Message.Debug "Updating the ancestor's region..." ;
      anc_marking_data.region <- new_anc_region ;
      
      Message.msg_string Message.Debug "This ancestor now looks like:" ;
      Message.msg_printer Message.Debug print_tree_node anc ;
      
        (* update the path *)
      Message.msg_string Message.Debug "Refining the nodes along the path..." ;
      refine_path anc path ;
      
        (* update the tree and the reached region *)
      Message.msg_string Message.Debug "Updating the markings and the reached region..." ;
      Stats.time "update after refine [PATH]"
          (update_tree_after_refinment entry_pts unprocessed_nodes
             anc_marking_data.time_stamp) coverers
    in

    (* this function deletes covered nodes from the tree *)
    let rec reclaim n = 
      if (Tree.has_child n || (not (Tree.has_parent n))) then ()
      else 
        begin
          let par = get_parent n in
          Tree.delete_child n; 
          reclaim par
        end
    in
      (* add the root to the pending unprocessed nodes *)
      unprocessed_nodes#add_element (tree_root) ;

      while (!continue && unprocessed_nodes#has_next ()) do
        stats_nb_iterations := !stats_nb_iterations + 1;

        (* the search is not finished yet *)
        if (!stats_nb_iterations mod 10 == 0) then
          begin
            Message.msg_string Message.Normal ("While loop tick:"^(string_of_int !stats_nb_iterations));
            flush stdout; flush stderr;
            Abstraction.print_abs_stats ()
          end ;
        Message.msg_string Message.Debug "\n\n****************************************************************************\n" ;
        Message.msg_string Message.Debug "Next iteration of model-check's big while-loop" ;
        Message.msg_printer Message.Debug Format.pp_print_int (!stats_nb_iterations);
        (* Message.msg_string Message.Debug " ;
           Message.msg_printer Message.Debug Region.print !reached_region ;*)

        (* let's process the next pending node *)
        let n        = unprocessed_nodes#next () in
          Message.msg_string Message.Normal (*Debug Normal*) "Now processing tree node:" ;
          Message.msg_printer Message.Normal (*Debug Normal*) print_tree_node n ;

          let n_data   = (Tree.get_node_label n) in

          let n_marking_data = 
            match n_data.mark with
              Unprocessed ->
                let region = match get_parent_edge n with
                  PathEdge op ->
                    Stats.time "main post" (Abstraction.post (get_region (get_parent n)) op)  global_variable_table
                | SummaryEdge {n_out = n_out} ->
                    let reg = get_region (get_parent n_out) in
                    let parent_reg = get_region (get_parent n) in
                    let op = match Abstraction.enabled_ops parent_reg with
                        [op] -> op 
                      | _ -> failwith "Multiple children of call node!" 
                    in
                      Abstraction.summary_post op parent_reg reg global_variable_table in
                { region = region;
                  time_stamp = (time := !time + 1 ; !time);
                  call_time_stamp = Some 0 };
            | Processed_Was_Covered_To_Reprocess md -> md
            | _ -> failwith "LazyModelChecker.model_check: unexpected marking data"
          in
            (* --- for debugging --- *)
            (* assert (n_data.mark == Unprocessed) ; *)

          let n_region = n_marking_data.region in

          (* the error region at this node *)
          let err_n = Stats.time "cap" (Region.cap n_region) err in
            Message.msg_string Message.Debug ("Error region at this node: " ^ (Region.to_string err_n)) ;

            if (Region.is_empty err_n)
            then
              begin
                (* no error found at this node *)
                Message.msg_string Message.Debug "No error found at this node" ;

                (* let's test whether this node is covered *)
                Message.msg_string Message.Debug "Let's test whether this node is covered" ;
                let coverable =  
                  if (Options.getValueOfBool "cov") 
                  then Abstraction.coverable n_region
                  else true
                in
                let covered = 
                  if coverable
                  then (Stats.time "Covered check:" (Region.findCoverer coverers) n_region)
                  else None
                in
                match (covered, Region.is_empty n_region) with
                  (_, true) -> ()
                | (Some n', _) ->
                    begin
                      (* this node is covered *)
                      Message.msg_string Message.Debug "This node is covered" ;
                     
                      print_string "*** COVERED ";
                      print_string (Region.to_string n_region);
                      print_string " BY: ";
                      print_node Format.std_formatter n';
                      print_char '\n';
                      flush stdout;
                        
                      let entries = entry_pts_node n in
                      let exits = exit_pts_node n' in
                      
                      print_string ("NEW SUMMARIES " ^ string_of_int (List.length entries) ^ " vs. " ^ string_of_int (List.length exits) ^ "\n");
                      (*print_string ";*)
                      List.iter (new_summary_edges entries) exits;
                      (*print_string "*)
  
                      (* mark n as processed and covered *)
                      n_data.mark <- Processed_Covered n_marking_data;
                      if (Options.getValueOfBool "reclaim") 
                      then
                        reclaim n;
                      ()
                    end
                | (None, _) ->
                  begin
                    (* this node is not covered *)
                    Message.msg_string Message.Debug "This node is not covered" ;
                    Message.msg_string Message.Debug "Constructing its successor children..." ;
                    
                    (* we construct its successor children *)

                    (* Adamc to-do:
                     * If n is a function call to f:
                     *    Create an Entry node for this function call
                     *    Add it to the worklist
                     *    Lift f's summary edges to this call site
                     * If n is a function exit from f:
                     *    Record n as a reachable exit point from f
                     *    Final all function entry pts EN that reach n
                     *    Create summary edges between EN x {n}
                     * Otherwise, n is a boring node, so:
                     *    Carry on as usual, letting Abstraction do the work
                     *)
                    
                    let enabled_ops = List.map (fun s -> PathEdge s)
                        (Abstraction.enabled_ops n_region) in
                    
                    (*Message.msg_string Message.Debug (*Normal*) " ;
                    List.iter (function child -> Message.msg_printer Message.Debug (*Normal*) print_tree_node child) children ;*)
                    
                    (* add the children to the set of pending nodes *)
                    let addChildren () =
                      let children = List.fold_left (construct_children n) [] enabled_ops in
                      Message.msg_string Message.Debug "Adding the children to the set of pending unprocessed#nodes" ;
                      unprocessed_nodes#add_list children ;
                      Message.msg_string Message.Debug ("Remaining nodes:"^(string_of_int (unprocessed_nodes#sizeof ()))); 
                      unprocessed_nodes#iter (fun x -> Message.msg_printer Message.Debug print_tree_node x) in

                    (* mark n as processed and uncovered *)
                    Message.msg_string Message.Debug "Updating the node's marking" ;
                    n_data.mark <- Processed_Uncovered n_marking_data ;
                                    
                    Message.msg_string Message.Debug "This node now looks like:" ;
                    Message.msg_printer Message.Debug print_tree_node n ;

                    (match enabled_ops with
                      [op] ->
                        let op = edge_to_op op in
                        (match Operation.get_info op with
                          Operation.Call (_, fname, _) ->
                            let n_entry = new_entry
                                (fun s -> Processed_Was_Covered_To_Reprocess s)
                                n op fname in
                            
                            let in_region = get_region n_entry in

                            let found_one = ref false in

                            (* Tell any matching function entry points that they have
                             * a new caller. *)
                            let checkEntry n_in =
                              if Region.eq in_region (get_region n_in) then
                                (let en = get_entry n_in in
                                en.call_sites <- nmap_add en.call_sites n in_region;
                                print_string "Matched a previous call!\n";
                                found_one := true)
                              else
                                (Format.printf "Did not match ";
                                 print_node Format.std_formatter n_in;
                                 Format.printf "@.")
                            in nset_iter checkEntry (get_pts entry_pts fname);

                            if not !found_one then
                              (add_pt entry_pts fname n_entry;
                               Format.printf "New entry point for %s.@." fname;
                               unprocessed_nodes#add_element n_entry);

                            (* Propagate any summary edges for matching calls that have
                             * already been explored to exit points. *)
                            lift_and_propagate (summary_edges fname) n in_region
                        | Operation.Ret exp ->
                            let child = new_exit n op in
                            let entries = entry_pts_node n in
                            Format.fprintf Format.std_formatter "|entries| = %d@."
                              (List.length entries);
                            print_string "New summary edges to exit node.\n";
                            new_summary_edges entries (child, ListPath [])
                        | Operation.Normal -> addChildren ())
                    | _ -> addChildren ());

                      (* add n's region to the reached region *)
                    if (coverable) then 
                      begin
                        Message.msg_string Message.Debug "Updating the currently reached region" ;
                        Region.addCoverer coverers n_region n;
                        (*print_string "*)
                      end
                  end
              end
            else
              begin
                (* error found *)
                Message.msg_string Message.Normal "Error found : checking validity." ;
                Message.msg_string Message.Debug ("Error at depth"^(string_of_int (Tree.node_depth n))); 
        (*        List.iter (function x -> Message.msg_printer Message.Debug print_tree_node x) (path_to_root n) ; *)
                if (Options.getValueOfBool "cref") 
                then
                  failwith "cref not supported."
                  (* Adamc: Ignoring cref option for now *)
                  (*begin
                    let path_to_root = path_to_root n in
                    let list_of_regs = (List.map (get_region)  (Misc.chop_last path_to_root))@[n_region] in
                    let list_of_ops = List.map (get_op) ( List.tl path_to_root) in
                    (* note that list_of_regs should be 1 longer than list of ops *)
                    let _ = 
                      try 
                        Message.msg_string Message.Normal ("^(string_of_int (List.length list_of_regs)));
                        Abstraction.analyze_trace list_of_regs list_of_ops
                      with fail_exception ->  
                        begin
                          List.iter (function x -> Message.msg_printer Message.Normal print_tree_node x)
                            path_to_root;
                          print_string ";
                          raise fail_exception
                        end 
                    in
                    stats_nb_refinment_processes := !stats_nb_refinment_processes + 1;
                    print_string ";
                    do_subtree_cut_refinement tree_root (get_region tree_root) n
                      
                  end*)
                else 
                  begin
                    Message.msg_string Message.Debug "Error found at this node" ;
                    
                    (* this node will have to be reprocessed after refinment *)
                    (* JHALA: why will this node have to be reprocessed after refinement ? *) 
                    Message.msg_string Message.Debug "Re-adding this node to the set of pending unprocessed nodes" ;
                    n_data.mark <- Processed_Was_Covered_To_Reprocess n_marking_data ;
                    Message.msg_string Message.Debug "Adding to unprocessed#nodes";
                    Message.msg_printer Message.Debug print_tree_node n ;
                    unprocessed_nodes#add_element n ;
                    
                (* let's now test whether this error is a real one *)
                    Message.msg_string Message.Debug "Testing whether this error is a real one" ; 
                    let check_refinement = 
(*
                      if (Options.getValueOfString " = ") then
                        check_error_fwd 
                      else *)
                        check_error
                    in
                      try 
                        match (Stats.time "check_error" (check_refinement n) err_n) with
                            EmptyErrorAtNode(err_anc, anc, path, err_path) ->
                                (* this is a false error *)
                              begin
                                Message.msg_string Message.Normal "This is a false error (seq)" ;
                                Message.msg_string Message.Debug "The check_error function ended up with" ;
                                Message.msg_string Message.Debug "     at ancestor: " ;
                                Message.msg_printer Message.Debug print_tree_node anc ;
                                Message.msg_string Message.Debug "     along the path (from the ancestor to the current node):" ;
                                Message.msg_printer Message.Debug print_tree_node anc ;
                                List.iter (function x -> Message.msg_printer Message.Debug print_tree_node x) path ;
                                demo_process n n_region false;
                                
                                if (Options.getValueOfBool "stop") then
                                  failwith ("FALSE ERROR CHOKE");

                                print_string "FALSE ERROR:\n";
                                List.iter (print_node Format.std_formatter) path;

                                (* let's refine *)
                                Message.msg_string Message.Debug "\n\nLet's refine the nodes along that path" ;
                                if (Options.getValueOfBool "traces") then dumppath n n_region;
                                
                                      let anc_region = (get_region anc) in
                                fprintf "@.anc_region is: ";
                                Region.print Format.std_formatter anc_region;
                                fprintf "@.";
                                let focused_anc_region = 
                                  try
                                    let rv = 
                                      match Options.getValueOfBool "block" with
                                          false ->
                                            Stats.time "focus" (Abstraction.focus anc_region) err_anc 
                                        | true -> Abstraction.focus_stamp anc_region
                                            (* analysis is already done! *) 
                                    in
                                      if (Options.getValueOfBool "restart" || Options.getValueOfBool "localrestart") then 
                                        begin
                                          Message.msg_string Message.Error "About to Restart";
                                          
                                          raise RestartException
                                            
                                        end
                                        else rv
                                  with Abstraction.NoNewPredicatesException ->
                                    begin
                                      fprintf "NO NEW PREDS!@.";
                                      (* Adamc: Ignoring predH for now *)
                                       if (Options.getValueOfInt "predH" = 3) then
                                        begin
                                          let path_to_root = path_to_root n in
                                          let list_of_regs = (List.map (get_region)  (Misc.chop_last path_to_root))@[n_region] in
                                          let list_of_ops = List.map get_op ( List.tl path_to_root) in
                                          Message.msg_string Message.Normal 
                                            ("\n No of regs: "^(string_of_int (List.length list_of_regs)));
                                          Message.msg_string Message.Normal 
                                            ("\n No of ops : "^(string_of_int (List.length list_of_ops)));
                                          try 
                                            (Abstraction.find_all_predicates list_of_regs list_of_ops; 
                                             raise RestartException
                                               )
                                          with e -> 
                                            
                                            begin
                                              if (e = RestartException) then raise e 
                                              else 
                                                begin
                                                  Message.msg_string Message.Minor "This is a false error" ;
                                                  Message.msg_string Message.Minor "The check_error function ended up with" ;
                                                  Message.msg_string Message.Minor ("     an empty error: " ^ (Region.to_string err_anc)) ;
                                                  Message.msg_string Message.Minor "     at ancestor: " ;
                                                  Message.msg_printer Message.Minor print_tree_node anc ;
                                                  Message.msg_string Message.Minor "     along the path (from the ancestor to the current node):" ;
                                                  Message.msg_printer Message.Minor  print_tree_node anc ;
                                                  List.iter (function x -> Message.msg_printer Message.Minor print_tree_node x) path ;
                                                  Message.msg_string Message.Normal ("find_all_predicates raises : "^(Printexc.to_string e)) ; 
                                                  dumptrace (false, list_of_ops, list_of_regs);
                                                  failwith ("problem in find_all_predicates !") 
                                                end
                                            end
                                        end
                                      else 
                                        if (Options.getValueOfInt "predH" = 1 && 
                                            (not (Abstraction.predicate_fixpoint_reached ()))) 
                                        then (Message.msg_string Message.Normal "Raising Restart"; raise RestartException)
                                        else
                                          (* Adamc: Only treating this case (i.e., predH not set) *)
                                          begin
                                            let path_to_root = path_to_root n in
                                            List.iter (fun n -> fprintf "On real path: ";print_node Format.std_formatter n; fprintf "@.") path_to_root;
                                            let path_to_root = expand_path path_to_root in
                                            List.iter (fun n -> fprintf "On path: ";print_node Format.std_formatter n; fprintf "@.") path_to_root;
                                            let list_of_regs = (List.map (get_region)  (Misc.chop_last path_to_root))@[n_region] in
                                            let list_of_ops = List.map (get_op) ( List.tl path_to_root) in
                                            dumptrace (false, list_of_ops, list_of_regs);
                                              failwith ("No new preds found !-- and not running allPreds ...")
                                          end
                                    end
                                in (* for the focused_anc_region *)
                                Message.msg_string Message.Debug "Done calling Focus";
                                Message.msg_string Message.Debug ("The focused region for the ancestor is: " ^ (Region.to_string focused_anc_region)) ;
                
                                stats_nb_refinment_processes := !stats_nb_refinment_processes + 1 ;

                                fprintf "REFINING with region @.";
                                Region.print Format.std_formatter focused_anc_region;
                                fprintf "!!@.";

                                begin
                                match (Options.getValueOfString "comp") with
                                    "path" -> 
                                      begin
                                        Stats.time "do_ref [PATH]" (do_refinment anc path) focused_anc_region ;
                                        Message.msg_string Message.Error "PATH"; 
                                        Message.msg_string Message.Debug "The refined path looks like:" ;
                                        Message.msg_printer Message.Debug print_tree_node anc ;
                                        List.iter (function x -> Message.msg_printer Message.Debug print_tree_node x) path ;
                                      end
                                  | _ ->
                                      Stats.time "subtree_cut_refinement" (do_subtree_cut_refinement anc focused_anc_region err_path) n
                              end
 end
                | NonEmptyErrorAtRoot(err_root, root, path) ->
                            (* --- for debugging --- *)
                            begin
                            assert (root == tree_root) ;
                            (* this is a real error *)
                            (* we put the error path in the appropriate variable *)
                        
                              let path = expand_path path in
                              List.iter (fun n -> fprintf "Path: "; print_node Format.std_formatter n; fprintf "@.") path;

                              resulting_error_path := Some(err_root,
                                                           List.map (get_op) path,
                                                           err_n) ;
                              offending_error_node := Some (Misc.list_last path) ;
                              (* print the unknown functions on the path *)
                              Abstraction.print_debug_info (List.map (get_op) path);
                              demo_process n n_region true;
                              
                              (* and break the while-loop *)
                              continue := false
                            end
                      with RestartException -> 
                        begin
                          failwith "Restart not supported yet"
                          (*stats_nb_refinment_processes := !stats_nb_refinment_processes + 1;
                          print_string ";
                          do_subtree_cut_refinement tree_root (get_region tree_root) n*)
                        end
                  end
              end
      done ;
    Message.msg_string Message.Normal ("Depth of tree: "^(string_of_int (Tree.subtree_depth tree_root)));
    fprintf "Function summaries:@.";
    print_summaries Format.std_formatter entry_pts;

    if interface <> "" && component <> "" && !resulting_error_path = None then
      begin
        let get_spec fname =
          let folder sums entry =
            let reg_in = get_region entry in
            let exits = (get_entry entry).exit_pts in
            let exits = nmap_fold (fun exits exit _ -> (get_region exit) :: exits) [] exits in
            (reg_in, exits) :: sums in
          let summaries = nset_fold folder [] (get_pts entry_pts fname) in
          Format.fprintf Format.std_formatter "@.--- Summaries for %s ---@." fname;

          Abstraction.build_spec fname summaries in
        Abstraction.init_spec ();
        let sInterface = get_spec interface in
        let sComponent = get_spec component in
        let res = Abstraction.check_spec sComponent sInterface in
        fprintf "@.@.Correct? ";
        match res with
          Abstraction.Yes -> fprintf "YES!@.";
        | Abstraction.No -> fprintf "NO!@.";
        | Abstraction.Maybe pred ->
            fprintf "Only if ";
            Predicate.print Format.std_formatter pred;
            fprintf "@."
      end;

    match (!resulting_error_path) with 
      Some ((_,_,err_n) as e_path) -> 
        begin
          let err_node = 
            match !offending_error_node with
                    Some n -> n
            | None -> failwith "Quit while w/ error loop w/o setting offending_error_node!"
          in
          let path_to_root = Tree.path_to_root err_node in
          let list_of_regs = (List.map (get_region)  (Misc.chop_last path_to_root))@[get_region err_node] in
          let list_of_ops = List.map (get_op) ( List.tl path_to_root) in
          dumptrace (true,list_of_ops,list_of_regs);
          Error_reached e_path
            
        end
    | None -> (* print the tree *) 
        begin
              if (Options.getValueOfBool "pf") 
              then 
                (Stats.time "Generate Proof:" (build_proof_tree ()) tree_root) 
              else (count_tree_nodes tree_root);
          (* !resulting_error_path *)
              No_error
        end