diff --git a/infer/src/biabduction/Dom.ml b/infer/src/biabduction/Dom.ml
index ed25eeea2..f2a12d772 100644
--- a/infer/src/biabduction/Dom.ml
+++ b/infer/src/biabduction/Dom.ml
@@ -48,7 +48,7 @@ let sigma_get_start_lexps_sort sigma =
 
 (** {2 Utility functions for side} *)
 
-type side = Lhs | Rhs
+type side = Lhs | Rhs [@@deriving compare]
 
 let select side e1 e2 = match side with Lhs -> e1 | Rhs -> e2
 
@@ -523,6 +523,8 @@ module Rename : sig
 
   val to_subst_proj : side -> unit Ident.HashQueue.t -> Sil.subst
 
+  val get_unify_eqs : unit -> (Exp.t * Exp.t) list
+
   val to_subst_emb : side -> Sil.subst
   (*
   val get : Exp.t -> Exp.t -> Exp.t option
@@ -656,6 +658,47 @@ end = struct
     else Sil.subst_of_list sub_list_side
 
 
+  module SideExpPairHash = Hashtbl.Make (struct
+    type t = side * Exp.t [@@deriving compare]
+
+    let hash = Hashtbl.hash
+
+    let equal = [%compare.equal: t]
+  end)
+
+  (* Each triple (L,R,U) in !tbl gives rise to an edge (Lhs,L)--(Rhs,R)
+  labeled by U. For each connected component, return equalities that constrain
+  all its Us to be equal. *)
+  let get_unify_eqs () : (Exp.t * Exp.t) list =
+    let find_classes () =
+      let module UF = Union_find in
+      let uf = Memo.general UF.create in
+      let handle_triple (le, re, _) = UF.union (uf (Lhs, le)) (uf (Rhs, re)) in
+      List.iter ~f:handle_triple !tbl ;
+      let get x = UF.get (uf x) in
+      get
+    in
+    let pick_rep get =
+      let module H = SideExpPairHash in
+      let rep_cache = H.create (2 * List.length !tbl) in
+      let handle_triple (le, re, ue) =
+        H.replace rep_cache (get (Lhs, le)) ue ;
+        H.replace rep_cache (get (Rhs, re)) ue
+      in
+      List.iter ~f:handle_triple !tbl ;
+      let rep x =
+        try H.find rep_cache (get x) with Caml.Not_found ->
+          L.die L.InternalError "Dom.Rename.get_unify_eqs broken"
+      in
+      rep
+    in
+    let make_eqs rep =
+      let f (le, _, ue) = (ue, rep (Lhs, le)) in
+      List.rev_map ~f !tbl
+    in
+    () |> find_classes |> pick_rep |> make_eqs
+
+
   let to_subst_emb (side : side) =
     let renaming_restricted =
       let pick_id_case (e1, e2, _) =
@@ -669,18 +712,11 @@ end = struct
       in
       List.map ~f:project renaming_restricted
     in
-    let sub_list_sorted =
-      let compare (i, _) (i', _) = Ident.compare i i' in
-      List.sort ~compare sub_list
-    in
-    let rec find_duplicates = function
-      | (i, _) :: ((i', _) :: _ as t) ->
-          Ident.equal i i' || find_duplicates t
-      | _ ->
-          false
+    let uniq_sub_list =
+      let compare (i, _) (j, _) = Ident.compare i j in
+      List.dedup_and_sort ~compare sub_list
     in
-    if find_duplicates sub_list_sorted then ( L.d_strln "failure reason 12" ; raise Sil.JoinFail )
-    else Sil.subst_of_list sub_list_sorted
+    Sil.subst_of_list uniq_sub_list
 
 
   let get_others' f_lookup side e =
@@ -1791,14 +1827,16 @@ let pi_partial_meet tenv (p : Prop.normal Prop.t) (ep1 : 'a Prop.t) (ep2 : 'b Pr
   in
   let f1 p' atom = Prop.prop_atom_and tenv p' (handle_atom sub1 dom1 atom) in
   let f2 p' atom = Prop.prop_atom_and tenv p' (handle_atom sub2 dom2 atom) in
+  let f3 p' (a, b) = Prop.conjoin_eq tenv a b p' in
   let pi1 = ep1.Prop.pi in
   let pi2 = ep2.Prop.pi in
   let p_pi1 = List.fold ~f:f1 ~init:p pi1 in
   let p_pi2 = List.fold ~f:f2 ~init:p_pi1 pi2 in
-  if Prover.check_inconsistency_base tenv p_pi2 then (
+  let p_pi3 = List.fold ~f:f3 ~init:p_pi2 (Rename.get_unify_eqs ()) in
+  if Prover.check_inconsistency_base tenv p_pi3 then (
     L.d_strln "check_inconsistency_base failed" ;
     raise Sil.JoinFail )
-  else p_pi2
+  else p_pi3
 
 
 (** {2 Join and Meet for Prop} *)
diff --git a/infer/src/biabduction/Prop.ml b/infer/src/biabduction/Prop.ml
index a3b4796d8..4282897ae 100644
--- a/infer/src/biabduction/Prop.ml
+++ b/infer/src/biabduction/Prop.ml
@@ -1721,16 +1721,25 @@ module Normalize = struct
       in
       if not footprint then p'
       else
+        let predicate_warning =
+          not (Sil.atom_free_vars a' |> Sequence.for_all ~f:Ident.is_footprint)
+        in
         let p'' =
-          match a' with
-          | Aeq (Exp.Var i, e) when not (Exp.ident_mem e i) ->
-              let mysub = Sil.subst_of_list [(i, e)] in
-              let sigma_fp' = sigma_normalize tenv mysub p'.sigma_fp in
-              let pi_fp' = a' :: pi_normalize tenv mysub sigma_fp' p'.pi_fp in
-              footprint_normalize tenv (set p' ~pi_fp:pi_fp' ~sigma_fp:sigma_fp')
-          | _ ->
-              footprint_normalize tenv (set p' ~pi_fp:(a' :: p'.pi_fp))
+          if predicate_warning then footprint_normalize tenv p'
+          else
+            match a' with
+            | Aeq (Exp.Var i, e) when not (Exp.ident_mem e i) ->
+                let mysub = Sil.subst_of_list [(i, e)] in
+                let sigma_fp' = sigma_normalize tenv mysub p'.sigma_fp in
+                let pi_fp' = a' :: pi_normalize tenv mysub sigma_fp' p'.pi_fp in
+                footprint_normalize tenv (set p' ~pi_fp:pi_fp' ~sigma_fp:sigma_fp')
+            | _ ->
+                footprint_normalize tenv (set p' ~pi_fp:(a' :: p'.pi_fp))
         in
+        if predicate_warning then (
+          L.d_warning "dropping non-footprint " ;
+          Sil.d_atom a' ;
+          L.d_ln () ) ;
         unsafe_cast_to_normal p''
 
 
diff --git a/infer/tests/codetoanalyze/cpp/errors/Makefile b/infer/tests/codetoanalyze/cpp/errors/Makefile
index d1aa4c172..3a986d81e 100644
--- a/infer/tests/codetoanalyze/cpp/errors/Makefile
+++ b/infer/tests/codetoanalyze/cpp/errors/Makefile
@@ -12,6 +12,7 @@ INFER_OPTIONS = --biabduction-only --ml-buckets cpp --debug-exceptions --project
 INFERPRINT_OPTIONS = --issues-tests
 
 SOURCES = \
+  $(wildcard biabduction/*.cpp) \
   $(wildcard c_tests/*.cpp) \
   include_header/header.h \
   include_header/include_templ.cpp \
diff --git a/infer/tests/codetoanalyze/cpp/errors/biabduction/process_splitting_assert.cpp b/infer/tests/codetoanalyze/cpp/errors/biabduction/process_splitting_assert.cpp
new file mode 100644
index 000000000..e6d6797fa
--- /dev/null
+++ b/infer/tests/codetoanalyze/cpp/errors/biabduction/process_splitting_assert.cpp
@@ -0,0 +1,43 @@
+/*
+ * Copyright (c) 2019-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+#include <memory.h>
+#define size_t int
+#define off_t int
+
+struct foo { // globals are treated differntly
+
+  char * memory_;
+  size_t memory_size_;
+
+  bool ReadBytes(void *buffer, size_t size, off_t offset) {
+    if (memory_) {
+      if (offset < 0) {
+        return false;
+      }
+      if (offset + size >= memory_size_) {
+          return false;
+      }
+      memcpy(buffer, memory_ + offset, size);
+      return true;
+    } else {
+      return false;
+    }
+  }
+
+  void FindHeader(off_t &offset) {
+    int magic;
+    ReadBytes(&magic, sizeof(magic), 0);
+    ReadBytes(&magic, sizeof(magic), 0);
+  }
+
+};
+
+void fail(char * x) {
+  if (x == 0) {
+    *x = 'a';
+  }
+}
diff --git a/infer/tests/codetoanalyze/cpp/errors/issues.exp b/infer/tests/codetoanalyze/cpp/errors/issues.exp
index 1bc68d49c..76a632e9d 100644
--- a/infer/tests/codetoanalyze/cpp/errors/issues.exp
+++ b/infer/tests/codetoanalyze/cpp/errors/issues.exp
@@ -1,6 +1,7 @@
 INFER_MODEL/cpp/include/infer_model/unique_ptr.h, std::operator!=<65d659492edc5cb5>, 1, Abduction_case_not_implemented, no_bucket, ERROR, [start of procedure std::operator!=<65d659492edc5cb5>()]
 INFER_MODEL/cpp/include/infer_model/unique_ptr.h, std::unique_ptr<int,unique_ptr_with_deleter::Deleter<int>>___infer_inner_destructor_~unique_ptr, 0, Missing_fld, no_bucket, ERROR, [start of procedure __infer_inner_destructor_~unique_ptr,start of procedure Pointer,return from a call to unique_ptr_with_deleter::Pointer<int>_Pointer,start of procedure Pointer,return from a call to unique_ptr_with_deleter::Pointer<int>_Pointer]
 INFER_MODEL/cpp/include/infer_model/unique_ptr.h, std::unique_ptr<int[_*4],unique_ptr_with_deleter::Deleter<int[_*4]>>___infer_inner_destructor_~unique_ptr, 0, Missing_fld, no_bucket, ERROR, [start of procedure __infer_inner_destructor_~unique_ptr,start of procedure Pointer,return from a call to unique_ptr_with_deleter::Pointer<int[_*4]>_Pointer,start of procedure Pointer,return from a call to unique_ptr_with_deleter::Pointer<int[_*4]>_Pointer]
+codetoanalyze/cpp/errors/biabduction/process_splitting_assert.cpp, fail, 2, NULL_DEREFERENCE, B5, ERROR, [start of procedure fail(),Taking true branch]
 codetoanalyze/cpp/errors/c_tests/c_bugs.cpp, crash_fgetc, 4, NULL_DEREFERENCE, B1, ERROR, [start of procedure crash_fgetc()]
 codetoanalyze/cpp/errors/c_tests/c_bugs.cpp, crash_getc, 4, NULL_DEREFERENCE, B1, ERROR, [start of procedure crash_getc()]
 codetoanalyze/cpp/errors/c_tests/c_bugs.cpp, malloc_fail_gets_reported, 2, NULL_DEREFERENCE, B1, ERROR, [start of procedure malloc_fail_gets_reported()]
diff --git a/infer/tests/codetoanalyze/objc/errors/issues.exp b/infer/tests/codetoanalyze/objc/errors/issues.exp
index 6cad5c9e3..d438cb5f9 100644
--- a/infer/tests/codetoanalyze/objc/errors/issues.exp
+++ b/infer/tests/codetoanalyze/objc/errors/issues.exp
@@ -20,7 +20,7 @@ codetoanalyze/objc/shared/block/BlockVar.m, BlockVar_navigateToURLInBackground,
 codetoanalyze/objc/shared/block/block.m, main1, 30, DIVIDE_BY_ZERO, no_bucket, ERROR, [start of procedure main1(),start of procedure block,start of procedure block,return from a call to objc_blockobjc_blockmain1_2_3,return from a call to objc_blockmain1_2,start of procedure block,return from a call to objc_blockmain1_1]
 codetoanalyze/objc/shared/block/block_no_args.m, My_manager_m, 10, NULL_DEREFERENCE, B1, ERROR, [start of procedure m,start of procedure block,return from a call to objc_blockMy_manager_m_1,Taking true branch]
 codetoanalyze/objc/shared/category_procdesc/main.c, CategoryProcdescMain, 5, MEMORY_LEAK, no_bucket, ERROR, [start of procedure CategoryProcdescMain(),Skipping performDaysWork: method has no implementation,return from a call to CategoryProcdescMain]
-codetoanalyze/objc/shared/field_superclass/SuperExample.m, ASuper_init, 2, NULL_DEREFERENCE, B2, ERROR, [start of procedure init,start of procedure init,return from a call to BSuper_init]
+codetoanalyze/objc/shared/field_superclass/SuperExample.m, ASuper_init, 2, NULL_DEREFERENCE, B2, ERROR, [start of procedure init]
 codetoanalyze/objc/errors/blocks_in_heap/BlockInHeap.m, block_in_heap_executed_after_bi_abduction_ok_test, 3, NULL_DEREFERENCE, B1, ERROR, [start of procedure block_in_heap_executed_after_bi_abduction_ok_test(),start of procedure block_in_heap_executed_after_bi_abduction_ok_no_retain_cycle(),start of procedure assign_block_to_ivar,Executing synthesized setter setHandler:,return from a call to BlockInHeap_assign_block_to_ivar,Executing synthesized getter handler,start of procedure block,return from a call to objc_blockBlockInHeap_assign_block_to_ivar_1,return from a call to block_in_heap_executed_after_bi_abduction_ok_no_retain_cycle,Taking true branch]
 codetoanalyze/objc/errors/field_superclass/SubtypingExample.m, Employee_initWithName:andAge:andEducation:, 3, NULL_TEST_AFTER_DEREFERENCE, no_bucket, WARNING, [start of procedure initWithName:andAge:andEducation:,start of procedure initWithName:andAge:,return from a call to Person_initWithName:andAge:,Taking false branch]
 codetoanalyze/objc/errors/field_superclass/SubtypingExample.m, Employee_initWithName:andAge:andEducation:, 6, DIVIDE_BY_ZERO, no_bucket, ERROR, [start of procedure initWithName:andAge:andEducation:,start of procedure initWithName:andAge:,return from a call to Person_initWithName:andAge:,Taking true branch]