diff --git a/infer/src/backend/CallSite.ml b/infer/src/IR/CallSite.ml
similarity index 100%
rename from infer/src/backend/CallSite.ml
rename to infer/src/IR/CallSite.ml
diff --git a/infer/src/backend/CallSite.mli b/infer/src/IR/CallSite.mli
similarity index 100%
rename from infer/src/backend/CallSite.mli
rename to infer/src/IR/CallSite.mli
diff --git a/infer/src/IR/Cfg.re b/infer/src/IR/Cfg.re
index 7e84a4c0c..266b5ea0e 100644
--- a/infer/src/IR/Cfg.re
+++ b/infer/src/IR/Cfg.re
@@ -900,22 +900,6 @@ let check_cfg_connectedness cfg => {
 };
 
 
-/** Removes seeds variables from a prop corresponding to captured variables in an objc block */
-let remove_seed_captured_vars_block tenv captured_vars prop => {
-  let is_captured pname vn => Mangled.equal pname vn;
-  let hpred_seed_captured =
-    fun
-    | Sil.Hpointsto (Exp.Lvar pv) _ _ => {
-        let pname = Pvar.get_name pv;
-        Pvar.is_seed pv && IList.mem is_captured pname captured_vars
-      }
-    | _ => false;
-  let sigma = prop.Prop.sigma;
-  let sigma' = IList.filter (fun hpred => not (hpred_seed_captured hpred)) sigma;
-  Prop.normalize tenv (Prop.set prop sigma::sigma')
-};
-
-
 /** Serializer for control flow graphs */
 let cfg_serializer: Serialization.serializer cfg = Serialization.create_serializer Serialization.cfg_key;
 
diff --git a/infer/src/IR/Cfg.rei b/infer/src/IR/Cfg.rei
index 623eed1d9..8f595b0ba 100644
--- a/infer/src/IR/Cfg.rei
+++ b/infer/src/IR/Cfg.rei
@@ -302,11 +302,6 @@ let get_defined_procs: cfg => list Procdesc.t;
 let check_cfg_connectedness: cfg => unit;
 
 
-/** Removes seeds variables from a prop corresponding to captured variables in an objc block */
-let remove_seed_captured_vars_block:
-  Tenv.t => list Mangled.t => Prop.t Prop.normal => Prop.t Prop.normal;
-
-
 /** Creates a copy of a procedure description and a list of type substitutions of the form
     (name, typ) where name is a parameter. The resulting procdesc is isomorphic but
     all the type of the parameters are replaced in the instructions according to the list.
diff --git a/infer/src/backend/errlog.ml b/infer/src/IR/Errlog.ml
similarity index 94%
rename from infer/src/backend/errlog.ml
rename to infer/src/IR/Errlog.ml
index 9e29e16e3..6d9df88aa 100644
--- a/infer/src/backend/errlog.ml
+++ b/infer/src/IR/Errlog.ml
@@ -26,11 +26,11 @@ type loc_trace = loc_trace_elem list
 (** Data associated to a specific error *)
 type err_data =
   (int * int) * int * Location.t * L.ml_loc option * loc_trace *
-  Prop.normal Prop.t option * Exceptions.err_class * Exceptions.exception_visibility
+  Exceptions.err_class * Exceptions.exception_visibility
 
 let err_data_compare
-    (_, _, loc1, _, _, _, _, _)
-    (_, _, loc2, _, _, _, _, _) =
+    (_, _, loc1, _, _, _, _)
+    (_, _, loc2, _, _, _, _) =
   Location.compare loc1 loc2
 
 module ErrDataSet = (* set err_data with no repeated loc *)
@@ -72,7 +72,6 @@ type iter_fun =
   bool ->
   Localise.t -> Localise.error_desc -> string ->
   loc_trace ->
-  Prop.normal Prop.t option ->
   Exceptions.err_class ->
   Exceptions.exception_visibility ->
   unit
@@ -81,10 +80,10 @@ type iter_fun =
 let iter (f: iter_fun) (err_log: t) =
   ErrLogHash.iter (fun (ekind, in_footprint, err_name, desc, severity) set ->
       ErrDataSet.iter
-        (fun (node_id_key, _, loc, ml_loc_opt, ltr, pre_opt, eclass, visibility) ->
+        (fun (node_id_key, _, loc, ml_loc_opt, ltr, eclass, visibility) ->
            f
              node_id_key loc ml_loc_opt ekind in_footprint err_name
-             desc severity ltr pre_opt eclass visibility)
+             desc severity ltr eclass visibility)
         set)
     err_log
 
@@ -113,7 +112,7 @@ let pp_warnings fmt (errlog : t) =
 let pp_html source path_to_root fmt (errlog: t) =
   let pp_eds fmt eds =
     let pp_nodeid_session_loc
-        fmt ((nodeid, _), session, loc, _, _, _, _, _) =
+        fmt ((nodeid, _), session, loc, _, _, _, _) =
       Io_infer.Html.pp_session_link source path_to_root fmt (nodeid, session, loc.Location.line) in
     ErrDataSet.iter (pp_nodeid_session_loc fmt) eds in
   let f do_fp ek (ekind, infp, err_name, desc, _) eds =
@@ -168,7 +167,7 @@ let update errlog_old errlog_new =
     (fun (ekind, infp, s, desc, severity) l ->
        ignore (add_issue errlog_old (ekind, infp, s, desc, severity) l)) errlog_new
 
-let log_issue _ekind err_log loc node_id_key session ltr pre_opt exn =
+let log_issue _ekind err_log loc node_id_key session ltr exn =
   let err_name, desc, ml_loc_opt, visibility, severity, force_kind, eclass =
     Exceptions.recognize_exception exn in
   let ekind = match force_kind with
@@ -191,7 +190,7 @@ let log_issue _ekind err_log loc node_id_key session ltr pre_opt exn =
       add_issue err_log
         (ekind, !Config.footprint, err_name, desc, severity_to_str severity)
         (ErrDataSet.singleton
-           (node_id_key, session, loc, ml_loc_opt, ltr, pre_opt, eclass, visibility)) in
+           (node_id_key, session, loc, ml_loc_opt, ltr, eclass, visibility)) in
     let should_print_now =
       match exn with
       | Exceptions.Internal_error _ -> true
@@ -270,7 +269,7 @@ module Err_table = struct
       ErrDataSet.iter (fun loc -> add_err loc err_name) eds in
     ErrLogHash.iter f err_table;
 
-    let pp ekind (nodeidkey, _, loc, ml_loc_opt, _, _, _, _) fmt err_names =
+    let pp ekind (nodeidkey, _, loc, ml_loc_opt, _, _, _) fmt err_names =
       IList.iter (fun (err_name, desc) ->
           Exceptions.pp_err nodeidkey loc ekind err_name desc ml_loc_opt fmt ()) err_names in
     F.fprintf fmt "@.Detailed errors during footprint phase:@.";
diff --git a/infer/src/backend/errlog.mli b/infer/src/IR/Errlog.mli
similarity index 94%
rename from infer/src/backend/errlog.mli
rename to infer/src/IR/Errlog.mli
index 41d657b4d..99d99dbe2 100644
--- a/infer/src/backend/errlog.mli
+++ b/infer/src/IR/Errlog.mli
@@ -37,7 +37,6 @@ type iter_fun =
   bool ->
   Localise.t -> Localise.error_desc -> string ->
   loc_trace ->
-  Prop.normal Prop.t option ->
   Exceptions.err_class ->
   Exceptions.exception_visibility ->
   unit
@@ -61,9 +60,7 @@ val size : (Exceptions.err_kind -> bool -> bool) -> t -> int
 val update : t -> t -> unit
 
 val log_issue :
-  Exceptions.err_kind ->
-  t -> Location.t -> (int * int) -> int -> loc_trace ->
-  (Prop.normal Prop.t) option -> exn -> unit
+  Exceptions.err_kind -> t -> Location.t -> (int * int) -> int -> loc_trace -> exn -> unit
 
 (** {2 Functions for manipulating per-file error tables} *)
 
diff --git a/infer/src/backend/exceptions.ml b/infer/src/IR/Exceptions.ml
similarity index 97%
rename from infer/src/backend/exceptions.ml
rename to infer/src/IR/Exceptions.ml
index 3b13dc290..f58e8b7c5 100644
--- a/infer/src/backend/exceptions.ml
+++ b/infer/src/IR/Exceptions.ml
@@ -45,6 +45,7 @@ exception Array_out_of_bounds_l2 of Localise.error_desc * L.ml_loc
 exception Array_out_of_bounds_l3 of Localise.error_desc * L.ml_loc
 exception Array_of_pointsto of L.ml_loc
 exception Bad_footprint of L.ml_loc
+exception Cannot_star of L.ml_loc
 exception Class_cast_exception of Localise.error_desc * L.ml_loc
 exception Codequery of Localise.error_desc
 exception Comparing_floats_for_equality of Localise.error_desc * L.ml_loc
@@ -67,7 +68,7 @@ exception Inherently_dangerous_function of Localise.error_desc
 exception Internal_error of Localise.error_desc
 exception Java_runtime_exception of Typename.t * string * Localise.error_desc
 exception Leak of
-    bool * Prop.normal Prop.t * Sil.hpred * (exception_visibility * Localise.error_desc)
+    bool * Sil.hpred * (exception_visibility * Localise.error_desc)
     * bool * PredSymb.resource * L.ml_loc
 exception Missing_fld of Ident.fieldname * L.ml_loc
 exception Premature_nil_termination of Localise.error_desc * L.ml_loc
@@ -77,7 +78,7 @@ exception Parameter_not_null_checked of Localise.error_desc * L.ml_loc
 exception Pointer_size_mismatch of Localise.error_desc * L.ml_loc
 exception Precondition_not_found of Localise.error_desc * L.ml_loc
 exception Precondition_not_met of Localise.error_desc * L.ml_loc
-exception Retain_cycle of Prop.normal Prop.t * Sil.hpred * Localise.error_desc * L.ml_loc
+exception Retain_cycle of Sil.hpred * Localise.error_desc * L.ml_loc
 exception Registered_observer_being_deallocated of Localise.error_desc * L.ml_loc
 exception Return_expression_required of Localise.error_desc * L.ml_loc
 exception Return_statement_missing of Localise.error_desc * L.ml_loc
@@ -132,7 +133,7 @@ let recognize_exception exn =
     | Bad_footprint ml_loc ->
         (Localise.from_string "Bad_footprint",
          Localise.no_desc, Some ml_loc, Exn_developer, Low, None, Nocat)
-    | Prop.Cannot_star ml_loc ->
+    | Cannot_star ml_loc ->
         (Localise.from_string "Cannot_star",
          Localise.no_desc, Some ml_loc, Exn_developer, Low, None, Nocat)
     | Class_cast_exception (desc, ml_loc) ->
@@ -208,7 +209,7 @@ let recognize_exception exn =
     | Java_runtime_exception (exn_name, _, desc) ->
         let exn_str = Typename.name exn_name in
         (Localise.from_string exn_str, desc, None, Exn_user, High, None, Prover)
-    | Leak (fp_part, _, _, (exn_vis, error_desc), done_array_abstraction, resource, ml_loc) ->
+    | Leak (fp_part, _, (exn_vis, error_desc), done_array_abstraction, resource, ml_loc) ->
         if done_array_abstraction
         then (Localise.from_string "Leak_after_array_abstraction",
               error_desc, Some ml_loc, Exn_developer, High, None, Prover)
@@ -244,7 +245,7 @@ let recognize_exception exn =
     | Precondition_not_met (desc, ml_loc) ->
         (Localise.precondition_not_met,
          desc, Some ml_loc, Exn_developer, Medium, Some Kwarning, Nocat) (* always a warning *)
-    | Retain_cycle (_, _, desc, ml_loc) ->
+    | Retain_cycle (_, desc, ml_loc) ->
         (Localise.retain_cycle,
          desc, Some ml_loc, Exn_user, High, None, Prover)
     | Registered_observer_being_deallocated (desc, ml_loc) ->
diff --git a/infer/src/backend/exceptions.mli b/infer/src/IR/Exceptions.mli
similarity index 96%
rename from infer/src/backend/exceptions.mli
rename to infer/src/IR/Exceptions.mli
index cacbab161..4855cdbb9 100644
--- a/infer/src/backend/exceptions.mli
+++ b/infer/src/IR/Exceptions.mli
@@ -40,6 +40,7 @@ exception Array_out_of_bounds_l1 of Localise.error_desc * Logging.ml_loc
 exception Array_out_of_bounds_l2 of Localise.error_desc * Logging.ml_loc
 exception Array_out_of_bounds_l3 of Localise.error_desc * Logging.ml_loc
 exception Bad_footprint of Logging.ml_loc
+exception Cannot_star of Logging.ml_loc
 exception Class_cast_exception of Localise.error_desc * Logging.ml_loc
 exception Codequery of Localise.error_desc
 exception Comparing_floats_for_equality of Localise.error_desc * Logging.ml_loc
@@ -62,7 +63,7 @@ exception Inherently_dangerous_function of Localise.error_desc
 exception Internal_error of Localise.error_desc
 exception Java_runtime_exception of Typename.t * string * Localise.error_desc
 exception Leak of
-    bool * Prop.normal Prop.t * Sil.hpred * (exception_visibility * Localise.error_desc)
+    bool * Sil.hpred * (exception_visibility * Localise.error_desc)
     * bool * PredSymb.resource * Logging.ml_loc
 exception Missing_fld of Ident.fieldname * Logging.ml_loc
 exception Premature_nil_termination of Localise.error_desc * Logging.ml_loc
@@ -72,7 +73,7 @@ exception Parameter_not_null_checked of Localise.error_desc * Logging.ml_loc
 exception Pointer_size_mismatch of Localise.error_desc * Logging.ml_loc
 exception Precondition_not_found of Localise.error_desc * Logging.ml_loc
 exception Precondition_not_met of Localise.error_desc * Logging.ml_loc
-exception Retain_cycle of Prop.normal Prop.t * Sil.hpred * Localise.error_desc * Logging.ml_loc
+exception Retain_cycle of Sil.hpred * Localise.error_desc * Logging.ml_loc
 exception Registered_observer_being_deallocated of Localise.error_desc * Logging.ml_loc
 exception Return_expression_required of Localise.error_desc * Logging.ml_loc
 exception Return_statement_missing of Localise.error_desc * Logging.ml_loc
diff --git a/infer/src/base/Io_infer.ml b/infer/src/IR/Io_infer.ml
similarity index 100%
rename from infer/src/base/Io_infer.ml
rename to infer/src/IR/Io_infer.ml
diff --git a/infer/src/base/Io_infer.mli b/infer/src/IR/Io_infer.mli
similarity index 100%
rename from infer/src/base/Io_infer.mli
rename to infer/src/IR/Io_infer.mli
diff --git a/infer/src/backend/lintIssues.ml b/infer/src/IR/LintIssues.ml
similarity index 100%
rename from infer/src/backend/lintIssues.ml
rename to infer/src/IR/LintIssues.ml
diff --git a/infer/src/backend/lintIssues.mli b/infer/src/IR/LintIssues.mli
similarity index 100%
rename from infer/src/backend/lintIssues.mli
rename to infer/src/IR/LintIssues.mli
diff --git a/infer/src/backend/localise.ml b/infer/src/IR/Localise.ml
similarity index 99%
rename from infer/src/backend/localise.ml
rename to infer/src/IR/Localise.ml
index 6b5608587..d72532ab3 100644
--- a/infer/src/backend/localise.ml
+++ b/infer/src/IR/Localise.ml
@@ -755,9 +755,8 @@ let desc_return_expression_required typ_str loc =
       (at_line tags loc) in
   { no_desc with descriptions = [description]; tags = !tags }
 
-let desc_retain_cycle prop cycle loc cycle_dotty =
+let desc_retain_cycle cycle loc cycle_dotty =
   Logging.d_strln "Proposition with retain cycle:";
-  Prop.d_prop prop; Logging.d_strln "";
   let ct = ref 1 in
   let tags = Tags.create () in
   let str_cycle = ref "" in
diff --git a/infer/src/backend/localise.mli b/infer/src/IR/Localise.mli
similarity index 99%
rename from infer/src/backend/localise.mli
rename to infer/src/IR/Localise.mli
index 0d05673a3..a9f955d4c 100644
--- a/infer/src/backend/localise.mli
+++ b/infer/src/IR/Localise.mli
@@ -246,7 +246,7 @@ val desc_precondition_not_met : pnm_kind option -> Procname.t -> Location.t -> e
 val desc_return_expression_required : string -> Location.t -> error_desc
 
 val desc_retain_cycle :
-  Prop.normal Prop.t -> ((Sil.strexp * Typ.t) * Ident.fieldname * Sil.strexp) list ->
+  ((Sil.strexp * Typ.t) * Ident.fieldname * Sil.strexp) list ->
   Location.t -> string option -> error_desc
 
 val registered_observer_being_deallocated_str : string -> string
diff --git a/infer/src/backend/mleak_buckets.ml b/infer/src/IR/Mleak_buckets.ml
similarity index 100%
rename from infer/src/backend/mleak_buckets.ml
rename to infer/src/IR/Mleak_buckets.ml
diff --git a/infer/src/backend/mleak_buckets.mli b/infer/src/IR/Mleak_buckets.mli
similarity index 100%
rename from infer/src/backend/mleak_buckets.mli
rename to infer/src/IR/Mleak_buckets.mli
diff --git a/infer/src/backend/objc_models.ml b/infer/src/IR/Objc_models.ml
similarity index 100%
rename from infer/src/backend/objc_models.ml
rename to infer/src/IR/Objc_models.ml
diff --git a/infer/src/backend/objc_models.mli b/infer/src/IR/Objc_models.mli
similarity index 100%
rename from infer/src/backend/objc_models.mli
rename to infer/src/IR/Objc_models.mli
diff --git a/infer/src/backend/InferPrint.re b/infer/src/backend/InferPrint.re
index 342697f7a..ff2a1dbec 100644
--- a/infer/src/backend/InferPrint.re
+++ b/infer/src/backend/InferPrint.re
@@ -344,7 +344,7 @@ let module IssuesCsv = {
   /** Write bug report in csv format */
   let pp_issues_of_error_log fmt error_filter _ proc_loc_opt procname err_log => {
     let pp x => F.fprintf fmt x;
-    let pp_row (_, node_key) loc _ ekind in_footprint error_name error_desc severity ltr _ eclass _ => {
+    let pp_row (_, node_key) loc _ ekind in_footprint error_name error_desc severity ltr eclass _ => {
       let source_file =
         switch proc_loc_opt {
         | Some proc_loc => proc_loc.Location.file
@@ -424,7 +424,6 @@ let module IssuesJson = {
         error_desc
         severity
         ltr
-        _
         eclass
         visibility => {
       let source_file =
@@ -479,7 +478,7 @@ let module IssuesJson = {
 let module IssuesTests = {
   /** Write bug report in a format suitable for tests on analysis results. */
   let pp_issues_of_error_log fmt error_filter _ proc_loc_opt proc_name err_log => {
-    let pp_row _ loc _ ekind in_footprint error_name error_desc _ _ _ _ _ => {
+    let pp_row _ loc _ ekind in_footprint error_name error_desc _ _ _ _ => {
       let (source_file, line_offset) =
         switch proc_loc_opt {
         | Some proc_loc =>
@@ -524,7 +523,7 @@ let module IssuesTests = {
 let module IssuesTxt = {
   /** Write bug report in text format */
   let pp_issues_of_error_log fmt error_filter _ proc_loc_opt _ err_log => {
-    let pp_row (node_id, node_key) loc _ ekind in_footprint error_name error_desc _ _ _ _ _ => {
+    let pp_row (node_id, node_key) loc _ ekind in_footprint error_name error_desc _ _ _ _ => {
       let source_file =
         switch proc_loc_opt {
         | Some proc_loc => proc_loc.Location.file
@@ -540,7 +539,6 @@ let module IssuesTxt = {
 
 let module IssuesXml = {
   let xml_issues_id = ref 0;
-  let include_precondition_tree = false;
   let loc_trace_to_xml linereader ltr => {
     let subtree label contents => Io_infer.Xml.create_tree label [] [Io_infer.Xml.String contents];
     let level_to_xml level => subtree Io_infer.Xml.tag_level (string_of_int level);
@@ -578,19 +576,7 @@ let module IssuesXml = {
 
   /** print issues from summary in xml */
   let pp_issues_of_error_log fmt error_filter linereader proc_loc_opt proc_name err_log => {
-    let do_row
-        (_, node_key)
-        loc
-        _
-        ekind
-        in_footprint
-        error_name
-        error_desc
-        severity
-        ltr
-        pre_opt
-        eclass
-        _ => {
+    let do_row (_, node_key) loc _ ekind in_footprint error_name error_desc severity ltr eclass _ => {
       let source_file =
         switch proc_loc_opt {
         | Some proc_loc => proc_loc.Location.file
@@ -598,13 +584,6 @@ let module IssuesXml = {
         };
       if (in_footprint && error_filter source_file error_desc error_name) {
         let err_desc_string = error_desc_to_xml_string error_desc;
-        let precondition_tree () =>
-          switch pre_opt {
-          | None => []
-          | Some pre =>
-            Dotty.reset_node_counter ();
-            [Dotty.prop_to_xml pre Io_infer.Xml.tag_precondition 1]
-          };
         let subtree label contents =>
           Io_infer.Xml.create_tree label [] [Io_infer.Xml.String contents];
         let kind = Exceptions.err_kind_string ekind;
@@ -633,13 +612,7 @@ let module IssuesXml = {
             Io_infer.Xml.create_tree
               Io_infer.Xml.tag_qualifier_tags [] (error_desc_to_xml_tags error_desc),
             subtree Io_infer.Xml.tag_hash (string_of_int bug_hash)
-          ] @ (
-            if include_precondition_tree {
-              precondition_tree ()
-            } else {
-              []
-            }
-          );
+          ];
           Io_infer.Xml.create_tree "bug" attributes forest
         };
         Io_infer.Xml.pp_inner_node fmt tree
@@ -784,7 +757,7 @@ let module Stats = {
   };
   let process_err_log error_filter linereader err_log stats => {
     let found_errors = ref false;
-    let process_row _ loc _ ekind in_footprint error_name error_desc _ ltr _ _ _ => {
+    let process_row _ loc _ ekind in_footprint error_name error_desc _ ltr _ _ => {
       let type_str = Localise.to_string error_name;
       if (in_footprint && error_filter error_desc error_name) {
         switch ekind {
diff --git a/infer/src/backend/abs.ml b/infer/src/backend/abs.ml
index 31fd1ba50..3269ad08a 100644
--- a/infer/src/backend/abs.ml
+++ b/infer/src/backend/abs.ml
@@ -1127,12 +1127,10 @@ let check_junk ?original_prop pname tenv prop =
                 | _ -> None in
               let exn_retain_cycle cycle =
                 let cycle_dotty = get_retain_cycle_dotty original_prop cycle in
-                let desc = Errdesc.explain_retain_cycle
-                    (remove_opt original_prop) cycle (State.get_loc ()) cycle_dotty in
-                Exceptions.Retain_cycle
-                  (remove_opt original_prop, hpred, desc, __POS__) in
+                let desc = Errdesc.explain_retain_cycle cycle (State.get_loc ()) cycle_dotty in
+                Exceptions.Retain_cycle (hpred, desc, __POS__) in
               let exn_leak = Exceptions.Leak
-                  (fp_part, prop, hpred,
+                  (fp_part, hpred,
                    Errdesc.explain_leak tenv hpred prop alloc_attribute ml_bucket_opt,
                    !Absarray.array_abstraction_performed,
                    resource,
diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml
index 4e041c17a..f8eec7e18 100644
--- a/infer/src/backend/errdesc.ml
+++ b/infer/src/backend/errdesc.ml
@@ -1064,8 +1064,8 @@ let explain_return_expression_required loc typ =
   Localise.desc_return_expression_required typ_str loc
 
 (** Explain retain cycle value error *)
-let explain_retain_cycle prop cycle loc dotty_str =
-  Localise.desc_retain_cycle prop cycle loc dotty_str
+let explain_retain_cycle cycle loc dotty_str =
+  Localise.desc_retain_cycle cycle loc dotty_str
 
 (** Explain a tainted value error *)
 let explain_tainted_value_reaching_sensitive_function
diff --git a/infer/src/backend/errdesc.mli b/infer/src/backend/errdesc.mli
index 38f83c0a6..0a3238543 100644
--- a/infer/src/backend/errdesc.mli
+++ b/infer/src/backend/errdesc.mli
@@ -102,7 +102,7 @@ val explain_return_statement_missing : Location.t -> Localise.error_desc
 
 (** explain a retain cycle *)
 val explain_retain_cycle :
-  Prop.normal Prop.t -> ((Sil.strexp * Typ.t) * Ident.fieldname * Sil.strexp) list ->
+  ((Sil.strexp * Typ.t) * Ident.fieldname * Sil.strexp) list ->
   Location.t -> string option -> Localise.error_desc
 
 (** explain unary minus applied to unsigned expression *)
diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml
index a8449e902..a3b1122cf 100644
--- a/infer/src/backend/interproc.ml
+++ b/infer/src/backend/interproc.ml
@@ -457,8 +457,7 @@ let check_assignement_guard node =
               if (is_prune_exp e) && not ((node_contains_call node) && (is_frontend_tmp e)) then (
                 let desc = Errdesc.explain_condition_is_assignment l_node in
                 let exn = Exceptions.Condition_is_assignment (desc, __POS__) in
-                let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop pname) in
-                Reporting.log_warning pname ~loc:l_node ?pre:pre_opt exn
+                Reporting.log_warning pname ~loc:l_node exn
               )
               else ()
           | _ ->
@@ -508,8 +507,8 @@ let forward_tabulate tenv wl source =
      | None -> ());
     L.d_strln "SIL INSTR:";
     Cfg.Node.d_instrs ~sub_instrs: true (State.get_instr ()) curr_node; L.d_ln ();
-    Reporting.log_error ?pre:pre_opt curr_pname exn;
-    State.mark_instr_fail pre_opt exn;
+    Reporting.log_error curr_pname exn;
+    State.mark_instr_fail exn;
     handled_some_exception := true in
 
   while not (Worklist.is_empty wl) do
@@ -1044,8 +1043,7 @@ let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t) so
             let exn =
               Exceptions.Internal_error
                 (Localise.verbatim_desc "Leak_while_collecting_specs_after_footprint") in
-            let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop pname) in
-            Reporting.log_error pname ?pre:pre_opt exn;
+            Reporting.log_error pname exn;
             [] (* retuning no specs *) in
       specs, Specs.FOOTPRINT in
     let wl = path_set_create_worklist pdesc in
@@ -1205,7 +1203,7 @@ let report_runtime_exceptions tenv pdesc summary =
         pp_to_string (Prop.pp_prop pe_text) (Specs.Jprop.to_prop pre) in
       let exn_desc = Localise.java_unchecked_exn_desc pname runtime_exception pre_str in
       let exn = Exceptions.Java_runtime_exception (runtime_exception, pre_str, exn_desc) in
-      Reporting.log_error pname ~pre:(Specs.Jprop.to_prop pre) exn in
+      Reporting.log_error pname exn in
   IList.iter report exn_preconditions
 
 
@@ -1218,7 +1216,7 @@ let report_custom_errors tenv summary =
       let loc = summary.Specs.attributes.ProcAttributes.loc in
       let err_desc = Localise.desc_custom_error loc in
       let exn = Exceptions.Custom_error (custom_error, err_desc) in
-      Reporting.log_error pname ~pre:(Specs.Jprop.to_prop pre) exn in
+      Reporting.log_error pname exn in
   IList.iter report error_preconditions
 
 module SpecMap = Map.Make (struct
diff --git a/infer/src/backend/printer.ml b/infer/src/backend/printer.ml
index 3d94871db..c47845cc4 100644
--- a/infer/src/backend/printer.ml
+++ b/infer/src/backend/printer.ml
@@ -435,7 +435,7 @@ let write_proc_html source whole_seconds pdesc =
 (** Creare a hash table mapping line numbers to the set of errors occurring on that line *)
 let create_table_err_per_line err_log =
   let err_per_line = Hashtbl.create 17 in
-  let add_err _ loc _ _ _ err_name desc _ _ _ _ _ =
+  let add_err _ loc _ _ _ err_name desc _ _ _ _ =
     let err_str =
       Localise.to_string err_name ^
       " " ^
diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml
index 89b12c233..1e1b48c4e 100644
--- a/infer/src/backend/prop.ml
+++ b/infer/src/backend/prop.ml
@@ -99,7 +99,6 @@ end
 
 include Core
 
-exception Cannot_star of L.ml_loc
 
 (** {2 Basic Functions for Propositions} *)
 
@@ -2210,6 +2209,20 @@ let prop_rename_fav_with_existentials tenv (p : normal t) : normal t =
   (*L.d_strln "Prop after renaming:"; d_prop p'; L.d_strln "";*)
   Normalize.normalize tenv p'
 
+(** Removes seeds variables from a prop corresponding to captured variables in an objc block *)
+let remove_seed_captured_vars_block tenv captured_vars prop =
+  let is_captured pname vn = Mangled.equal pname vn in
+  let hpred_seed_captured =
+    function
+    | Sil.Hpointsto (Exp.Lvar pv, _, _) ->
+        let pname = Pvar.get_name pv in
+        (Pvar.is_seed pv) && (IList.mem is_captured pname captured_vars)
+    | _ -> false in
+  let sigma = prop.sigma in
+  let sigma' =
+    IList.filter (fun hpred  -> not (hpred_seed_captured hpred)) sigma in
+  Normalize.normalize tenv (set prop ~sigma:sigma')
+
 (** {2 Prop iterators} *)
 
 (** Iterator state over sigma. *)
diff --git a/infer/src/backend/prop.mli b/infer/src/backend/prop.mli
index d600173ea..f7a8970ee 100644
--- a/infer/src/backend/prop.mli
+++ b/infer/src/backend/prop.mli
@@ -40,7 +40,6 @@ type struct_init_mode =
   | No_init
   | Fld_init
 
-exception Cannot_star of Logging.ml_loc
 
 (** {2 Basic Functions for propositions} *)
 
@@ -311,6 +310,9 @@ val set : ?sub:Sil.subst -> ?pi:pi -> ?sigma:sigma -> ?pi_fp:pi -> ?sigma_fp:sig
 (** Rename free variables in a prop replacing them with existentially quantified vars *)
 val prop_rename_fav_with_existentials : Tenv.t -> normal t -> normal t
 
+(** Removes seeds variables from a prop corresponding to captured variables in an objc block *)
+val remove_seed_captured_vars_block: Tenv.t -> Mangled.t list -> normal t -> normal t
+
 (** {2 Prop iterators} *)
 
 (** Iterator over the sigma part. Each iterator has a current [hpred]. *)
diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml
index 5c3115df5..704324a46 100644
--- a/infer/src/backend/rearrange.ml
+++ b/infer/src/backend/rearrange.ml
@@ -62,16 +62,14 @@ let check_bad_index tenv pname p len index loc =
         let exn =
           Exceptions.Array_out_of_bounds_l1
             (Errdesc.explain_array_access tenv deref_str p loc, __POS__) in
-        let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop pname) in
-        Reporting.log_warning pname ?pre:pre_opt exn
+        Reporting.log_warning pname exn
       else if len_is_constant then
         let deref_str = Localise.deref_str_array_bound len_const_opt index_const_opt in
         let desc = Errdesc.explain_array_access tenv deref_str p loc in
         let exn = if index_has_bounds ()
           then Exceptions.Array_out_of_bounds_l2 (desc, __POS__)
           else Exceptions.Array_out_of_bounds_l3 (desc, __POS__) in
-        let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop pname) in
-        Reporting.log_warning pname ?pre:pre_opt exn
+        Reporting.log_warning pname exn
     end
 
 (** Perform bounds checking *)
@@ -1065,8 +1063,7 @@ let check_type_size tenv pname prop texp off typ_from_instr =
         let exn =
           Exceptions.Pointer_size_mismatch (
             Errdesc.explain_dereference tenv deref_str prop loc, __POS__) in
-        let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop pname) in
-        Reporting.log_warning pname ?pre:pre_opt exn
+        Reporting.log_warning pname exn
       end
   | None ->
       L.d_str "texp: "; Sil.d_texp_full texp; L.d_ln ()
diff --git a/infer/src/backend/reporting.ml b/infer/src/backend/reporting.ml
index a62444a76..d73734c63 100644
--- a/infer/src/backend/reporting.ml
+++ b/infer/src/backend/reporting.ml
@@ -16,7 +16,6 @@ type log_t =
   ?node_id: (int * int) ->
   ?session: int ->
   ?ltr: Errlog.loc_trace ->
-  ?pre: Prop.normal Prop.t ->
   exn ->
   unit
 
@@ -24,7 +23,7 @@ type log_issue = Procname.t -> log_t
 
 type log_issue_from_errlog = Errlog.t -> log_t
 
-let log_issue_from_errlog err_kind err_log ?loc ?node_id ?session ?ltr ?pre exn =
+let log_issue_from_errlog err_kind err_log ?loc ?node_id ?session ?ltr exn =
   let loc = match loc with
     | None -> State.get_loc ()
     | Some loc -> loc in
@@ -42,7 +41,7 @@ let log_issue_from_errlog err_kind err_log ?loc ?node_id ?session ?ltr ?pre exn
     | _ -> let err_name, _, _, _, _, _, _ =  Exceptions.recognize_exception exn in
         (Localise.to_string err_name) in
   if (Inferconfig.is_checker_enabled err_name) then
-    Errlog.log_issue err_kind err_log loc node_id session ltr pre exn
+    Errlog.log_issue err_kind err_log loc node_id session ltr exn
 
 
 let log_issue
@@ -52,7 +51,6 @@ let log_issue
     ?node_id
     ?session
     ?ltr
-    ?pre
     exn =
   let should_suppress_warnings summary =
     !Config.curr_language = Config.Java &&
@@ -64,7 +62,7 @@ let log_issue
   | Some summary when should_suppress_warnings summary -> ()
   | Some summary ->
       let err_log = summary.Specs.attributes.ProcAttributes.err_log in
-      log_issue_from_errlog err_kind err_log ?loc ?node_id ?session ?ltr ?pre exn
+      log_issue_from_errlog err_kind err_log ?loc ?node_id ?session ?ltr exn
   | None -> ()
 
 let log_error = log_issue Exceptions.Kerror
diff --git a/infer/src/backend/reporting.mli b/infer/src/backend/reporting.mli
index 76247a031..aca3bb07b 100644
--- a/infer/src/backend/reporting.mli
+++ b/infer/src/backend/reporting.mli
@@ -16,7 +16,6 @@ type log_t =
   ?node_id: (int * int) ->
   ?session: int ->
   ?ltr: Errlog.loc_trace ->
-  ?pre: Prop.normal Prop.t ->
   exn ->
   unit
 
diff --git a/infer/src/backend/state.ml b/infer/src/backend/state.ml
index 7d1a3de40..7bd428ece 100644
--- a/infer/src/backend/state.ml
+++ b/infer/src/backend/state.ml
@@ -24,8 +24,8 @@ type failure_stats = {
   mutable node_fail: int; (* number of node failures (i.e. at least one instruction failure) *)
   mutable node_ok: int; (* number of node successes (i.e. no instruction failures) *)
   mutable first_failure :
-    (Location.t * (int * int) * int * Errlog.loc_trace *
-     (Prop.normal Prop.t) option * exn) option (* exception at the first failure *)
+    (Location.t * (int * int) * int * Errlog.loc_trace * exn) option
+    (* exception at the first failure *)
 }
 
 module NodeHash = Cfg.NodeHash
@@ -296,14 +296,14 @@ let mark_instr_ok () =
   let fs = get_failure_stats (get_node ()) in
   fs.instr_ok <- fs.instr_ok + 1
 
-let mark_instr_fail pre_opt exn =
+let mark_instr_fail exn =
   let loc = get_loc () in
   let key = (get_node_id_key () :> int * int) in
   let session = get_session () in
   let loc_trace = get_loc_trace () in
   let fs = get_failure_stats (get_node ()) in
   if fs.first_failure = None then
-    fs.first_failure <- Some (loc, key, (session :> int), loc_trace, pre_opt, exn);
+    fs.first_failure <- Some (loc, key, (session :> int), loc_trace, exn);
   fs.instr_fail <- fs.instr_fail + 1
 
 type log_issue =
@@ -312,7 +312,6 @@ type log_issue =
   ?node_id: (int * int) ->
   ?session: int ->
   ?ltr: Errlog.loc_trace ->
-  ?pre: Prop.normal Prop.t ->
   exn ->
   unit
 
@@ -320,12 +319,11 @@ let process_execution_failures (log_issue : log_issue) pname =
   let do_failure _ fs =
     (* L.err "Node:%a node_ok:%d node_fail:%d@." Cfg.Node.pp node fs.node_ok fs.node_fail; *)
     match fs.node_ok, fs.first_failure with
-    | 0, Some (loc, key, _, loc_trace, pre_opt, exn) ->
+    | 0, Some (loc, key, _, loc_trace, exn) ->
         let ex_name, _, ml_loc_opt, _, _, _, _ = Exceptions.recognize_exception exn in
         let desc' = Localise.verbatim_desc ("exception: " ^ Localise.to_string ex_name) in
         let exn' = Exceptions.Analysis_stops (desc', ml_loc_opt) in
-        log_issue
-          pname ~loc ~node_id:key ~ltr:loc_trace ?pre:pre_opt exn'
+        log_issue pname ~loc ~node_id:key ~ltr:loc_trace exn'
     | _ -> () in
   NodeHash.iter do_failure !gs.failure_map
 
diff --git a/infer/src/backend/state.mli b/infer/src/backend/state.mli
index bdd582afb..8a571f935 100644
--- a/infer/src/backend/state.mli
+++ b/infer/src/backend/state.mli
@@ -74,7 +74,7 @@ val mark_execution_end : Cfg.Node.t -> unit
 val mark_execution_start : Cfg.Node.t -> unit
 
 (** Mark that the execution of the current instruction failed *)
-val mark_instr_fail : (Prop.normal Prop.t) option -> exn -> unit
+val mark_instr_fail : exn -> unit
 
 (** Mark that the execution of the current instruction was OK *)
 val mark_instr_ok : unit -> unit
@@ -90,7 +90,6 @@ type log_issue =
   ?node_id: (int * int) ->
   ?session: int ->
   ?ltr: Errlog.loc_trace ->
-  ?pre: Prop.normal Prop.t ->
   exn ->
   unit
 
diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml
index 16ef734ac..e4bcb13de 100644
--- a/infer/src/backend/symExec.ml
+++ b/infer/src/backend/symExec.ml
@@ -61,7 +61,7 @@ let check_block_retain_cycle tenv caller_pname prop block_nullified =
         fst (IList.split attributes.ProcAttributes.captured)
     | None ->
         [] in
-  let prop' = Cfg.remove_seed_captured_vars_block tenv block_captured prop in
+  let prop' = Prop.remove_seed_captured_vars_block tenv block_captured prop in
   let prop'' = Prop.prop_rename_fav_with_existentials tenv prop' in
   let _ : Prop.normal Prop.t = Abs.abstract_junk ~original_prop: prop caller_pname tenv prop'' in
   ()
@@ -113,8 +113,7 @@ let rec apply_offlist
             let deref_str = Localise.deref_str_uninitialized alloc_attribute_opt in
             let err_desc = Errdesc.explain_memory_access tenv deref_str p (State.get_loc ()) in
             let exn = (Exceptions.Uninitialized_value (err_desc, __POS__)) in
-            let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop pname) in
-            Reporting.log_warning pname ?pre:pre_opt exn;
+            Reporting.log_warning pname exn;
             Sil.update_inst inst_curr inst
         | Sil.Ilookup -> (* a lookup does not change an inst unless it is inst_initial *)
             lookup_inst := Some inst_curr;
@@ -374,8 +373,7 @@ let check_inherently_dangerous_function caller_pname callee_pname =
     let exn =
       Exceptions.Inherently_dangerous_function
         (Localise.desc_inherently_dangerous_function callee_pname) in
-    let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop caller_pname) in
-    Reporting.log_warning caller_pname ?pre:pre_opt exn
+    Reporting.log_warning caller_pname exn
 
 let proc_is_defined proc_name =
   match AttributesTable.load_attributes proc_name with
@@ -417,16 +415,14 @@ let check_arith_norm_exp tenv pname exp prop =
   | Some (Attribute.Div0 div), prop' ->
       let desc = Errdesc.explain_divide_by_zero tenv div (State.get_node ()) (State.get_loc ()) in
       let exn = Exceptions.Divide_by_zero (desc, __POS__) in
-      let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop pname) in
-      Reporting.log_warning pname ?pre:pre_opt exn;
+      Reporting.log_warning pname exn;
       Prop.exp_normalize_prop tenv prop exp, prop'
   | Some (Attribute.UminusUnsigned (e, typ)), prop' ->
       let desc =
         Errdesc.explain_unary_minus_applied_to_unsigned_expression tenv
           e typ (State.get_node ()) (State.get_loc ()) in
       let exn = Exceptions.Unary_minus_applied_to_unsigned_expression (desc, __POS__) in
-      let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop pname) in
-      Reporting.log_warning pname ?pre:pre_opt exn;
+      Reporting.log_warning pname exn;
       Prop.exp_normalize_prop tenv prop exp, prop'
   | None, prop' -> Prop.exp_normalize_prop tenv prop exp, prop'
 
@@ -463,8 +459,7 @@ let check_already_dereferenced tenv pname cond prop =
           (Exp.Var id) (State.get_node ()) n (State.get_loc ()) in
       let exn =
         (Exceptions.Null_test_after_dereference (desc, __POS__)) in
-      let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop pname) in
-      Reporting.log_warning pname ?pre:pre_opt exn
+      Reporting.log_warning pname exn
   | None -> ()
 
 (** Check whether symbolic execution de-allocated a stack variable or a constant string,
@@ -1057,8 +1052,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
               let desc = Errdesc.explain_condition_always_true_false tenv i cond node loc in
               let exn =
                 Exceptions.Condition_always_true_false (desc, not (IntLit.iszero i), __POS__) in
-              let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop current_pname) in
-              Reporting.log_warning current_pname ?pre:pre_opt exn
+              Reporting.log_warning current_pname exn
           | _ -> () in
       if not Config.report_runtime_exceptions then
         check_already_dereferenced tenv current_pname cond prop__;
@@ -1559,8 +1553,7 @@ and proc_call summary {Builtin.pdesc; tenv; prop_= pre; path; ret_id; args= actu
     && Specs.get_flag callee_pname proc_flag_ignore_return = None then
       let err_desc = Localise.desc_return_value_ignored callee_pname loc in
       let exn = (Exceptions.Return_value_ignored (err_desc, __POS__)) in
-      let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop caller_pname) in
-      Reporting.log_warning caller_pname ?pre:pre_opt exn in
+      Reporting.log_warning caller_pname exn in
   check_inherently_dangerous_function caller_pname callee_pname;
   begin
     let formal_types = IList.map (fun (_, typ) -> typ) (Specs.get_formals summary) in
diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml
index b16490163..49d5ed8ee 100644
--- a/infer/src/backend/tabulation.ml
+++ b/infer/src/backend/tabulation.ml
@@ -372,8 +372,7 @@ let check_path_errors_in_post tenv caller_pname post post_path =
             else current_path, None (* position not found, only use the path up to the callee *) in
           State.set_path new_path path_pos_opt;
           let exn = Exceptions.Divide_by_zero (desc, __POS__) in
-          let pre_opt = State.get_normalized_pre (fun _ p -> p) (* Abs.abstract_no_symop *) in
-          Reporting.log_warning caller_pname ?pre:pre_opt exn
+          Reporting.log_warning caller_pname exn
     | _ -> () in
   IList.iter check_attr (Attribute.get_all post)
 
@@ -513,7 +512,7 @@ let sigma_star_fld tenv (sigma1 : Sil.hpred list) (sigma2 : Sil.hpred list) : Si
     L.d_str "cannot star ";
     Prop.d_sigma sigma1; L.d_str " and "; Prop.d_sigma sigma2;
     L.d_ln ();
-    raise (Prop.Cannot_star __POS__)
+    raise (Exceptions.Cannot_star __POS__)
 
 let hpred_typing_lhs_compare hpred1 (e2, _) = match hpred1 with
   | Sil.Hpointsto(e1, _, _) -> Exp.compare e1 e2
@@ -546,7 +545,7 @@ let sigma_star_typ
     L.d_str "cannot star ";
     Prop.d_sigma sigma1; L.d_str " and "; Prover.d_typings typings2;
     L.d_ln ();
-    raise (Prop.Cannot_star __POS__)
+    raise (Exceptions.Cannot_star __POS__)
 
 (** [prop_footprint_add_pi_sigma_starfld_sigma prop pi sigma missing_fld]
     extends the footprint of [prop] with [pi,sigma]
diff --git a/infer/src/backend/Process.ml b/infer/src/base/Process.ml
similarity index 100%
rename from infer/src/backend/Process.ml
rename to infer/src/base/Process.ml
diff --git a/infer/src/backend/Process.mli b/infer/src/base/Process.mli
similarity index 100%
rename from infer/src/backend/Process.mli
rename to infer/src/base/Process.mli
diff --git a/infer/src/backend/StatisticsToolbox.re b/infer/src/base/StatisticsToolbox.re
similarity index 100%
rename from infer/src/backend/StatisticsToolbox.re
rename to infer/src/base/StatisticsToolbox.re
diff --git a/infer/src/backend/StatisticsToolbox.rei b/infer/src/base/StatisticsToolbox.rei
similarity index 100%
rename from infer/src/backend/StatisticsToolbox.rei
rename to infer/src/base/StatisticsToolbox.rei
diff --git a/infer/src/backend/SymOp.ml b/infer/src/base/SymOp.ml
similarity index 100%
rename from infer/src/backend/SymOp.ml
rename to infer/src/base/SymOp.ml
diff --git a/infer/src/backend/SymOp.mli b/infer/src/base/SymOp.mli
similarity index 100%
rename from infer/src/backend/SymOp.mli
rename to infer/src/base/SymOp.mli
diff --git a/infer/src/harness/stacktrace.ml b/infer/src/checkers/Stacktrace.ml
similarity index 100%
rename from infer/src/harness/stacktrace.ml
rename to infer/src/checkers/Stacktrace.ml
diff --git a/infer/src/harness/stacktrace.mli b/infer/src/checkers/Stacktrace.mli
similarity index 100%
rename from infer/src/harness/stacktrace.mli
rename to infer/src/checkers/Stacktrace.mli