diff --git a/infer/src/backend/callbacks.ml b/infer/src/backend/callbacks.ml
index db00d649f..8f8896816 100644
--- a/infer/src/backend/callbacks.ml
+++ b/infer/src/backend/callbacks.ml
@@ -181,9 +181,7 @@ let iterate_callbacks call_graph exe_env =
   (* Store all the summaries to disk *)
   List.iter
     ~f:(fun pname ->
-        let updated_summary_opt =
-          Option.map (Specs.get_summary pname) ~f:Specs.increment_timestamp in
-        Option.iter ~f:(Specs.store_summary pname) updated_summary_opt)
+        Specs.store_summary pname (Specs.get_summary_unsafe "Checkers: store summaries" pname))
     procs_to_analyze;
 
   Config.curr_language := saved_language
diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml
index db9ee3a66..54ace86ed 100644
--- a/infer/src/backend/interproc.ml
+++ b/infer/src/backend/interproc.ml
@@ -533,8 +533,9 @@ let forward_tabulate tenv pdesc wl source =
       let summary = Specs.get_summary_unsafe "forward_tabulate" proc_name in
       let phase_string =
         if Specs.equal_phase (Specs.get_phase summary) Specs.FOOTPRINT then "FP" else "RE" in
-      let timestamp = Specs.get_timestamp summary in
-      F.sprintf "[%s:%d] %s" phase_string timestamp (Procname.to_string proc_name) in
+      let status = Specs.get_status summary in
+      F.sprintf
+        "[%s:%s] %s" phase_string (Specs.string_of_status status) (Procname.to_string proc_name) in
     L.d_strln ("**** " ^ (log_string pname) ^ " " ^
                "Node: " ^ string_of_int (Procdesc.Node.get_id curr_node :> int) ^ ", " ^
                "Procedure: " ^ Procname.to_string pname ^ ", " ^
@@ -989,17 +990,9 @@ type exe_phase = (unit -> unit) * (unit -> Prop.normal Specs.spec list * Specs.p
     [go ()] was interrupted by and exception. *)
 let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Procdesc.t) source
   : exe_phase =
-  let summary = Specs.get_summary_unsafe "check_recursion_level" pname in
+  let summary = Specs.get_summary_unsafe "perform_analysis_phase" pname in
   let start_node = Procdesc.get_start_node pdesc in
 
-  let check_recursion_level () =
-    let recursion_level = Specs.get_timestamp summary in
-    if recursion_level > Config.max_recursion then
-      begin
-        L.err "Reached maximum level of recursion, raising a Timeout@.";
-        raise (SymOp.Analysis_failure_exe (FKrecursion_timeout recursion_level))
-      end in
-
   let compute_footprint () : exe_phase =
     let go (wl : Worklist.t) () =
       let init_prop = initial_prop_from_emp tenv pdesc in
@@ -1020,7 +1013,6 @@ let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Procdesc.t) source
       L.d_strln "initial props =";
       Propset.d Prop.prop_emp init_props; L.d_ln (); L.d_ln();
       L.d_decrease_indent 1;
-      check_recursion_level ();
       Worklist.add wl start_node;
       Config.arc_mode :=
         Hashtbl.mem
@@ -1057,7 +1049,6 @@ let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Procdesc.t) source
     let valid_specs = ref [] in
     let go () =
       L.out "@.#### Start: Re-Execution for %a ####@." Procname.pp pname;
-      check_recursion_level ();
       let filter p =
         let wl = path_set_create_worklist pdesc in
         let speco = execute_filter_prop wl tenv pdesc start_node p source in
@@ -1286,8 +1277,7 @@ let update_specs tenv proc_name phase (new_specs : Specs.NormSpec.t list)
 (** update a summary after analysing a procedure *)
 let update_summary tenv prev_summary specs phase proc_name elapsed res =
   let normal_specs = List.map ~f:(Specs.spec_normalize tenv) specs in
-  let new_specs, changed = update_specs tenv proc_name phase normal_specs in
-  let timestamp = max 1 (prev_summary.Specs.timestamp + if changed then 1 else 0) in
+  let new_specs, _ = update_specs tenv proc_name phase normal_specs in
   let stats_time = prev_summary.Specs.stats.Specs.stats_time +. elapsed in
   let symops = prev_summary.Specs.stats.Specs.symops + SymOp.get_total () in
   let stats_failure = match res with
@@ -1310,7 +1300,6 @@ let update_summary tenv prev_summary specs phase proc_name elapsed res =
     Specs.phase;
     stats;
     payload;
-    timestamp;
   }
 
 
@@ -1355,8 +1344,7 @@ let transition_footprint_re_exe tenv proc_name joined_pres =
         { summary.Specs.payload with
           Specs.preposts = Some specs; } in
       { summary with
-        Specs.timestamp = 0;
-        phase = Specs.RE_EXECUTION;
+        Specs.phase = Specs.RE_EXECUTION;
         payload;
       } in
   Specs.add_summary proc_name summary'
diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml
index b87dbc804..e75b1a744 100644
--- a/infer/src/backend/ondemand.ml
+++ b/infer/src/backend/ondemand.ml
@@ -55,7 +55,7 @@ let should_be_analyzed proc_name proc_attributes =
   let already_analyzed () =
     match Specs.get_summary proc_name with
     | Some summary ->
-        Specs.get_timestamp summary > 0
+        Specs.equal_status (Specs.get_status summary) Specs.Analyzed
     | None ->
         false in
   proc_attributes.ProcAttributes.is_defined && (* we have the implementation *)
@@ -142,29 +142,23 @@ let run_proc_analysis ~propagate_exceptions analyze_proc curr_pdesc callee_pdesc
       then Some callee_pdesc
       else None in
     Specs.reset_summary call_graph callee_pname attributes_opt callee_pdesc_option;
-    Specs.set_status callee_pname Specs.ACTIVE;
+    Specs.set_status callee_pname Specs.Active;
     source in
 
   let postprocess source =
     decr nesting;
     let summary = Specs.get_summary_unsafe "ondemand" callee_pname in
-    let summary' =
-      { summary with
-        Specs.status = Specs.INACTIVE;
-        timestamp = summary.Specs.timestamp + 1 } in
-    Specs.store_summary callee_pname summary';
+    Specs.store_summary callee_pname summary;
     Printer.write_proc_html source false callee_pdesc;
-    summary' in
+    summary in
 
   let log_error_and_continue exn kind =
     Reporting.log_error callee_pname exn;
     let prev_summary = Specs.get_summary_unsafe "Ondemand.do_analysis" callee_pname in
-    let timestamp = max 1 (prev_summary.Specs.timestamp) in
     let stats = { prev_summary.Specs.stats with Specs.stats_failure = Some kind } in
     let payload =
       { prev_summary.Specs.payload with Specs.preposts = Some []; } in
-    let new_summary =
-      { prev_summary with Specs.stats; payload; timestamp; } in
+    let new_summary = { prev_summary with Specs.stats; payload } in
     Specs.store_summary callee_pname new_summary;
     new_summary in
 
diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml
index 306af6bdf..a1f34ba35 100644
--- a/infer/src/backend/specs.ml
+++ b/infer/src/backend/specs.ml
@@ -305,7 +305,15 @@ type stats =
     call_stats : call_stats;
   }
 
-type status = ACTIVE | INACTIVE | STALE [@@deriving compare]
+type status = Initialized | Active | Analyzed [@@deriving compare]
+
+let string_of_status = function
+  | Initialized -> "Initialized"
+  | Active -> "Active"
+  | Analyzed -> "Analyzed"
+
+let pp_status fmt status =
+  F.fprintf fmt "%s" (string_of_status status)
 
 let equal_status = [%compare.equal : status]
 
@@ -335,8 +343,7 @@ type summary = {
   payload: payload;  (** payload containing the result of some analysis *)
   sessions: int ref; (** Session number: how many nodes went trough symbolic execution *)
   stats: stats;  (** statistics: execution time and list of errors *)
-  status: status; (** ACTIVE when the proc is being analyzed *)
-  timestamp: int; (** Timestamp of the specs, >= 0, increased every time the specs change *)
+  status: status; (** Analysis status of the procedure *)
   attributes : ProcAttributes.t; (** Attributes of the procedure *)
   proc_desc_option : Procdesc.t option;
 }
@@ -407,12 +414,6 @@ let pp_specs pe fmt specs =
                      F.fprintf fmt "\\subsection*{Spec %d of %d}@\n\\(%a\\)@\n"
                        !cnt total (pp_spec pe None) spec) specs
 
-let describe_timestamp summary =
-  ("Timestamp", Printf.sprintf "%d" summary.timestamp)
-
-let describe_status summary =
-  ("Status", if equal_status summary.status ACTIVE then "ACTIVE" else "INACTIVE")
-
 let describe_phase summary =
   ("Phase", if equal_phase summary.phase FOOTPRINT then "FOOTPRINT" else "RE_EXECUTION")
 
@@ -444,8 +445,7 @@ let get_specs_from_payload summary =
 let pp_summary_no_stats_specs fmt summary =
   let pp_pair fmt (x, y) = F.fprintf fmt "%s: %s" x y in
   F.fprintf fmt "%s@\n" (get_signature summary);
-  F.fprintf fmt "%a@\n" pp_pair (describe_timestamp summary);
-  F.fprintf fmt "%a@\n" pp_pair (describe_status summary);
+  F.fprintf fmt "%a@\n" pp_status summary.status;
   F.fprintf fmt "%a@\n" pp_pair (describe_phase summary)
 
 let pp_payload pe fmt { preposts; typestate; crashcontext_frame; quandary; siof; threadsafety; buffer_overrun } =
@@ -561,8 +561,9 @@ let store_summary pname (summ1: summary) =
     else
       { summ2 with
         stats = { summ1.stats with stats_time = 0.0} } in
+  let final_summary = { summ3 with status = Analyzed } in
   add_summary pname summ3 (* Make sure the summary in memory is identical to the saved one *);
-  Serialization.write_to_file summary_serializer (res_dir_specs_filename pname) summ3
+  Serialization.write_to_file summary_serializer (res_dir_specs_filename pname) final_summary
 
 (** Load procedure summary from the given file *)
 let load_summary specs_file =
@@ -668,13 +669,7 @@ let get_status summary =
   summary.status
 
 let is_active summary =
-  equal_status (get_status summary) ACTIVE
-
-let get_timestamp summary =
-  summary.timestamp
-
-let increment_timestamp summary =
-  { summary with timestamp = summary.timestamp + 1 }
+  equal_status (get_status summary) Active
 
 let get_proc_name summary =
   summary.attributes.ProcAttributes.proc_name
@@ -746,8 +741,7 @@ let init_summary
       sessions = ref 0;
       payload = empty_payload;
       stats = empty_stats calls in_out_calls_opt;
-      status = INACTIVE;
-      timestamp = 0;
+      status = Initialized;
       attributes =
         { proc_attributes with
           ProcAttributes.proc_flags = proc_flags; };
diff --git a/infer/src/backend/specs.mli b/infer/src/backend/specs.mli
index 0e4c9a838..02768f6ad 100644
--- a/infer/src/backend/specs.mli
+++ b/infer/src/backend/specs.mli
@@ -115,7 +115,17 @@ type stats =
     call_stats : CallStats.t;
   }
 
-type status = ACTIVE | INACTIVE | STALE
+(** Analysis status of the procedure:
+    - Initialized means that the summary has been created by the procedure has not been analyzed yet
+    - Active meas that the procedure is being analyzed
+    - Analyzed means that the analysis of the procedure is finished *)
+type status = Initialized | Active | Analyzed
+
+val equal_status : status -> status -> bool
+
+val string_of_status : status -> string
+
+val pp_status : Format.formatter -> status -> unit
 
 type phase = FOOTPRINT | RE_EXECUTION
 
@@ -144,8 +154,7 @@ type summary = {
   payload: payload;  (** payload containing the result of some analysis *)
   sessions: int ref; (** Session number: how many nodes went trough symbolic execution *)
   stats: stats;  (** statistics: execution time and list of errors *)
-  status: status; (** ACTIVE when the proc is being analyzed *)
-  timestamp: int; (** Timestamp of the specs, >= 0, increased every time the specs change *)
+  status: status; (** Analysis status of the procedure *)
   attributes : ProcAttributes.t; (** Attributes of the procedure *)
   proc_desc_option : Procdesc.t option;
 }
@@ -198,12 +207,6 @@ val get_specs_from_payload : summary -> Prop.normal spec list
 (** @deprecated Return the summary for the procedure name. Raises an exception when not found. *)
 val get_summary_unsafe : string -> Procname.t -> summary
 
-(** Return the current timestamp for the summary *)
-val get_timestamp : summary -> int
-
-(** Increment the number of times a summary has been updated *)
-val increment_timestamp : summary -> summary
-
 (** Return the status (active v.s. inactive) of a procedure summary *)
 val get_status : summary -> status
 
diff --git a/infer/src/base/Serialization.ml b/infer/src/base/Serialization.ml
index 33b6e63cb..07b5c5bf5 100644
--- a/infer/src/base/Serialization.ml
+++ b/infer/src/base/Serialization.ml
@@ -34,7 +34,7 @@ module Key = struct
 end
 
 (** version of the binary files, to be incremented for each change *)
-let version = 26
+let version = 27
 
 
 (** Retry the function while an exception filtered is thrown,
diff --git a/infer/src/checkers/summary.ml b/infer/src/checkers/summary.ml
index cf7b2ed39..32706c9bc 100644
--- a/infer/src/checkers/summary.ml
+++ b/infer/src/checkers/summary.ml
@@ -24,8 +24,7 @@ module type S = sig
   type summary
   (*  type astate*)
 
-  (** Write the [summary] for the procname to persistent storage. Returns the summary actually
-      written. *)
+  (** Write the [summary] for the procname to persistent storage. *)
   val write_summary : Procname.t -> summary -> unit
 
   (** read and return the summary for [callee_pname] called from [caller_pdesc]. does the analysis
@@ -40,8 +39,7 @@ module Make (H : Helper) = struct
     match Specs.get_summary pname with
     | Some global_summary ->
         let payload = H.update_payload summary global_summary.Specs.payload in
-        let timestamp = global_summary.timestamp + 1 in
-        Specs.store_summary pname { global_summary with payload; timestamp; }
+        Specs.store_summary pname { global_summary with payload; }
     | None ->
         failwithf "Summary for %a should exist, but does not!@." Procname.pp pname