diff --git a/infer/src/biabduction/Dom.ml b/infer/src/biabduction/Dom.ml
index e5ada3a3a..2e7c132e5 100644
--- a/infer/src/biabduction/Dom.ml
+++ b/infer/src/biabduction/Dom.ml
@@ -2109,12 +2109,6 @@ let pathset_collapse tenv pset =
 let pathset_join pname tenv (pset1 : Paths.PathSet.t) (pset2 : Paths.PathSet.t) :
     Paths.PathSet.t * Paths.PathSet.t =
   let mode = JoinState.Post in
-  let pset_to_plist pset =
-    let f_list p pa acc = (p, pa) :: acc in
-    Paths.PathSet.fold f_list pset []
-  in
-  let ppalist1 = pset_to_plist pset1 in
-  let ppalist2 = pset_to_plist pset2 in
   let rec join_proppath_plist ppalist2_acc ((p2, pa2) as ppa2) = function
     | [] ->
         (ppa2, List.rev ppalist2_acc)
@@ -2149,7 +2143,9 @@ let pathset_join pname tenv (pset1 : Paths.PathSet.t) (pset2 : Paths.PathSet.t)
         let ppa2_new, ppalist1_cur' = join_proppath_plist [] ppa2'' ppalist1_cur in
         join ppalist1_cur' (ppa2_new :: ppalist2_acc') ppalist2_rest'
   in
-  let ppalist1_res_, ppalist2_res_ = join ppalist1 [] ppalist2 in
+  let ppalist1_res_, ppalist2_res_ =
+    join (Paths.PathSet.elements pset1) [] (Paths.PathSet.elements pset2)
+  in
   let ren l = List.map ~f:(fun (p, x) -> (Prop.prop_rename_primed_footprint_vars tenv p, x)) l in
   let ppalist1_res, ppalist2_res = (ren ppalist1_res_, ren ppalist2_res_) in
   let res =
diff --git a/infer/src/biabduction/interproc.ml b/infer/src/biabduction/interproc.ml
index 7467c5b75..150ad011e 100644
--- a/infer/src/biabduction/interproc.ml
+++ b/infer/src/biabduction/interproc.ml
@@ -139,19 +139,16 @@ let htable_retrieve (htable : (Procdesc.Node.id, Paths.PathSet.t) Hashtbl.t)
 
 (** Add [d] to the pathset todo at [node] returning true if changed *)
 let path_set_put_todo (wl : Worklist.t) (node : Procdesc.Node.t) (d : Paths.PathSet.t) : bool =
-  let changed =
-    if Paths.PathSet.is_empty d then false
-    else
-      let node_id = Procdesc.Node.get_id node in
-      let old_todo = htable_retrieve wl.Worklist.path_set_todo node_id in
-      let old_visited = htable_retrieve wl.Worklist.path_set_visited node_id in
-      let d' = Paths.PathSet.diff d old_visited in
-      (* differential fixpoint *)
-      let todo_new = Paths.PathSet.union old_todo d' in
-      Hashtbl.replace wl.Worklist.path_set_todo node_id todo_new ;
-      not (Paths.PathSet.equal old_todo todo_new)
-  in
-  changed
+  if Paths.PathSet.is_empty d then false
+  else
+    let node_id = Procdesc.Node.get_id node in
+    let old_todo = htable_retrieve wl.Worklist.path_set_todo node_id in
+    let old_visited = htable_retrieve wl.Worklist.path_set_visited node_id in
+    let d' = Paths.PathSet.diff d old_visited in
+    (* differential fixpoint *)
+    let todo_new = Paths.PathSet.union old_todo d' in
+    Hashtbl.replace wl.Worklist.path_set_todo node_id todo_new ;
+    not (Paths.PathSet.equal old_todo todo_new)
 
 
 let path_set_checkout_todo (wl : Worklist.t) (node : Procdesc.Node.t) : Paths.PathSet.t =
@@ -718,7 +715,7 @@ let prop_init_formals_seed tenv new_formals (prop : 'a Prop.t) : Prop.exposed Pr
 
 (** Construct an initial prop by extending [prop] with locals, and formals if [add_formals] is true
     as well as seed variables *)
-let initial_prop tenv (curr_f : Procdesc.t) (prop : 'a Prop.t) add_formals : Prop.normal Prop.t =
+let initial_prop tenv (curr_f : Procdesc.t) (prop : 'a Prop.t) ~add_formals : Prop.normal Prop.t =
   let construct_decl (x, typ) = (Pvar.mk x (Procdesc.get_proc_name curr_f), typ) in
   let new_formals =
     if add_formals then List.map ~f:construct_decl (Procdesc.get_formals curr_f) else []
@@ -733,7 +730,7 @@ let initial_prop tenv (curr_f : Procdesc.t) (prop : 'a Prop.t) add_formals : Pro
 
 
 (** Construct an initial prop from the empty prop *)
-let initial_prop_from_emp tenv curr_f = initial_prop tenv curr_f Prop.prop_emp true
+let initial_prop_from_emp tenv curr_f = initial_prop tenv curr_f Prop.prop_emp ~add_formals:true
 
 (** Construct an initial prop from an existing pre with formals *)
 let initial_prop_from_pre tenv curr_f pre =
@@ -745,8 +742,8 @@ let initial_prop_from_pre tenv curr_f pre =
     let sub = Sil.subst_of_list sub_list in
     let pre2 = Prop.prop_sub sub pre in
     let pre3 = Prop.set pre2 ~pi_fp:(Prop.get_pure pre2) ~sigma_fp:pre2.Prop.sigma in
-    initial_prop tenv curr_f pre3 false
-  else initial_prop tenv curr_f pre false
+    initial_prop tenv curr_f pre3 ~add_formals:false
+  else initial_prop tenv curr_f pre ~add_formals:false
 
 
 (** Re-execute one precondition and return some spec if there was no re-execution error. *)