diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml
index 51db15245..60db49ec5 100644
--- a/infer/src/pulse/Pulse.ml
+++ b/infer/src/pulse/Pulse.ml
@@ -8,6 +8,18 @@ open! IStd
 module F = Format
 module L = Logging
 open Result.Monad_infix
+module AbstractAddress = PulseDomain.AbstractAddress
+
+include (* ocaml ignores the warning suppression at toplevel, hence the [include struct ... end] trick *)
+  struct
+  [@@@warning "-60"]
+
+  (** Do not use {!PulseDomain} directly as it could result in bypassing abduction mechanisms in
+     {!PulseOperations} and {!PulseAbductiveDomain} that take care of propagating facts to the
+     precondition. *)
+  module PulseDomain = struct end
+  [@@deprecated "Use PulseAbductiveDomain or PulseOperations instead."]
+end
 
 let report summary diagnostic =
   let open PulseDiagnostic in
@@ -27,7 +39,7 @@ let check_error summary = function
 
 module PulseTransferFunctions = struct
   module CFG = ProcCfg.Exceptional
-  module Domain = PulseDomain
+  module Domain = PulseAbductiveDomain
 
   type extras = Summary.t
 
@@ -137,8 +149,7 @@ module PulseTransferFunctions = struct
         model call_loc ~ret ~actuals astate
 
 
-  let exec_instr (astate : PulseDomain.t) {ProcData.extras= summary} _cfg_node (instr : HilInstr.t)
-      =
+  let exec_instr (astate : Domain.t) {ProcData.extras= summary} _cfg_node (instr : HilInstr.t) =
     match instr with
     | Assign (lhs_access, rhs_exp, loc) ->
         let post = exec_assign summary lhs_access rhs_exp loc astate |> check_error summary in
@@ -190,10 +201,10 @@ module DisjunctiveAnalyzer =
 
 let checker {Callbacks.proc_desc; tenv; summary} =
   let proc_data = ProcData.make proc_desc tenv summary in
-  PulseDomain.AbstractAddress.init () ;
+  AbstractAddress.init () ;
   ( try
       ignore
         (DisjunctiveAnalyzer.compute_post proc_data
-           ~initial:(DisjunctiveTransferFunctions.Disjuncts.singleton PulseDomain.initial))
+           ~initial:(DisjunctiveTransferFunctions.Disjuncts.singleton PulseAbductiveDomain.empty))
     with AbstractDomain.Stop_analysis -> () ) ;
   summary
diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml
new file mode 100644
index 000000000..7637a0c2f
--- /dev/null
+++ b/infer/src/pulse/PulseAbductiveDomain.ml
@@ -0,0 +1,237 @@
+(*
+ * Copyright (c) 2019-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+open! IStd
+module F = Format
+module AbstractAddress = PulseDomain.AbstractAddress
+module Attributes = PulseDomain.Attributes
+module BaseStack = PulseDomain.Stack
+module BaseMemory = PulseDomain.Memory
+
+(** signature common to the "normal" [Domain], representing the post at the current program point,
+    and the inverted [InvertedDomain], representing the inferred pre-condition*)
+module type BaseDomain = sig
+  (* private because the lattice is not the same for preconditions and postconditions so we don't
+     want to confuse them *)
+  type t = private PulseDomain.t [@@deriving compare]
+
+  val empty : t
+
+  val make : BaseStack.t -> BaseMemory.t -> t
+
+  val update : ?stack:BaseStack.t -> ?heap:BaseMemory.t -> t -> t
+
+  include AbstractDomain.NoJoin with type t := t
+end
+
+(* just to expose the [heap] and [stack] record field names without having to type
+   [PulseDomain.heap] *)
+type base_domain = PulseDomain.t = {heap: BaseMemory.t; stack: BaseStack.t}
+
+(** operations common to [Domain] and [InvertedDomain], see also the [BaseDomain] signature *)
+module BaseDomainCommon = struct
+  let make stack heap = {stack; heap}
+
+  let update ?stack ?heap foot =
+    let new_stack, new_heap =
+      (Option.value ~default:foot.stack stack, Option.value ~default:foot.heap heap)
+    in
+    if phys_equal new_stack foot.stack && phys_equal new_heap foot.heap then foot
+    else {stack= new_stack; heap= new_heap}
+end
+
+(** represents the post abstract state at each program point *)
+module Domain : BaseDomain = struct
+  include BaseDomainCommon
+  include PulseDomain
+end
+
+(** represents the inferred pre-condition at each program point, biabduction style *)
+module InvertedDomain : BaseDomain = struct
+  include BaseDomainCommon
+
+  type t = PulseDomain.t [@@deriving compare]
+
+  let empty = PulseDomain.empty
+
+  let pp = PulseDomain.pp
+
+  (** inverted lattice *)
+  let ( <= ) ~lhs ~rhs = PulseDomain.( <= ) ~rhs:lhs ~lhs:rhs
+end
+
+(** biabduction-style pre/post state *)
+type t =
+  { post: Domain.t  (** state at the current program point*)
+  ; pre: InvertedDomain.t  (** inferred pre at the current program point *) }
+[@@deriving compare]
+
+let pp f {post; pre} = F.fprintf f "@[<v>%a@;[%a]@]" Domain.pp post InvertedDomain.pp pre
+
+let ( <= ) ~lhs ~rhs =
+  match
+    PulseDomain.isograph_map PulseDomain.empty_mapping
+      ~lhs:(rhs.pre :> PulseDomain.t)
+      ~rhs:(lhs.pre :> PulseDomain.t)
+  with
+  | NotIsomorphic ->
+      false
+  | IsomorphicUpTo foot_mapping ->
+      PulseDomain.is_isograph foot_mapping
+        ~lhs:(lhs.post :> PulseDomain.t)
+        ~rhs:(rhs.post :> PulseDomain.t)
+
+
+module Stack = struct
+  let is_abducible _var =
+    (* TODO: need to keep only formals + return variable + globals in the pre *) true
+
+
+  (** [astate] with [astate.post.stack = f astate.post.stack] *)
+  let map_post_stack ~f astate =
+    let new_post = Domain.update astate.post ~stack:(f (astate.post :> base_domain).stack) in
+    if phys_equal new_post astate.post then astate else {astate with post= new_post}
+
+
+  let materialize var astate =
+    match BaseStack.find_opt var (astate.post :> base_domain).stack with
+    | Some addr_loc_opt ->
+        (astate, addr_loc_opt)
+    | None ->
+        let addr_loc_opt' = (AbstractAddress.mk_fresh (), None) in
+        let post_stack = BaseStack.add var addr_loc_opt' (astate.post :> base_domain).stack in
+        let pre =
+          if is_abducible var then
+            let foot_stack = BaseStack.add var addr_loc_opt' (astate.pre :> base_domain).stack in
+            let foot_heap =
+              BaseMemory.register_address (fst addr_loc_opt') (astate.pre :> base_domain).heap
+            in
+            InvertedDomain.make foot_stack foot_heap
+          else astate.pre
+        in
+        ({post= Domain.update astate.post ~stack:post_stack; pre}, addr_loc_opt')
+
+
+  let add var addr_loc_opt astate =
+    map_post_stack astate ~f:(fun stack -> BaseStack.add var addr_loc_opt stack)
+
+
+  let remove_vars vars astate =
+    map_post_stack astate ~f:(fun stack ->
+        BaseStack.filter (fun var _ -> not (List.mem ~equal:Var.equal vars var)) stack )
+
+
+  let fold f astate accum = BaseStack.fold f (astate.post :> base_domain).stack accum
+
+  let find_opt var astate = BaseStack.find_opt var (astate.post :> base_domain).stack
+end
+
+module Memory = struct
+  open Result.Monad_infix
+  module Access = BaseMemory.Access
+
+  (** [astate] with [astate.post.heap = f astate.post.heap] *)
+  let map_post_heap ~f astate =
+    let new_post = Domain.update astate.post ~heap:(f (astate.post :> base_domain).heap) in
+    if phys_equal new_post astate.post then astate else {astate with post= new_post}
+
+
+  (** if [address] is in [pre] and it should be valid then that fact goes in the precondition *)
+  let record_must_be_valid actor address (pre : InvertedDomain.t) =
+    if BaseMemory.mem_edges address (pre :> base_domain).heap then
+      InvertedDomain.update pre
+        ~heap:
+          (BaseMemory.add_attributes address
+             (Attributes.singleton (MustBeValid actor))
+             (pre :> base_domain).heap)
+    else pre
+
+
+  let check_valid actor addr ({post; pre} as astate) =
+    BaseMemory.check_valid addr (post :> base_domain).heap
+    >>| fun () ->
+    let new_pre = record_must_be_valid actor addr pre in
+    if phys_equal new_pre pre then astate else {astate with pre= new_pre}
+
+
+  let add_edge addr access new_addr_trace astate =
+    map_post_heap astate ~f:(fun heap -> BaseMemory.add_edge addr access new_addr_trace heap)
+
+
+  let add_edge_and_back_edge addr access new_addr_trace astate =
+    map_post_heap astate ~f:(fun heap ->
+        BaseMemory.add_edge_and_back_edge addr access new_addr_trace heap )
+
+
+  let materialize_edge addr access astate =
+    match BaseMemory.find_edge_opt addr access (astate.post :> base_domain).heap with
+    | Some addr_trace' ->
+        (astate, addr_trace')
+    | None ->
+        let addr_trace' = (AbstractAddress.mk_fresh (), []) in
+        let post_heap =
+          BaseMemory.add_edge_and_back_edge addr access addr_trace'
+            (astate.post :> base_domain).heap
+        in
+        let foot_heap =
+          if BaseMemory.mem_edges addr (astate.pre :> base_domain).heap then
+            BaseMemory.add_edge_and_back_edge addr access addr_trace'
+              (astate.pre :> base_domain).heap
+            |> BaseMemory.register_address (fst addr_trace')
+          else (astate.pre :> base_domain).heap
+        in
+        ( { post= Domain.update astate.post ~heap:post_heap
+          ; pre= InvertedDomain.update astate.pre ~heap:foot_heap }
+        , addr_trace' )
+
+
+  let invalidate address actor astate =
+    map_post_heap astate ~f:(fun heap -> BaseMemory.invalidate address actor heap)
+
+
+  let add_attributes address attributes astate =
+    map_post_heap astate ~f:(fun heap -> BaseMemory.add_attributes address attributes heap)
+
+
+  let std_vector_reserve addr astate =
+    map_post_heap astate ~f:(fun heap -> BaseMemory.std_vector_reserve addr heap)
+
+
+  let is_std_vector_reserved addr astate =
+    BaseMemory.is_std_vector_reserved addr (astate.post :> base_domain).heap
+
+
+  let find_opt address astate = BaseMemory.find_opt address (astate.post :> base_domain).heap
+
+  let set_cell addr cell astate =
+    map_post_heap astate ~f:(fun heap -> BaseMemory.set_cell addr cell heap)
+
+
+  module Edges = BaseMemory.Edges
+end
+
+let empty = {post= Domain.empty; pre= InvertedDomain.empty}
+
+let discard_unreachable ({pre; post} as astate) =
+  let pre_addresses = PulseDomain.visit (pre :> PulseDomain.t) in
+  let pre_old_heap = (pre :> PulseDomain.t).heap in
+  let pre_new_heap =
+    PulseDomain.Memory.filter
+      (fun address -> PulseDomain.AbstractAddressSet.mem address pre_addresses)
+      pre_old_heap
+  in
+  let post_addresses = PulseDomain.visit (post :> PulseDomain.t) in
+  let all_addresses = PulseDomain.AbstractAddressSet.union pre_addresses post_addresses in
+  let post_old_heap = (post :> PulseDomain.t).heap in
+  let post_new_heap =
+    PulseDomain.Memory.filter
+      (fun address -> PulseDomain.AbstractAddressSet.mem address all_addresses)
+      post_old_heap
+  in
+  if phys_equal pre_new_heap pre_old_heap && phys_equal post_new_heap post_old_heap then astate
+  else
+    { pre= InvertedDomain.make (pre :> PulseDomain.t).stack pre_new_heap
+    ; post= Domain.make (post :> PulseDomain.t).stack post_new_heap }
diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli
new file mode 100644
index 000000000..8f1a33a0b
--- /dev/null
+++ b/infer/src/pulse/PulseAbductiveDomain.mli
@@ -0,0 +1,66 @@
+(*
+ * Copyright (c) 2019-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+open! IStd
+module AbstractAddress = PulseDomain.AbstractAddress
+module Attributes = PulseDomain.Attributes
+
+(* layer on top of {!PulseDomain} to propagate operations on the current state to the pre-condition
+   when necessary
+
+   The abstract type [t] is a pre/post pair in the style of biabduction.
+*)
+
+include AbstractDomain.NoJoin
+
+val empty : t
+
+(** stack operations like {!PulseDomain.Stack} but that also take care of propagating facts to the
+    precondition *)
+module Stack : sig
+  val add : Var.t -> PulseDomain.Stack.value -> t -> t
+
+  val remove_vars : Var.t list -> t -> t
+
+  val fold : (Var.t -> PulseDomain.Stack.value -> 'a -> 'a) -> t -> 'a -> 'a
+
+  val find_opt : Var.t -> t -> PulseDomain.Stack.value option
+
+  val materialize : Var.t -> t -> t * PulseDomain.Stack.value
+end
+
+(** stack operations like {!PulseDomain.Heap} but that also take care of propagating facts to the
+    precondition *)
+module Memory : sig
+  module Access = PulseDomain.Memory.Access
+  module Edges = PulseDomain.Memory.Edges
+
+  val add_attributes : AbstractAddress.t -> Attributes.t -> t -> t
+
+  val add_edge : AbstractAddress.t -> Access.t -> PulseDomain.AddrTracePair.t -> t -> t
+
+  val add_edge_and_back_edge :
+    AbstractAddress.t -> Access.t -> PulseDomain.AddrTracePair.t -> t -> t
+
+  val check_valid :
+    PulseDiagnostic.actor -> AbstractAddress.t -> t -> (t, PulseInvalidation.t) result
+
+  val find_opt : AbstractAddress.t -> t -> PulseDomain.Memory.cell option
+
+  val set_cell : AbstractAddress.t -> PulseDomain.Memory.cell -> t -> t
+
+  val invalidate : AbstractAddress.t -> PulseInvalidation.t -> t -> t
+
+  val is_std_vector_reserved : AbstractAddress.t -> t -> bool
+
+  val std_vector_reserve : AbstractAddress.t -> t -> t
+
+  val materialize_edge : AbstractAddress.t -> Access.t -> t -> t * PulseDomain.AddrTracePair.t
+end
+
+val discard_unreachable : t -> t
+(** garbage collect unreachable addresses in the state to make it smaller, just for convenience and
+   keep its size down *)
diff --git a/infer/src/pulse/PulseDomain.ml b/infer/src/pulse/PulseDomain.ml
index 567985bf3..759ba4da7 100644
--- a/infer/src/pulse/PulseDomain.ml
+++ b/infer/src/pulse/PulseDomain.ml
@@ -20,6 +20,7 @@ module Attribute = struct
   type t =
     (* DO NOT MOVE, see toplevel comment *)
     | Invalid of Invalidation.t
+    | MustBeValid of PulseDiagnostic.actor
     | AddressOfCppTemporary of Var.t * Location.t option
     | Closure of Typ.Procname.t
     | StdVectorReserve
@@ -28,6 +29,9 @@ module Attribute = struct
   let pp f = function
     | Invalid invalidation ->
         Invalidation.pp f invalidation
+    | MustBeValid actor ->
+        F.fprintf f "MustBeValid (read by %a @ %a)" HilExp.AccessExpression.pp actor.access_expr
+          Location.pp actor.location
     | AddressOfCppTemporary (var, location_opt) ->
         F.fprintf f "&%a (%a)" Var.pp var (Pp.option Location.pp) location_opt
     | Closure pname ->
@@ -86,6 +90,8 @@ end = struct
   let set_state counter = next_fresh := counter
 end
 
+module AbstractAddressSet = PrettyPrintable.MakePPSet (AbstractAddress)
+
 (* {3 Heap domain } *)
 
 module AddrTracePair = struct
@@ -120,8 +126,12 @@ module Memory : sig
 
   val set_cell : AbstractAddress.t -> cell -> t -> t
 
+  val mem_edges : AbstractAddress.t -> t -> bool
+
   val pp : F.formatter -> t -> unit
 
+  val register_address : AbstractAddress.t -> t -> t
+
   val add_edge : AbstractAddress.t -> Access.t -> AddrTracePair.t -> t -> t
 
   val add_edge_and_back_edge : AbstractAddress.t -> Access.t -> AddrTracePair.t -> t -> t
@@ -162,6 +172,11 @@ end = struct
       ~snd:(Graph.pp ~pp_value:Attributes.pp)
 
 
+  let register_address addr memory =
+    if Graph.mem addr (fst memory) then memory
+    else (Graph.add addr Edges.empty (fst memory), snd memory)
+
+
   (* {3 Helper functions to traverse the two maps at once } *)
 
   let add_edge addr_src access value memory =
@@ -248,6 +263,9 @@ end = struct
     let heap = Graph.filter (fun address _ -> f address) (fst memory) in
     let attrs = Graph.filter (fun address _ -> f address) (snd memory) in
     if phys_equal heap (fst memory) && phys_equal attrs (snd memory) then memory else (heap, attrs)
+
+
+  let mem_edges addr memory = Graph.mem addr (fst memory)
 end
 
 (** Stacks: map addresses of variables to values and initialisation location. *)
@@ -285,7 +303,7 @@ end
 
 type t = {heap: Memory.t; stack: Stack.t} [@@deriving compare]
 
-let initial =
+let empty =
   { heap=
       Memory.empty
       (* TODO: we could record that 0 is an invalid address at this point but this makes the
@@ -447,16 +465,14 @@ let pp fmt {heap; stack} =
 
 
 module GraphGC : sig
-  val minimize : t -> t
+  val visit : t -> AbstractAddressSet.t
   (** compute the set of abstract addresses that are "used" in the abstract state, i.e. reachable
-     from the stack variables, then removes all the unused addresses from the heap *)
+     from the stack variables *)
 end = struct
-  module AddressSet = PrettyPrintable.MakePPSet (AbstractAddress)
-
   let visit address visited =
-    if AddressSet.mem address visited then `AlreadyVisited
+    if AbstractAddressSet.mem address visited then `AlreadyVisited
     else
-      let visited = AddressSet.add address visited in
+      let visited = AbstractAddressSet.add address visited in
       `NotAlreadyVisited visited
 
 
@@ -478,17 +494,11 @@ end = struct
       edges visited
 
 
-  let visit_stack astate visited =
+  let visit astate =
     Stack.fold
       (fun _var (address, _loc) visited -> visit_address astate address visited)
-      astate.stack visited
-
-
-  let minimize astate =
-    let visited = visit_stack astate AddressSet.empty in
-    let heap = Memory.filter (fun address -> AddressSet.mem address visited) astate.heap in
-    if phys_equal heap astate.heap then astate else {astate with heap}
+      astate.stack AbstractAddressSet.empty
 end
 
-include GraphGC
 include GraphComparison
+include GraphGC
diff --git a/infer/src/pulse/PulseDomain.mli b/infer/src/pulse/PulseDomain.mli
index 43816889a..bc9317ef7 100644
--- a/infer/src/pulse/PulseDomain.mli
+++ b/infer/src/pulse/PulseDomain.mli
@@ -11,12 +11,15 @@ module F = Format
 module Attribute : sig
   type t =
     | Invalid of PulseInvalidation.t
+    | MustBeValid of PulseDiagnostic.actor
     | AddressOfCppTemporary of Var.t * Location.t option
     | Closure of Typ.Procname.t
     | StdVectorReserve
   [@@deriving compare]
 end
 
+module Attributes : PrettyPrintable.PPSet with type elt = Attribute.t
+
 module AbstractAddress : sig
   type t = private int [@@deriving compare]
 
@@ -35,6 +38,8 @@ module AbstractAddress : sig
   val set_state : state -> unit
 end
 
+module AbstractAddressSet : PrettyPrintable.PPSet with type elt = AbstractAddress.t
+
 module Stack : sig
   include
     PrettyPrintable.MonoMap
@@ -50,8 +55,6 @@ module AddrTracePair : sig
   type t = AbstractAddress.t * PulseTrace.t [@@deriving compare]
 end
 
-module Attributes : PrettyPrintable.PPSet with type elt = Attribute.t
-
 module Memory : sig
   module Access :
     PrettyPrintable.PrintableOrderedType with type t = AbstractAddress.t HilExp.Access.t
@@ -64,10 +67,16 @@ module Memory : sig
 
   type t [@@deriving compare]
 
+  val filter : (AbstractAddress.t -> bool) -> t -> t
+
   val find_opt : AbstractAddress.t -> t -> cell option
 
   val set_cell : AbstractAddress.t -> cell -> t -> t
 
+  val mem_edges : AbstractAddress.t -> t -> bool
+
+  val register_address : AbstractAddress.t -> t -> t
+
   val add_edge : AbstractAddress.t -> Access.t -> AddrTracePair.t -> t -> t
 
   val add_edge_and_back_edge : AbstractAddress.t -> Access.t -> AddrTracePair.t -> t -> t
@@ -87,8 +96,22 @@ end
 
 type t = {heap: Memory.t; stack: Stack.t} [@@deriving compare]
 
-val initial : t
+val empty : t
 
 include AbstractDomain.NoJoin with type t := t
 
-val minimize : t -> t
+val visit : t -> AbstractAddressSet.t
+(** compute the set of abstract addresses that are "used" in the abstract state, i.e. reachable
+     from the stack variables *)
+
+type mapping
+
+val empty_mapping : mapping
+
+type isograph_relation =
+  | NotIsomorphic  (** no mapping was found that can make LHS the same as the RHS *)
+  | IsomorphicUpTo of mapping  (** [mapping(lhs)] is isomorphic to [rhs] *)
+
+val isograph_map : lhs:t -> rhs:t -> mapping -> isograph_relation
+
+val is_isograph : lhs:t -> rhs:t -> mapping -> bool
diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml
index 3c1bfd569..bb7555da2 100644
--- a/infer/src/pulse/PulseModels.ml
+++ b/infer/src/pulse/PulseModels.ml
@@ -11,13 +11,13 @@ type exec_fun =
      Location.t
   -> ret:Var.t * Typ.t
   -> actuals:HilExp.t list
-  -> PulseDomain.t
-  -> PulseDomain.t PulseOperations.access_result
+  -> PulseAbductiveDomain.t
+  -> PulseAbductiveDomain.t PulseOperations.access_result
 
 type model = exec_fun
 
 module Misc = struct
-  let early_exit : model = fun _ ~ret:_ ~actuals:_ _ -> Ok PulseDomain.initial
+  let early_exit : model = fun _ ~ret:_ ~actuals:_ _ -> Ok PulseAbductiveDomain.empty
 end
 
 module C = struct
diff --git a/infer/src/pulse/PulseModels.mli b/infer/src/pulse/PulseModels.mli
index ee36aeadc..109bbbd50 100644
--- a/infer/src/pulse/PulseModels.mli
+++ b/infer/src/pulse/PulseModels.mli
@@ -10,8 +10,8 @@ type exec_fun =
      Location.t
   -> ret:Var.t * Typ.t
   -> actuals:HilExp.t list
-  -> PulseDomain.t
-  -> PulseDomain.t PulseOperations.access_result
+  -> PulseAbductiveDomain.t
+  -> PulseAbductiveDomain.t PulseOperations.access_result
 
 type model = exec_fun
 
diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml
index 7d88c816a..d233a5fe6 100644
--- a/infer/src/pulse/PulseOperations.ml
+++ b/infer/src/pulse/PulseOperations.ml
@@ -9,21 +9,27 @@ module L = Logging
 module AbstractAddress = PulseDomain.AbstractAddress
 module Attribute = PulseDomain.Attribute
 module Attributes = PulseDomain.Attributes
-module Memory = PulseDomain.Memory
-module Stack = PulseDomain.Stack
+module Memory = PulseAbductiveDomain.Memory
+module Stack = PulseAbductiveDomain.Stack
 open Result.Monad_infix
 
-type t = PulseDomain.t = {heap: Memory.t; stack: Stack.t}
+include (* ocaml ignores the warning suppression at toplevel, hence the [include struct ... end] trick *)
+  struct
+  [@@@warning "-60"]
+
+  (** Do not use {!PulseDomain} directly, go through {!PulseAbductiveDomain} instead *)
+  module PulseDomain = struct end [@@deprecated "Use PulseAbductiveDomain instead."]
+end
+
+type t = PulseAbductiveDomain.t
 
 type 'a access_result = ('a, PulseDiagnostic.t) result
 
 (** Check that the address is not known to be invalid *)
 let check_addr_access actor (address, trace) astate =
-  match Memory.check_valid address astate.heap with
-  | Ok () ->
-      Ok astate
-  | Error invalidated_by ->
-      Error (PulseDiagnostic.AccessToInvalidAddress {invalidated_by; accessed_by= actor; trace})
+  Memory.check_valid actor address astate
+  |> Result.map_error ~f:(fun invalidated_by ->
+         PulseDiagnostic.AccessToInvalidAddress {invalidated_by; accessed_by= actor; trace} )
 
 
 (** Walk the heap starting from [addr] and following [path]. Stop either at the element before last
@@ -46,38 +52,22 @@ let rec walk ~dereference_to_ignore actor ~on_last addr_trace path astate =
   | [a], `Overwrite new_addr_trace ->
       check_addr_access_optional actor addr_trace astate
       >>| fun astate ->
-      let heap = Memory.add_edge_and_back_edge (fst addr_trace) a new_addr_trace astate.heap in
-      ({astate with heap}, new_addr_trace)
-  | a :: path, _ -> (
+      let astate = Memory.add_edge_and_back_edge (fst addr_trace) a new_addr_trace astate in
+      (astate, new_addr_trace)
+  | a :: path, _ ->
       check_addr_access_optional actor addr_trace astate
       >>= fun astate ->
       let dereference_to_ignore =
         Option.map ~f:(fun index -> max 0 (index - 1)) dereference_to_ignore
       in
-      let addr = fst addr_trace in
-      match Memory.find_edge_opt addr a astate.heap with
-      | None ->
-          let addr_trace' = (AbstractAddress.mk_fresh (), []) in
-          let heap = Memory.add_edge_and_back_edge addr a addr_trace' astate.heap in
-          let astate = {astate with heap} in
-          walk ~dereference_to_ignore actor ~on_last addr_trace' path astate
-      | Some addr_trace' ->
-          walk ~dereference_to_ignore actor ~on_last addr_trace' path astate )
+      let astate, addr_trace' = Memory.materialize_edge (fst addr_trace) a astate in
+      walk ~dereference_to_ignore actor ~on_last addr_trace' path astate
 
 
 let write_var var new_addr_trace astate =
-  let astate, var_address_of =
-    match Stack.find_opt var astate.stack with
-    | Some (addr, _) ->
-        (astate, addr)
-    | None ->
-        let addr = AbstractAddress.mk_fresh () in
-        let stack = Stack.add var (addr, None) astate.stack in
-        ({astate with stack}, addr)
-  in
+  let astate, (var_address_of, _) = Stack.materialize var astate in
   (* Update heap with var_address_of -*-> new_addr *)
-  let heap = Memory.add_edge var_address_of HilExp.Access.Dereference new_addr_trace astate.heap in
-  {astate with heap}
+  Memory.add_edge var_address_of HilExp.Access.Dereference new_addr_trace astate
 
 
 let ends_with_addressof = function HilExp.AccessExpression.AddressOf _ -> true | _ -> false
@@ -129,17 +119,12 @@ and walk_access_expr ~on_last astate access_expr location =
       Ok (write_var access_var new_addr_trace astate, new_addr_trace)
   | `Access, _ | `Overwrite _, _ :: _ -> (
       let astate, base_addr_trace =
-        match Stack.find_opt access_var astate.stack with
-        | Some (addr, init_loc_opt) ->
-            let trace =
-              Option.value_map init_loc_opt ~default:[] ~f:(fun init_loc ->
-                  [PulseTrace.VariableDeclaration init_loc] )
-            in
-            (astate, (addr, trace))
-        | None ->
-            let addr = AbstractAddress.mk_fresh () in
-            let stack = Stack.add access_var (addr, None) astate.stack in
-            ({astate with stack}, (addr, []))
+        let astate, (addr, init_loc_opt) = Stack.materialize access_var astate in
+        let trace =
+          Option.value_map init_loc_opt ~default:[] ~f:(fun init_loc ->
+              [PulseTrace.VariableDeclaration init_loc] )
+        in
+        (astate, (addr, trace))
       in
       match access_list with
       | [HilExp.Access.TakeAddress] ->
@@ -189,9 +174,7 @@ let overwrite_address astate access_expr new_addr_trace =
 
 
 (** Add the given address to the set of know invalid addresses. *)
-let mark_invalid actor address astate =
-  {astate with heap= Memory.invalidate address actor astate.heap}
-
+let mark_invalid actor address astate = Memory.invalidate address actor astate
 
 let havoc_var trace var astate = write_var var (AbstractAddress.mk_fresh (), trace) astate
 
@@ -215,7 +198,7 @@ let invalidate_array_elements cause location access_expr astate =
   >>= fun (astate, addr_trace) ->
   check_addr_access {access_expr; location} addr_trace astate
   >>| fun astate ->
-  match Memory.find_opt (fst addr_trace) astate.heap with
+  match Memory.find_opt (fst addr_trace) astate with
   | None ->
       astate
   | Some (edges, _) ->
@@ -233,10 +216,10 @@ let check_address_of_local_variable proc_desc address astate =
   let proc_location = Procdesc.get_loc proc_desc in
   let proc_name = Procdesc.get_proc_name proc_desc in
   let check_address_of_cpp_temporary () =
-    Memory.find_opt address astate.heap
+    Memory.find_opt address astate
     |> Option.fold_result ~init:() ~f:(fun () (_, attrs) ->
-           Container.fold_result ~fold:(IContainer.fold_of_pervasives_fold ~fold:Attributes.fold)
-             attrs ~init:() ~f:(fun () attr ->
+           IContainer.iter_result ~fold:(IContainer.fold_of_pervasives_fold ~fold:Attributes.fold)
+             attrs ~f:(fun attr ->
                match attr with
                | Attribute.AddressOfCppTemporary (variable, location_opt) ->
                    let location = Option.value ~default:proc_location location_opt in
@@ -245,57 +228,58 @@ let check_address_of_local_variable proc_desc address astate =
                    Ok () ) )
   in
   let check_address_of_stack_variable () =
-    Container.fold_result ~fold:(IContainer.fold_of_pervasives_map_fold ~fold:Stack.fold)
-      astate.stack ~init:() ~f:(fun () (variable, (var_address, init_location)) ->
+    IContainer.iter_result ~fold:(IContainer.fold_of_pervasives_map_fold ~fold:Stack.fold) astate
+      ~f:(fun (variable, (var_address, init_location)) ->
         if
           AbstractAddress.equal var_address address
           && ( Var.is_cpp_temporary variable
              || Var.is_local_to_procedure proc_name variable
                 && not (Procdesc.is_captured_var proc_desc variable) )
-        then
+        then (
           let location = Option.value ~default:proc_location init_location in
-          Error (PulseDiagnostic.StackVariableAddressEscape {variable; location})
+          L.d_printfln_escaped "Stack Variable &%a detected at address %a" Var.pp variable
+            AbstractAddress.pp address ;
+          Error (PulseDiagnostic.StackVariableAddressEscape {variable; location}) )
         else Ok () )
   in
   check_address_of_cpp_temporary () >>= check_address_of_stack_variable >>| fun () -> astate
 
 
-let mark_address_of_cpp_temporary location variable address heap =
+let mark_address_of_cpp_temporary location variable address astate =
   Memory.add_attributes address
     (Attributes.singleton (AddressOfCppTemporary (variable, location)))
-    heap
+    astate
 
 
 let remove_vars vars astate =
-  let heap =
-    List.fold vars ~init:astate.heap ~f:(fun heap var ->
-        match Stack.find_opt var astate.stack with
+  let astate =
+    List.fold vars ~init:astate ~f:(fun heap var ->
+        match Stack.find_opt var astate with
         | Some (address, location) when Var.is_cpp_temporary var ->
             (* TODO: it would be good to record the location of the temporary creation in the
                  stack and save it here in the attribute for reporting *)
-            mark_address_of_cpp_temporary location var address heap
+            mark_address_of_cpp_temporary location var address astate
         | _ ->
             heap )
   in
-  let stack = Stack.filter (fun var _ -> not (List.mem ~equal:Var.equal vars var)) astate.stack in
-  if phys_equal stack astate.stack && phys_equal heap astate.heap then astate
-  else PulseDomain.minimize {stack; heap}
+  let astate' = Stack.remove_vars vars astate in
+  if phys_equal astate' astate then astate else PulseAbductiveDomain.discard_unreachable astate'
 
 
 let record_var_decl_location location var astate =
   let addr =
-    match Stack.find_opt var astate.stack with
+    match Stack.find_opt var astate with
     | Some (addr, _) ->
         addr
     | None ->
         AbstractAddress.mk_fresh ()
   in
-  let stack = Stack.add var (addr, Some location) astate.stack in
-  {astate with stack}
+  Stack.add var (addr, Some location) astate
 
 
 module Closures = struct
   open Result.Monad_infix
+  module Memory = PulseAbductiveDomain.Memory
 
   let fake_capture_field_prefix = "__capture_"
 
@@ -324,7 +308,7 @@ module Closures = struct
 
 
   let check_captured_addresses location lambda addr astate =
-    match Memory.find_opt addr astate.heap with
+    match Memory.find_opt addr astate with
     | None ->
         Ok astate
     | Some (edges, attributes) ->
@@ -350,12 +334,7 @@ module Closures = struct
       astate
     >>| fun astate ->
     let fake_capture_edges = mk_capture_edges captured in
-    let heap =
-      Memory.set_cell closure_addr
-        (fake_capture_edges, Attributes.singleton (Closure pname))
-        astate.heap
-    in
-    {astate with heap}
+    Memory.set_cell closure_addr (fake_capture_edges, Attributes.singleton (Closure pname)) astate
 
 
   let record location access_expr pname captured astate =
@@ -377,13 +356,14 @@ end
 
 module StdVector = struct
   open Result.Monad_infix
+  module Memory = PulseAbductiveDomain.Memory
 
   let is_reserved location vector_access_expr astate =
     read location vector_access_expr astate
-    >>| fun (astate, (addr, _)) -> (astate, Memory.is_std_vector_reserved addr astate.heap)
+    >>| fun (astate, (addr, _)) -> (astate, Memory.is_std_vector_reserved addr astate)
 
 
   let mark_reserved location vector_access_expr astate =
     read location vector_access_expr astate
-    >>| fun (astate, (addr, _)) -> {astate with heap= Memory.std_vector_reserve addr astate.heap}
+    >>| fun (astate, (addr, _)) -> Memory.std_vector_reserve addr astate
 end
diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli
index e3cfbf2b0..f658bcb4b 100644
--- a/infer/src/pulse/PulseOperations.mli
+++ b/infer/src/pulse/PulseOperations.mli
@@ -6,8 +6,9 @@
  *)
 
 open! IStd
+module AbstractAddress = PulseDomain.AbstractAddress
 
-type t = PulseDomain.t = {heap: PulseDomain.Memory.t; stack: PulseDomain.Stack.t}
+type t = PulseAbductiveDomain.t
 
 type 'a access_result = ('a, PulseDiagnostic.t) result
 
@@ -40,7 +41,7 @@ val read :
      Location.t
   -> HilExp.AccessExpression.t
   -> t
-  -> (t * (PulseDomain.AbstractAddress.t * PulseTrace.t)) access_result
+  -> (t * (AbstractAddress.t * PulseTrace.t)) access_result
 
 val read_all : Location.t -> HilExp.AccessExpression.t list -> t -> t access_result
 
@@ -48,12 +49,12 @@ val havoc_var : PulseTrace.t -> Var.t -> t -> t
 
 val havoc : PulseTrace.t -> Location.t -> HilExp.AccessExpression.t -> t -> t access_result
 
-val write_var : Var.t -> PulseDomain.AbstractAddress.t * PulseTrace.t -> t -> t
+val write_var : Var.t -> AbstractAddress.t * PulseTrace.t -> t -> t
 
 val write :
      Location.t
   -> HilExp.AccessExpression.t
-  -> PulseDomain.AbstractAddress.t * PulseTrace.t
+  -> AbstractAddress.t * PulseTrace.t
   -> t
   -> t access_result
 
@@ -68,5 +69,4 @@ val record_var_decl_location : Location.t -> Var.t -> t -> t
 val remove_vars : Var.t list -> t -> t
 
 (* TODO: better name and pass location to report where we returned *)
-val check_address_of_local_variable :
-  Procdesc.t -> PulseDomain.AbstractAddress.t -> t -> t access_result
+val check_address_of_local_variable : Procdesc.t -> AbstractAddress.t -> t -> t access_result