diff --git a/infer/src/backend/dom.ml b/infer/src/backend/dom.ml
index c55418cfc..f23ca4083 100644
--- a/infer/src/backend/dom.ml
+++ b/infer/src/backend/dom.ml
@@ -1501,9 +1501,9 @@ let rec sigma_partial_join' tenv mode (sigma_acc: Prop.sigma)
         assert false (* Should be handled by a guarded case *)
 
   with Todo.Empty ->
-    match sigma1_in, sigma2_in with
-    | _:: _, _:: _ -> L.d_strln "todo is empty, but the sigmas are not"; raise IList.Fail
-    | _ -> sigma_acc, sigma1_in, sigma2_in
+  match sigma1_in, sigma2_in with
+  | _:: _, _:: _ -> L.d_strln "todo is empty, but the sigmas are not"; raise IList.Fail
+  | _ -> sigma_acc, sigma1_in, sigma2_in
 
 let sigma_partial_join tenv mode (sigma1: Prop.sigma) (sigma2: Prop.sigma)
   : (Prop.sigma * Prop.sigma * Prop.sigma) =
@@ -1555,9 +1555,9 @@ let rec sigma_partial_meet' tenv (sigma_acc: Prop.sigma) (sigma1_in: Prop.sigma)
         (L.d_strln "failure reason 65"; raise IList.Fail)
 
   with Todo.Empty ->
-    match sigma1_in, sigma2_in with
-    | [], [] -> sigma_acc
-    | _, _ -> L.d_strln "todo is empty, but the sigmas are not"; raise IList.Fail
+  match sigma1_in, sigma2_in with
+  | [], [] -> sigma_acc
+  | _, _ -> L.d_strln "todo is empty, but the sigmas are not"; raise IList.Fail
 
 let sigma_partial_meet tenv (sigma1: Prop.sigma) (sigma2: Prop.sigma) : Prop.sigma =
   sigma_partial_meet' tenv [] sigma1 sigma2
@@ -1574,11 +1574,6 @@ let pi_partial_join tenv mode
     (ep1: Prop.exposed Prop.t) (ep2: Prop.exposed Prop.t)
     (pi1: Prop.pi) (pi2: Prop.pi) : Prop.pi
   =
-  let exp_is_const = function
-    (* | Exp.Var id -> is_normal id *)
-    | Exp.Const _ -> true
-    (* | Exp.Lvar _ -> true *)
-    | _ -> false in
   let get_array_len prop =
     (* find some array length in the prop, to be used as heuritic for upper bound in widening *)
     let len_list = ref [] in
@@ -1666,18 +1661,6 @@ let pi_partial_join tenv mode
               | None -> atom_list
               | Some a' -> a' :: atom_list))
     | Some a' -> a' :: atom_list in
-  let filter_atom = function
-    | Sil.Aneq(e, e') | Sil.Aeq(e, e')
-      when (exp_is_const e && exp_is_const e') ->
-        true
-    | Sil.Aneq(Exp.Var _, e') | Sil.Aneq(e', Exp.Var _)
-    | Sil.Aeq(Exp.Var _, e') | Sil.Aeq(e', Exp.Var _)
-      when (exp_is_const e') ->
-        true
-    | Sil.Aneq _ -> false
-    | Sil.Aeq _ as e -> Prop.atom_is_inequality e
-    | Sil.Apred (_, es) | Anpred (_, es) ->
-        IList.for_all exp_is_const es in
   begin
     if Config.trace_join then begin
       L.d_str "pi1: "; Prop.d_pi pi1; L.d_ln ();
@@ -1687,18 +1670,15 @@ let pi_partial_join tenv mode
       let p2 = Prop.normalize tenv ep2 in
       IList.fold_left (handle_atom_with_widening Lhs p2 pi2) [] pi1 in
     if Config.trace_join then (L.d_str "atom_list1: "; Prop.d_pi atom_list1; L.d_ln ());
-    let atom_list_combined =
+    let atom_list2 =
       let p1 = Prop.normalize tenv ep1 in
-      IList.fold_left (handle_atom_with_widening Rhs p1 pi1) atom_list1 pi2 in
+      IList.fold_left (handle_atom_with_widening Rhs p1 pi1) [] pi2 in
     if Config.trace_join then
-      (L.d_str "atom_list_combined: "; Prop.d_pi atom_list_combined; L.d_ln ());
-    let atom_list_filtered =
-      IList.filter filter_atom atom_list_combined in
+      (L.d_str "atom_list2: "; Prop.d_pi atom_list2; L.d_ln ());
+    let atom_list_combined = IList.inter Sil.atom_compare atom_list1 atom_list2 in
     if Config.trace_join then
-      (L.d_str "atom_list_filtered: "; Prop.d_pi atom_list_filtered; L.d_ln ());
-    let atom_list_res =
-      IList.rev atom_list_filtered in
-    atom_list_res
+      (L.d_str "atom_list_combined: "; Prop.d_pi atom_list_combined; L.d_ln ());
+    atom_list_combined
   end
 
 let pi_partial_meet tenv (p: Prop.normal Prop.t) (ep1: 'a Prop.t) (ep2: 'b Prop.t) : Prop.normal Prop.t =
diff --git a/infer/src/base/IList.ml b/infer/src/base/IList.ml
index dccaf73e8..1e3a85c59 100644
--- a/infer/src/base/IList.ml
+++ b/infer/src/base/IList.ml
@@ -199,6 +199,25 @@ let intersect compare l1 l2 =
         else f l1 l2' in
   f l1_sorted l2_sorted
 
+let inter compare xs ys =
+  let rev_sort xs = sort (fun x y -> compare y x) xs in
+  let rev_xs = rev_sort xs in
+  let rev_ys = rev_sort ys in
+  let rec inter_ is rev_xxs rev_yys =
+    match rev_xxs, rev_yys with
+    | ([], _) | (_, []) ->
+        is
+    | (x :: rev_xs, y :: rev_ys) ->
+        let c = compare x y in
+        if c = 0 then
+          inter_ (x :: is) rev_xs rev_ys
+        else if c < 0 then
+          inter_ is rev_xs rev_yys
+        else
+          inter_ is rev_xxs rev_ys
+  in
+  inter_ [] rev_xs rev_ys
+
 exception Fail
 
 (** Apply [f] to pairs of elements; raise [Fail] if the two lists have different lenghts. *)
diff --git a/infer/src/base/IList.mli b/infer/src/base/IList.mli
index a7d1c5edf..c8d2b98b7 100644
--- a/infer/src/base/IList.mli
+++ b/infer/src/base/IList.mli
@@ -98,6 +98,9 @@ val merge_sorted_nodup : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list -> '
     The compare function is required to sort the lists. *)
 val intersect : ('a -> 'a -> int) -> 'a list -> 'a list -> bool
 
+(** [inter cmp xs ys] are the elements in both [xs] and [ys], sorted according to [cmp]. *)
+val inter : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list
+
 (** Like List.mem_assoc but without builtin equality *)
 val mem_assoc : ('a -> 'a -> bool) -> 'a -> ('a * 'b) list -> bool
 
diff --git a/infer/tests/codetoanalyze/java/infer/GuardedByExample.java b/infer/tests/codetoanalyze/java/infer/GuardedByExample.java
index ce63fec89..920a7e902 100644
--- a/infer/tests/codetoanalyze/java/infer/GuardedByExample.java
+++ b/infer/tests/codetoanalyze/java/infer/GuardedByExample.java
@@ -356,7 +356,7 @@ public class GuardedByExample {
 
   int n;
 
-  public void FP_withloop2() {
+  public void withloop2() {
     synchronized (mLock) {
       for (int i = 0; i<=n; i++) {
         f = 42;
diff --git a/infer/tests/codetoanalyze/java/infer/issues.exp b/infer/tests/codetoanalyze/java/infer/issues.exp
index c5e6f3888..e626e0bb6 100644
--- a/infer/tests/codetoanalyze/java/infer/issues.exp
+++ b/infer/tests/codetoanalyze/java/infer/issues.exp
@@ -74,7 +74,6 @@ FilterOutputStreamLeaks.java, void FilterOutputStreamLeaks.printStreamNotClosedA
 GuardedByExample.java, Object GuardedByExample.byRefTrickyBad(), 5, UNSAFE_GUARDED_BY_ACCESS
 GuardedByExample.java, String GuardedByExample$3.readFromInnerClassBad1(), 2, UNSAFE_GUARDED_BY_ACCESS
 GuardedByExample.java, String GuardedByExample$4.readFromInnerClassBad2(), 1, UNSAFE_GUARDED_BY_ACCESS
-GuardedByExample.java, void GuardedByExample.FP_withloop2(), 3, UNSAFE_GUARDED_BY_ACCESS
 GuardedByExample.java, void GuardedByExample.readFAfterBlockBad(), 3, UNSAFE_GUARDED_BY_ACCESS
 GuardedByExample.java, void GuardedByExample.readFBad(), 1, UNSAFE_GUARDED_BY_ACCESS
 GuardedByExample.java, void GuardedByExample.readFBadWrongAnnotation(), 1, UNSAFE_GUARDED_BY_ACCESS