diff --git a/infer/src/IR/cg.ml b/infer/src/IR/cg.ml
index de8349086..3f1e959ff 100644
--- a/infer/src/IR/cg.ml
+++ b/infer/src/IR/cg.ml
@@ -328,7 +328,7 @@ let store_to_file (filename : DB.filename) (call_graph : t) =
 
 let pp_graph_dotty get_specs (g: t) fmt =
   let nodes_with_calls = get_all_nodes g in
-  let num_specs n = try IList.length (get_specs n) with exn when exn_not_failure exn -> - 1 in
+  let num_specs n = try IList.length (get_specs n) with exn when SymOp.exn_not_failure exn -> - 1 in
   let get_color (n, _) =
     if num_specs n != 0 then "green" else "red" in
   let get_shape (n, _) =
diff --git a/infer/src/backend/SymOp.ml b/infer/src/backend/SymOp.ml
new file mode 100644
index 000000000..ec60c0669
--- /dev/null
+++ b/infer/src/backend/SymOp.ml
@@ -0,0 +1,154 @@
+(*
+ * Copyright (c) 2009 - 2013 Monoidics ltd.
+ * Copyright (c) 2013 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ *)
+
+(** Symbolic Operations and Failures: the units in which analysis work is measured *)
+
+open! Utils
+
+module F = Format
+
+
+type failure_kind =
+  | FKtimeout (* max time exceeded *)
+  | FKsymops_timeout of int (* max symop's exceeded *)
+  | FKrecursion_timeout of int (* max recursion level exceeded *)
+  | FKcrash of string (* uncaught exception or failed assertion *)
+
+(** failure that prevented analysis from finishing *)
+exception Analysis_failure_exe of failure_kind
+
+let exn_not_failure = function
+  | Analysis_failure_exe _ -> false
+  | _ -> true
+
+let pp_failure_kind fmt = function
+  | FKtimeout -> F.fprintf fmt "TIMEOUT"
+  | FKsymops_timeout symops -> F.fprintf fmt "SYMOPS TIMEOUT (%d)" symops
+  | FKrecursion_timeout level -> F.fprintf fmt "RECURSION TIMEOUT(%d)" level
+  | FKcrash msg -> F.fprintf fmt "CRASH (%s)" msg
+
+
+(** Count the number of symbolic operations *)
+
+(** Timeout in seconds for each function *)
+let timeout_seconds = ref (!Config.seconds_per_iteration *. (float_of_int !Config.iterations))
+
+(** Timeout in SymOps *)
+let timeout_symops = ref (!Config.symops_per_iteration * !Config.iterations)
+
+let get_timeout_seconds () = !timeout_seconds
+
+(** Internal state of the module *)
+type t =
+  {
+    (** Only throw timeout exception when alarm is active *)
+    mutable alarm_active : bool;
+
+    (** last wallclock set by an alarm, if any *)
+    mutable last_wallclock : float option;
+
+    (** Number of symop's *)
+    mutable symop_count : int;
+
+    (** Counter for the total number of symop's.
+        The new state created when save_state is called shares this counter
+        if keep_symop_total is true. Otherwise, a new counter is created. *)
+    symop_total : int ref;
+  }
+
+let initial () : t =
+  {
+    alarm_active = false;
+    last_wallclock = None;
+    symop_count = 0;
+    symop_total = ref 0;
+  }
+
+(** Global State *)
+let gs : t ref = ref (initial ())
+
+(** Restore the old state. *)
+let restore_state state =
+  gs := state
+
+(** Return the old state, and revert the current state to the initial one.
+    If keep_symop_total is true, share the total counter. *)
+let save_state ~keep_symop_total =
+  let old_state = !gs in
+  let new_state =
+    let st = initial () in
+    if keep_symop_total
+    then
+      { st with symop_total = old_state.symop_total }
+    else
+      st in
+  gs := new_state;
+  old_state
+
+(** handler for the wallclock timeout *)
+let wallclock_timeout_handler = ref None
+
+(** set the handler for the wallclock timeout *)
+let set_wallclock_timeout_handler handler =
+  wallclock_timeout_handler := Some handler
+
+(** Set the wallclock alarm checked at every pay() *)
+let set_wallclock_alarm nsecs =
+  !gs.last_wallclock <- Some (Unix.gettimeofday () +. nsecs)
+
+(** Unset the wallclock alarm checked at every pay() *)
+let unset_wallclock_alarm () =
+  !gs.last_wallclock <- None
+
+(** if the wallclock alarm has expired, raise a timeout exception *)
+let check_wallclock_alarm () =
+  match !gs.last_wallclock, !wallclock_timeout_handler with
+  | Some alarm_time, Some handler when Unix.gettimeofday () >= alarm_time ->
+      unset_wallclock_alarm ();
+      handler ()
+  | _ -> ()
+
+(** Return the time remaining before the wallclock alarm expires *)
+let get_remaining_wallclock_time () =
+  match !gs.last_wallclock with
+  | Some alarm_time ->
+      max 0.0 (alarm_time -. Unix.gettimeofday ())
+  | None ->
+      0.0
+
+(** Return the total number of symop's since the beginning *)
+let get_total () =
+  !(!gs.symop_total)
+
+(** Reset the total number of symop's *)
+let reset_total () =
+  !gs.symop_total := 0
+
+(** Count one symop *)
+let pay () =
+  !gs.symop_count <- !gs.symop_count + 1;
+  !gs.symop_total := !(!gs.symop_total) + 1;
+  if !gs.symop_count > !timeout_symops &&
+     !gs.alarm_active
+  then raise (Analysis_failure_exe (FKsymops_timeout !gs.symop_count));
+  check_wallclock_alarm ()
+
+(** Reset the counter *)
+let reset_count () =
+  !gs.symop_count <- 0
+
+(** Reset the counter and activate the alarm *)
+let set_alarm () =
+  reset_count ();
+  !gs.alarm_active <- true
+
+(** De-activate the alarm *)
+let unset_alarm () =
+  !gs.alarm_active <- false
diff --git a/infer/src/backend/SymOp.mli b/infer/src/backend/SymOp.mli
new file mode 100644
index 000000000..5d70fa187
--- /dev/null
+++ b/infer/src/backend/SymOp.mli
@@ -0,0 +1,71 @@
+(*
+ * Copyright (c) 2009 - 2013 Monoidics ltd.
+ * Copyright (c) 2013 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ *)
+
+(** Symbolic Operations and Failures: the units in which analysis work is measured *)
+
+open! Utils
+
+(** Internal state of the module *)
+type t
+
+(** if the wallclock alarm has expired, raise a timeout exception *)
+val check_wallclock_alarm : unit -> unit
+
+(** Return the time remaining before the wallclock alarm expires *)
+val get_remaining_wallclock_time : unit -> float
+
+(** Timeout in seconds for each function *)
+val get_timeout_seconds : unit -> float
+
+(** Return the total number of symop's since the beginning *)
+val get_total : unit -> int
+
+(** Count one symop *)
+val pay : unit -> unit
+
+(** Reset the total number of symop's *)
+val reset_total : unit -> unit
+
+(** Restore the old state. *)
+val restore_state : t -> unit
+
+(** Return the old state, and revert the current state to the initial one.
+    If keep_symop_total is true, share the total counter. *)
+val save_state : keep_symop_total:bool -> t
+
+(** Reset the counter and activate the alarm *)
+val set_alarm : unit -> unit
+
+(** Set the wallclock alarm checked at every pay() *)
+val set_wallclock_alarm : float -> unit
+
+(** set the handler for the wallclock timeout *)
+val set_wallclock_timeout_handler : (unit -> unit) -> unit
+
+(** De-activate the alarm *)
+val unset_alarm : unit -> unit
+
+(** Unset the wallclock alarm checked at every pay() *)
+val unset_wallclock_alarm : unit -> unit
+
+
+type failure_kind =
+  | FKtimeout (* max time exceeded *)
+  | FKsymops_timeout of int (* max symop's exceeded *)
+  | FKrecursion_timeout of int (* max recursion level exceeded *)
+  | FKcrash of string (* uncaught exception or failed assertion *)
+
+(** Timeout exception *)
+exception Analysis_failure_exe of failure_kind
+
+(** check that the exception is not a timeout exception *)
+val exn_not_failure : exn -> bool
+
+val pp_failure_kind : Format.formatter -> failure_kind -> unit
diff --git a/infer/src/backend/config.ml b/infer/src/backend/config.ml
index e2b742669..165d1f144 100644
--- a/infer/src/backend/config.ml
+++ b/infer/src/backend/config.ml
@@ -362,6 +362,29 @@ let default_failure_name = "ASSERTION_FAILURE"
 
 let analyze_models = from_env_variable "INFER_ANALYZE_MODELS"
 
+(** initial time of the analysis, i.e. when this module is loaded, gotten from Unix.time *)
+let initial_analysis_time = Unix.time ()
+
+let symops_timeout, seconds_timeout =
+  let default_symops_timeout = 333 in
+  let default_seconds_timeout = 10.0 in
+  let long_symops_timeout = 1000 in
+  let long_seconds_timeout = 30.0 in
+  if analyze_models then
+    (* use longer timeouts when analyzing models *)
+    long_symops_timeout, long_seconds_timeout
+  else
+    default_symops_timeout, default_seconds_timeout
+
+(** number of symops to multiply by the number of iterations, after which there is a timeout *)
+let symops_per_iteration = ref symops_timeout
+
+(** number of seconds to multiply by the number of iterations, after which there is a timeout *)
+let seconds_per_iteration = ref seconds_timeout
+
+(** Set the timeout values in seconds and symops, computed as a multiple of the integer parameter *)
+let iterations = ref 1
+
 (** experimental: dynamic dispatch for interface calls only in Java. off by default because of the
     cost *)
 let sound_dynamic_dispatch = from_env_variable "INFER_SOUND_DYNAMIC_DISPATCH"
diff --git a/infer/src/backend/dotty.ml b/infer/src/backend/dotty.ml
index 9c8f50382..337fd8a32 100644
--- a/infer/src/backend/dotty.ml
+++ b/infer/src/backend/dotty.ml
@@ -513,7 +513,7 @@ let rec dotty_mk_set_links dotnodes sigma p f cycle =
            let nodes_e = select_nodes_exp_lambda dotnodes e lambda in
            let address_struct_id =
              try get_coordinate_id (IList.hd (IList.filter (is_source_node_of_exp e) nodes_e))
-             with exn when exn_not_failure exn -> assert false in
+             with exn when SymOp.exn_not_failure exn -> assert false in
            (* we need to exclude the address node from the sorce of fields. no fields should start from there*)
            let nl'= IList.filter (fun id -> address_struct_id != id) nl in
            let links_from_fields = IList.flatten (IList.map ff nl') in
@@ -877,7 +877,7 @@ let pp_dotty_prop_list_in_path f plist prev_n curr_n =
                  pp_dotty f (Generic_proposition) po None) plist;
     if prev_n <> - 1 then F.fprintf f "\n state%iN ->state%iN\n" prev_n curr_n;
     F.fprintf f "\n } \n"
-  with exn when exn_not_failure exn ->
+  with exn when SymOp.exn_not_failure exn ->
     ()
 
 let pp_dotty_prop fmt (prop, cycle) =
@@ -890,7 +890,7 @@ let pp_dotty_prop fmt (prop, cycle) =
 let dotty_prop_to_str prop cycle =
   try
     Some (pp_to_string pp_dotty_prop (prop, cycle))
-  with exn when exn_not_failure exn -> None
+  with exn when SymOp.exn_not_failure exn -> None
 
 (* create a dotty file with a single proposition *)
 let dotty_prop_to_dotty_file fname prop cycle =
@@ -899,7 +899,7 @@ let dotty_prop_to_dotty_file fname prop cycle =
     let fmt_dot = Format.formatter_of_out_channel out_dot in
     pp_dotty_prop fmt_dot (prop, cycle);
     close_out out_dot
-  with exn when exn_not_failure exn ->
+  with exn when SymOp.exn_not_failure exn ->
     ()
 
 (* this is used only to print a list of prop parsed with the external parser. Basically deprecated.*)
@@ -916,7 +916,7 @@ let pp_proplist_parsed2dotty_file filename plist =
     let fmt = F.formatter_of_out_channel outc in
     F.fprintf fmt "#### Dotty version:  ####@.%a@.@." pp_list plist;
     close_out outc
-  with exn when exn_not_failure exn ->
+  with exn when SymOp.exn_not_failure exn ->
     ()
 
 (********** START of Print interprocedural cfgs in dotty format  *)
@@ -1058,7 +1058,7 @@ let pp_speclist_to_file (filename : DB.filename) spec_list =
 
 let pp_speclist_dotty_file (filename : DB.filename) spec_list =
   try pp_speclist_to_file filename spec_list
-  with exn when exn_not_failure exn ->
+  with exn when SymOp.exn_not_failure exn ->
     ()
 
 (**********************************************************************)
diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml
index 5a6d7daa2..8f6ab03ed 100644
--- a/infer/src/backend/errdesc.ml
+++ b/infer/src/backend/errdesc.ml
@@ -511,7 +511,7 @@ let explain_leak tenv hpred prop alloc_att_opt bucket =
         (try
            let t2 = Tenv.expand_type tenv _t2 in
            Sil.typ_equal t1 t2
-         with exn when exn_not_failure exn -> false)
+         with exn when SymOp.exn_not_failure exn -> false)
     | Some (Sil.Sizeof (Sil.Tint _, _)), Some (Sil.Sizeof (Sil.Tint _, _))
       when is_file -> (* must be a file opened with "open" *)
         true
@@ -948,7 +948,7 @@ let explain_nth_function_parameter use_buckets deref_str prop n pvar_off =
                Some (dexp_apply_pvar_off de pvar_off)
            | None -> None in
          create_dereference_desc ~use_buckets dexp_opt' deref_str prop loc
-       with exn when exn_not_failure exn -> Localise.no_desc)
+       with exn when SymOp.exn_not_failure exn -> Localise.no_desc)
   | _ -> Localise.no_desc
 
 (** Find a program variable whose value is [exp] or pointing to a struct containing [exp] *)
diff --git a/infer/src/backend/exceptions.ml b/infer/src/backend/exceptions.ml
index c0f49ec1b..93fcda3c1 100644
--- a/infer/src/backend/exceptions.ml
+++ b/infer/src/backend/exceptions.ml
@@ -252,7 +252,7 @@ let recognize_exception exn =
     | Return_value_ignored (desc, ml_loc) ->
         (Localise.return_value_ignored,
          desc, Some ml_loc, Exn_user, Medium, None, Nocat)
-    | Analysis_failure_exe _ ->
+    | SymOp.Analysis_failure_exe _ ->
         (Localise.from_string "Failure_exe",
          Localise.no_desc, None, Exn_system, Low, None, Nocat)
     | Skip_function desc ->
diff --git a/infer/src/backend/inferanalyze.ml b/infer/src/backend/inferanalyze.ml
index c8efb3cc1..419f2c2ec 100644
--- a/infer/src/backend/inferanalyze.ml
+++ b/infer/src/backend/inferanalyze.ml
@@ -60,7 +60,7 @@ let arg_desc =
         "use file for the err channel"
         ;
         "-iterations",
-        Arg.Int set_iterations,
+        Arg.Set_int Config.iterations,
         Some "n",
         "set the max number of operations for each function, \
          expressed as a multiple of symbolic operations (default n=1)"
@@ -194,7 +194,7 @@ let arg_desc =
         "Add buckets to issue descriptions, useful when developing infer"
         ;
         "-seconds_per_iteration",
-        Arg.Set_float seconds_per_iteration,
+        Arg.Set_float Config.seconds_per_iteration,
         Some "n",
         "set the number of seconds per iteration (default n=30)"
         ;
@@ -204,10 +204,10 @@ let arg_desc =
         "use the multirange subtyping domain"
         ;
         "-symops_per_iteration",
-        Arg.Set_int symops_per_iteration,
+        Arg.Set_int Config.symops_per_iteration,
         Some "n",
         "set the number of symbolic operations per iteration (default n="
-        ^ (string_of_int !symops_per_iteration) ^ ")"
+        ^ (string_of_int !Config.symops_per_iteration) ^ ")"
         ;
         "-tracing",
         Arg.Unit (fun () -> Config.report_runtime_exceptions := true),
diff --git a/infer/src/backend/inferprint.ml b/infer/src/backend/inferprint.ml
index 045c39c9d..990d50b99 100644
--- a/infer/src/backend/inferprint.ml
+++ b/infer/src/backend/inferprint.ml
@@ -388,7 +388,7 @@ let summary_values top_proc_set summary =
     logscale (c1 * in_calls + c2 * out_calls) in
 
   let pp_failure failure =
-    pp_to_string pp_failure_kind failure in
+    pp_to_string SymOp.pp_failure_kind failure in
 
 
   { vname = Procname.to_string proc_name;
diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml
index 35a12db2f..2ac94a460 100644
--- a/infer/src/backend/interproc.ml
+++ b/infer/src/backend/interproc.ml
@@ -947,7 +947,7 @@ let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t)
     if recursion_level > !Config.max_recursion then
       begin
         L.err "Reached maximum level of recursion, raising a Timeout@.";
-        raise (Analysis_failure_exe (FKrecursion_timeout recursion_level))
+        raise (SymOp.Analysis_failure_exe (FKrecursion_timeout recursion_level))
       end in
 
   let compute_footprint : (unit -> unit) * (unit -> Prop.normal Specs.spec list * Specs.phase) =
@@ -1330,7 +1330,7 @@ let perform_transition exe_env tenv proc_name =
               let start_node = Cfg.Procdesc.get_start_node pdesc in
               f start_node
           | None -> ()
-        with exn when exn_not_failure exn -> () in
+        with exn when SymOp.exn_not_failure exn -> () in
       apply_start_node (do_before_node 0);
       try
         Config.allowleak := true;
@@ -1338,7 +1338,7 @@ let perform_transition exe_env tenv proc_name =
         Config.allowleak := allowleak;
         apply_start_node do_after_node;
         res
-      with exn when exn_not_failure exn ->
+      with exn when SymOp.exn_not_failure exn ->
         apply_start_node do_after_node;
         Config.allowleak := allowleak;
         L.err "Error in collect_preconditions for %a@." Procname.pp proc_name;
diff --git a/infer/src/backend/io_infer.ml b/infer/src/backend/io_infer.ml
index f9f3d9b08..3bc1494c1 100644
--- a/infer/src/backend/io_infer.ml
+++ b/infer/src/backend/io_infer.ml
@@ -150,7 +150,7 @@ struct
   let modified_during_analysis path =
     let fname = get_full_fname path in
     if DB.file_exists fname then
-      DB.file_modified_time fname >= initial_analysis_time
+      DB.file_modified_time fname >= Config.initial_analysis_time
     else false
 
   (** Close an Html file *)
diff --git a/infer/src/backend/logging.ml b/infer/src/backend/logging.ml
index eef93cb0f..e1b5ef6de 100644
--- a/infer/src/backend/logging.ml
+++ b/infer/src/backend/logging.ml
@@ -210,12 +210,12 @@ let log_progress_timeout_event failure_kind =
   if !Config.developer_mode then
     begin
       match failure_kind with
-      | FKtimeout ->
+      | SymOp.FKtimeout ->
           log_progress_simple "T"
-      | FKsymops_timeout _ ->
+      | SymOp.FKsymops_timeout _ ->
           log_progress_simple "S"
-      | FKrecursion_timeout _ ->
+      | SymOp.FKrecursion_timeout _ ->
           log_progress_simple "R"
-      | FKcrash _ ->
+      | SymOp.FKcrash _ ->
           log_progress_simple "C"
     end
diff --git a/infer/src/backend/logging.mli b/infer/src/backend/logging.mli
index 3eaf93cce..684d41d55 100644
--- a/infer/src/backend/logging.mli
+++ b/infer/src/backend/logging.mli
@@ -151,4 +151,4 @@ val log_progress_file : unit -> unit
 val log_progress_procedure : unit -> unit
 
 (** Progress bar: log a timeout event if in developer mode. *)
-val log_progress_timeout_event : failure_kind -> unit
+val log_progress_timeout_event : SymOp.failure_kind -> unit
diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml
index bc0b4ce7b..293b429e0 100644
--- a/infer/src/backend/ondemand.ml
+++ b/infer/src/backend/ondemand.ml
@@ -191,7 +191,7 @@ let run_proc_analysis ~propagate_exceptions analyze_proc curr_pdesc callee_pdesc
       raise exn
     else
       match exn with
-      | Analysis_failure_exe kind ->
+      | SymOp.Analysis_failure_exe kind ->
           (* in production mode, log the timeout/crash and continue with the summary we had before
              the failure occurred *)
           log_error_and_continue exn kind
diff --git a/infer/src/backend/paths.ml b/infer/src/backend/paths.ml
index b1aa40d3e..f1bae8ffd 100644
--- a/infer/src/backend/paths.ml
+++ b/infer/src/backend/paths.ml
@@ -318,7 +318,7 @@ end = struct
         | Some node ->
             pos_opt <> None && filter node
         | None -> false
-      with exn when exn_not_failure exn -> false in
+      with exn when SymOp.exn_not_failure exn -> false in
     let position_seen = ref false in
     let inverse_sequence =
       let log = ref [] in
diff --git a/infer/src/backend/printer.ml b/infer/src/backend/printer.ml
index 0e2268371..0cc5344fb 100644
--- a/infer/src/backend/printer.ml
+++ b/infer/src/backend/printer.ml
@@ -51,7 +51,7 @@ struct
       let lines_arr = read_file (DB.source_file_to_string fname) in
       Hashtbl.add hash fname lines_arr;
       Some lines_arr
-    with exn when exn_not_failure exn -> None
+    with exn when SymOp.exn_not_failure exn -> None
 
   let from_file_linenum_original hash fname linenum =
     match file_data hash fname with
diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml
index 3f9f9fbc4..372a4a59a 100644
--- a/infer/src/backend/prover.ml
+++ b/infer/src/backend/prover.ml
@@ -17,7 +17,7 @@ module F = Format
 
 let decrease_indent_when_exception thunk =
   try (thunk ())
-  with exn when exn_not_failure exn -> (L.d_decrease_indent 1; raise exn)
+  with exn when SymOp.exn_not_failure exn -> (L.d_decrease_indent 1; raise exn)
 
 let compute_max_from_nonempty_int_list l =
   IList.hd (IList.rev (IList.sort Sil.Int.compare_value l))
@@ -1853,7 +1853,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
                         decrease_indent_when_exception
                           (fun () ->
                              try sigma_imply tenv calc_index_frame calc_missing subs prop1 hpred_list2
-                             with exn when exn_not_failure exn ->
+                             with exn when SymOp.exn_not_failure exn ->
                                begin
                                  (L.d_strln_color Red) "backtracking lseg: trying rhs of length exactly 1";
                                  let (_, para_inst3) = Sil.hpara_instantiate para2 _e2 _f2 elist2 in
diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml
index 232cd5129..340ffc31b 100644
--- a/infer/src/backend/specs.ml
+++ b/infer/src/backend/specs.ml
@@ -292,7 +292,8 @@ type call_stats = CallStats.t
 (** Execution statistics *)
 type stats =
   { stats_time: float; (** Analysis time for the procedure *)
-    stats_failure: failure_kind option; (** what type of failure stopped the analysis (if any) *)
+    stats_failure:
+      SymOp.failure_kind option; (** what type of failure stopped the analysis (if any) *)
     stats_calls: Cg.in_out_calls; (** num of procs calling, and called *)
     symops: int; (** Number of SymOp's throughout the whole analysis of the function *)
     mutable nodes_visited_fp : IntSet.t; (** Nodes visited during the footprint phase *)
@@ -351,7 +352,7 @@ let pp_time whole_seconds fmt t =
   else F.fprintf fmt "%f s" t
 
 let pp_failure_kind_opt fmt failure_kind_opt = match failure_kind_opt with
-  | Some failure_kind -> pp_failure_kind fmt failure_kind
+  | Some failure_kind -> SymOp.pp_failure_kind fmt failure_kind
   | None -> F.fprintf fmt "NONE"
 
 let pp_stats err_log whole_seconds fmt stats =
diff --git a/infer/src/backend/specs.mli b/infer/src/backend/specs.mli
index 9389ac604..a7398fbd7 100644
--- a/infer/src/backend/specs.mli
+++ b/infer/src/backend/specs.mli
@@ -102,7 +102,8 @@ end
 (** Execution statistics *)
 type stats =
   { stats_time: float; (** Analysis time for the procedure *)
-    stats_failure: failure_kind option; (** what type of failure stopped the analysis (if any) *)
+    stats_failure:
+      SymOp.failure_kind option; (** what type of failure stopped the analysis (if any) *)
     stats_calls: Cg.in_out_calls; (** num of procs calling, and called *)
     symops: int; (** Number of SymOp's throughout the whole analysis of the function *)
     mutable nodes_visited_fp : IntSet.t; (** Nodes visited during the footprint phase *)
diff --git a/infer/src/backend/state.ml b/infer/src/backend/state.ml
index 4920c0d43..78a7e3333 100644
--- a/infer/src/backend/state.ml
+++ b/infer/src/backend/state.ml
@@ -269,7 +269,7 @@ let extract_pre p tenv pdesc abstract_fun =
     Sil.sub_of_list (IList.map (fun id -> incr count; (id, Sil.Var (Ident.create_normal Ident.name_spec !count))) idlist) in
   let _, p' = Cfg.remove_locals_formals pdesc p in
   let pre, _ = Prop.extract_spec p' in
-  let pre' = try abstract_fun tenv pre with exn when exn_not_failure exn -> pre in
+  let pre' = try abstract_fun tenv pre with exn when SymOp.exn_not_failure exn -> pre in
   Prop.normalize (Prop.prop_sub sub pre')
 
 (** return the normalized precondition extracted form the last prop seen, if any
diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml
index 0b7fe2e38..a8275bdac 100644
--- a/infer/src/backend/symExec.ml
+++ b/infer/src/backend/symExec.ml
@@ -1212,7 +1212,7 @@ and instrs ?(mask_errors=false) tenv pdesc instrs ppl =
   let exe_instr instr (p, path) =
     L.d_str "Executing Generated Instruction "; Sil.d_instr instr; L.d_ln ();
     try sym_exec tenv pdesc instr p path
-    with exn when exn_not_failure exn && mask_errors ->
+    with exn when SymOp.exn_not_failure exn && mask_errors ->
       let err_name, _, ml_source, _ , _, _, _ = Exceptions.recognize_exception exn in
       let loc = (match ml_source with
           | Some ml_loc -> "at " ^ (L.ml_loc_to_string ml_loc)
@@ -1409,7 +1409,7 @@ and check_variadic_sentinel
     let letderef = Sil.Letderef (tmp_id_deref, lexp, typ, loc) in
     try
       instrs tenv pdesc [letderef] result
-    with e when exn_not_failure e ->
+    with e when SymOp.exn_not_failure e ->
       if not fails_on_nil then
         let deref_str = Localise.deref_str_nil_argument_in_variadic_method proc_name nargs i in
         let err_desc =
diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml
index 2d12bd2d9..fba02fb07 100644
--- a/infer/src/backend/tabulation.ml
+++ b/infer/src/backend/tabulation.ml
@@ -427,7 +427,7 @@ let rec fsel_star_fld fsel1 fsel2 = match fsel1, fsel2 with
 
 and array_content_star se1 se2 =
   try sexp_star_fld se1 se2 with
-  | exn when exn_not_failure exn -> se1 (* let postcondition override *)
+  | exn when SymOp.exn_not_failure exn -> se1 (* let postcondition override *)
 
 and esel_star_fld esel1 esel2 = match esel1, esel2 with
   | [], esel2 -> (* don't know whether element is read or written in fun call with array *)
@@ -504,7 +504,7 @@ let sigma_star_fld (sigma1 : Sil.hpred list) (sigma2 : Sil.hpred list) : Sil.hpr
         end
   in
   try star sigma1 sigma2
-  with exn when exn_not_failure exn ->
+  with exn when SymOp.exn_not_failure exn ->
     L.d_str "cannot star ";
     Prop.d_sigma sigma1; L.d_str " and "; Prop.d_sigma sigma2;
     L.d_ln ();
@@ -537,7 +537,7 @@ let sigma_star_typ
           | _ -> star sg1 typings2'
         end in
   try star sigma1 typings2
-  with exn when exn_not_failure exn ->
+  with exn when SymOp.exn_not_failure exn ->
     L.d_str "cannot star ";
     Prop.d_sigma sigma1; L.d_str " and "; Prover.d_typings typings2;
     L.d_ln ();
diff --git a/infer/src/backend/timeout.ml b/infer/src/backend/timeout.ml
index 0b25eacbf..f0e7504d7 100644
--- a/infer/src/backend/timeout.ml
+++ b/infer/src/backend/timeout.ml
@@ -81,7 +81,7 @@ let set_status status =
 
 let timeout_action _ =
   unset_alarm ();
-  raise (Analysis_failure_exe (FKtimeout))
+  raise (SymOp.Analysis_failure_exe (FKtimeout))
 
 let () = begin
   match Config.os_type with
@@ -111,7 +111,7 @@ let resume_previous_timeout () =
 let exe_timeout f x =
   let suspend_existing_timeout_and_start_new_one () =
     suspend_existing_timeout ~keep_symop_total:true;
-    set_alarm (get_timeout_seconds ());
+    set_alarm (SymOp.get_timeout_seconds ());
     SymOp.set_alarm () in
   try
     suspend_existing_timeout_and_start_new_one ();
@@ -119,10 +119,10 @@ let exe_timeout f x =
     resume_previous_timeout ();
     None
   with
-  | Analysis_failure_exe kind ->
+  | SymOp.Analysis_failure_exe kind ->
       resume_previous_timeout ();
       L.log_progress_timeout_event kind;
-      Errdesc.warning_err (State.get_loc ()) "TIMEOUT: %a@." pp_failure_kind kind;
+      Errdesc.warning_err (State.get_loc ()) "TIMEOUT: %a@." SymOp.pp_failure_kind kind;
       Some kind
   | exe ->
       resume_previous_timeout ();
diff --git a/infer/src/backend/timeout.mli b/infer/src/backend/timeout.mli
index 1421002b1..756d84919 100644
--- a/infer/src/backend/timeout.mli
+++ b/infer/src/backend/timeout.mli
@@ -12,7 +12,7 @@ open! Utils
 (** Handle timeout events *)
 
 (** Execute the function up to a given timeout. *)
-val exe_timeout : ('a -> unit) -> 'a -> failure_kind option
+val exe_timeout : ('a -> unit) -> 'a -> SymOp.failure_kind option
 
 (** Resume a previously suspended timeout. *)
 val resume_previous_timeout : unit -> unit
diff --git a/infer/src/backend/utils.ml b/infer/src/backend/utils.ml
index 7c966dd67..aa8d43328 100644
--- a/infer/src/backend/utils.ml
+++ b/infer/src/backend/utils.ml
@@ -16,12 +16,6 @@ module F = Format
     functions and builtin equality. Use IList instead. *)
 module List = struct end
 
-(** initial time of the analysis, i.e. when this module is loaded, gotten from Unix.time *)
-let initial_analysis_time = Unix.time ()
-
-(** precise time of day at the start of the analysis *)
-let initial_timeofday = Unix.gettimeofday ()
-
 (** {2 Generic Utility Functions} *)
 
 (** Compare police: generic compare disabled. *)
@@ -232,175 +226,14 @@ let pp_current_time f () =
   let tm = Unix.localtime (Unix.time ()) in
   F.fprintf f "%02d/%02d/%4d %02d:%02d" tm.Unix.tm_mday tm.Unix.tm_mon (tm.Unix.tm_year + 1900) tm.Unix.tm_hour tm.Unix.tm_min
 
+(** precise time of day at the start of the analysis *)
+let initial_timeofday = Unix.gettimeofday ()
+
 (** Print the time in seconds elapsed since the beginning of the execution of the current command. *)
 let pp_elapsed_time fmt () =
   let elapsed = Unix.gettimeofday () -. initial_timeofday in
   Format.fprintf fmt "%f" elapsed
 
-(** {2 SymOp and Failures: units of symbolic execution} *)
-
-type failure_kind =
-  | FKtimeout (* max time exceeded *)
-  | FKsymops_timeout of int (* max symop's exceeded *)
-  | FKrecursion_timeout of int (* max recursion level exceeded *)
-  | FKcrash of string (* uncaught exception or failed assertion *)
-
-(** failure that prevented analysis from finishing *)
-exception Analysis_failure_exe of failure_kind
-
-let exn_not_failure = function
-  | Analysis_failure_exe _ -> false
-  | _ -> true
-
-let pp_failure_kind fmt = function
-  | FKtimeout -> F.fprintf fmt "TIMEOUT"
-  | FKsymops_timeout symops -> F.fprintf fmt "SYMOPS TIMEOUT (%d)" symops
-  | FKrecursion_timeout level -> F.fprintf fmt "RECURSION TIMEOUT(%d)" level
-  | FKcrash msg -> F.fprintf fmt "CRASH (%s)" msg
-
-let symops_timeout, seconds_timeout =
-  (* default timeout and long timeout are the same for now, but this will change shortly *)
-  let default_symops_timeout = 333 in
-  let default_seconds_timeout = 10.0 in
-  let long_symops_timeout = 1000 in
-  let long_seconds_timeout = 30.0 in
-  if Config.analyze_models then
-    (* use longer timeouts when analyzing models *)
-    long_symops_timeout, long_seconds_timeout
-  else
-    default_symops_timeout, default_seconds_timeout
-
-(** number of symops to multiply by the number of iterations, after which there is a timeout *)
-let symops_per_iteration = ref symops_timeout
-
-(** number of seconds to multiply by the number of iterations, after which there is a timeout *)
-let seconds_per_iteration = ref seconds_timeout
-
-(** Timeout in seconds for each function *)
-let timeout_seconds = ref !seconds_per_iteration
-
-(** Timeout in SymOps *)
-let timeout_symops = ref !symops_per_iteration
-
-(** Set the timeout values in seconds and symops, computed as a multiple of the integer parameter *)
-let set_iterations n =
-  timeout_symops := !symops_per_iteration * n;
-  timeout_seconds := !seconds_per_iteration *. (float_of_int n)
-
-let get_timeout_seconds () = !timeout_seconds
-
-(** Count the number of symbolic operations *)
-module SymOp = struct
-
-  (** Internal state of the module *)
-  type t =
-    {
-      (** Only throw timeout exception when alarm is active *)
-      mutable alarm_active : bool;
-
-      (** last wallclock set by an alarm, if any *)
-      mutable last_wallclock : float option;
-
-      (** Number of symop's *)
-      mutable symop_count : int;
-
-      (** Counter for the total number of symop's.
-          The new state created when save_state is called shares this counter
-          if keep_symop_total is true. Otherwise, a new counter is created. *)
-      symop_total : int ref;
-    }
-
-  let initial () : t =
-    {
-      alarm_active = false;
-      last_wallclock = None;
-      symop_count = 0;
-      symop_total = ref 0;
-    }
-
-  (** Global State *)
-  let gs : t ref = ref (initial ())
-
-  (** Restore the old state. *)
-  let restore_state state =
-    gs := state
-
-  (** Return the old state, and revert the current state to the initial one.
-      If keep_symop_total is true, share the total counter. *)
-  let save_state ~keep_symop_total =
-    let old_state = !gs in
-    let new_state =
-      let st = initial () in
-      if keep_symop_total
-      then
-        { st with symop_total = old_state.symop_total }
-      else
-        st in
-    gs := new_state;
-    old_state
-
-  (** handler for the wallclock timeout *)
-  let wallclock_timeout_handler = ref None
-
-  (** set the handler for the wallclock timeout *)
-  let set_wallclock_timeout_handler handler =
-    wallclock_timeout_handler := Some handler
-
-  (** Set the wallclock alarm checked at every pay() *)
-  let set_wallclock_alarm nsecs =
-    !gs.last_wallclock <- Some (Unix.gettimeofday () +. nsecs)
-
-  (** Unset the wallclock alarm checked at every pay() *)
-  let unset_wallclock_alarm () =
-    !gs.last_wallclock <- None
-
-  (** if the wallclock alarm has expired, raise a timeout exception *)
-  let check_wallclock_alarm () =
-    match !gs.last_wallclock, !wallclock_timeout_handler with
-    | Some alarm_time, Some handler when Unix.gettimeofday () >= alarm_time ->
-        unset_wallclock_alarm ();
-        handler ()
-    | _ -> ()
-
-  (** Return the time remaining before the wallclock alarm expires *)
-  let get_remaining_wallclock_time () =
-    match !gs.last_wallclock with
-    | Some alarm_time ->
-        max 0.0 (alarm_time -. Unix.gettimeofday ())
-    | None ->
-        0.0
-
-  (** Return the total number of symop's since the beginning *)
-  let get_total () =
-    !(!gs.symop_total)
-
-  (** Reset the total number of symop's *)
-  let reset_total () =
-    !gs.symop_total := 0
-
-  (** Count one symop *)
-  let pay () =
-    !gs.symop_count <- !gs.symop_count + 1;
-    !gs.symop_total := !(!gs.symop_total) + 1;
-    if !gs.symop_count > !timeout_symops &&
-       !gs.alarm_active
-    then raise (Analysis_failure_exe (FKsymops_timeout !gs.symop_count));
-    check_wallclock_alarm ()
-
-  (** Reset the counter *)
-  let reset_count () =
-    !gs.symop_count <- 0
-
-  (** Reset the counter and activate the alarm *)
-  let set_alarm () =
-    reset_count ();
-    !gs.alarm_active <- true
-
-  (** De-activate the alarm *)
-  let unset_alarm () =
-    !gs.alarm_active <- false
-end
-
 (** Check if the lhs is a substring of the rhs. *)
 let string_is_prefix s1 s2 =
   String.length s1 <= String.length s2 &&
diff --git a/infer/src/backend/utils.mli b/infer/src/backend/utils.mli
index 726d32881..8c6a4d033 100644
--- a/infer/src/backend/utils.mli
+++ b/infer/src/backend/utils.mli
@@ -142,80 +142,6 @@ val pp_current_time : Format.formatter -> unit -> unit
 (** Print the time in seconds elapsed since the beginning of the execution of the current command. *)
 val pp_elapsed_time : Format.formatter -> unit -> unit
 
-(** {2 SymOp and Failures: units of symbolic execution} *)
-
-(** initial time of the analysis, i.e. when this module is loaded, gotten from Unix.time *)
-val initial_analysis_time : float
-
-(** number of symops to multiply by the number of iterations, after which there is a timeout *)
-val symops_per_iteration : int ref
-
-(** number of seconds to multiply by the number of iterations, after which there is a timeout *)
-val seconds_per_iteration : float ref
-
-(** Timeout in seconds for each function *)
-val get_timeout_seconds : unit -> float
-
-(** Set the timeout values in seconds and symops, computed as a multiple of the integer parameter *)
-val set_iterations : int -> unit
-
-type failure_kind =
-  | FKtimeout (* max time exceeded *)
-  | FKsymops_timeout of int (* max symop's exceeded *)
-  | FKrecursion_timeout of int (* max recursion level exceeded *)
-  | FKcrash of string (* uncaught exception or failed assertion *)
-
-(** Timeout exception *)
-exception Analysis_failure_exe of failure_kind
-
-(** check that the exception is not a timeout exception *)
-val exn_not_failure : exn -> bool
-
-val pp_failure_kind : Format.formatter -> failure_kind -> unit
-
-(** Count the number of symbolic operations *)
-module SymOp : sig
-  (** Internal state of the module *)
-  type t
-
-  (** if the wallclock alarm has expired, raise a timeout exception *)
-  val check_wallclock_alarm : unit -> unit
-
-  (** Return the time remaining before the wallclock alarm expires *)
-  val get_remaining_wallclock_time : unit -> float
-
-  (** Return the total number of symop's since the beginning *)
-  val get_total : unit -> int
-
-  (** Count one symop *)
-  val pay : unit -> unit
-
-  (** Reset the total number of symop's *)
-  val reset_total : unit -> unit
-
-  (** Restore the old state. *)
-  val restore_state : t -> unit
-
-  (** Return the old state, and revert the current state to the initial one.
-      If keep_symop_total is true, share the total counter. *)
-  val save_state : keep_symop_total:bool -> t
-
-  (** Reset the counter and activate the alarm *)
-  val set_alarm : unit -> unit
-
-  (** Set the wallclock alarm checked at every pay() *)
-  val set_wallclock_alarm : float -> unit
-
-  (** set the handler for the wallclock timeout *)
-  val set_wallclock_timeout_handler : (unit -> unit) -> unit
-
-  (** De-activate the alarm *)
-  val unset_alarm : unit -> unit
-
-  (** Unset the wallclock alarm checked at every pay() *)
-  val unset_wallclock_alarm : unit -> unit
-end
-
 module Arg : sig
   include module type of Arg with type spec = Arg.spec