diff --git a/infer/src/absint/TransferFunctions.ml b/infer/src/absint/TransferFunctions.ml
index b18cc0d0d..42424550e 100644
--- a/infer/src/absint/TransferFunctions.ml
+++ b/infer/src/absint/TransferFunctions.ml
@@ -28,3 +28,74 @@ end
 module type HIL = sig
   include S with type instr := HilInstr.t
 end
+
+module type MakeHIL = functor (C : ProcCfg.S) -> sig
+  include HIL with module CFG = C
+end
+
+module type DisjunctiveConfig = sig
+  type domain_t [@@deriving compare]
+
+  val join_policy : [`JoinAfter of int | `UnderApproximateAfter of int | `NeverJoin]
+
+  val widen_policy : [`UnderApproximateAfterNumIterations of int]
+end
+
+module MakeHILDisjunctive
+    (TransferFunctions : HIL)
+    (DConfig : DisjunctiveConfig with type domain_t = TransferFunctions.Domain.t) =
+struct
+  module CFG = TransferFunctions.CFG
+
+  type extras = TransferFunctions.extras
+
+  module Domain = struct
+    module Set = AbstractDomain.FiniteSet (struct
+      include TransferFunctions.Domain
+
+      let compare = DConfig.compare_domain_t
+    end)
+
+    let real_join lhs rhs =
+      let union = Set.join lhs rhs in
+      match DConfig.join_policy with
+      | `NeverJoin ->
+          union
+      | `UnderApproximateAfter n ->
+          if Set.cardinal union <= n then union else lhs
+      | `JoinAfter n ->
+          if Set.cardinal union <= n then union
+          else
+            let joined =
+              Set.fold
+                (fun dom joined ->
+                  match joined with
+                  | None ->
+                      Some dom
+                  | Some joined ->
+                      Some (TransferFunctions.Domain.join dom joined) )
+                union None
+            in
+            Set.singleton (Option.value_exn joined)
+
+
+    let real_widen ~prev ~next ~num_iters =
+      let (`UnderApproximateAfterNumIterations max_iter) = DConfig.widen_policy in
+      if num_iters > max_iter then prev else real_join prev next
+
+
+    include Set
+
+    let join = real_join
+
+    let widen = real_widen
+  end
+
+  let exec_instr disj_dom extras node instr =
+    Domain.map (fun dom -> TransferFunctions.exec_instr dom extras node instr) disj_dom
+
+
+  let pp_session_name node f = TransferFunctions.pp_session_name node f
+
+  let of_domain x = Domain.singleton x
+end
diff --git a/infer/src/absint/TransferFunctions.mli b/infer/src/absint/TransferFunctions.mli
index a09092183..99b3eb8dc 100644
--- a/infer/src/absint/TransferFunctions.mli
+++ b/infer/src/absint/TransferFunctions.mli
@@ -36,3 +36,32 @@ end
 module type HIL = sig
   include S with type instr := HilInstr.t
 end
+
+module type DisjunctiveConfig = sig
+  (** the underlying domain *)
+  type domain_t [@@deriving compare]
+
+  val join_policy :
+    [ `JoinAfter of int
+      (** when the set of disjuncts gets bigger than [n] the underlying domain's join is called to
+       collapse them into one state *)
+    | `UnderApproximateAfter of int
+      (** When the set of disjuncts gets bigger than [n] then just stop adding new states to it,
+         drop any further states on the floor. This corresponds to an under-approximation/bounded
+         approach. *)
+    | `NeverJoin  (** keep accumaluting states *) ]
+
+  val widen_policy : [`UnderApproximateAfterNumIterations of int]
+end
+
+(** In the disjunctive interpreter, the domain is a set of abstract states representing a
+   disjunction between these states. The transfer functions are executed on each state in the
+   disjunct independently. The join on the disjunctive state is governed by the policy described in
+   [DConfig]. *)
+module MakeHILDisjunctive
+    (TransferFunctions : HIL)
+    (DConfig : DisjunctiveConfig with type domain_t = TransferFunctions.Domain.t) : sig
+  include HIL with type extras = TransferFunctions.extras and module CFG = TransferFunctions.CFG
+
+  val of_domain : DConfig.domain_t -> Domain.t
+end
diff --git a/infer/src/checkers/Pulse.ml b/infer/src/checkers/Pulse.ml
index 97f6377d3..fd673afc0 100644
--- a/infer/src/checkers/Pulse.ml
+++ b/infer/src/checkers/Pulse.ml
@@ -24,7 +24,7 @@ let check_error summary = function
       raise_notrace AbstractDomain.Stop_analysis
 
 
-module TransferFunctions (CFG : ProcCfg.S) = struct
+module PulseTransferFunctions (CFG : ProcCfg.S) = struct
   module CFG = CFG
   module Domain = PulseDomain
 
@@ -133,13 +133,29 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
 end
 
 module HilConfig = LowerHil.DefaultConfig
-module Analyzer =
+
+module DisjunctiveTransferFunctions =
+  TransferFunctions.MakeHILDisjunctive
+    (PulseTransferFunctions
+       (ProcCfg.Exceptional))
+       (struct
+         type domain_t = PulseDomain.t [@@deriving compare]
+
+         let join_policy = `JoinAfter 1
+
+         let widen_policy = `UnderApproximateAfterNumIterations 5
+       end)
+
+module DisjunctiveAnalyzer =
   LowerHil.MakeAbstractInterpreterWithConfig (AbstractInterpreter.MakeWTO) (HilConfig)
-    (TransferFunctions (ProcCfg.Exceptional))
+    (DisjunctiveTransferFunctions)
 
 let checker {Callbacks.proc_desc; tenv; summary} =
   let proc_data = ProcData.make proc_desc tenv summary in
   PulseDomain.AbstractAddress.init () ;
-  ( try ignore (Analyzer.compute_post proc_data ~initial:PulseDomain.initial)
+  ( try
+      ignore
+        (DisjunctiveAnalyzer.compute_post proc_data
+           ~initial:(DisjunctiveTransferFunctions.of_domain PulseDomain.initial))
     with AbstractDomain.Stop_analysis -> () ) ;
   summary
diff --git a/infer/src/checkers/PulseDomain.ml b/infer/src/checkers/PulseDomain.ml
index c936fbb65..e6542e46e 100644
--- a/infer/src/checkers/PulseDomain.ml
+++ b/infer/src/checkers/PulseDomain.ml
@@ -87,7 +87,7 @@ module Memory : sig
 
   type cell = edges * Attributes.t
 
-  type t
+  type t [@@deriving compare]
 
   val empty : t
 
@@ -124,13 +124,13 @@ end = struct
 
   module Edges = PrettyPrintable.MakePPMap (Access)
 
-  type edges = AbstractAddressSet.t Edges.t
+  type edges = AbstractAddressSet.t Edges.t [@@deriving compare]
 
-  type cell = edges * Attributes.t
+  type cell = edges * Attributes.t [@@deriving compare]
 
   module Graph = PrettyPrintable.MakePPMap (AbstractAddress)
 
-  type t = cell Graph.t
+  type t = cell Graph.t [@@deriving compare]
 
   let pp =
     Graph.pp ~pp_value:(Pp.pair ~fst:(Edges.pp ~pp_value:AbstractAddressSet.pp) ~snd:Attributes.pp)
@@ -238,10 +238,14 @@ end
     own. It so happens that the join on abstract states uses the join of stacks provided by this
     functor followed by normalization wrt the unification found between abstract locations so it's
     convenient to define stacks as elements of this domain. *)
-module Stack = AbstractDomain.Map (Var) (AbstractAddressSet)
+module Stack = struct
+  include AbstractDomain.Map (Var) (AbstractAddressSet)
+
+  let compare = compare AbstractAddressSet.compare
+end
 
 (** the domain *)
-type astate = {heap: Memory.t; stack: Stack.t}
+type astate = {heap: Memory.t; stack: Stack.t} [@@deriving compare]
 
 let initial =
   { heap=
@@ -830,4 +834,7 @@ module StdVector = struct
 end
 
 include Domain
+
+let compare = compare_astate
+
 include Operations
diff --git a/infer/src/checkers/PulseDomain.mli b/infer/src/checkers/PulseDomain.mli
index 9ed2e7f57..82345f91d 100644
--- a/infer/src/checkers/PulseDomain.mli
+++ b/infer/src/checkers/PulseDomain.mli
@@ -15,6 +15,8 @@ end
 
 include AbstractDomain.S
 
+val compare : t -> t -> int
+
 module AbstractAddressSet : sig
   type t
 end