let build_proof_tree () root =
      Message.msg_string Message.Normal "In build_proof_tree"; 
      Message.msg_string Message.Error "In build_proof_tree"; (* Say that we are building proof 
                                                                 on both stdout and stderr *)
      (* open file for outputting vampyre proofs *)
      let lfPfFile = Options.getValueOfString "pffile" in
      let _ =    (VampyreErrormsg.proofChannel := open_out lfPfFile;
                  ignore (VampyrePretty.fprintf (!VampyreErrormsg.proofChannel) "ANN_STARTLF\n");
                  ignore (VampyrePretty.fprintf (!VampyreErrormsg.proofChannel) "IMPORT blast.ans\n"))
      in
      let rec process_node (n (* : tree_node *) ,np (* : proof_tree_node*) ):proof_tree_node =
        let process_child n_1  = 
                 let op = get_op n_1 in (* n --op--> n_1 *)
      (* We make a corresponding np --op--> np_1 *)
          let (child_proof_region,lemma_token) = 
            Abstraction.post_proof (get_region n) op global_variable_table
          in
          let np_1_data = 
            {  pt_id  = (get_id n_1);
               pt_region = child_proof_region;
               covering_nodes = None; (* Jhala: TBD, adding the covering proof *)
            }
          in
            stats_nb_proof_tree_nodes := (!stats_nb_proof_tree_nodes) + 1;
            let np_1 = ((Tree.create_child np_1_data (op,lemma_token) np) : proof_tree_node)
            in
              if  (Abstraction.check_reg_eq child_proof_region (get_region n_1)) 
              then
                process_node (n_1,np_1)
              else  (Message.msg_string Message.Error "mismatched regions!";
                     process_node (n_1, np_1))
                
        in
        let children = get_children n in
          (* let us just count how many covered nodes there are *)
          if ((List.length children) = 0) then stats_nb_proof_tree_covered_nodes := !stats_nb_proof_tree_covered_nodes + 1;
          let _ = List.map process_child children in
            np
      in                
        (* first make the root of the proof tree *)
      let pt_root_data = 
        { pt_id  = (get_id root);
          pt_region = Abstraction.extract_proof_region (get_region root) ;
          covering_nodes = None; (* Jhala: TBD, adding the covering proof *)
        }
      in
      let pt_root = process_node (root, ((Tree.create_root pt_root_data) : proof_tree_node))        
      in
        (*let dump_node_to_chan chan node = Marshal.to_channel chan  (Tree.get_node_label node) [] 
          in *)
        
      let tree_chan = open_out_bin "foo.tree" in
      Marshal.to_channel tree_chan pt_root [];
      close_out tree_chan;
      Abstraction.print_proofTable ();
        (* print_proof_tree pt_root;*)
      ignore (VampyrePretty.fprintf !VampyreErrormsg.proofChannel "ANN_ENDLF\n");
      close_out (!VampyreErrormsg.proofChannel);
      let _ = Unix.system ("gzip -9 -f foo.tree") in
      let lfsz = (Unix.stat lfPfFile).Unix.st_size in 
      let treesz = (Unix.stat "foo.tree.gz").Unix.st_size in
      Message.msg_string Message.Normal ("Proof size: (tree)"^(string_of_int treesz));
      Message.msg_string Message.Normal ("         (Vampyre)"^(string_of_int lfsz));
      
      ()