diff --git a/infer/src/IR/Procdesc.re b/infer/src/IR/Procdesc.re
index cdc7fc78b..3c70b4e12 100644
--- a/infer/src/IR/Procdesc.re
+++ b/infer/src/IR/Procdesc.re
@@ -119,7 +119,9 @@ module Node = {
   /** Get the name of the procedure the node belongs to */
   let get_proc_name node =>
     switch node.pname_opt {
-    | None => failwithf "get_proc_name: at node %d" node.id
+    | None =>
+      L.out "get_proc_name: at node %d@\n" node.id;
+      assert false
     | Some pname => pname
     };
 
diff --git a/infer/src/IR/Typ.re b/infer/src/IR/Typ.re
index 5eea23f98..57a66b779 100644
--- a/infer/src/IR/Typ.re
+++ b/infer/src/IR/Typ.re
@@ -371,7 +371,10 @@ let name typ =>
 let unsome s =>
   fun
   | Some default_typ => default_typ
-  | None => failwithf "No default typ in %s@." s;
+  | None => {
+      L.out "No default typ in %s@." s;
+      assert false
+    };
 
 
 /** turn a *T into a T. fails if [typ] is not a pointer type */
diff --git a/infer/src/backend/abs.ml b/infer/src/backend/abs.ml
index a5bcaece1..d49174ff2 100644
--- a/infer/src/backend/abs.ml
+++ b/infer/src/backend/abs.ml
@@ -99,7 +99,7 @@ let mk_rule_ptspts_ls tenv impl_ok1 impl_ok2 (para: Sil.hpara) =
   let (para_fst_start, para_fst_rest) =
     let mark_impl_flag hpred = { Match.hpred = hpred; Match.flag = impl_ok1 } in
     match para_fst with
-    | [] -> failwithf "mk_rule_ptspts_ls (Empty Para): %a" (Sil.pp_hpara Pp.text) para
+    | [] -> L.out "@.@.ERROR (Empty Para): %a @.@." (Sil.pp_hpara Pp.text) para; assert false
     | hpred :: hpreds ->
         let hpat = mark_impl_flag hpred in
         let hpats = List.map ~f:mark_impl_flag hpreds in
@@ -128,7 +128,7 @@ let mk_rule_ptsls_ls tenv k2 impl_ok1 impl_ok2 para =
   let (ids_exist, para_inst) = Sil.hpara_instantiate para exp_base exp_next exps_shared in
   let (para_inst_start, para_inst_rest) =
     match para_inst with
-    | [] -> failwithf "mk_rule_ptsls_ls (Empty Para): %a" (Sil.pp_hpara Pp.text) para
+    | [] -> L.out "@.@.ERROR (Empty Para): %a @.@." (Sil.pp_hpara Pp.text) para; assert false
     | hpred :: hpreds ->
         let allow_impl hpred = { Match.hpred = hpred; Match.flag = impl_ok1 } in
         (allow_impl hpred, List.map ~f:allow_impl hpreds) in
@@ -252,7 +252,7 @@ let mk_rule_ptspts_dll tenv impl_ok1 impl_ok2 para =
   let (para_fst_start, para_fst_rest) =
     let mark_impl_flag hpred = { Match.hpred = hpred; Match.flag = impl_ok1 } in
     match para_fst with
-    | [] -> failwithf "mk_rule_ptspts_dll (Empty DLL para): %a" (Sil.pp_hpara_dll Pp.text) para
+    | [] -> L.out "@.@.ERROR (Empty DLL para): %a@.@." (Sil.pp_hpara_dll Pp.text) para; assert false
     | hpred :: hpreds ->
         let hpat = mark_impl_flag hpred in
         let hpats = List.map ~f:mark_impl_flag hpreds in
@@ -430,7 +430,8 @@ let typ_get_recursive_flds tenv typ_exp =
   | Exp.Var _ -> [] (* type of |-> not known yet *)
   | Exp.Const _ -> []
   | _ ->
-      failwithf "@.typ_get_recursive: unexpected type expr: %a@." Exp.pp typ_exp
+      L.out "@.typ_get_recursive: unexpected type expr: %a@." Exp.pp typ_exp;
+      assert false
 
 let discover_para_roots tenv p root1 next1 root2 next2 : Sil.hpara option =
   let eq_arg1 = Exp.equal root1 next1 in
@@ -601,7 +602,7 @@ let eqs_solve ids_in eqs_in =
       if not (List.exists ~f:(fun id' -> Ident.equal id id') ids_in) then None
       else
         let sub' = match Sil.extend_sub sub id e with
-          | None -> failwithf "ERROR : Buggy Implementation"
+          | None -> L.out "@.@.ERROR : Buggy Implementation.@.@."; assert false
           | Some sub' -> sub' in
         let eqs_rest' = eqs_sub sub' eqs_rest in
         solve sub' eqs_rest' in
diff --git a/infer/src/backend/dotty.ml b/infer/src/backend/dotty.ml
index d31d68cb6..01fd5c19d 100644
--- a/infer/src/backend/dotty.ml
+++ b/infer/src/backend/dotty.ml
@@ -113,8 +113,10 @@ let strip_special_chars b =
   let replace st c c' =
     if String.contains st c then begin
       let idx = String.index_exn st c in
-      String.set st idx c';
-      st
+      try
+        String.set st idx c';
+        st
+      with Invalid_argument _ -> L.out "@\n@\n Invalid argument!!! @\n @.@.@."; assert false
     end else st in
   let s0 = replace b '(' 'B' in
   let s1 = replace s0 '$' 'D' in
@@ -427,7 +429,7 @@ let rec compute_target_struct_fields dotnodes list_fld p f lambda cycle =
                end else
                  [(LinkStructToExp, Fieldname.to_string fn, n,"")]
            | _ -> (* by construction there must be at most 2 nodes for an expression*)
-               failwithf "Got more than 2 nodes, this should never happen!")
+               L.out "@\n Too many nodes! Error! @\n@.@."; assert false)
     | Sil.Estruct (_, _) -> [] (* inner struct are printed by print_struc function *)
     | Sil.Earray _ -> [] (* inner arrays are printed by print_array function *) in
   match list_fld with
@@ -460,7 +462,7 @@ let rec compute_target_array_elements dotnodes list_elements p f lambda =
                end else
                  [(LinkArrayToExp, Exp.to_string idx, n,"")]
            | _ -> (* by construction there must be at most 2 nodes for an expression*)
-               failwithf "Got more than 2 nodes, this should never happen!"
+               L.out "@\n Too many nodes! Error! @\n@.@."; assert false
           )
     | Sil.Estruct (_, _) -> [] (* inner struct are printed by print_struc function *)
     | Sil.Earray _ ->[] (* inner arrays are printed by print_array function *)
diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml
index 1e27f6c73..b5f13940e 100644
--- a/infer/src/backend/interproc.ml
+++ b/infer/src/backend/interproc.ml
@@ -117,7 +117,8 @@ module Worklist = struct
         Procdesc.NodeMap.add min.node (min.visits + 1) wl.visit_map; (* increase the visits *)
       min.node
     with Not_found -> begin
-        failwithf "Work list is empty! Impossible to remove edge."
+        L.out "@\n...Work list is empty! Impossible to remove edge...@\n";
+        assert false
       end
 end
 (* =============== END of module Worklist =============== *)
@@ -161,7 +162,8 @@ let path_set_checkout_todo (wl : Worklist.t) (node: Procdesc.Node.t) : Paths.Pat
     Hashtbl.replace wl.Worklist.path_set_visited node_id new_visited;
     todo
   with Not_found ->
-    failwithf "could not find todo for node %a" Procdesc.Node.pp node
+    L.out "@.@.ERROR: could not find todo for node %a@.@." Procdesc.Node.pp node;
+    assert false
 
 (* =============== END of the edge_set object =============== *)
 
diff --git a/infer/src/backend/match.ml b/infer/src/backend/match.ml
index cf1d3cc90..865fe4f68 100644
--- a/infer/src/backend/match.ml
+++ b/infer/src/backend/match.ml
@@ -143,11 +143,10 @@ and isel_match isel1 sub vars isel2 =
       let sanity_check = not (List.exists ~f:(fun id -> Sil.ident_in_exp id idx2) vars) in
       if (not sanity_check) then begin
         let pe = Pp.text in
-        failwithf "@[.... Sanity Check Failure while Matching Index-Strexps ....@\n\
-                   @[<4>    IDX1: %a, STREXP1: %a@\n\
-                   @[<4>    IDX2: %a, STREXP2: %a@\n@."
-          (Sil.pp_exp_printenv pe) idx1 (Sil.pp_sexp pe) se1'
-          (Sil.pp_exp_printenv pe) idx2 (Sil.pp_sexp pe) se2'
+        L.out "@[.... Sanity Check Failure while Matching Index-Strexps ....@.";
+        L.out "@[<4>    IDX1: %a, STREXP1: %a@." (Sil.pp_exp_printenv pe) idx1 (Sil.pp_sexp pe) se1';
+        L.out "@[<4>    IDX2: %a, STREXP2: %a@\n@." (Sil.pp_exp_printenv pe) idx2 (Sil.pp_sexp pe) se2';
+        assert false
       end
       else if Exp.equal idx1 idx2 then begin
         match strexp_match se1' sub vars se2' with
diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml
index 098b1220c..28395f4a0 100644
--- a/infer/src/backend/prop.ml
+++ b/infer/src/backend/prop.ml
@@ -1356,7 +1356,8 @@ module Normalize = struct
       | Var _ ->
           Estruct ([], inst)
       | te ->
-          failwithf "trying to create ptsto with type: %a@\n@." (Sil.pp_texp_full Pp.text) te in
+          L.out "trying to create ptsto with type: %a@\n@." (Sil.pp_texp_full Pp.text) te;
+          assert false in
     let strexp : Sil.strexp = match expo with
       | Some e -> Eexp (e, inst)
       | None -> default_strexp () in
@@ -2360,12 +2361,11 @@ let prop_iter_make_id_primed tenv id iter =
         begin
           match eq with
           | Aeq (Var id1, e1) when Sil.ident_in_exp id1 e1 ->
-              failwithf "@[<2>#### ERROR: an assumption of the analyzer broken ####@\n\
-                         Broken Assumption: id notin e for all (id,e) in sub@\n\
-                         (id,e) : (%a,%a)@\n\
-                         PROP : %a@\n@."
-                (Ident.pp Pp.text) id1 Exp.pp e1
-                (pp_prop Pp.text) (prop_iter_to_prop tenv iter)
+              L.out "@[<2>#### ERROR: an assumption of the analyzer broken ####@\n";
+              L.out "Broken Assumption: id notin e for all (id,e) in sub@\n";
+              L.out "(id,e) : (%a,%a)@\n" (Ident.pp Pp.text) id1 Exp.pp e1;
+              L.out "PROP : %a@\n@." (pp_prop Pp.text) (prop_iter_to_prop tenv iter);
+              assert false
           | Aeq (Var id1, e1) when Ident.equal pid id1 ->
               split pairs_unpid ((id1, e1):: pairs_pid) eqs_cur
           | Aeq (Var id1, e1) ->
diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml
index 985682569..94495c39c 100644
--- a/infer/src/backend/symExec.ml
+++ b/infer/src/backend/symExec.ml
@@ -1235,7 +1235,8 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
         | [], _ ->
             ret_old_path [prop_]
         | _ ->
-            failwithf "Pvar %a appears on the LHS of >1 heap predicate!@." (Pvar.pp Pp.text) pvar
+            L.out "Pvar %a appears on the LHS of >1 heap predicate!@." (Pvar.pp Pp.text) pvar;
+            assert false
       end
   | Sil.Abstract _ ->
       let node = State.get_node () in
diff --git a/infer/src/base/DB.ml b/infer/src/base/DB.ml
index b4fdfdb78..523ccf56e 100644
--- a/infer/src/base/DB.ml
+++ b/infer/src/base/DB.ml
@@ -164,7 +164,8 @@ let update_file_with_lock dir fname update =
     Unix.lockf fd ~mode:Unix.F_ULOCK ~len:0L;
     Unix.close fd
   ) else (
-    failwithf "save_with_lock: fail on path: %s@." path
+    L.out "@.save_with_lock: fail on path: %s@." path;
+    assert false
   )
 
 (** Read a file using a lock to allow write attempts in parallel. *)
diff --git a/infer/src/base/Logging.ml b/infer/src/base/Logging.ml
index b453d688f..b73a70e47 100644
--- a/infer/src/base/Logging.ml
+++ b/infer/src/base/Logging.ml
@@ -227,7 +227,7 @@ let assert_false ((file, lnum, cnum, _) as ml_loc) =
   raise (Assert_failure (file, lnum, cnum))
 
 (** print a warning with information of the position in the ml source where it oririnated.
-    use as: warning_position "description" (try assert false with Assert_failure x -> x); *)
+    use as: warning_position "description" __POS__; *)
 let warning_position (s: string) (ml_loc: ml_loc) =
   out "WARNING: %s in %a@." s pp_ml_loc_opt (Some ml_loc)
 
diff --git a/infer/src/base/Logging.mli b/infer/src/base/Logging.mli
index 0956fe5d8..55de4d907 100644
--- a/infer/src/base/Logging.mli
+++ b/infer/src/base/Logging.mli
@@ -108,7 +108,7 @@ val pp_ml_loc_opt : Format.formatter -> ml_loc option -> unit
 val assert_false : ml_loc -> 'a
 
 (** print a warning with information of the position in the ml source where it oririnated.
-    use as: warning_position "description" (try assert false with Assert_failure x -> x); *)
+    use as: warning_position "description" __POS__; *)
 val warning_position: string -> ml_loc -> unit
 
 (** dump a string *)
diff --git a/infer/src/clang/Capture.re b/infer/src/clang/Capture.re
index ce2e799ed..52c7651ef 100644
--- a/infer/src/clang/Capture.re
+++ b/infer/src/clang/Capture.re
@@ -22,7 +22,8 @@ let catch_biniou_buffer_errors f x =>
     /* suppress warning: allow this one case because we're just reraising the error with another
        error message so it doesn't really matter if this eventually fails */
     | Invalid_argument "Bi_inbuf.refill_from_channel" =>
-      failwith "WARNING: biniou buffer too short, skipping the file"
+      Logging.out "WARNING: biniou buffer too short, skipping the file@\n";
+      assert false
     }
   )
   [@warning "-52"];
diff --git a/infer/src/clang/cFrontend_errors.ml b/infer/src/clang/cFrontend_errors.ml
index b3ed5f039..8547a2c96 100644
--- a/infer/src/clang/cFrontend_errors.ml
+++ b/infer/src/clang/cFrontend_errors.ml
@@ -82,7 +82,8 @@ let evaluate_place_holder ph an =
   | "%iphoneos_target_sdk_version%" ->
       MF.monospaced_to_string (CFrontend_checkers.iphoneos_target_sdk_version an)
   | "%available_ios_sdk%" -> MF.monospaced_to_string (CFrontend_checkers.available_ios_sdk an)
-  | _ -> failwithf "Helper function %s is unknown" ph
+  | _ -> (Logging.out "ERROR: helper function %s is unknown. Stop.\n" ph;
+          assert false)
 
 (* given a message this function searches for a place-holder identifier,
    eg %id%. Then it evaluates id and replaces %id% in message
@@ -113,13 +114,16 @@ let string_to_err_kind = function
   | "ERROR" -> Exceptions.Kerror
   | "INFO" -> Exceptions.Kinfo
   | "ADVICE" -> Exceptions.Kadvice
-  | s -> failwithf "Severity %s does not exist" s
+  | s -> (Logging.out "\n[ERROR] Severity %s does not exist. Stop.\n" s;
+          assert false)
 
 let string_to_issue_mode m =
   match m with
   | "ON" -> CIssue.On
   | "OFF" -> CIssue.Off
-  | s -> failwithf "Mode %s does not exist. Please specify ON/OFF" s
+  | s ->
+      (Logging.out "\n[ERROR] Mode %s does not exist. Please specify ON/OFF\n" s;
+       assert false)
 
 (** Convert a parsed checker in list of linters *)
 let create_parsed_linters linters_def_file checkers : linter list =
diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml
index aec4d4624..71cfef936 100644
--- a/infer/src/clang/cTrans.ml
+++ b/infer/src/clang/cTrans.ml
@@ -880,7 +880,8 @@ struct
           if Int.equal (List.length params) (List.length params_stmt) then
             params
           else
-            failwith "ERROR: stmt_list and res_trans_par.exps must have same size" in
+            (Logging.out "ERROR: stmt_list and res_trans_par.exps must have same size\n";
+             assert false) in
         let act_params = if is_cf_retain_release then
             (Exp.Const (Const.Cint IntLit.one), Typ.mk (Tint Typ.IBool)) :: act_params
           else act_params in
diff --git a/infer/src/clang/cTrans_utils.ml b/infer/src/clang/cTrans_utils.ml
index 637b5dd0e..9ae3abb05 100644
--- a/infer/src/clang/cTrans_utils.ml
+++ b/infer/src/clang/cTrans_utils.ml
@@ -572,7 +572,8 @@ let rec get_type_from_exp_stmt stmt =
       get_type_from_exp_stmt (extract_stmt_from_singleton stmt_list "WARNING: We expect only one stmt.")
   | DeclRefExpr(_, _, _, info) -> do_decl_ref_exp info
   | _ ->
-      failwithf "Cannot get type fo stmt %s" (Clang_ast_j.string_of_stmt stmt)
+      Logging.out "Failing with: %s@\n%!" (Clang_ast_j.string_of_stmt stmt);
+      assert false
 
 module Self =
 struct
diff --git a/infer/src/harness/inhabit.ml b/infer/src/harness/inhabit.ml
index fe007eeb7..8c803fbcd 100644
--- a/infer/src/harness/inhabit.ml
+++ b/infer/src/harness/inhabit.ml
@@ -142,7 +142,8 @@ let rec inhabit_typ tenv typ cfg env =
       | Typ.Tint (_) -> (Exp.Const (Const.Cint (IntLit.zero)), env)
       | Typ.Tfloat (_) -> (Exp.Const (Const.Cfloat 0.0), env)
       | _ ->
-          failwithf "Couldn't inhabit typ: %a" (Typ.pp Pp.text) typ in
+          L.out "Couldn't inhabit typ: %a@." (Typ.pp Pp.text) typ;
+          assert false in
     let (inhabited_exp, env') =
       inhabit_internal typ { env with cur_inhabiting = TypSet.add typ env.cur_inhabiting } in
     (inhabited_exp, { env' with cache = TypMap.add typ inhabited_exp env.cache;