diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml
index df04ed4aa..aff2518a7 100644
--- a/infer/src/pulse/Pulse.ml
+++ b/infer/src/pulse/Pulse.ml
@@ -41,7 +41,7 @@ module PulseTransferFunctions = struct
     AnalysisCallbacks.proc_resolve_attributes pname |> Option.map ~f:ProcAttributes.get_pvar_formals
 
 
-  let interprocedural_call {InterproceduralAnalysis.analyze_dependency; proc_desc; tenv} ret
+  let interprocedural_call {InterproceduralAnalysis.analyze_dependency; tenv; proc_desc} ret
       callee_pname call_exp actuals call_loc astate =
     match callee_pname with
     | Some callee_pname when not Config.pulse_intraprocedural_only ->
@@ -123,7 +123,7 @@ module PulseTransferFunctions = struct
         astate
 
 
-  let dispatch_call ({InterproceduralAnalysis.proc_desc; tenv} as analysis_data) ret call_exp
+  let dispatch_call ({tenv; InterproceduralAnalysis.proc_desc} as analysis_data) ret call_exp
       actuals call_loc flags astate =
     (* evaluate all actuals *)
     let<*> astate, rev_func_args =
@@ -196,7 +196,7 @@ module PulseTransferFunctions = struct
           | Error _ as err ->
               Some err
           | Ok exec_state ->
-              ExecutionDomain.force_exit_program proc_desc exec_state
+              ExecutionDomain.force_exit_program tenv proc_desc exec_state
               |> Option.map ~f:(fun exec_state -> Ok exec_state) )
     else exec_states_res
 
@@ -263,7 +263,7 @@ module PulseTransferFunctions = struct
 
 
   let exec_instr_aux (astate : Domain.t)
-      ({InterproceduralAnalysis.proc_desc; tenv} as analysis_data) _cfg_node (instr : Sil.instr) :
+      ({tenv; InterproceduralAnalysis.proc_desc} as analysis_data) _cfg_node (instr : Sil.instr) :
       Domain.t list =
     match astate with
     | ISLLatentMemoryError _ | AbortProgram _ | LatentAbortProgram _ ->
@@ -370,7 +370,7 @@ module PulseTransferFunctions = struct
                     astate :: astates
                 | ContinueProgram astate ->
                     let astate =
-                      ( match PulseOperations.remove_vars vars location astate with
+                      ( match PulseOperations.remove_vars tenv vars location astate with
                       | Ok astate ->
                           Ok [astate]
                       | Error _ as error ->
@@ -428,7 +428,7 @@ let with_debug_exit_node proc_desc ~f =
     ~f
 
 
-let checker ({InterproceduralAnalysis.proc_desc; err_log; tenv} as analysis_data) =
+let checker ({tenv; InterproceduralAnalysis.proc_desc; err_log} as analysis_data) =
   AbstractValue.State.reset () ;
   let initial_astate = ExecutionDomain.mk_initial tenv proc_desc in
   let initial = [initial_astate] in
@@ -438,7 +438,7 @@ let checker ({InterproceduralAnalysis.proc_desc; err_log; tenv} as analysis_data
           let updated_posts =
             PulseObjectiveCSummary.update_objc_method_posts analysis_data ~initial_astate ~posts
           in
-          let summary = PulseSummary.of_posts proc_desc updated_posts in
+          let summary = PulseSummary.of_posts tenv proc_desc updated_posts in
           report_topl_errors proc_desc err_log summary ;
           Some summary )
   | None ->
diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml
index 3312a1aa1..28fd2093e 100644
--- a/infer/src/pulse/PulseAbductiveDomain.ml
+++ b/infer/src/pulse/PulseAbductiveDomain.ml
@@ -142,6 +142,16 @@ let leq ~lhs ~rhs =
 
 let initialize address astate = {astate with post= PostDomain.initialize address astate.post}
 
+let simplify_instanceof tenv astate =
+  let attrs = (astate.post :> BaseDomain.t).attrs in
+  let path_condition =
+    PathCondition.simplify_instanceof tenv
+      ~get_dynamic_type:(BaseAddressAttributes.get_dynamic_type attrs)
+      astate.path_condition
+  in
+  {astate with path_condition}
+
+
 module Stack = struct
   let is_abducible astate var =
     (* HACK: formals are pre-registered in the initial state *)
@@ -747,12 +757,17 @@ let canonicalize astate =
   {astate with pre; post}
 
 
-let summary_of_post pdesc astate =
+let summary_of_post tenv pdesc astate =
   let open SatUnsat.Import in
   (* NOTE: we normalize (to strengthen the equality relation used by canonicalization) then
      canonicalize *before* garbage collecting unused addresses in case we detect any last-minute
      contradictions about addresses we are about to garbage collect *)
-  let path_condition, is_unsat, new_eqs = PathCondition.is_unsat_expensive astate.path_condition in
+  let attrs = (astate.post :> BaseDomain.t).attrs in
+  let path_condition, is_unsat, new_eqs =
+    PathCondition.is_unsat_expensive tenv
+      ~get_dynamic_type:(BaseAddressAttributes.get_dynamic_type attrs)
+      astate.path_condition
+  in
   if is_unsat then Unsat
   else
     let astate = {astate with path_condition} in
@@ -766,7 +781,9 @@ let summary_of_post pdesc astate =
     in
     let astate, live_addresses, _ = discard_unreachable astate in
     let* path_condition, new_eqs =
-      PathCondition.simplify ~keep:live_addresses astate.path_condition
+      PathCondition.simplify tenv ~keep:live_addresses
+        ~get_dynamic_type:(BaseAddressAttributes.get_dynamic_type attrs)
+        astate.path_condition
     in
     let+ astate = incorporate_new_eqs astate new_eqs in
     let astate =
diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli
index b66c9fb9f..f770d83cd 100644
--- a/infer/src/pulse/PulseAbductiveDomain.mli
+++ b/infer/src/pulse/PulseAbductiveDomain.mli
@@ -89,6 +89,8 @@ val get_pre : t -> BaseDomain.t
 
 val get_post : t -> BaseDomain.t
 
+val simplify_instanceof : Tenv.t -> t -> t
+
 (** stack operations like {!BaseStack} but that also take care of propagating facts to the
     precondition *)
 module Stack : sig
@@ -194,7 +196,7 @@ val set_path_condition : PathCondition.t -> t -> t
 (** private type to make sure {!summary_of_post} is always called when creating summaries *)
 type summary = private t [@@deriving compare, equal, yojson_of]
 
-val summary_of_post : Procdesc.t -> t -> summary SatUnsat.t
+val summary_of_post : Tenv.t -> Procdesc.t -> t -> summary SatUnsat.t
 (** trim the state down to just the procedure's interface (formals and globals), and simplify and
     normalize the state *)
 
diff --git a/infer/src/pulse/PulseBaseAddressAttributes.ml b/infer/src/pulse/PulseBaseAddressAttributes.ml
index bfefa1e6a..3075bc19e 100644
--- a/infer/src/pulse/PulseBaseAddressAttributes.ml
+++ b/infer/src/pulse/PulseBaseAddressAttributes.ml
@@ -76,8 +76,6 @@ let allocate procname (address, history) location memory =
   add_one address (Attribute.Allocated (procname, Immediate {location; history})) memory
 
 
-let add_dynamic_type typ address memory = add_one address (Attribute.DynamicType typ) memory
-
 let mark_as_end_of_collection address memory = add_one address Attribute.EndOfCollection memory
 
 let check_valid address attrs =
@@ -150,6 +148,10 @@ let get_must_be_valid_or_allocated_isl address attrs =
 
 let get_must_be_initialized = get_attribute Attributes.get_must_be_initialized
 
+let add_dynamic_type typ address memory = add_one address (Attribute.DynamicType typ) memory
+
+let get_dynamic_type attrs v = get_attribute Attributes.get_dynamic_type v attrs
+
 let std_vector_reserve address memory = add_one address Attribute.StdVectorReserve memory
 
 let is_end_of_collection address attrs =
diff --git a/infer/src/pulse/PulseBaseAddressAttributes.mli b/infer/src/pulse/PulseBaseAddressAttributes.mli
index 6cbe78562..800917f55 100644
--- a/infer/src/pulse/PulseBaseAddressAttributes.mli
+++ b/infer/src/pulse/PulseBaseAddressAttributes.mli
@@ -45,6 +45,8 @@ val get_must_be_initialized : AbstractValue.t -> t -> Trace.t option
 
 val add_dynamic_type : Typ.t -> AbstractValue.t -> t -> t
 
+val get_dynamic_type : t -> AbstractValue.t -> Typ.t option
+
 val std_vector_reserve : AbstractValue.t -> t -> t
 
 val is_std_vector_reserved : AbstractValue.t -> t -> bool
diff --git a/infer/src/pulse/PulseExecutionDomain.ml b/infer/src/pulse/PulseExecutionDomain.ml
index cd5466a0a..b0e388440 100644
--- a/infer/src/pulse/PulseExecutionDomain.ml
+++ b/infer/src/pulse/PulseExecutionDomain.ml
@@ -78,9 +78,9 @@ let is_unsat_cheap exec_state = PathCondition.is_unsat_cheap (get_astate exec_st
 
 type summary = AbductiveDomain.summary base_t [@@deriving compare, equal, yojson_of]
 
-let summary_of_post_common ~continue_program proc_desc = function
+let summary_of_post_common tenv ~continue_program proc_desc = function
   | ContinueProgram astate | ISLLatentMemoryError astate -> (
-    match AbductiveDomain.summary_of_post proc_desc astate with
+    match AbductiveDomain.summary_of_post tenv proc_desc astate with
     | Unsat ->
         None
     | Sat astate ->
@@ -94,10 +94,10 @@ let summary_of_post_common ~continue_program proc_desc = function
       Some (LatentAbortProgram {astate; latent_issue})
 
 
-let summary_of_posts proc_desc posts =
+let summary_of_posts tenv proc_desc posts =
   List.filter_mapi posts ~f:(fun i exec_state ->
       L.d_printfln "Creating spec out of state #%d:@\n%a" i pp exec_state ;
-      summary_of_post_common proc_desc exec_state ~continue_program:(fun astate ->
+      summary_of_post_common tenv proc_desc exec_state ~continue_program:(fun astate ->
           match (astate :> AbductiveDomain.t).isl_status with
           | ISLOk ->
               ContinueProgram astate
@@ -105,5 +105,5 @@ let summary_of_posts proc_desc posts =
               ISLLatentMemoryError astate ) )
 
 
-let force_exit_program proc_desc post =
-  summary_of_post_common proc_desc post ~continue_program:(fun astate -> ExitProgram astate)
+let force_exit_program tenv proc_desc post =
+  summary_of_post_common tenv proc_desc post ~continue_program:(fun astate -> ExitProgram astate)
diff --git a/infer/src/pulse/PulseExecutionDomain.mli b/infer/src/pulse/PulseExecutionDomain.mli
index 20e4218dc..8999062b4 100644
--- a/infer/src/pulse/PulseExecutionDomain.mli
+++ b/infer/src/pulse/PulseExecutionDomain.mli
@@ -34,6 +34,6 @@ val is_unsat_cheap : t -> bool
 
 type summary = AbductiveDomain.summary base_t [@@deriving compare, equal, yojson_of]
 
-val summary_of_posts : Procdesc.t -> t list -> summary list
+val summary_of_posts : Tenv.t -> Procdesc.t -> t list -> summary list
 
-val force_exit_program : Procdesc.t -> t -> t option
+val force_exit_program : Tenv.t -> Procdesc.t -> t -> t option
diff --git a/infer/src/pulse/PulseFormula.ml b/infer/src/pulse/PulseFormula.ml
index ed570aa66..92825e8b3 100644
--- a/infer/src/pulse/PulseFormula.ml
+++ b/infer/src/pulse/PulseFormula.ml
@@ -329,7 +329,7 @@ module Term = struct
     | NotEqual (t1, t2) ->
         F.fprintf fmt "%a≠%a" (pp_paren pp_var ~needs_paren) t1 (pp_paren pp_var ~needs_paren) t2
     | IsInstanceOf (v, t) ->
-        F.fprintf fmt "%a instanceof %a" pp_var v (Typ.pp Pp.text) t
+        F.fprintf fmt "(%a instanceof %a)" pp_var v (Typ.pp Pp.text) t
 
 
   let of_q q = Const q
@@ -1374,8 +1374,43 @@ let prune_binop ~negated (bop : Binop.t) x y phi =
   ({phi with pruned; both}, new_eqs)
 
 
-let normalize phi =
+module DynamicTypes = struct
+  let evaluate_instanceof tenv ~get_dynamic_type v typ =
+    get_dynamic_type v
+    |> Option.map ~f:(fun dynamic_type ->
+           let is_instanceof =
+             match (Typ.name dynamic_type, Typ.name typ) with
+             | Some name1, Some name2 ->
+                 PatternMatch.is_subtype tenv name1 name2
+             | _, _ ->
+                 Typ.equal dynamic_type typ
+           in
+           Term.of_bool is_instanceof )
+
+
+  let simplify tenv ~get_dynamic_type phi =
+    let changed = ref false in
+    let atoms =
+      Atom.Set.map
+        (fun atom ->
+          Atom.map_terms atom ~f:(function
+            | Term.IsInstanceOf (v, typ) as t -> (
+              match evaluate_instanceof tenv ~get_dynamic_type v typ with
+              | None ->
+                  t
+              | Some t' ->
+                  changed := true ;
+                  t' )
+            | t ->
+                t ) )
+        phi.both.atoms
+    in
+    if !changed then {phi with both= {phi.both with atoms}} else phi
+end
+
+let normalize tenv ~get_dynamic_type phi =
   let open SatUnsat.Import in
+  let phi = DynamicTypes.simplify tenv ~get_dynamic_type phi in
   let* both, new_eqs = Formula.Normalizer.normalize phi.both in
   let* known, _ = Formula.Normalizer.normalize phi.known in
   let+ pruned =
@@ -1621,9 +1656,9 @@ module DeadVariables = struct
     {known; pruned; both}
 end
 
-let simplify ~keep phi =
+let simplify tenv ~get_dynamic_type ~keep phi =
   let open SatUnsat.Import in
-  let* phi, new_eqs = normalize phi in
+  let* phi, new_eqs = normalize tenv ~get_dynamic_type phi in
   L.d_printfln_escaped "Simplifying %a wrt {%a}" pp phi Var.Set.pp keep ;
   (* get rid of as many variables as possible *)
   let+ phi = QuantifierElimination.eliminate_vars ~keep phi in
diff --git a/infer/src/pulse/PulseFormula.mli b/infer/src/pulse/PulseFormula.mli
index 22cd8bcc3..4c16d1574 100644
--- a/infer/src/pulse/PulseFormula.mli
+++ b/infer/src/pulse/PulseFormula.mli
@@ -53,10 +53,15 @@ val prune_binop : negated:bool -> Binop.t -> operand -> operand -> t -> (t * new
 
 (** {3 Operations} *)
 
-val normalize : t -> (t * new_eqs) SatUnsat.t
+val normalize : Tenv.t -> get_dynamic_type:(Var.t -> Typ.t option) -> t -> (t * new_eqs) SatUnsat.t
 (** think a bit harder about the formula *)
 
-val simplify : keep:Var.Set.t -> t -> (t * new_eqs) SatUnsat.t
+val simplify :
+     Tenv.t
+  -> get_dynamic_type:(Var.t -> Typ.t option)
+  -> keep:Var.Set.t
+  -> t
+  -> (t * new_eqs) SatUnsat.t
 
 val and_fold_subst_variables :
      t
@@ -73,3 +78,10 @@ val has_no_assumptions : t -> bool
 
 val get_var_repr : t -> Var.t -> Var.t
 (** get the canonical representative for the variable according to the equality relation *)
+
+(** Module for reasoning about dynamic types. **)
+module DynamicTypes : sig
+  val simplify : Tenv.t -> get_dynamic_type:(Var.t -> Typ.t option) -> t -> t
+  (** Simplifies [IsInstanceOf(var, typ)] predicate when dynamic type information is available in
+      state. **)
+end
diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml
index 7b53768fa..c62a3b7bb 100644
--- a/infer/src/pulse/PulseModels.ml
+++ b/infer/src/pulse/PulseModels.ml
@@ -49,8 +49,8 @@ module Misc = struct
 
 
   let early_exit : model =
-   fun {proc_desc} ~callee_procname:_ _ ~ret:_ astate ->
-    match AbductiveDomain.summary_of_post proc_desc astate with
+   fun {tenv; proc_desc} ~callee_procname:_ _ ~ret:_ astate ->
+    match AbductiveDomain.summary_of_post tenv proc_desc astate with
     | Unsat ->
         []
     | Sat astate ->
@@ -232,7 +232,7 @@ module ObjC = struct
 
 
   let dispatch_sync args : model =
-   fun {analyze_dependency; proc_desc; tenv} ~callee_procname:_ location ~ret astate ->
+   fun {analyze_dependency; tenv; proc_desc} ~callee_procname:_ location ~ret astate ->
     match List.last args with
     | None ->
         ok_continue astate
@@ -570,7 +570,7 @@ end
 module StdFunction = struct
   let operator_call ProcnameDispatcher.Call.FuncArg.{arg_payload= lambda_ptr_hist; typ} actuals :
       model =
-   fun {analyze_dependency; proc_desc; tenv} ~callee_procname:_ location ~ret astate ->
+   fun {analyze_dependency; tenv; proc_desc} ~callee_procname:_ location ~ret astate ->
     let havoc_ret (ret_id, _) astate =
       let event = ValueHistory.Call {f= Model "std::function::operator()"; location; in_call= []} in
       [PulseOperations.havoc_id ret_id [event] astate]
@@ -933,7 +933,6 @@ module Java = struct
     | Exp.Sizeof {typ} ->
         PulseArithmetic.and_equal_instanceof res_addr argv typ astate
         |> PulseArithmetic.prune_positive argv
-        |> PulseArithmetic.and_eq_int res_addr IntLit.one
         |> PulseOperations.write_id ret_id (res_addr, event :: hist)
         |> ok_continue
     (* The type expr is sometimes a Var expr but this is not expected.
diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml
index b9b966ff0..3eff45f19 100644
--- a/infer/src/pulse/PulseOperations.ml
+++ b/infer/src/pulse/PulseOperations.ml
@@ -536,9 +536,13 @@ let get_dynamic_type_unreachable_values vars astate =
   List.map ~f:(fun (var, _, typ) -> (var, typ)) res
 
 
-let remove_vars vars location orig_astate =
+let remove_vars tenv vars location orig_astate =
   let astate =
-    List.fold vars ~init:orig_astate ~f:(fun astate var ->
+    (* Simplification of [IsInstanceOf(var, typ)] term is necessary here, as a variable can die before
+       the normalization function is called. This could cause [IsInstanceOf(var, typ)] terms that
+       reference dead vars to be collected before they are evaluated to detect a contradiction *)
+    List.fold vars ~init:(AbductiveDomain.simplify_instanceof tenv orig_astate)
+      ~f:(fun astate var ->
         match Stack.find_opt var astate with
         | Some (address, history) ->
             let astate =
@@ -627,7 +631,7 @@ let unknown_call tenv call_loc reason ~ret ~actuals ~formals_opt astate =
   |> havoc_ret ret |> add_skipped_proc
 
 
-let apply_callee ~caller_proc_desc callee_pname call_loc callee_exec_state ~ret
+let apply_callee tenv ~caller_proc_desc callee_pname call_loc callee_exec_state ~ret
     ~captured_vars_with_actuals ~formals ~actuals astate =
   let map_call_result callee_prepost ~f =
     match
@@ -658,7 +662,7 @@ let apply_callee ~caller_proc_desc callee_pname call_loc callee_exec_state ~ret
       map_call_result
         (astate :> AbductiveDomain.t)
         ~f:(fun astate ->
-          let+ astate_summary = AbductiveDomain.summary_of_post caller_proc_desc astate in
+          let+ astate_summary = AbductiveDomain.summary_of_post tenv caller_proc_desc astate in
           match callee_exec_state with
           | ContinueProgram _ | ISLLatentMemoryError _ ->
               assert false
@@ -744,7 +748,7 @@ let call tenv ~caller_proc_desc ~(callee_data : (Procdesc.t * PulseSummary.t) op
           else
             (* apply all pre/post specs *)
             match
-              apply_callee ~caller_proc_desc callee_pname call_loc callee_exec_state
+              apply_callee tenv ~caller_proc_desc callee_pname call_loc callee_exec_state
                 ~captured_vars_with_actuals ~formals ~actuals ~ret astate
             with
             | Unsat ->
diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli
index d6c16a079..041b55129 100644
--- a/infer/src/pulse/PulseOperations.mli
+++ b/infer/src/pulse/PulseOperations.mli
@@ -179,7 +179,7 @@ val get_dynamic_type_unreachable_values : Var.t list -> t -> (Var.t * Typ.t) lis
 (** Given a list of variables, computes the unreachable values if the variables were removed from
     the stack, then return the dynamic types of those values if they are available *)
 
-val remove_vars : Var.t list -> Location.t -> t -> t access_result
+val remove_vars : Tenv.t -> Var.t list -> Location.t -> t -> t access_result
 
 val check_address_escape :
   Location.t -> Procdesc.t -> AbstractValue.t -> ValueHistory.t -> t -> t access_result
diff --git a/infer/src/pulse/PulsePathCondition.ml b/infer/src/pulse/PulsePathCondition.ml
index e8f13629a..4cd067c51 100644
--- a/infer/src/pulse/PulsePathCondition.ml
+++ b/infer/src/pulse/PulsePathCondition.ml
@@ -107,10 +107,10 @@ let and_eq_vars v1 v2 phi =
   ({is_unsat; bo_itvs; citvs; formula}, new_eqs)
 
 
-let simplify ~keep phi =
+let simplify tenv ~keep ~get_dynamic_type phi =
   let result =
     let+ {is_unsat; bo_itvs; citvs; formula} = phi in
-    let+| formula, new_eqs = Formula.simplify ~keep formula in
+    let+| formula, new_eqs = Formula.simplify tenv ~keep ~get_dynamic_type formula in
     let is_in_keep v _ = AbstractValue.Set.mem v keep in
     ( { is_unsat
       ; bo_itvs= BoItvs.filter is_in_keep bo_itvs
@@ -121,6 +121,11 @@ let simplify ~keep phi =
   if (fst result).is_unsat then Unsat else Sat result
 
 
+let simplify_instanceof tenv ~get_dynamic_type phi =
+  let formula = Formula.DynamicTypes.simplify tenv ~get_dynamic_type phi.formula in
+  {phi with formula}
+
+
 let subst_find_or_new subst addr_callee =
   match AbstractValue.Map.find_opt addr_callee subst with
   | None ->
@@ -420,12 +425,12 @@ let is_known_not_equal_zero phi v =
 
 let is_unsat_cheap phi = phi.is_unsat
 
-let is_unsat_expensive phi =
+let is_unsat_expensive tenv ~get_dynamic_type phi =
   (* note: contradictions are detected eagerly for all sub-domains except formula, so just
      evaluate that one *)
   if is_unsat_cheap phi then (phi, true, [])
   else
-    match Formula.normalize phi.formula with
+    match Formula.normalize tenv ~get_dynamic_type phi.formula with
     | Unsat ->
         (false_, true, [])
     | Sat (formula, new_eqs) ->
diff --git a/infer/src/pulse/PulsePathCondition.mli b/infer/src/pulse/PulsePathCondition.mli
index 755b4b3c4..b174fbdb2 100644
--- a/infer/src/pulse/PulsePathCondition.mli
+++ b/infer/src/pulse/PulsePathCondition.mli
@@ -34,10 +34,17 @@ val and_eq_int : AbstractValue.t -> IntLit.t -> t -> t * new_eqs
 
 val and_eq_vars : AbstractValue.t -> AbstractValue.t -> t -> t * new_eqs
 
-val simplify : keep:AbstractValue.Set.t -> t -> (t * new_eqs) SatUnsat.t
+val simplify :
+     Tenv.t
+  -> keep:AbstractValue.Set.t
+  -> get_dynamic_type:(AbstractValue.t -> Typ.t option)
+  -> t
+  -> (t * new_eqs) SatUnsat.t
 (** [simplify ~keep phi] attempts to get rid of as many variables in [fv phi] but not in [keep] as
     possible *)
 
+val simplify_instanceof : Tenv.t -> get_dynamic_type:(AbstractValue.t -> Typ.t option) -> t -> t
+
 val and_callee :
      (AbstractValue.t * ValueHistory.t) AbstractValue.Map.t
   -> t
@@ -73,7 +80,8 @@ val is_known_not_equal_zero : t -> AbstractValue.t -> bool
 val is_unsat_cheap : t -> bool
 (** whether the state contains a contradiction, call this as often as you want *)
 
-val is_unsat_expensive : t -> t * bool * new_eqs
+val is_unsat_expensive :
+  Tenv.t -> get_dynamic_type:(AbstractValue.t -> Typ.t option) -> t -> t * bool * new_eqs
   [@@warning "-32"]
 (** whether the state contains a contradiction, only call this when you absolutely have to *)
 
diff --git a/infer/src/pulse/PulseReport.ml b/infer/src/pulse/PulseReport.ml
index 4d1bd8f1b..49f569470 100644
--- a/infer/src/pulse/PulseReport.ml
+++ b/infer/src/pulse/PulseReport.ml
@@ -31,7 +31,7 @@ let report_latent_issue proc_desc err_log latent_issue =
   report ~extra_trace proc_desc err_log diagnostic
 
 
-let suppress_error proc_desc tenv diagnostic =
+let suppress_error tenv proc_desc diagnostic =
   match Procdesc.get_proc_name proc_desc with
   | Procname.Java jn
     when (not Config.pulse_nullsafe_report_npe)
@@ -42,11 +42,11 @@ let suppress_error proc_desc tenv diagnostic =
       false
 
 
-let report_error proc_desc tenv err_log access_result =
+let report_error tenv proc_desc err_log access_result =
   let open SatUnsat.Import in
   Result.map_error access_result ~f:(fun (diagnostic, astate) ->
-      let+ astate_summary = AbductiveDomain.summary_of_post proc_desc astate in
-      let is_suppressed = suppress_error proc_desc tenv diagnostic in
+      let+ astate_summary = AbductiveDomain.summary_of_post tenv proc_desc astate in
+      let is_suppressed = suppress_error tenv proc_desc diagnostic in
       match LatentIssue.should_report_diagnostic astate_summary diagnostic with
       | `ReportNow ->
           if not is_suppressed then report proc_desc err_log diagnostic ;
@@ -66,9 +66,9 @@ let exec_list_of_list_result = function
       [post]
 
 
-let report_list_result {InterproceduralAnalysis.proc_desc; tenv; err_log} result =
+let report_list_result {tenv; InterproceduralAnalysis.proc_desc; err_log} result =
   let open Result.Monad_infix in
-  report_error proc_desc tenv err_log result
+  report_error tenv proc_desc err_log result
   >>| List.map ~f:(fun post -> ExecutionDomain.ContinueProgram post)
   |> exec_list_of_list_result
 
@@ -82,6 +82,6 @@ let post_of_report_result = function
       Some post
 
 
-let report_results {InterproceduralAnalysis.proc_desc; tenv; err_log} results =
+let report_results {tenv; InterproceduralAnalysis.proc_desc; err_log} results =
   List.filter_map results ~f:(fun exec_result ->
-      report_error proc_desc tenv err_log exec_result |> post_of_report_result )
+      report_error tenv proc_desc err_log exec_result |> post_of_report_result )
diff --git a/infer/src/pulse/PulseSummary.ml b/infer/src/pulse/PulseSummary.ml
index ac9b02c0b..65deaf692 100644
--- a/infer/src/pulse/PulseSummary.ml
+++ b/infer/src/pulse/PulseSummary.ml
@@ -19,4 +19,4 @@ let pp fmt summary =
   F.close_box ()
 
 
-let of_posts pdesc posts = ExecutionDomain.summary_of_posts pdesc posts
+let of_posts tenv pdesc posts = ExecutionDomain.summary_of_posts tenv pdesc posts
diff --git a/infer/src/pulse/PulseSummary.mli b/infer/src/pulse/PulseSummary.mli
index 1d648fd61..00733f818 100644
--- a/infer/src/pulse/PulseSummary.mli
+++ b/infer/src/pulse/PulseSummary.mli
@@ -10,6 +10,6 @@ open PulseDomainInterface
 
 type t = ExecutionDomain.summary list [@@deriving yojson_of]
 
-val of_posts : Procdesc.t -> ExecutionDomain.t list -> t
+val of_posts : Tenv.t -> Procdesc.t -> ExecutionDomain.t list -> t
 
 val pp : Format.formatter -> t -> unit
diff --git a/infer/src/pulse/PulseTopl.ml b/infer/src/pulse/PulseTopl.ml
index f4d9815f7..aecd5eed8 100644
--- a/infer/src/pulse/PulseTopl.ml
+++ b/infer/src/pulse/PulseTopl.ml
@@ -359,9 +359,14 @@ let is_unsat_cheap path_condition pruned =
   PathCondition.is_unsat_cheap (Constraint.prune_path pruned path_condition)
 
 
+let dummy_tenv = Tenv.create ()
+
 let is_unsat_expensive path_condition pruned =
   let _path_condition, unsat, _new_eqs =
-    PathCondition.is_unsat_expensive (Constraint.prune_path pruned path_condition)
+    (* Not enabling dynamic type reasoning in TOPL for now *)
+    PathCondition.is_unsat_expensive dummy_tenv
+      ~get_dynamic_type:(fun _ -> None)
+      (Constraint.prune_path pruned path_condition)
   in
   unsat
 
diff --git a/infer/src/pulse/PulseTopl.mli b/infer/src/pulse/PulseTopl.mli
index 755563690..a39195d75 100644
--- a/infer/src/pulse/PulseTopl.mli
+++ b/infer/src/pulse/PulseTopl.mli
@@ -23,7 +23,7 @@ val small_step : Location.t -> PulsePathCondition.t -> event -> state -> state
 val large_step :
      call_location:Location.t
   -> callee_proc_name:Procname.t
-  -> substitution:(PulseAbstractValue.t * PulseValueHistory.t) PulseAbstractValue.Map.t
+  -> substitution:(value * PulseValueHistory.t) PulseAbstractValue.Map.t
   -> condition:PulsePathCondition.t
   -> callee_prepost:state
   -> state
diff --git a/infer/src/pulse/unit/PulseFormulaTest.ml b/infer/src/pulse/unit/PulseFormulaTest.ml
index fad20b4a3..5e58f4303 100644
--- a/infer/src/pulse/unit/PulseFormulaTest.ml
+++ b/infer/src/pulse/unit/PulseFormulaTest.ml
@@ -122,9 +122,19 @@ let test ~f phi =
   phi ttrue >>= f >>| fst |> F.printf "%a" normalized_pp
 
 
-let normalize phi = test ~f:normalize phi
+let dummy_tenv = Tenv.create ()
+
+let dummy_get_dynamic_type _ = None
+
+let normalize phi = test ~f:(normalize dummy_tenv ~get_dynamic_type:dummy_get_dynamic_type) phi
+
+let simplify ~keep phi =
+  test
+    ~f:
+      (simplify dummy_tenv ~get_dynamic_type:dummy_get_dynamic_type
+         ~keep:(AbstractValue.Set.of_list keep))
+    phi
 
-let simplify ~keep phi = test ~f:(simplify ~keep:(AbstractValue.Set.of_list keep)) phi
 
 let%test_module "normalization" =
   ( module struct
diff --git a/infer/tests/codetoanalyze/java/pulse/InstanceOfExample.java b/infer/tests/codetoanalyze/java/pulse/InstanceOfExample.java
index a94af95de..1cbf623e2 100644
--- a/infer/tests/codetoanalyze/java/pulse/InstanceOfExample.java
+++ b/infer/tests/codetoanalyze/java/pulse/InstanceOfExample.java
@@ -4,6 +4,9 @@
  * This source code is licensed under the MIT license found in the
  * LICENSE file in the root directory of this source tree.
  */
+
+import java.util.*;
+
 public class InstanceOfExample {
   abstract class Person {}
 
@@ -28,48 +31,86 @@ public class InstanceOfExample {
       new_p = p;
     }
 
-    if (p instanceof Professor) {
-      new_p = null;
-    }
-
     return new_p;
   }
 
-  public void FP_testInstanceOfObjProfessorOk() {
-    Person p = new Professor();
+  public void testInstanceOfObjStudentOk() {
+    Person p = new Student();
     if (p instanceof Student) {
-      String x = updatePerson(p).toString();
+      Person x = updatePerson(p);
+      x.toString();
     }
   }
 
-  public void FP_testInstanceOfObjStudentOk() {
-    Person p = new Student();
+  public void testInstanceOfObjProfessorBad() {
+    Person p = new Professor();
     Person new_p = updatePerson(p);
     new_p.toString();
   }
 
-  public Object checkInstanceArray(Object array) {
+  public void testInstanceOfObjProfessorOk() {
+    Person p = new Professor();
+    if (p instanceof Student) {
+      Person new_p = updatePerson(p);
+      new_p.toString();
+    }
+  }
+
+  public void testInstanceOfNullOk() {
+    Person p = new Professor();
+    // p is null after this call
+    p = updatePerson(p);
+    // null is not an instance of any class
+    if (p instanceof Professor) {
+      p.toString();
+    }
+  }
+
+  public void checkInstanceArray(Object array) {
     Object o = null;
-    if (array instanceof boolean[]) {
+    if (array instanceof int[]) {
       o = new Object();
     }
 
-    if (array instanceof int[]) {
+    if (array instanceof boolean[]) {
       o.toString();
     }
-
-    return o;
   }
 
-  public void FN_testInstanceOfArrayIntBad() {
+  public void testInstanceOfIntArrayOk() {
     int arr[] = new int[10];
     checkInstanceArray(arr);
   }
 
-  public void testInstanceOfNullOk() {
-    Student s = null;
-    if (s instanceof Student) {
-      s.toString();
+  public void testInstanceOfBooleanArrayBad() {
+    boolean arr[] = new boolean[10];
+    checkInstanceArray(arr);
+  }
+
+  public List<Integer> createsEmptyList() {
+    return new ArrayList<Integer>();
+  }
+
+  public void testInstanceOfArrayListOk() {
+    List<Integer> elems = createsEmptyList();
+    Person p = null;
+    if (elems instanceof ArrayList) {
+      p = new Student();
     }
+    p.toString();
+  }
+
+  public String getClassByName(Object o) {
+    return o.getClass().getName();
+  }
+
+  /*
+   * This example triggers a call to instanceof with a Var expression instead of a literal type.
+   * This only happens in some peculiar cases. For instance, if we inline the getClassByName call
+   * we don't have this problem. For now, we do not handle this example properly but we hope to
+   * investigate soon.
+   */
+  public void requiresFurtherInvestigationOk(List<Person> people) {
+    people.stream().filter(p -> getClassByName(p).equals("Student") && p instanceof Student);
   }
 }
diff --git a/infer/tests/codetoanalyze/java/pulse/issues.exp b/infer/tests/codetoanalyze/java/pulse/issues.exp
index 6138e2be9..6120fba98 100644
--- a/infer/tests/codetoanalyze/java/pulse/issues.exp
+++ b/infer/tests/codetoanalyze/java/pulse/issues.exp
@@ -14,8 +14,9 @@ codetoanalyze/java/pulse/DynamicDispatch.java, codetoanalyze.java.infer.DynamicD
 codetoanalyze/java/pulse/DynamicDispatch.java, codetoanalyze.java.infer.DynamicDispatch.dynamicDispatchShouldNotCauseFalseNegativeEasyBad():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Object DynamicDispatch$Subtype.foo()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object DynamicDispatch$Subtype.foo()`,return from call to `Object DynamicDispatch$Subtype.foo()`,assigned,invalid access occurs here]
 codetoanalyze/java/pulse/DynamicDispatch.java, codetoanalyze.java.infer.DynamicDispatch.dynamicResolutionWithVariadicMethodBad():void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Object DynamicDispatch.variadicMethod(DynamicDispatch$Supertype[])` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object DynamicDispatch.variadicMethod(DynamicDispatch$Supertype[])`,return from call to `Object DynamicDispatch.variadicMethod(DynamicDispatch$Supertype[])`,assigned,invalid access occurs here]
 codetoanalyze/java/pulse/DynamicDispatch.java, codetoanalyze.java.infer.DynamicDispatch.interfaceShouldNotCauseFalseNegativeEasyBad():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Object DynamicDispatch$Impl.foo()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `Object DynamicDispatch$Impl.foo()`,return from call to `Object DynamicDispatch$Impl.foo()`,assigned,invalid access occurs here]
-codetoanalyze/java/pulse/InstanceOfExample.java, InstanceOfExample.FP_testInstanceOfObjProfessorOk():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `InstanceOfExample$Person InstanceOfExample.updatePerson(InstanceOfExample$Person)` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `InstanceOfExample$Person InstanceOfExample.updatePerson(InstanceOfExample$Person)`,return from call to `InstanceOfExample$Person InstanceOfExample.updatePerson(InstanceOfExample$Person)`,assigned,invalid access occurs here]
-codetoanalyze/java/pulse/InstanceOfExample.java, InstanceOfExample.FP_testInstanceOfObjStudentOk():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `InstanceOfExample$Person InstanceOfExample.updatePerson(InstanceOfExample$Person)` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `InstanceOfExample$Person InstanceOfExample.updatePerson(InstanceOfExample$Person)`,return from call to `InstanceOfExample$Person InstanceOfExample.updatePerson(InstanceOfExample$Person)`,assigned,invalid access occurs here]
+codetoanalyze/java/pulse/InstanceOfExample.java, InstanceOfExample.checkInstanceArray(java.lang.Object):void, 7, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
+codetoanalyze/java/pulse/InstanceOfExample.java, InstanceOfExample.testInstanceOfBooleanArrayBad():void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [calling context starts here,in call to `void InstanceOfExample.checkInstanceArray(Object)`,invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
+codetoanalyze/java/pulse/InstanceOfExample.java, InstanceOfExample.testInstanceOfObjProfessorBad():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `InstanceOfExample$Person InstanceOfExample.updatePerson(InstanceOfExample$Person)` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `InstanceOfExample$Person InstanceOfExample.updatePerson(InstanceOfExample$Person)`,return from call to `InstanceOfExample$Person InstanceOfExample.updatePerson(InstanceOfExample$Person)`,assigned,invalid access occurs here]
 codetoanalyze/java/pulse/IntegerExample.java, codetoanalyze.java.infer.IntegerExample.FP_testIntegerBuiltInEqualOperatorCachedValuesOk():void, 19, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
 codetoanalyze/java/pulse/IntegerExample.java, codetoanalyze.java.infer.IntegerExample.testIntegerBuiltInEqualOperatorNonCachedValuesBad():void, 7, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
 codetoanalyze/java/pulse/IntegerExample.java, codetoanalyze.java.infer.IntegerExample.testIntegerEqualsMethodBad():void, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]