diff --git a/infer/src/pulse/PulseFormula.ml b/infer/src/pulse/PulseFormula.ml
index 7e8c6a498..350881517 100644
--- a/infer/src/pulse/PulseFormula.ml
+++ b/infer/src/pulse/PulseFormula.ml
@@ -448,10 +448,20 @@ module Term = struct
     fold_map_direct_subterms t ~init:() ~f:(fun () t' -> ((), f t')) |> snd
 
 
-  let rec map_subterms t ~f =
-    let t' = map_direct_subterms t ~f:(fun t' -> map_subterms t' ~f) in
-    f t'
+  let rec fold_map_subterms t ~init ~f =
+    let acc, t' =
+      fold_map_direct_subterms t ~init ~f:(fun acc t' -> fold_map_subterms t' ~init:acc ~f)
+    in
+    f acc t'
+
+
+  let fold_subterms t ~init ~f = fold_map_subterms t ~init ~f:(fun acc t' -> (f acc t', t')) |> fst
 
+  let map_subterms t ~f = fold_map_subterms t ~init:() ~f:(fun () t' -> ((), f t')) |> snd
+
+  let iter_subterms t ~f = Container.iter ~fold:fold_subterms t ~f
+
+  let exists_subterm t ~f = Container.exists ~iter:iter_subterms t ~f
 
   let rec fold_subst_variables t ~init ~f =
     match t with
@@ -1075,7 +1085,9 @@ module Formula = struct
     { var_eqs: var_eqs  (** equality relation between variables *)
     ; linear_eqs: linear_eqs
           (** equalities of the form [x = l] where [l] is from linear arithmetic *)
-    ; term_eqs: Term.VarMap.t_  (** equalities of the form [t = x] *)
+    ; term_eqs: Term.VarMap.t_
+          (** equalities of the form [t = x], used to detect when two abstract values are equal to
+              the same term (hence equal) *)
     ; atoms: Atom.Set.t  (** "everything else"; not always normalized w.r.t. the components above *)
     }
   [@@deriving compare, equal, yojson_of]
@@ -1107,6 +1119,8 @@ module Formula = struct
   module Normalizer : sig
     val and_var_linarith : Var.t -> LinArith.t -> t * new_eqs -> (t * new_eqs) SatUnsat.t
 
+    val and_var_term : Var.t -> Term.t -> t * new_eqs -> (t * new_eqs) SatUnsat.t
+
     val and_var_var : Var.t -> Var.t -> t * new_eqs -> (t * new_eqs) SatUnsat.t
 
     val and_atom : Atom.t -> t * new_eqs -> (t * new_eqs) SatUnsat.t
@@ -1151,7 +1165,7 @@ module Formula = struct
 
     (** substitute vars in [l] *once* with their linear form to discover more simplification
         opportunities *)
-    let apply phi l =
+    let normalize_linear phi l =
       LinArith.subst_variables l ~f:(fun v ->
           let repr = (get_repr phi v :> Var.t) in
           match Var.Map.find_opt repr phi.linear_eqs with
@@ -1161,6 +1175,22 @@ module Formula = struct
               LinSubst l' )
 
 
+    let normalize_var_const phi t =
+      Term.subst_variables t ~f:(fun v ->
+          let v_canon = (get_repr phi v :> Var.t) in
+          match Var.Map.find_opt v_canon phi.linear_eqs with
+          | None ->
+              VarSubst v_canon
+          | Some l -> (
+            match LinArith.get_as_const l with
+            | None ->
+                (* OPTIM: don't make the term bigger *) VarSubst v_canon
+            | Some q ->
+                (* replace vars by constants when available to possibly trigger further
+                   simplifications in atoms. This is not actually needed for [term_eqs]. *)
+                QSubst q ) )
+
+
     let add_lin_eq_to_new_eqs v l new_eqs =
       match LinArith.get_as_const l with
       | Some q when Q.is_zero q ->
@@ -1169,6 +1199,9 @@ module Formula = struct
           new_eqs
 
 
+    (** add [l1 = l2] to [phi.linear_eqs] and resolves consequences of that new fact
+
+        [l1] and [l2] should have already been through {!normalize_linear} (w.r.t. [phi]) *)
     let rec solve_normalized_lin_eq ~fuel new_eqs l1 l2 phi =
       LinArith.solve_eq l1 l2
       >>= function
@@ -1181,10 +1214,14 @@ module Formula = struct
         | None -> (
           match Var.Map.find_opt (v :> Var.t) phi.linear_eqs with
           | None ->
+              (* add to the [term_eqs] relation only when we also add to [linear_eqs] *)
+              let+ phi, new_eqs =
+                solve_normalized_term_eq_no_lin ~fuel new_eqs (Term.Linear l) (v :> Var.t) phi
+              in
               let new_eqs = add_lin_eq_to_new_eqs v l new_eqs in
               (* this can break the (as a result non-)invariant that variables in the domain of
                  [linear_eqs] do not appear in the range of [linear_eqs] *)
-              Sat ({phi with linear_eqs= Var.Map.add (v :> Var.t) l phi.linear_eqs}, new_eqs)
+              ({phi with linear_eqs= Var.Map.add (v :> Var.t) l phi.linear_eqs}, new_eqs)
           | Some l' ->
               (* This is the only step that consumes fuel: discovering an equality [l = l']: because we
                  do not record these anywhere (except when their consequence can be recorded as [y =
@@ -1192,7 +1229,7 @@ module Formula = struct
                  diverge otherwise. Or could we? *)
               (* [l'] is possibly not normalized w.r.t. the current [phi] so take this opportunity to
                  normalize it, and replace [v]'s current binding *)
-              let l'' = apply phi l' in
+              let l'' = normalize_linear phi l' in
               let phi =
                 if phys_equal l' l'' then phi
                 else {phi with linear_eqs= Var.Map.add (v :> Var.t) l'' phi.linear_eqs}
@@ -1206,6 +1243,72 @@ module Formula = struct
                 Sat (phi, new_eqs) ) ) )
 
 
+    (** add [t = v] to [phi.term_eqs] and resolves consequences of that new fact; don't use directly
+        as it doesn't do any checks on what else should be done about [t = v] *)
+    and solve_normalized_term_eq_no_lin_ ~fuel new_eqs t v phi =
+      match Term.VarMap.find_opt t phi.term_eqs with
+      | None ->
+          (* [t] isn't known already: add it *)
+          Sat ({phi with term_eqs= Term.VarMap.add t v phi.term_eqs}, new_eqs)
+      | Some v' ->
+          (* [t = v'] already in the map, need to explore consequences of [v = v']*)
+          merge_vars ~fuel new_eqs v v' phi
+
+
+    (** add [t = v] to [phi.term_eqs] and resolves consequences of that new fact; assumes that
+        linear facts have been or will be added to [phi.linear_eqs] separately
+
+        [t] should have already been through {!normalize_var_const} and [v] should be a
+        representative from {!get_repr} (w.r.t. [phi]) *)
+    and solve_normalized_term_eq_no_lin ~fuel new_eqs (t : Term.t) v phi =
+      match t with
+      | Linear l when LinArith.get_as_var l |> Option.is_some ->
+          (* [v1=v2] is already taken care of by [var_eqs] *)
+          Sat (phi, new_eqs)
+      | _ ->
+          let t =
+            match t with
+            | Linear l -> (
+              match LinArith.get_as_const l with Some c -> Term.Const c | None -> t )
+            | _ ->
+                t
+          in
+          solve_normalized_term_eq_no_lin_ ~fuel new_eqs t v phi
+
+
+    (** same as {!solve_normalized_eq_no_lin} but also adds linear to [phi.linear_eqs] *)
+    and solve_normalized_term_eq ~fuel new_eqs (t : Term.t) v phi =
+      match t with
+      | Linear l when LinArith.get_as_var l |> Option.is_some ->
+          (* [v1=v2] is already taken care of by [var_eqs] *)
+          Sat (phi, new_eqs)
+      | Linear l -> (
+          (* [l = v]: need to first solve it to get [l' = v'] such that [v' < vars(l')], and [l'] is
+             normalized wrt [phi.linear_eqs] (to get a canonical form), add this to [term_eqs], then
+             in order to know which equality should be added to [linear_eqs] we still need to
+             substitute [v'] with [linear_eqs] and solve again *)
+          LinArith.solve_eq (normalize_linear phi l) (LinArith.of_var v)
+          >>= function
+          | None ->
+              (* [v = v], we can drop this tautology *)
+              Sat (phi, new_eqs)
+          | Some (v', l') ->
+              (* [l'] could contain [v], which hasn't been through [linear_eqs], so normalize again *)
+              let l' = normalize_linear phi l' in
+              let* phi, new_eqs =
+                solve_normalized_term_eq_no_lin_ ~fuel new_eqs (Term.Linear l') v' phi
+              in
+              solve_normalized_lin_eq ~fuel new_eqs l'
+                (normalize_linear phi (LinArith.of_var v'))
+                phi )
+      | Const c ->
+          (* same as above but constants ([c]) are always normalized so it's simpler *)
+          let* phi, new_eqs = solve_normalized_term_eq_no_lin_ ~fuel new_eqs t v phi in
+          solve_normalized_lin_eq ~fuel new_eqs (LinArith.of_q c) (LinArith.of_var v) phi
+      | _ ->
+          solve_normalized_term_eq_no_lin ~fuel new_eqs t v phi
+
+
     and merge_vars ~fuel new_eqs v1 v2 phi =
       let var_eqs, subst_opt = VarUF.union phi.var_eqs v1 v2 in
       let phi = {phi with var_eqs} in
@@ -1262,7 +1365,8 @@ module Formula = struct
     let base_fuel = 10
 
     let solve_lin_eq new_eqs t1 t2 phi =
-      solve_normalized_lin_eq ~fuel:base_fuel new_eqs (apply phi t1) (apply phi t2) phi
+      solve_normalized_lin_eq ~fuel:base_fuel new_eqs (normalize_linear phi t1)
+        (normalize_linear phi t2) phi
 
 
     let and_var_linarith v l (phi, new_eqs) = solve_lin_eq new_eqs l (LinArith.of_var v) phi
@@ -1271,7 +1375,7 @@ module Formula = struct
       Var.Map.fold
         (fun v l acc ->
           let* changed, ((_, new_eqs) as phi_new_eqs) = acc in
-          let l' = apply phi0 l in
+          let l' = normalize_linear phi0 l in
           let+ phi', new_eqs' = and_var_linarith v l' phi_new_eqs in
           let changed', new_eqs' =
             if phys_equal l l' then (changed, new_eqs) else (true, new_eqs')
@@ -1282,19 +1386,33 @@ module Formula = struct
 
 
     let normalize_atom phi (atom : Atom.t) =
-      let normalize_term phi t =
-        Term.subst_variables t ~f:(fun v ->
-            let v_canon = (get_repr phi v :> Var.t) in
-            match Var.Map.find_opt v_canon phi.linear_eqs with
-            | None ->
-                VarSubst v_canon
-            | Some l -> (
-              match LinArith.get_as_const l with None -> LinSubst l | Some q -> QSubst q ) )
-      in
-      let atom' = Atom.map_terms atom ~f:(fun t -> normalize_term phi t) in
+      let atom' = Atom.map_terms atom ~f:(fun t -> normalize_var_const phi t) in
       Atom.eval atom' |> sat_of_eval_result
 
 
+    let and_var_term ~fuel v t (phi, new_eqs) =
+      let t' : Term.t = normalize_var_const phi t |> Atom.eval_term in
+      let v' = (get_repr phi v :> Var.t) in
+      (* check if unsat given what we know of [v'] and [t'], in other words be at least as
+         complete as general atoms *)
+      let* _ = Atom.eval (Equal (t', normalize_var_const phi (Var v'))) |> sat_of_eval_result in
+      solve_normalized_term_eq ~fuel new_eqs t' v' phi
+
+
+    let normalize_term_eqs (phi0, new_eqs0) =
+      Term.VarMap.fold
+        (fun t v acc_sat_unsat ->
+          let* new_lin, ((_phi, new_eqs) as phi_new_eqs) = acc_sat_unsat in
+          let+ phi', new_eqs' = and_var_term ~fuel:base_fuel v t phi_new_eqs in
+          let new_lin, new_eqs' =
+            if phys_equal phi'.linear_eqs phi0.linear_eqs then (new_lin, new_eqs)
+            else (true, new_eqs')
+          in
+          (new_lin, (phi', new_eqs')) )
+        phi0.term_eqs
+        (Sat (false, ({phi0 with term_eqs= Term.VarMap.empty}, new_eqs0)))
+
+
     (** return [(new_linear_equalities, phi ∧ atom)], where [new_linear_equalities] is [true] if
         [phi.linear_eqs] was changed as a result *)
     let and_atom atom (phi, new_eqs) =
@@ -1302,12 +1420,19 @@ module Formula = struct
       >>= function
       | None ->
           Sat (false, (phi, new_eqs))
+      | Some (Atom.Equal (Linear _, Linear _)) ->
+          assert false
       | Some (Atom.Equal (Linear l, Const c)) | Some (Atom.Equal (Const c, Linear l)) ->
           (* NOTE: {!normalize_atom} calls {!Atom.eval}, which normalizes linear equalities so
              they end up only on one side, hence only this match case is needed to detect linear
              equalities *)
           let+ phi', new_eqs = solve_lin_eq new_eqs l (LinArith.of_q c) phi in
           (true, (phi', new_eqs))
+      | Some (Atom.Equal (Linear l, t) | Atom.Equal (t, Linear l))
+        when Option.is_some (LinArith.get_as_var l) ->
+          let v = Option.value_exn (LinArith.get_as_var l) in
+          let+ phi_new_eqs' = solve_normalized_term_eq ~fuel:base_fuel new_eqs t v phi in
+          (false, phi_new_eqs')
       | Some atom' ->
           Sat (false, ({phi with atoms= Atom.Set.add atom' phi.atoms}, new_eqs))
 
@@ -1321,22 +1446,23 @@ module Formula = struct
           (changed || changed', phi_new_eqs) )
 
 
-    let rec normalize_with_fuel ~fuel ((phi0, new_eqs0) as phi_new_eqs0) =
+    let rec normalize_with_fuel ~fuel phi_new_eqs0 =
       if fuel < 0 then (
         L.d_printfln "ran out of fuel when normalizing" ;
         Sat phi_new_eqs0 )
       else
-        (* reconstruct the linear relation from scratch *)
         let* new_linear_eqs, phi_new_eqs' =
-          let* new_linear_eqs_from_linear, phi_new_eqs = normalize_linear_eqs (phi0, new_eqs0) in
+          let* new_linear_eqs_from_linear, phi_new_eqs = normalize_linear_eqs phi_new_eqs0 in
           if new_linear_eqs_from_linear && fuel > 0 then
             (* do another round of linear normalization early if we will renormalize again anyway;
-               no need to first normalize atoms w.r.t. a linear relation that's going to change and
-               trigger a recompute of these anyway *)
+               no need to first normalize term_eqs and atoms w.r.t. a linear relation that's going
+               to change and trigger a recompute of these anyway *)
             Sat (true, phi_new_eqs)
           else
+            let* new_linear_eqs_from_terms, phi_new_eqs = normalize_term_eqs phi_new_eqs in
             let+ new_linear_eqs_from_atoms, phi_new_eqs = normalize_atoms phi_new_eqs in
-            (new_linear_eqs_from_linear || new_linear_eqs_from_atoms, phi_new_eqs)
+            ( new_linear_eqs_from_linear || new_linear_eqs_from_terms || new_linear_eqs_from_atoms
+            , phi_new_eqs )
         in
         if new_linear_eqs then (
           L.d_printfln "new linear equalities, consuming fuel (from %d)" fuel ;
@@ -1350,6 +1476,8 @@ module Formula = struct
 
     let and_atom atom phi_new_eqs = and_atom atom phi_new_eqs >>| snd
 
+    let and_var_term v t phi_new_eqs = and_var_term ~fuel:base_fuel v t phi_new_eqs
+
     let and_var_var v1 v2 (phi, new_eqs) = merge_vars ~fuel:base_fuel new_eqs v1 v2 phi
 
     let implies_atom phi atom =
@@ -1455,6 +1583,21 @@ module DynamicTypes = struct
           t
     in
     let changed = ref false in
+    let term_eqs =
+      if
+        Term.VarMap.exists
+          (fun t _ -> Term.exists_subterm t ~f:(function IsInstanceOf _ -> true | _ -> false))
+          phi.both.term_eqs
+      then
+        (* slow path: reconstruct everything *)
+        Term.VarMap.fold
+          (fun t v term_eqs' ->
+            let t' = Term.map_subterms t ~f:simplify_is_instance_of in
+            changed := !changed || not (phys_equal t t') ;
+            Term.VarMap.add t' v term_eqs' )
+          phi.both.term_eqs Term.VarMap.empty
+      else (* fast path: nothing to do *) phi.both.term_eqs
+    in
     let atoms =
       Atom.Set.map
         (fun atom ->
@@ -1464,7 +1607,7 @@ module DynamicTypes = struct
               t' ) )
         phi.both.atoms
     in
-    if !changed then {phi with both= {phi.both with atoms}} else phi
+    if !changed then {phi with both= {phi.both with atoms; term_eqs}} else phi
 end
 
 let normalize tenv ~get_dynamic_type phi =
@@ -1517,6 +1660,14 @@ let and_fold_subst_variables phi0 ~up_to_f:phi_foreign ~init ~f:f_var =
         let phi_new_eqs = Formula.Normalizer.and_var_linarith v l phi_new_eqs |> sat_value_exn in
         (acc_f, phi_new_eqs) )
   in
+  let and_term_eqs term_eqs_foreign acc_phi_new_eqs =
+    IContainer.fold_of_pervasives_map_fold Term.VarMap.fold term_eqs_foreign ~init:acc_phi_new_eqs
+      ~f:(fun (acc_f, phi_new_eqs) (t_foreign, v_foreign) ->
+        let acc_f, t = Term.fold_subst_variables t_foreign ~init:acc_f ~f:f_subst in
+        let acc_f, v = f_var acc_f v_foreign in
+        let phi_new_eqs = Formula.Normalizer.and_var_term v t phi_new_eqs |> sat_value_exn in
+        (acc_f, phi_new_eqs) )
+  in
   let and_atoms atoms_foreign acc_phi_new_eqs =
     IContainer.fold_of_pervasives_set_fold Atom.Set.fold atoms_foreign ~init:acc_phi_new_eqs
       ~f:(fun (acc_f, phi_new_eqs) atom_foreign ->
@@ -1529,6 +1680,7 @@ let and_fold_subst_variables phi0 ~up_to_f:phi_foreign ~init ~f:f_var =
       Sat
         ( and_var_eqs phi_foreign.Formula.var_eqs (acc, (phi, []))
         |> and_linear_eqs phi_foreign.Formula.linear_eqs
+        |> and_term_eqs phi_foreign.Formula.term_eqs
         |> and_atoms phi_foreign.Formula.atoms )
     with Contradiction -> Unsat
   in
@@ -1637,15 +1789,18 @@ module DeadVariables = struct
         |> Seq.fold_left (fun vs v -> Var.Set.add v vs) (Var.Set.singleton v)
         |> add_all )
       phi.Formula.linear_eqs ;
+    (* helper function: compute [vs U vars(t)] *)
+    let union_vars_of_term t vs =
+      Term.fold_variables t ~init:vs ~f:(fun vs v -> Var.Set.add v vs)
+    in
     (* add edges between all pairs of variables appearing in [t1] or [t2] (yes this is quadratic in
        the number of variables of these terms) *)
     let add_from_terms t1 t2 =
-      (* compute [vs U vars(t)] *)
-      let union_vars_of_term t vs =
-        Term.fold_variables t ~init:vs ~f:(fun vs v -> Var.Set.add v vs)
-      in
       union_vars_of_term t1 Var.Set.empty |> union_vars_of_term t2 |> add_all
     in
+    Term.VarMap.iter
+      (fun t v -> union_vars_of_term t (Var.Set.singleton v) |> add_all)
+      phi.Formula.term_eqs ;
     Atom.Set.iter
       (fun atom ->
         let t1, t2 = Atom.get_terms atom in
@@ -1693,7 +1848,7 @@ module DeadVariables = struct
        result. *)
     let var_graph = build_var_graph phi.both in
     let vars_to_keep = get_reachable_from var_graph keep in
-    L.d_printfln "Reachable vars: {%a}" Var.Set.pp vars_to_keep ;
+    L.d_printfln "Reachable vars: %a" Var.Set.pp vars_to_keep ;
     (* discard atoms which have variables *not* in [vars_to_keep], which in particular is enough
        to guarantee that *none* of their variables are in [vars_to_keep] thanks to transitive
        closure on the graph above *)
@@ -1720,12 +1875,13 @@ end
 let simplify tenv ~get_dynamic_type ~keep phi =
   let open SatUnsat.Import 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 ;
+  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
   (* TODO: doing [QuantifierElimination.eliminate_vars; DeadVariables.eliminate] a few times may
      eliminate even more variables *)
-  (DeadVariables.eliminate ~keep phi, new_eqs)
+  let phi = DeadVariables.eliminate ~keep phi in
+  (phi, new_eqs)
 
 
 let is_known_zero phi v =
diff --git a/infer/src/pulse/unit/PulseFormulaTest.ml b/infer/src/pulse/unit/PulseFormulaTest.ml
index b4bd92247..5618ceaa2 100644
--- a/infer/src/pulse/unit/PulseFormulaTest.ml
+++ b/infer/src/pulse/unit/PulseFormulaTest.ml
@@ -176,9 +176,8 @@ let%test_module "normalization" =
       normalize (of_binop Eq x y = i 0 && x = i 0 && y = i 1) ;
       [%expect
         {|
-        known=true (no var=var) && x = 0 ∧ y = 1 ∧ v6 = 0 && true (no term_eqs) && true (no atoms),
-        pruned=true (no atoms),
-        both=true (no var=var) && x = 0 ∧ y = 1 ∧ v6 = 0 && true (no term_eqs) && true (no atoms)|}]
+        known=x=v6 && x = 0 ∧ y = 1 && 0=x∧1=y && true (no atoms), pruned=true (no atoms),
+        both=x=v6 && x = 0 ∧ y = 1 && 0=x∧1=y && true (no atoms)|}]
 
     let%expect_test _ =
       normalize (x = i 0 && x < i 0) ;
@@ -196,36 +195,36 @@ let%test_module "normalization" =
               &&
               x = -v6 + v8 -1 ∧ v7 = v8 -1 ∧ v10 = 0
               &&
-              true (no term_eqs)
+              0=v10∧[-v6 + v8 -1]=x∧[v8 -1]=v7∧[z]×[v8]=v9∧[v]×[y]=v6∧[v9]÷[w]=v10
               &&
-              {0 = [v9]÷[w]}∧{[v6] = [v]×[y]}∧{[v9] = [z]×[v8]},
+              true (no atoms),
         pruned=true (no atoms),
         both=true (no var=var)
              &&
              x = -v6 + v8 -1 ∧ v7 = v8 -1 ∧ v10 = 0
              &&
-             true (no term_eqs)
+             0=v10∧[-v6 + v8 -1]=x∧[v8 -1]=v7∧[z]×[v8]=v9∧[v]×[y]=v6∧[v9]÷[w]=v10
              &&
-             {0 = [v9]÷[w]}∧{[v6] = [v]×[y]}∧{[v9] = [z]×[v8]} |}]
+             true (no atoms) |}]
 
     (* check that this becomes all linear equalities *)
     let%expect_test _ =
       normalize (i 12 * (x + (i 3 * y) + i 1) / i 7 = i 0) ;
       [%expect
         {|
-        known=true (no var=var)
+        known=v8=v9=v10
               &&
-              x = -v6 -1 ∧ y = 1/3·v6 ∧ v7 = -1 ∧ v8 = 0 ∧ v9 = 0 ∧ v10 = 0
+              x = -v6 -1 ∧ y = 1/3·v6 ∧ v7 = -1 ∧ v8 = 0
               &&
-              true (no term_eqs)
+              -1=v7∧0=v8∧[-v6 -1]=x∧[1/3·v6]=y
               &&
               true (no atoms),
         pruned=true (no atoms),
-        both=true (no var=var)
+        both=v8=v9=v10
              &&
-             x = -v6 -1 ∧ y = 1/3·v6 ∧ v7 = -1 ∧ v8 = 0 ∧ v9 = 0 ∧ v10 = 0
+             x = -v6 -1 ∧ y = 1/3·v6 ∧ v7 = -1 ∧ v8 = 0
              &&
-             true (no term_eqs)
+             -1=v7∧0=v8∧[-v6 -1]=x∧[1/3·v6]=y
              &&
              true (no atoms)|}]
 
@@ -234,21 +233,19 @@ let%test_module "normalization" =
       normalize (z * (x + (v * y) + i 1) / w = i 0 && z = i 12 && v = i 3 && w = i 7) ;
       [%expect
         {|
-        known=true (no var=var)
+        known=v8=v9=v10
               &&
-              x = -v6 -1 ∧ y = 1/3·v6 ∧ z = 12 ∧ w = 7 ∧ v = 3 ∧ v7 = -1
-               ∧ v8 = 0 ∧ v9 = 0 ∧ v10 = 0
+              x = -v6 -1 ∧ y = 1/3·v6 ∧ z = 12 ∧ w = 7 ∧ v = 3 ∧ v7 = -1 ∧ v8 = 0
               &&
-              true (no term_eqs)
+              -1=v7∧0=v8∧3=v∧7=w∧12=z∧[-v6 -1]=x∧[1/3·v6]=y
               &&
               true (no atoms),
         pruned=true (no atoms),
-        both=true (no var=var)
+        both=v8=v9=v10
              &&
-             x = -v6 -1 ∧ y = 1/3·v6 ∧ z = 12 ∧ w = 7 ∧ v = 3 ∧ v7 = -1
-              ∧ v8 = 0 ∧ v9 = 0 ∧ v10 = 0
+             x = -v6 -1 ∧ y = 1/3·v6 ∧ z = 12 ∧ w = 7 ∧ v = 3 ∧ v7 = -1 ∧ v8 = 0
              &&
-             true (no term_eqs)
+             -1=v7∧0=v8∧3=v∧7=w∧12=z∧[-v6 -1]=x∧[1/3·v6]=y
              &&
              true (no atoms)|}]
   end )
@@ -266,31 +263,31 @@ let%test_module "variable elimination" =
       simplify ~keep:[x_var] (x = i 0 && y = i 1 && z = i 2 && w = i 3) ;
       [%expect
         {|
-        known=true (no var=var) && x = 0 && true (no term_eqs) && true (no atoms), pruned=true (no atoms),
-        both=true (no var=var) && x = 0 && true (no term_eqs) && true (no atoms)|}]
+        known=true (no var=var) && x = 0 && 0=x && true (no atoms), pruned=true (no atoms),
+        both=true (no var=var) && x = 0 && 0=x && true (no atoms)|}]
 
     let%expect_test _ =
       simplify ~keep:[x_var] (x = y + i 1 && x = i 0) ;
       [%expect
         {|
-          known=true (no var=var) && x = 0 && true (no term_eqs) && true (no atoms), pruned=true (no atoms),
-          both=true (no var=var) && x = 0 && true (no term_eqs) && true (no atoms)|}]
+          known=true (no var=var) && x = 0 && 0=x && true (no atoms), pruned=true (no atoms),
+          both=true (no var=var) && x = 0 && 0=x && true (no atoms)|}]
 
     let%expect_test _ =
       simplify ~keep:[y_var] (x = y + i 1 && x = i 0) ;
       [%expect
         {|
-        known=true (no var=var) && y = -1 && true (no term_eqs) && true (no atoms), pruned=true (no atoms),
-        both=true (no var=var) && y = -1 && true (no term_eqs) && true (no atoms)|}]
+        known=true (no var=var) && y = -1 && -1=y && true (no atoms), pruned=true (no atoms),
+        both=true (no var=var) && y = -1 && -1=y && true (no atoms)|}]
 
     (* should keep most of this or realize that [w = z] hence this boils down to [z+1 = 0] *)
     let%expect_test _ =
       simplify ~keep:[y_var; z_var] (x = y + z && w = x - y && v = w + i 1 && v = i 0) ;
       [%expect
         {|
-        known=true (no var=var) && x = y -1 ∧ z = -1 && true (no term_eqs) && true (no atoms),
+        known=true (no var=var) && x = y -1 ∧ z = -1 && -1=z∧[y -1]=x && true (no atoms),
         pruned=true (no atoms),
-        both=true (no var=var) && x = y -1 ∧ z = -1 && true (no term_eqs) && true (no atoms)|}]
+        both=true (no var=var) && x = y -1 ∧ z = -1 && -1=z∧[y -1]=x && true (no atoms)|}]
 
     let%expect_test _ =
       simplify ~keep:[x_var; y_var] (x = y + z && w + x + y = i 0 && v = w + i 1) ;
@@ -300,7 +297,7 @@ let%test_module "variable elimination" =
                 &&
                 x = -v + v7 +1 ∧ y = -v7 ∧ z = -v + 2·v7 +1 ∧ w = v -1
                 &&
-                true (no term_eqs)
+                [v -1]=w∧[-v7]=y∧[-v + v7 +1]=x∧[-v + 2·v7 +1]=z
                 &&
                 true (no atoms),
           pruned=true (no atoms),
@@ -308,7 +305,7 @@ let%test_module "variable elimination" =
                &&
                x = -v + v7 +1 ∧ y = -v7 ∧ z = -v + 2·v7 +1 ∧ w = v -1
                &&
-               true (no term_eqs)
+               [v -1]=w∧[-v7]=y∧[-v + v7 +1]=x∧[-v + 2·v7 +1]=z
                &&
                true (no atoms)|}]
 
@@ -316,8 +313,8 @@ let%test_module "variable elimination" =
       simplify ~keep:[x_var; y_var] (x = y + i 4 && x = w && y = z) ;
       [%expect
         {|
-        known=true (no var=var) && x = y +4 && true (no term_eqs) && true (no atoms),
-        pruned=true (no atoms), both=true (no var=var) && x = y +4 && true (no term_eqs) && true (no atoms)|}]
+        known=true (no var=var) && x = y +4 && [y +4]=x && true (no atoms), pruned=true (no atoms),
+        both=true (no var=var) && x = y +4 && [y +4]=x && true (no atoms)|}]
   end )
 
 let%test_module "non-linear simplifications" =
@@ -326,15 +323,15 @@ let%test_module "non-linear simplifications" =
       simplify ~keep:[w_var] (((i 0 / (x * z)) & v) * v mod y = w) ;
       [%expect
         {|
-        known=true (no var=var) && w = 0 && true (no term_eqs) && true (no atoms), pruned=true (no atoms),
-        both=true (no var=var) && w = 0 && true (no term_eqs) && true (no atoms)|}]
+        known=true (no var=var) && w = 0 && 0=w && true (no atoms), pruned=true (no atoms),
+        both=true (no var=var) && w = 0 && 0=w && true (no atoms)|}]
 
     let%expect_test "constant propagation: bitshift" =
       simplify ~keep:[x_var] (of_binop Shiftlt (of_binop Shiftrt (i 0b111) (i 2)) (i 2) = x) ;
       [%expect
         {|
-        known=true (no var=var) && x = 4 && true (no term_eqs) && true (no atoms), pruned=true (no atoms),
-        both=true (no var=var) && x = 4 && true (no term_eqs) && true (no atoms)|}]
+        known=true (no var=var) && x = 4 && 4=x && true (no atoms), pruned=true (no atoms),
+        both=true (no var=var) && x = 4 && 4=x && true (no atoms)|}]
 
     let%expect_test "non-linear becomes linear" =
       normalize (w = (i 2 * z) - i 3 && z = x * y && y = i 2) ;
@@ -344,7 +341,7 @@ let%test_module "non-linear simplifications" =
                 &&
                 x = 1/4·v6 ∧ y = 2 ∧ z = 1/2·v6 ∧ w = v6 -3
                 &&
-                true (no term_eqs)
+                2=y∧[v6 -3]=w∧[1/4·v6]=x∧[1/2·v6]=z
                 &&
                 true (no atoms),
           pruned=true (no atoms),
@@ -352,7 +349,7 @@ let%test_module "non-linear simplifications" =
                &&
                x = 1/4·v6 ∧ y = 2 ∧ z = 1/2·v6 ∧ w = v6 -3
                &&
-               true (no term_eqs)
+               2=y∧[v6 -3]=w∧[1/4·v6]=x∧[1/2·v6]=z
                &&
                true (no atoms)|}]
   end )
diff --git a/infer/tests/codetoanalyze/c/pulse/issues.exp b/infer/tests/codetoanalyze/c/pulse/issues.exp
index 0752afb80..3323f2c02 100644
--- a/infer/tests/codetoanalyze/c/pulse/issues.exp
+++ b/infer/tests/codetoanalyze/c/pulse/issues.exp
@@ -8,6 +8,7 @@ codetoanalyze/c/pulse/memory_leak.c, malloc_interproc_no_free_bad2, 4, MEMORY_LE
 codetoanalyze/c/pulse/memory_leak.c, malloc_no_free_bad, 0, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here]
 codetoanalyze/c/pulse/nullptr.c, FN_bug_after_malloc_result_test_bad, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here]
 codetoanalyze/c/pulse/nullptr.c, malloc_no_check_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,allocated by call to `malloc` (modelled),is the null pointer,null pointer dereference part of the trace starts here,allocated by call to `malloc` (modelled),assigned,invalid access occurs here]
+codetoanalyze/c/pulse/nullptr.c, malloc_then_call_create_null_path_then_deref_unconditionally_latent, 7, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,allocated by call to `malloc` (modelled),is the null pointer,null pointer dereference part of the trace starts here,parameter `p` of malloc_then_call_create_null_path_then_deref_unconditionally_latent,invalid access occurs here]
 codetoanalyze/c/pulse/nullptr.c, nullptr_deref_young_bad, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here]
 codetoanalyze/c/pulse/uninit.c, call_to_use_and_mayinit_bad, 2, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [variable `x` declared here,read to uninitialized value occurs here]
 codetoanalyze/c/pulse/uninit.c, dereference_bad, 2, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [variable `p` declared here,read to uninitialized value occurs here]
diff --git a/infer/tests/codetoanalyze/c/pulse/nullptr.c b/infer/tests/codetoanalyze/c/pulse/nullptr.c
index 953471b6a..7fed5bf07 100644
--- a/infer/tests/codetoanalyze/c/pulse/nullptr.c
+++ b/infer/tests/codetoanalyze/c/pulse/nullptr.c
@@ -37,7 +37,8 @@ void create_null_path2_ok(int* p) {
 }
 
 // combine several of the difficulties above
-void malloc_then_call_create_null_path_then_deref_unconditionally_ok(int* p) {
+void malloc_then_call_create_null_path_then_deref_unconditionally_latent(
+    int* p) {
   int* x = (int*)malloc(sizeof(int));
   if (p) {
     *p = 32;
@@ -59,7 +60,7 @@ void nullptr_deref_young_bad(int* x) {
 // due to the recency model of memory accesses, vec[0] can get forgotten
 // by the time we have processed the last element of the
 // initialization so we don't report here
-void nullptr_deref_old_bad_FP(int* x) {
+void FN_nullptr_deref_old_bad(int* x) {
   int* vec[65] = {NULL, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x,
                   x,    x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x,
                   x,    x, x, x, x, x, x, x, x, x, x, x, x, x, x, x, x,
diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp
index 877ef6390..6d0c9b1a6 100644
--- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp
+++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp
@@ -5,6 +5,7 @@ codetoanalyze/cpp/pulse/basic_string.cpp, use_range_of_invalidated_temporary_str
 codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_latent, 6, USE_AFTER_DELETE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_latent,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_latent,invalid access occurs here]
 codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_latent, 6, USE_AFTER_DELETE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_latent,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_latent,invalid access occurs here]
 codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_latent, 5, USE_AFTER_DELETE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_latent,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_latent,invalid access occurs here]
+codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_latent, 8, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_latent,invalid access occurs here]
 codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_latent, 8, USE_AFTER_DELETE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_latent,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_latent,invalid access occurs here]
 codetoanalyze/cpp/pulse/closures.cpp, call_lambda_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,when calling `call_lambda_bad::lambda_closures.cpp:163:12::operator()` here,parameter `s` of call_lambda_bad::lambda_closures.cpp:163:12::operator(),invalid access occurs here]
 codetoanalyze/cpp/pulse/closures.cpp, call_lambda_std_fun_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,when calling `call_lambda_std_fun_bad::lambda_closures.cpp:171:7::operator()` here,parameter `s` of call_lambda_std_fun_bad::lambda_closures.cpp:171:7::operator(),invalid access occurs here]
@@ -50,7 +51,7 @@ codetoanalyze/cpp/pulse/interprocedural.cpp, delete_inner_then_write_bad, 2, USE
 codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_read_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of delete_then_read_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `x` of delete_then_read_bad,when calling `wraps_read` here,parameter `x` of wraps_read,when calling `wraps_read_inner` here,parameter `x` of wraps_read_inner,invalid access occurs here]
 codetoanalyze/cpp/pulse/interprocedural.cpp, delete_then_write_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of delete_then_write_bad,when calling `wraps_delete` here,parameter `x` of wraps_delete,when calling `wraps_delete_inner` here,parameter `x` of wraps_delete_inner,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `x` of delete_then_write_bad,when calling `wraps_read` here,parameter `x` of wraps_read,when calling `wraps_read_inner` here,parameter `x` of wraps_read_inner,invalid access occurs here]
 codetoanalyze/cpp/pulse/interprocedural.cpp, feed_invalid_into_access_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `may_return_invalid_ptr_ok` here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `may_return_invalid_ptr_ok`,return from call to `may_return_invalid_ptr_ok`,assigned,when calling `call_store` here,parameter `y` of call_store,when calling `store` here,parameter `y` of store,invalid access occurs here]
-codetoanalyze/cpp/pulse/interprocedural.cpp, set_x_then_crash_double_latent, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,when calling `set_first_non_null_ok` here,parameter `y` of set_first_non_null_ok,invalid access occurs here]
+codetoanalyze/cpp/pulse/interprocedural.cpp, set_x_then_crash_double_latent, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,parameter `x` of set_x_then_crash_double_latent,when calling `set_first_non_null_ok` here,parameter `y` of set_first_non_null_ok,invalid access occurs here]
 codetoanalyze/cpp/pulse/interprocedural.cpp, set_x_then_crash_double_latent, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_bad, 1, USE_AFTER_DELETE, no_bucket, ERROR, [calling context starts here,in call to `invalidate_node_alias_latent`,invalidation part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/join.cpp, invalidate_node_alias_latent, 12, USE_AFTER_DELETE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `head` of invalidate_node_alias_latent,assigned,assigned,invalid access occurs here]
@@ -64,23 +65,18 @@ codetoanalyze/cpp/pulse/nullptr.cpp, std_true_type_deref_bad, 3, NULLPTR_DEREFER
 codetoanalyze/cpp/pulse/nullptr.cpp, test_after_dereference2_latent, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,is the null pointer,null pointer dereference part of the trace starts here,parameter `x` of test_after_dereference2_latent,invalid access occurs here]
 codetoanalyze/cpp/pulse/optional.cpp, assign2_bad, 4, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `folly::Optional<int>::operator=` here,passed as argument to `folly::Optional::reset()` (modelled),return from call to `folly::Optional::reset()` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `folly::Optional<int>::operator=`,passed as argument to `folly::Optional::reset()` (modelled),return from call to `folly::Optional::reset()` (modelled),return from call to `folly::Optional<int>::operator=`,invalid access occurs here]
 codetoanalyze/cpp/pulse/optional.cpp, assign_bad, 5, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),passed as argument to `folly::Optional<int>::operator=`,parameter `other` of folly::Optional<int>::operator=,passed as argument to `folly::Optional::assign(folly::Optional<Value> arg)` (modelled),return from call to `folly::Optional::assign(folly::Optional<Value> arg)` (modelled),return from call to `folly::Optional<int>::operator=`,invalid access occurs here]
-codetoanalyze/cpp/pulse/optional.cpp, cannot_be_empty_FP, 2, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `getOptionalValue` here,passed as argument to `std::optional::optional(=nullopt)` (modelled),return from call to `std::optional::optional(=nullopt)` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `getOptionalValue`,passed as argument to `std::optional::optional(=nullopt)` (modelled),return from call to `std::optional::optional(=nullopt)` (modelled),return from call to `getOptionalValue`,invalid access occurs here]
-codetoanalyze/cpp/pulse/optional.cpp, get_pointer_no_check_none_check_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,passed as argument to `folly::Optional::get_pointer()` (modelled),return from call to `folly::Optional::get_pointer()` (modelled),is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `folly::Optional::get_pointer()` (modelled),return from call to `folly::Optional::get_pointer()` (modelled),assigned,invalid access occurs here]
+codetoanalyze/cpp/pulse/optional.cpp, get_pointer_no_check_none_check_bad, 3, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `folly::Optional::get_pointer()` (modelled),return from call to `folly::Optional::get_pointer()` (modelled),assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/optional.cpp, inside_try_catch_FP, 3, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `might_return_none` here,passed as argument to `std::optional::optional(=nullopt)` (modelled),return from call to `std::optional::optional(=nullopt)` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `might_return_none`,passed as argument to `std::optional::optional(=nullopt)` (modelled),return from call to `std::optional::optional(=nullopt)` (modelled),return from call to `might_return_none`,invalid access occurs here]
 codetoanalyze/cpp/pulse/optional.cpp, none_copy_bad, 3, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),passed as argument to `folly::Optional::Optional(folly::Optional<Value> arg)` (modelled),return from call to `folly::Optional::Optional(folly::Optional<Value> arg)` (modelled),invalid access occurs here]
 codetoanalyze/cpp/pulse/optional.cpp, none_no_check_bad, 2, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),invalid access occurs here]
 codetoanalyze/cpp/pulse/optional.cpp, not_none_check_value_ok_FP, 5, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),invalid access occurs here]
 codetoanalyze/cpp/pulse/optional.cpp, operator_arrow_bad, 0, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),when calling `emplace` here,parameter `state` of emplace,passed as argument to `folly::Optional::operator->()` (modelled),return from call to `folly::Optional::operator->()` (modelled),invalid access occurs here]
-codetoanalyze/cpp/pulse/optional.cpp, smart_pointer_FP, 2, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `Node::getShared` here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `Node::getShared`,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),return from call to `Node::getShared`,invalid access occurs here]
 codetoanalyze/cpp/pulse/optional.cpp, std_assign2_bad, 4, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `std::optional::operator=(None)` (modelled),return from call to `std::optional::operator=(None)` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `std::optional::operator=(None)` (modelled),return from call to `std::optional::operator=(None)` (modelled),invalid access occurs here]
 codetoanalyze/cpp/pulse/optional.cpp, std_assign_bad, 5, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `std::optional::optional(=nullopt)` (modelled),return from call to `std::optional::optional(=nullopt)` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `std::optional::optional(=nullopt)` (modelled),return from call to `std::optional::optional(=nullopt)` (modelled),passed as argument to `std::optional::operator=(std::optional<Value> arg)` (modelled),return from call to `std::optional::operator=(std::optional<Value> arg)` (modelled),invalid access occurs here]
 codetoanalyze/cpp/pulse/optional.cpp, std_none_copy_bad, 3, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `std::optional::optional(=nullopt)` (modelled),return from call to `std::optional::optional(=nullopt)` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `std::optional::optional(=nullopt)` (modelled),return from call to `std::optional::optional(=nullopt)` (modelled),passed as argument to `std::optional::optional(std::optional<Value> arg)` (modelled),return from call to `std::optional::optional(std::optional<Value> arg)` (modelled),invalid access occurs here]
 codetoanalyze/cpp/pulse/optional.cpp, std_none_no_check_bad, 2, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `std::optional::optional(=nullopt)` (modelled),return from call to `std::optional::optional(=nullopt)` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `std::optional::optional(=nullopt)` (modelled),return from call to `std::optional::optional(=nullopt)` (modelled),invalid access occurs here]
 codetoanalyze/cpp/pulse/optional.cpp, std_not_none_check_value_ok_FP, 5, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `std::optional::optional(=nullopt)` (modelled),return from call to `std::optional::optional(=nullopt)` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `std::optional::optional(=nullopt)` (modelled),return from call to `std::optional::optional(=nullopt)` (modelled),invalid access occurs here]
-codetoanalyze/cpp/pulse/optional.cpp, std_operator_arrow_bad, 0, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `std::optional::optional(=nullopt)` (modelled),return from call to `std::optional::optional(=nullopt)` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `std::optional::optional(=nullopt)` (modelled),return from call to `std::optional::optional(=nullopt)` (modelled),when calling `std_emplace` here,parameter `state` of std_emplace,passed as argument to `std::optional::operator->()` (modelled),return from call to `std::optional::operator->()` (modelled),invalid access occurs here]
-codetoanalyze/cpp/pulse/optional.cpp, std_value_or_check_value_ok_FP, 5, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `std::optional::optional(=nullopt)` (modelled),return from call to `std::optional::optional(=nullopt)` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `std::optional::optional(=nullopt)` (modelled),return from call to `std::optional::optional(=nullopt)` (modelled),invalid access occurs here]
 codetoanalyze/cpp/pulse/optional.cpp, test_trace_ref, 4, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `folly::Optional<int>::operator=` here,passed as argument to `folly::Optional::reset()` (modelled),return from call to `folly::Optional::reset()` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `folly::Optional<int>::operator=`,passed as argument to `folly::Optional::reset()` (modelled),return from call to `folly::Optional::reset()` (modelled),return from call to `folly::Optional<int>::operator=`,invalid access occurs here]
-codetoanalyze/cpp/pulse/optional.cpp, value_or_check_value_ok_FP, 5, OPTIONAL_EMPTY_ACCESS, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),is optional empty,use-after-lifetime part of the trace starts here,passed as argument to `folly::Optional::Optional(=None)` (modelled),return from call to `folly::Optional::Optional(=None)` (modelled),invalid access occurs here]
 codetoanalyze/cpp/pulse/path.cpp, faulty_call_bad, 0, NULLPTR_DEREFERENCE, no_bucket, ERROR, [calling context starts here,in call to `only_bad_on_42_latent`,source of the null value part of the trace starts here,when calling `may_return_null` here,assigned,is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `may_return_null`,return from call to `may_return_null`,assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/path.cpp, only_bad_on_42_latent, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,when calling `may_return_null` here,assigned,is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `may_return_null`,return from call to `may_return_null`,assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/reference_wrapper.cpp, reference_wrapper_heap_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `getwrapperHeap` here,passed as argument to `WrapsB::WrapsB`,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,return from call to `WrapsB::WrapsB`,when calling `WrapsB::~WrapsB` here,parameter `this` of WrapsB::~WrapsB,when calling `WrapsB::__infer_inner_destructor_~WrapsB` here,parameter `this` of WrapsB::__infer_inner_destructor_~WrapsB,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `getwrapperHeap`,passed as argument to `WrapsB::WrapsB`,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,return from call to `WrapsB::WrapsB`,passed as argument to `ReferenceWrapperHeap::ReferenceWrapperHeap`,parameter `a` of ReferenceWrapperHeap::ReferenceWrapperHeap,passed as argument to `WrapsB::getb`,return from call to `WrapsB::getb`,assigned,return from call to `ReferenceWrapperHeap::ReferenceWrapperHeap`,return from call to `getwrapperHeap`,invalid access occurs here]
@@ -133,7 +129,6 @@ codetoanalyze/cpp/pulse/use_after_free.cpp, trigger_assumed_aliasing3_bad, 0, US
 codetoanalyze/cpp/pulse/use_after_free.cpp, trigger_assumed_aliasing_bad, 0, USE_AFTER_FREE, no_bucket, ERROR, [calling context starts here,in call to `assumed_aliasing_latent`,invalidation part of the trace starts here,parameter `x` of assumed_aliasing_latent,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `y` of assumed_aliasing_latent,invalid access occurs here]
 codetoanalyze/cpp/pulse/use_after_free.cpp, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of use_after_free_simple_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of use_after_free_simple_bad,invalid access occurs here]
 codetoanalyze/cpp/pulse/use_after_scope.cpp, access_out_of_scope_stack_ref_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `p` declared here,when calling `invalidate_local_ok` here,variable `t` declared here,is the address of a stack variable `t` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `p` declared here,passed as argument to `invalidate_local_ok`,variable `t` declared here,assigned,return from call to `invalidate_local_ok`,invalid access occurs here]
-codetoanalyze/cpp/pulse/values.cpp, FP_int_over_cap_ok, 13, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/values.cpp, FP_ints_are_not_rationals_ok, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/values.cpp, error_under_true_conditionals_bad, 5, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of error_under_true_conditionals_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of error_under_true_conditionals_bad,invalid access occurs here]
 codetoanalyze/cpp/pulse/values.cpp, free_if_deref_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of free_if_deref_bad,when calling `free_if` here,parameter `x` of free_if,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of free_if_deref_bad,invalid access occurs here]
diff --git a/infer/tests/codetoanalyze/cpp/pulse/optional.cpp b/infer/tests/codetoanalyze/cpp/pulse/optional.cpp
index 956d526d9..fd64fb62a 100644
--- a/infer/tests/codetoanalyze/cpp/pulse/optional.cpp
+++ b/infer/tests/codetoanalyze/cpp/pulse/optional.cpp
@@ -184,9 +184,9 @@ int value_or_check_empty_ok() {
   return -1;
 }
 
-// missing a more precise model for
-// constructing an optional from a value
-int value_or_check_value_ok_FP() {
+// missing a more precise model for constructing an optional from a
+// value, which could cause an FP but doesn't at the moment
+int value_or_check_value_ok() {
   folly::Optional<int> foo{5};
   int x = foo.value_or(0);
   if (x != 5) {
@@ -295,7 +295,7 @@ void std_emplace(std::optional<State> state) {
   auto pos = state->vec.begin();
 }
 
-void std_operator_arrow_bad() { std_emplace(std::nullopt); }
+void FN_std_operator_arrow_bad() { std_emplace(std::nullopt); }
 
 int std_value_or_check_empty_ok() {
   std::optional<int> foo{std::nullopt};
@@ -305,7 +305,7 @@ int std_value_or_check_empty_ok() {
   return -1;
 }
 
-int std_value_or_check_value_ok_FP() {
+int std_value_or_check_value_ok() {
   std::optional<int> foo{5};
   int x = foo.value_or(0);
   if (x != 5) {
@@ -372,7 +372,7 @@ E getEnum() {
   return E::OP2;
 }
 
-std::optional<std::string> cannot_be_empty_FP() {
+std::optional<std::string> cannot_be_empty() {
   if (getEnum() == E::OP1) {
     return getOptionalValue().value();
   }
@@ -399,7 +399,7 @@ struct Node {
   }
 };
 
-int smart_pointer_FP(const Node& node) {
+int smart_pointer(const Node& node) {
   if (node.getShared().has_value()) {
     return *(node.getShared().value());
   }
diff --git a/infer/tests/codetoanalyze/cpp/pulse/values.cpp b/infer/tests/codetoanalyze/cpp/pulse/values.cpp
index 5d428749a..68bba2b8d 100644
--- a/infer/tests/codetoanalyze/cpp/pulse/values.cpp
+++ b/infer/tests/codetoanalyze/cpp/pulse/values.cpp
@@ -116,8 +116,9 @@ void function_empty_range_interproc_ok() {
   find_first_non_space(x);
 }
 
-// arithmetic on integers does not wrap around but ignores too-large values
-void FP_int_over_cap_ok() {
+// arithmetic on integers does not wrap around but ignores too-large
+// values. However, somehow the FP is gone for other reasons.
+void int_over_cap_ok() {
   unsigned long one = 1;
   // 2^(63+63+3) + 2*2^(63+3) + 1*8 = 2^129 + 2^67 + 8 = 8 mod 2^64
   // this is convoluted to escape various simplifications from Z that would
@@ -169,3 +170,10 @@ void shift_by_too_much_ok(int x) {
     *p = 42;
   }
 }
+
+void interproc_mult_ok(int v, int w) {
+  if (mult(32, 52) != 1664 || mult(10, v) != 10 * v || mult(v, w) != v * w) {
+    int* p = nullptr;
+    *p = 42;
+  }
+}