let modelCheck o_err_loc =
  (* Get the abstraction of this C system description *)
  let module This_C_Abstraction = 
      Abstraction.Make_C_Abstraction(C_System_Descr) 
  in
  let module This_Cf_C_Abstraction = 
    CfAbstraction.Make_C_Abstraction(C_System_Descr) 
  in
  (* Create the lazy model checker for this abstraction *)
  let module This_LMC = LazyModelChecker.Make_Lazy_Model_Checker(This_C_Abstraction) in
  let module This_LMC_CF = CfLazyModelChecker.Make_Lazy_Model_Checker(This_Cf_C_Abstraction) in 
  let module Region = This_C_Abstraction.Region in
  This_C_Abstraction.check_races := Options.getValueOfBool "checkRace";

  This_C_Abstraction.assumed_invariants := Stats.time "read invariants" constructInvariants();  
  This_C_Abstraction.assumed_invariants_region := This_C_Abstraction.assumed_invariants_list_to_region();
  
(*
     ( let data = Region.Concrete { Region.pred = Predicate.conjoinL !assumed_invariants ; } in
       Region.Atomic { Region.location = C_SD.fake_location ;
                       Region.data = data ;
                       Region.stack = Region.EveryStack ; } );
*)
  (* Parsing in and adding the environment assumptions *)
  
  let _ = This_LMC.process_env_assumptions (constructEnvironmentAssumptions ()) in

  (* Add seed predicates, if any to system *)
  let seedPredsFile = Options.getValueOfString "pred" in
  let seedPreds = Predicate.conjoinL (Stats.time "read seeds" constructInitialPredicates seedPredsFile)
  in
  let initStateFile = Options.getValueOfString "init" in
  let initialState = Predicate.conjoinL (Stats.time "read initial state" constructInitialPredicates initStateFile) in
  let mainFunctions = Options.getValueOfStringList "main" in
    (* JHALA: Kill hacks *)
  let killLabel = Options.getValueOfString "killLoc" in
  let kill_location =
    match (C_System_Descr.get_locations_at_label killLabel) with
        [l] -> Some(l)
      | []  ->
          if (killLabel = "") then ()
          else
            Message.msg_string Message.Normal ("Kill label '" ^ killLabel ^
                                            "' was not found in the source file(s)") ;
          None
      | _   ->
          Message.msg_string Message.Error ("Kill label '" ^ killLabel ^
                                            "' appears multiple times in the source file(s)") ;
          exit 1
  in  
  let killPreds = constructKillPredicates () in
  let _ = This_C_Abstraction.initKill kill_location killPreds in
  let _ = This_C_Abstraction.initialize_abstraction () in
  (* JHALA: end kill hacks *)
  (* JHALA: custom abstraction hacks 
  let _ = if not (Options.getValueOfString " = ") then
    This_C_Abstraction.build_custom_abstraction (inputCustomAbs ()) in *)
  (* JHALA: end custom abstraction hacks *)

  let _ = Message.msg_string Message.Error "Done adding seed predicates" in
  if (Options.getValueOfInt "predH" > 0) then 
    This_C_Abstraction.make_const_table () ;

    Message.msg_string Message.Normal "\n\n\n********** Now running the model-checker **********\n\n" ;
    flush stdout;
    begin
            (* [Greg] This is really a first draft...t
               Put this in a printer function, with formatting boxes, etc. *)
      let indent_loc = "                                                " in
      let print_op indent_op op =
        let target_loc = C_System_Descr.get_target op
        and c_command = C_System_Descr.get_command op
        in
        Message.msg_string Message.Normal
          (indent_op ^ (C_Command.to_string c_command)) ;
        Message.msg_string Message.Normal
          (indent_loc ^ (C_System_Descr.location_to_string target_loc)) ;
        match c_command.C_Command.code with
          C_Command.FunctionCall _ ->
            indent_op ^ "   "
        | C_Command.Block l ->
            begin
              match (List.hd (List.rev l)) with
              | C_Command.Return _ ->
                  String.sub indent_op 0 ((String.length indent_op) - 3)
              | _ -> indent_op
            end
        | _ -> indent_op
      in
      let mc_return_val = 
        try
          if (Options.getValueOfBool "cf")
          then
            begin
              let init_region =
                let rec buildloclist lst loclist =
                  match lst with [] -> loclist
                  | a ::rest -> 
                      try
                        buildloclist rest ((C_System_Descr.lookup_entry_location a) :: loclist) 
                      with 
                        Not_found -> 
                          (Format.printf "Creating init_region: No function %s defined in program. Exiting\n" (a);
                           failwith ("No function "^(a)^" defined"))
        in
                let loclist = buildloclist mainFunctions [] in
                This_Cf_C_Abstraction.create_region 
                  loclist false seedPreds initialState
                  
              and error_region =
                match o_err_loc with
                | Some err_loc ->
                    if (Options.getValueOfBool "par") then
                      begin
            (* first get the number of threads *)
                        let num_of_threads = List.length (Options.getValueOfStringList "main") in
                        Some (This_Cf_C_Abstraction.create_error_region err_loc num_of_threads Predicate.True) 
                      end
                    else
                      Some (This_Cf_C_Abstraction.create_region [err_loc] true Predicate.True Predicate.True)
                | None -> None
                
              in let mc_return_val = This_LMC_CF.model_check init_region error_region
              in match (mc_return_val) with
                No_error ->
                  Message.msg_string Message.Normal "\n\nNo error found.  The system is safe :-)\n"
              | Error_reached (reg_i, op_list, reg_e) ->
                  Message.msg_string Message.Normal "\n\nError found! The system is unsafe :-(\n\n Error trace:\n" ;
                  Message.msg_printer Message.Normal This_Cf_C_Abstraction.Region.print reg_i ;
                  Message.msg_string Message.Normal "..\n\n" ;
          
                  Message.msg_string Message.Normal
                    (indent_loc ^ (C_System_Descr.location_to_string
                                     (C_System_Descr.get_source (List.hd op_list)))) ;
                  let _ = List.fold_left print_op "" op_list in
                  Message.msg_string Message.Normal "\n\n" ;
                  Message.msg_printer Message.Normal This_Cf_C_Abstraction.Region.print reg_e;
                  if (Options.getValueOfBool "xml") then This_Cf_C_Abstraction.dumpXml op_list
              | Race_condition ((reg1,oplist1, reg1'), (reg2, oplist2, reg2'), lv1, lv2) ->
                  Message.msg_string Message.Normal "\n\nRace condition found! The system is unsafe :-(\n\n\n";
                  Message.msg_string Message.Normal (Printf.sprintf "\n On the lvalues %s, %s \n" (Ast.Expression.lvalToString lv1) (Ast.Expression.lvalToString lv2));
                  (* print out the first trace *)
                  Message.msg_string Message.Normal "Printing out the first trace.\n" ;
                  Message.msg_printer Message.Normal This_Cf_C_Abstraction.Region.print reg1 ;
                  Message.msg_string Message.Normal "\n\n" ;
          
                  Message.msg_string Message.Normal
                    (indent_loc ^ (C_System_Descr.location_to_string
                                     (C_System_Descr.get_source (List.hd oplist1)))) ;
                  let _ = List.fold_left print_op "" oplist1 in
                  Message.msg_string Message.Normal "\n\n" ;
                  Message.msg_printer Message.Normal This_Cf_C_Abstraction.Region.print reg1';
                  if (Options.getValueOfBool "xml") then This_Cf_C_Abstraction.dumpXml oplist1 ;
                  (* print out the second trace *)
                  Message.msg_string Message.Normal "\n\nPrinting out the second trace.\n" ;
                  Message.msg_printer Message.Normal This_Cf_C_Abstraction.Region.print reg2 ;
                  Message.msg_string Message.Normal "\n\n" ;
          
                  Message.msg_string Message.Normal
                    (indent_loc ^ (C_System_Descr.location_to_string
                                     (C_System_Descr.get_source (List.hd oplist2)))) ;
                  let _ = List.fold_left print_op "" oplist2 in
                  Message.msg_string Message.Normal "\n\n" ;
                  Message.msg_printer Message.Normal This_Cf_C_Abstraction.Region.print reg2';
                  if (Options.getValueOfBool "xml") then This_Cf_C_Abstraction.dumpXml oplist2 
            end
          else
            begin
              let init_region =
                let rec buildloclist lst loclist =
                  match lst with [] -> loclist
                  | a ::rest -> 
                      try
                        buildloclist rest ((C_System_Descr.lookup_entry_location a) :: loclist) 
                      with 
                        Not_found -> 
                          (Format.printf "Creating init_region: No function %s defined in program. Exiting\n" (a);
                           failwith ("No function "^(a)^" defined"))
                in
                let loclist = buildloclist mainFunctions [] in
                This_C_Abstraction.create_region 
                  loclist false seedPreds initialState
                  
              and error_region =
                match o_err_loc with
                | Some err_loc ->
                    if (Options.getValueOfBool "par") then
                      begin
            (* first get the number of threads *)
                        let num_of_threads = List.length (Options.getValueOfStringList "main") in
                        Some (This_C_Abstraction.create_error_region err_loc num_of_threads Predicate.True) 
                      end
                    else
                      Some (This_C_Abstraction.create_region [err_loc] true Predicate.True Predicate.True)
                | None -> None

              in
              let mc_return_val =
                if (Options.getValueOfBool "checkRace") 
                then (This_LMC.model_check_tar init_region error_region) 
                else (This_LMC.model_check init_region error_region)
              in match (mc_return_val) with
                No_error ->
                  Message.msg_string Message.Normal "\n\nNo error found.  The system is safe :-)\n"
              | Error_reached (reg_i, op_list, reg_e) ->
                  Message.msg_string Message.Normal "\n\nError found! The system is unsafe :-(\n\n Error trace:\n" ;
                  (* this next line raises a seg fault for some reason...
                     Message.msg_printer Message.Normal This_C_Abstraction.Region.print reg_i ;
                     Message.msg_string Message.Normal " ;
                  *)
                  Message.msg_string Message.Normal
                    (indent_loc ^ (C_System_Descr.location_to_string
                                     (C_System_Descr.get_source (List.hd op_list)))) ;
                  let _ = List.fold_left print_op "" op_list in
                  Message.msg_string Message.Normal "\n\n" ;
                  Message.msg_printer Message.Normal This_C_Abstraction.Region.print reg_e;
                  if (Options.getValueOfBool "xml") then This_C_Abstraction.dumpXml op_list 
              | Race_condition ((reg1,oplist1, reg1'), (reg2, oplist2, reg2'), lv1, lv2) ->
                  Message.msg_string Message.Normal "\n\nRace condition found! The system is unsafe :-(\n\n\n";
                  Message.msg_string Message.Normal (Printf.sprintf "\n On the lvalues %s, %s \n" (Ast.Expression.lvalToString lv1) (Ast.Expression.lvalToString lv2));
                  (* print out the first trace *)
                  Message.msg_string Message.Normal "Printing out the first trace.\n" ;
                  Message.msg_printer Message.Normal This_C_Abstraction.Region.print reg1 ;
                  Message.msg_string Message.Normal "\n\n" ;
          
                  Message.msg_string Message.Normal
                    (indent_loc ^ (C_System_Descr.location_to_string
                                     (C_System_Descr.get_source (List.hd oplist1)))) ;
                  let _ = List.fold_left print_op "" oplist1 in
                  Message.msg_string Message.Normal "\n\n" ;
                  Message.msg_printer Message.Normal This_C_Abstraction.Region.print reg1';
                  if (Options.getValueOfBool "xml") then This_C_Abstraction.dumpXml oplist1 ;
                  (* print out the second trace *)
                  Message.msg_string Message.Normal "\n\nPrinting out the second trace.\n" ;
                  Message.msg_printer Message.Normal This_C_Abstraction.Region.print reg2 ;
                  Message.msg_string Message.Normal "\n\n" ;
          
                  Message.msg_string Message.Normal
                    (indent_loc ^ (C_System_Descr.location_to_string
                                     (C_System_Descr.get_source (List.hd oplist2)))) ;
                  let _ = List.fold_left print_op "" oplist2 in
                  Message.msg_string Message.Normal "\n\n" ;
                  Message.msg_printer Message.Normal This_C_Abstraction.Region.print reg2';
                  if (Options.getValueOfBool "xml") then This_C_Abstraction.dumpXml oplist2 
            end
        with e -> 
          begin 
            This_C_Abstraction.dump_abs (); 
            Message.msg_string Message.Error ("Exception raised :("^(Printexc.to_string e));
            raise e
          end
      in 
      ()
    end ;
  Message.msg_string Message.Normal "\n\nPhi Regions:\n" ;
  Message.msg_string Message.Normal (This_LMC.print_phis false) ;
  Message.msg_string Message.Normal "\n\nModel checker stats:\n" ;
  Message.msg_printer Message.Normal This_LMC.print_stats () ;
  Message.msg_string Message.Normal "\n\nAbstractor stats:\n" ;
  Message.msg_printer Message.Normal This_C_Abstraction.print_stats ()