diff --git a/infer/src/IR/Cfg.re b/infer/src/IR/Cfg.re
index 098adbb7e..41fde0f92 100644
--- a/infer/src/IR/Cfg.re
+++ b/infer/src/IR/Cfg.re
@@ -962,8 +962,8 @@ let remove_abducted_retvars p =>
             fun
             | Sil.Aeq lhs rhs
             | Sil.Aneq lhs rhs => exp_contains lhs || exp_contains rhs
-            | Sil.Apred _ e
-            | Sil.Anpred _ e => exp_contains e
+            | Sil.Apred _ es
+            | Sil.Anpred _ es => IList.exists exp_contains es
           )
           pi
       };
diff --git a/infer/src/IR/Sil.re b/infer/src/IR/Sil.re
index 13e609ef4..cafec9ee7 100644
--- a/infer/src/IR/Sil.re
+++ b/infer/src/IR/Sil.re
@@ -85,7 +85,14 @@ type res_action = {
 };
 
 
-/** Attributes */
+/** Attributes are nary function symbols that are applied to expression arguments in Apred and
+    Anpred atomic formulas.  Many operations don't make much sense for nullary predicates, and are
+    generally treated as no-ops.  The first argument is treated specially, as the "anchor" of the
+    predicate application.  For example, adding or removing an attribute uses the anchor to identify
+    the atom to operate on.  Also, abstraction and normalization operations treat the anchor
+    specially and maintain more information on it than other arguments.  Therefore when attaching an
+    attribute to an expression, that expression should be the first argument, optionally followed by
+    additional related expressions. */
 type attribute =
   | Aresource of res_action /** resource acquire/release */
   | Aautorelease
@@ -203,8 +210,8 @@ type offset = | Off_fld of Ident.fieldname Typ.t | Off_index of exp;
 type atom =
   | Aeq of exp exp /** equality */
   | Aneq of exp exp /** disequality */
-  | Apred of attribute exp /** predicate symbol applied to an exp */
-  | Anpred of attribute exp /** negated predicate symbol applied to an exp */;
+  | Apred of attribute (list exp) /** predicate symbol applied to exps */
+  | Anpred of attribute (list exp) /** negated predicate symbol applied to exps */;
 
 
 /** kind of lseg or dllseg predicates */
@@ -705,21 +712,21 @@ let atom_compare a b =>
       }
     | (Aneq _, _) => (-1)
     | (_, Aneq _) => 1
-    | (Apred a1 e1, Apred a2 e2) =>
+    | (Apred a1 es1, Apred a2 es2) =>
       let n = attribute_compare a1 a2;
       if (n != 0) {
         n
       } else {
-        exp_compare e1 e2
+        IList.compare exp_compare es1 es2
       }
     | (Apred _, _) => (-1)
     | (_, Apred _) => 1
-    | (Anpred a1 e1, Anpred a2 e2) =>
+    | (Anpred a1 es1, Anpred a2 es2) =>
       let n = attribute_compare a1 a2;
       if (n != 0) {
         n
       } else {
-        exp_compare e1 e2
+        IList.compare exp_compare es1 es2
       }
     }
   };
@@ -1286,8 +1293,8 @@ let pp_atom pe0 f a => {
     | PP_HTML => F.fprintf f "%a != %a" (pp_exp pe) e1 (pp_exp pe) e2
     | PP_LATEX => F.fprintf f "%a{\\neq}%a" (pp_exp pe) e1 (pp_exp pe) e2
     }
-  | Apred a e => F.fprintf f "%s(%a)" (attribute_to_string pe a) (pp_exp pe) e
-  | Anpred a e => F.fprintf f "!%s(%a)" (attribute_to_string pe a) (pp_exp pe) e
+  | Apred a es => F.fprintf f "%s(%a)" (attribute_to_string pe a) (pp_comma_seq (pp_exp pe)) es
+  | Anpred a es => F.fprintf f "!%s(%a)" (attribute_to_string pe a) (pp_comma_seq (pp_exp pe)) es
   };
   color_post_wrapper changed pe0 f
 };
@@ -1942,8 +1949,8 @@ let atom_expmap (f: exp => exp) =>
   fun
   | Aeq e1 e2 => Aeq (f e1) (f e2)
   | Aneq e1 e2 => Aneq (f e1) (f e2)
-  | Apred a e => Apred a (f e)
-  | Anpred a e => Anpred a (f e);
+  | Apred a es => Apred a (IList.map f es)
+  | Anpred a es => Anpred a (IList.map f es);
 
 let atom_list_expmap (f: exp => exp) (alist: list atom) => IList.map (atom_expmap f) alist;
 
@@ -2080,8 +2087,8 @@ let atom_fpv =
   fun
   | Aeq e1 e2 => exp_fpv e1 @ exp_fpv e2
   | Aneq e1 e2 => exp_fpv e1 @ exp_fpv e2
-  | Apred _ e
-  | Anpred _ e => exp_fpv e;
+  | Apred _ es
+  | Anpred _ es => IList.fold_left (fun fpv e => IList.rev_append (exp_fpv e) fpv) [] es;
 
 let rec strexp_fpv =
   fun
@@ -2292,8 +2299,8 @@ let atom_fav_add fav =>
       exp_fav_add fav e1;
       exp_fav_add fav e2
     }
-  | Apred _ e
-  | Anpred _ e => exp_fav_add fav e;
+  | Apred _ es
+  | Anpred _ es => IList.iter (fun e => exp_fav_add fav e) es;
 
 let atom_fav = fav_imperative_to_functional atom_fav_add;
 
diff --git a/infer/src/IR/Sil.rei b/infer/src/IR/Sil.rei
index 5c7694c0e..668e645a9 100644
--- a/infer/src/IR/Sil.rei
+++ b/infer/src/IR/Sil.rei
@@ -73,7 +73,14 @@ type res_action = {
 };
 
 
-/** Attributes */
+/** Attributes are nary function symbols that are applied to expression arguments in Apred and
+    Anpred atomic formulas.  Many operations don't make much sense for nullary predicates, and are
+    generally treated as no-ops.  The first argument is treated specially, as the "anchor" of the
+    predicate application.  For example, adding or removing an attribute uses the anchor to identify
+    the atom to operate on.  Also, abstraction and normalization operations treat the anchor
+    specially and maintain more information on it than other arguments.  Therefore when attaching an
+    attribute to an expression, that expression should be the first argument, optionally followed by
+    additional related expressions. */
 type attribute =
   | Aresource of res_action /** resource acquire/release */
   | Aautorelease
@@ -197,8 +204,8 @@ type offset = | Off_fld of Ident.fieldname Typ.t | Off_index of exp;
 type atom =
   | Aeq of exp exp /** equality */
   | Aneq of exp exp /** disequality */
-  | Apred of attribute exp /** predicate symbol applied to an exp */
-  | Anpred of attribute exp /** negated predicate symbol applied to an exp */;
+  | Apred of attribute (list exp) /** predicate symbol applied to exps */
+  | Anpred of attribute (list exp) /** negated predicate symbol applied to exps */;
 
 
 /** kind of lseg or dllseg predicates */
diff --git a/infer/src/backend/abs.ml b/infer/src/backend/abs.ml
index 2e3de29b4..0ac431581 100644
--- a/infer/src/backend/abs.ml
+++ b/infer/src/backend/abs.ml
@@ -788,7 +788,7 @@ let abstract_pure_part p ~(from_abstract_footprint: bool) =
                 | Sil.Const _ -> a :: pi
                 | _ -> pi)
            | Sil.Aneq (Var _, _)
-           | Sil.Apred (_, Var _) | Anpred (_, Var _) -> a :: pi
+           | Sil.Apred (_, Var _ :: _) | Anpred (_, Var _ :: _) -> a :: pi
            | Sil.Aeq _ | Aneq _ | Apred _ | Anpred _ -> pi
         )
         [] pi_filtered in
@@ -820,11 +820,11 @@ let abstract_gc p =
         let no_fav_e1 = Sil.fav_is_empty fav_e1 in
         let no_fav_e2 = Sil.fav_is_empty fav_e2 in
         (no_fav_e1 || intersect_e1 ()) && (no_fav_e2 || intersect_e2 ())
-    | Sil.Apred (_, e) | Anpred (_, e) ->
-        let fav_e = Sil.exp_fav e in
-        Sil.fav_is_empty fav_e
+    | (Sil.Apred _ | Anpred _) as a ->
+        let fav_a = Sil.atom_fav a in
+        Sil.fav_is_empty fav_a
         ||
-        IList.intersect Ident.compare (Sil.fav_to_list fav_e) (Sil.fav_to_list fav_p_without_pi) in
+        IList.intersect Ident.compare (Sil.fav_to_list fav_a) (Sil.fav_to_list fav_p_without_pi) in
   let new_pi = IList.filter strong_filter pi in
   let prop = Prop.normalize (Prop.replace_pi new_pi p) in
   match Prop.prop_iter_create prop with
diff --git a/infer/src/backend/dom.ml b/infer/src/backend/dom.ml
index 5f455cc2f..8bfeebd91 100644
--- a/infer/src/backend/dom.ml
+++ b/infer/src/backend/dom.ml
@@ -718,13 +718,13 @@ end = struct
           when (exp_contains_only_normal_ids e' && not (Ident.is_normal id)) ->
             build_other_atoms (fun e0 -> Prop.mk_neq e0 e') side e
 
-        | Sil.Apred (a, (Var id as e))
-          when not (Ident.is_normal id) ->
-            build_other_atoms (fun e0 -> Prop.mk_pred a e0) side e
+        | Sil.Apred (a, (Var id as e) :: es)
+          when not (Ident.is_normal id) && IList.for_all exp_contains_only_normal_ids es ->
+            build_other_atoms (fun e0 -> Prop.mk_pred a (e0 :: es)) side e
 
-        | Sil.Anpred (a, (Var id as e))
-          when not (Ident.is_normal id) ->
-            build_other_atoms (fun e0 -> Prop.mk_npred a e0) side e
+        | Sil.Anpred (a, (Var id as e) :: es)
+          when not (Ident.is_normal id) && IList.for_all exp_contains_only_normal_ids es ->
+            build_other_atoms (fun e0 -> Prop.mk_npred a (e0 :: es)) side e
 
         | Sil.Aeq((Sil.Var id as e), e') | Sil.Aeq(e', (Sil.Var id as e))
           when (exp_contains_only_normal_ids e' && not (Ident.is_normal id)) ->
@@ -1674,8 +1674,8 @@ let pi_partial_join mode
         true
     | Sil.Aneq _ -> false
     | Sil.Aeq _ as e -> Prop.atom_is_inequality e
-    | Sil.Apred (_, e) | Anpred (_, e) ->
-        exp_is_const e in
+    | 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 ();
diff --git a/infer/src/backend/modelBuiltins.ml b/infer/src/backend/modelBuiltins.ml
index ce3442894..7355fd08a 100644
--- a/infer/src/backend/modelBuiltins.ml
+++ b/infer/src/backend/modelBuiltins.ml
@@ -313,7 +313,7 @@ let execute___cast builtin_args
 let set_resource_attribute prop path n_lexp loc ra_res =
   let prop' = match Prop.get_resource_attribute prop n_lexp with
     | Some (Apred (Aresource ra, _)) ->
-        Prop.add_or_replace_exp_attribute prop (Apred (Aresource { ra with ra_res }, n_lexp))
+        Prop.add_or_replace_attribute prop (Apred (Aresource { ra with ra_res }, [n_lexp]))
     | _ ->
         let pname = Sil.mem_alloc_pname Sil.Mnew in
         let ra =
@@ -323,7 +323,7 @@ let set_resource_attribute prop path n_lexp loc ra_res =
             ra_pname = pname;
             ra_loc = loc;
             ra_vpath = None } in
-        Prop.add_or_replace_exp_attribute prop (Apred (Aresource ra, n_lexp)) in
+        Prop.add_or_replace_attribute prop (Apred (Aresource ra, [n_lexp])) in
   [(prop', path)]
 
 (** Set the attibute of the value as file *)
@@ -545,7 +545,7 @@ let execute___set_autorelease_attribute
       let prop = return_result lexp prop_ ret_ids in
       if Config.objc_memory_model_on then
         let n_lexp, prop = check_arith_norm_exp pname lexp prop in
-        let prop' = Prop.add_or_replace_exp_attribute prop (Apred (Aautorelease, n_lexp)) in
+        let prop' = Prop.add_or_replace_attribute prop (Apred (Aautorelease, [n_lexp])) in
         [(prop', path)]
       else execute___no_op prop path
   | _ -> raise (Exceptions.Wrong_argument_number __POS__)
@@ -555,11 +555,11 @@ let execute___release_autorelease_pool
     ({ Builtin.prop_; path; } as builtin_args)
   : Builtin.ret_typ =
   if Config.objc_memory_model_on then
-    let autoreleased_objects = Prop.get_atoms_with_attribute Sil.Aautorelease prop_ in
+    let autoreleased_objects = Prop.get_atoms_with_attribute prop_ Sil.Aautorelease in
     let prop_without_attribute = Prop.remove_attribute prop_ Aautorelease in
-    let call_release res exp =
-      match res with
-      | (prop', path'):: _ ->
+    let call_release res atom =
+      match res, atom with
+      | ((prop', path') :: _, Sil.Apred (_, exp :: _)) ->
           (try
              let hpred = IList.find (function
                  | Sil.Hpointsto(e1, _, _) -> Sil.exp_equal e1 exp
@@ -575,19 +575,19 @@ let execute___release_autorelease_pool
                  res1
              | _ -> res
            with Not_found -> res)
-      | [] -> res in
+      | _ -> res in
     IList.fold_left call_release [(prop_without_attribute, path)] autoreleased_objects
   else execute___no_op prop_ path
 
 let set_attr pdesc prop path exp attr =
   let pname = Cfg.Procdesc.get_proc_name pdesc in
   let n_lexp, prop = check_arith_norm_exp pname exp prop in
-  [(Prop.add_or_replace_exp_attribute prop (Apred (attr, n_lexp)), path)]
+  [(Prop.add_or_replace_attribute prop (Apred (attr, [n_lexp])), path)]
 
 let delete_attr pdesc prop path exp attr =
   let pname = Cfg.Procdesc.get_proc_name pdesc in
   let n_lexp, prop = check_arith_norm_exp pname exp prop in
-  [(Prop.remove_attribute_from_exp prop (Apred (attr, n_lexp)), path)]
+  [(Prop.remove_attribute_from_exp prop (Apred (attr, [n_lexp])), path)]
 
 
 (** Set attibute att *)
@@ -694,8 +694,8 @@ let _execute_free mk loc acc iter =
           Sil.ra_vpath = None } in
       (* mark value as freed *)
       let p_res =
-        Prop.add_or_replace_exp_attribute_check_changed
-          Tabulation.check_attr_dealloc_mismatch prop (Apred (Aresource ra, lexp)) in
+        Prop.add_or_replace_attribute_check_changed
+          Tabulation.check_attr_dealloc_mismatch prop (Apred (Aresource ra, [lexp])) in
       p_res :: acc
   | (Sil.Hpointsto _, _ :: _) -> assert false (* alignment error *)
   | _ -> assert false (* should not happen *)
@@ -796,7 +796,7 @@ let execute_alloc mk can_return_null
         Sil.ra_loc = loc;
         Sil.ra_vpath = None } in
     (* mark value as allocated *)
-    Prop.add_or_replace_exp_attribute prop' (Apred (Aresource ra, exp_new)) in
+    Prop.add_or_replace_attribute prop' (Apred (Aresource ra, [exp_new])) in
   let prop_alloc = Prop.conjoin_eq (Sil.Var ret_id) exp_new prop_plus_ptsto in
   if can_return_null then
     let prop_null = Prop.conjoin_eq (Sil.Var ret_id) Sil.exp_zero prop in
diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml
index b19e02040..ff5703748 100644
--- a/infer/src/backend/prop.ml
+++ b/infer/src/backend/prop.ml
@@ -1034,10 +1034,10 @@ let atom_normalize sub a0 =
         handle_boolean_operation true e1 e2
     | Sil.Aneq (e1, e2) ->
         handle_boolean_operation false e1 e2
-    | Sil.Apred (a, e) ->
-        Sil.Apred (a, exp_normalize sub e)
-    | Sil.Anpred (a, e) ->
-        Sil.Anpred (a, exp_normalize sub e) in
+    | Sil.Apred (a, es) ->
+        Sil.Apred (a, IList.map (fun e -> exp_normalize sub e) es)
+    | Sil.Anpred (a, es) ->
+        Sil.Anpred (a, IList.map (fun e -> exp_normalize sub e) es) in
   if atom_is_inequality a' then inequality_normalize a' else a'
 
 (** Negate an atom *)
@@ -1048,8 +1048,8 @@ let atom_negate = function
       mk_inequality (Sil.exp_le e2 e1)
   | Sil.Aeq (e1, e2) -> Sil.Aneq (e1, e2)
   | Sil.Aneq (e1, e2) -> Sil.Aeq (e1, e2)
-  | Sil.Apred (a, e) -> Sil.Anpred (a, e)
-  | Sil.Anpred (a, e) -> Sil.Apred (a, e)
+  | Sil.Apred (a, es) -> Sil.Anpred (a, es)
+  | Sil.Anpred (a, es) -> Sil.Apred (a, es)
 
 let rec strexp_normalize sub se =
   match se with
@@ -1475,10 +1475,10 @@ let mk_neq e1 e2 = mk_atom (Aneq (e1, e2))
 let mk_eq e1 e2 = mk_atom (Aeq (e1, e2))
 
 (** Construct a pred. *)
-let mk_pred a e = mk_atom (Apred (a, e))
+let mk_pred a es = mk_atom (Apred (a, es))
 
 (** Construct a negated pred. *)
-let mk_npred a e = mk_atom (Anpred (a, e))
+let mk_npred a es = mk_atom (Anpred (a, es))
 
 (** Construct a points-to predicate for a single program variable.
     If [expand_structs] is true, initialize the fields of structs with fresh variables. *)
@@ -1613,7 +1613,7 @@ let compute_reachable_atoms pi exps =
   IList.filter
     (function
       | Sil.Aeq (lhs, rhs) | Aneq (lhs, rhs) -> exp_contains lhs || exp_contains rhs
-      | Sil.Apred (_, e) | Anpred (_, e) -> exp_contains e)
+      | Sil.Apred (_, es) | Anpred (_, es) -> IList.exists exp_contains es)
     pi
 
 (** Eliminates all empty lsegs from sigma, and collect equalities
@@ -1776,21 +1776,21 @@ let prop_reset_inst inst_map prop =
 (** {2 Attributes} *)
 
 (** Return the exp and attribute marked in the atom if any, and return None otherwise *)
-let atom_get_exp_attribute atom =
+let atom_get_attribute atom =
   match atom with
   | Sil.Apred _ | Anpred _ -> Some atom
   | _ -> None
 
 (** Check whether an atom is used to mark an attribute *)
 let atom_is_attribute a =
-  atom_get_exp_attribute a <> None
+  atom_get_attribute a <> None
 
 (** Get the attribute associated to the expression, if any *)
-let get_exp_attributes prop exp =
+let get_attributes prop exp =
   let nexp = exp_normalize_prop prop exp in
   let atom_get_attr attributes atom =
     match atom with
-    | Sil.Apred (_, e) | Anpred (_, e) when Sil.exp_equal e nexp -> atom :: attributes
+    | Sil.Apred (_, es) | Anpred (_, es) when IList.mem Sil.exp_equal nexp es -> atom :: attributes
     | _ -> attributes in
   IList.fold_left atom_get_attr [] prop.pi
 
@@ -1800,7 +1800,7 @@ let attributes_in_same_category attr1 attr2 =
   Sil.attribute_category_equal cat1 cat2
 
 let get_attribute prop exp category =
-  let atts = get_exp_attributes prop exp in
+  let atts = get_attributes prop exp in
   try
     Some
       (IList.find (function
@@ -1835,7 +1835,7 @@ let get_retval_attribute prop exp =
   get_attribute prop exp Sil.ACretval
 
 let has_dangling_uninit_attribute prop exp =
-  let la = get_exp_attributes prop exp in
+  let la = get_attributes prop exp in
   IList.exists (function
       | Sil.Apred (a, _) -> Sil.attribute_equal a (Adangling DAuninit)
       | _ -> false
@@ -1844,49 +1844,50 @@ let has_dangling_uninit_attribute prop exp =
 (** Get all the attributes of the prop *)
 let get_all_attributes prop =
   let res = ref [] in
-  let do_atom a = match atom_get_exp_attribute a with
+  let do_atom a = match atom_get_attribute a with
     | Some attr -> res := attr :: !res
     | None -> () in
   IList.iter do_atom prop.pi;
   IList.rev !res
 
-(** Set an attribute associated to the expression *)
-let set_exp_attribute ?(footprint = false) ?(polarity = true) prop attr exp =
+(** Set an attribute associated to the argument expressions *)
+let set_attribute ?(footprint = false) ?(polarity = true) prop attr args =
   prop_atom_and ~footprint prop
-    (if polarity then Sil.Apred (attr, exp) else Sil.Anpred (attr, exp))
+    (if polarity then Sil.Apred (attr, args) else Sil.Anpred (attr, args))
 
 (** Replace an attribute associated to the expression *)
-let add_or_replace_exp_attribute_check_changed check_attribute_change prop atom0 =
+let add_or_replace_attribute_check_changed check_attribute_change prop atom0 =
   match atom0 with
-  | Sil.Apred (att0, exp0) | Anpred (att0, exp0) ->
-      let nexp = exp_normalize_prop prop exp0 in
-      let atom = Sil.atom_replace_exp [(exp0, nexp)] atom0 in
+  | Sil.Apred (att0, ((_ :: _) as exps0)) | Anpred (att0, ((_ :: _) as exps0)) ->
+      let nexps = IList.map (fun e -> exp_normalize_prop prop e) exps0 in
+      let nexp = IList.hd nexps in (* len nexps = len exps0 > 0 by match *)
+      let natom = Sil.atom_replace_exp (IList.combine exps0 nexps) atom0 in
       let atom_map = function
-        | Sil.Apred (att, exp) | Anpred (att, exp)
+        | Sil.Apred (att, exp :: _) | Anpred (att, exp :: _)
           when Sil.exp_equal nexp exp && attributes_in_same_category att att0 ->
             check_attribute_change att att0;
-            atom
-        | a ->
-            a in
+            natom
+        | atom ->
+            atom in
       let pi = get_pi prop in
       let pi' = IList.map_changed atom_map pi in
       if pi == pi'
-      then prop_atom_and prop atom
+      then prop_atom_and prop natom
       else replace_pi pi' prop
   | _ ->
       prop
 
-let add_or_replace_exp_attribute prop atom =
+let add_or_replace_attribute prop atom =
   (* wrapper for the most common case: do nothing *)
   let check_attr_changed = (fun _ _ -> ()) in
-  add_or_replace_exp_attribute_check_changed check_attr_changed prop atom
+  add_or_replace_attribute_check_changed check_attr_changed prop atom
 
 (** mark Sil.Var's or Sil.Lvar's as undefined *)
 let mark_vars_as_undefined prop vars_to_mark callee_pname ret_annots loc path_pos =
   let att_undef = Sil.Aundef (callee_pname, ret_annots, loc, path_pos) in
   let mark_var_as_undefined exp prop =
     match exp with
-    | Sil.Var _ | Lvar _ -> add_or_replace_exp_attribute prop (Apred (att_undef, exp))
+    | Sil.Var _ | Lvar _ -> add_or_replace_attribute prop (Apred (att_undef, [exp]))
     | _ -> prop in
   IList.fold_left (fun prop id -> mark_var_as_undefined id prop) prop vars_to_mark
 
@@ -1910,9 +1911,9 @@ let remove_resource_attribute ra_kind ra_res =
 
 let remove_attribute_from_exp prop atom =
   match atom with
-  | Sil.Apred (_, exp) | Anpred (_, exp) ->
-      let nexp = exp_normalize_prop prop exp in
-      let natom = Sil.atom_replace_exp [(exp,nexp)] atom in
+  | Sil.Apred (_, exps) | Anpred (_, exps) ->
+      let nexps = IList.map (fun e -> exp_normalize_prop prop e) exps in
+      let natom = Sil.atom_replace_exp (IList.combine exps nexps) atom in
       let f a = not (Sil.atom_equal natom a) in
       filter_atoms ~f prop
   | _ ->
@@ -1925,7 +1926,7 @@ let replace_objc_null prop lhs_exp rhs_exp =
       let prop = remove_attribute_from_exp prop atom in
       let prop = conjoin_eq rhs_exp Sil.exp_zero prop in
       let natom = Sil.atom_replace_exp [(rhs_exp, lhs_exp)] atom in
-      add_or_replace_exp_attribute prop natom
+      add_or_replace_attribute prop natom
   | _ -> prop
 
 let rec nullify_exp_with_objc_null prop exp =
@@ -1944,14 +1945,11 @@ let rec nullify_exp_with_objc_null prop exp =
   | _ -> prop
 
 (** Get all the attributes of the prop *)
-let get_atoms_with_attribute att prop =
-  let atom_remove atom autoreleased_atoms = match atom with
-    | Sil.Apred (att_old, e) | Anpred (att_old, e) ->
-        if Sil.attribute_equal att_old att then
-          e:: autoreleased_atoms
-        else autoreleased_atoms
-    | _ -> autoreleased_atoms in
-  IList.fold_right atom_remove (get_pi prop) []
+let get_atoms_with_attribute prop att =
+  IList.filter (function
+      | Sil.Apred (att', _) | Anpred (att', _) -> Sil.attribute_equal att' att
+      | _ -> false
+    ) (get_pi prop)
 
 (** Apply f to every resource attribute in the prop *)
 let attribute_map_resource prop f =
@@ -1959,8 +1957,8 @@ let attribute_map_resource prop f =
     | Sil.Aresource ra -> Sil.Aresource (f e ra)
     | att -> att in
   let atom_map = function
-    | Sil.Apred (att, e) -> Sil.Apred (attribute_map e att, e)
-    | Sil.Anpred (att, e) -> Sil.Anpred (attribute_map e att, e)
+    | Sil.Apred (att, ([e] as es)) -> Sil.Apred (attribute_map e att, es)
+    | Sil.Anpred (att, ([e] as es)) -> Sil.Anpred (attribute_map e att, es)
     | atom -> atom in
   replace_pi (IList.map atom_map (get_pi prop)) prop
 
@@ -1981,7 +1979,7 @@ let find_arithmetic_problem proc_node_session prop exp =
     match exp_normalize_prop prop e with
     | Sil.Const c when iszero_int_float c -> true
     | _ ->
-        res := add_or_replace_exp_attribute !res (Apred (Adiv0 proc_node_session, e));
+        res := add_or_replace_attribute !res (Apred (Adiv0 proc_node_session, [e]));
         false in
   let rec walk = function
     | Sil.Var _ -> ()
@@ -2039,7 +2037,8 @@ let deallocate_stack_vars p pvars =
       if Sil.fav_mem p'_fav freshv then (* the address of a de-allocated stack var in in the post *)
         begin
           stack_vars_address_in_post := v :: !stack_vars_address_in_post;
-          res := add_or_replace_exp_attribute !res (Apred (Adangling DAaddr_stack_var, Var freshv))
+          let pred = Sil.Apred (Adangling DAaddr_stack_var, [Sil.Var freshv]) in
+          res := add_or_replace_attribute !res pred
         end in
     IList.iter do_var !fresh_address_vars;
     !res in
@@ -2301,10 +2300,10 @@ let atom_captured_ren ren = function
       Sil.Aeq (exp_captured_ren ren e1, exp_captured_ren ren e2)
   | Sil.Aneq (e1, e2) ->
       Sil.Aneq (exp_captured_ren ren e1, exp_captured_ren ren e2)
-  | Sil.Apred (a, e) ->
-      Sil.Apred (a, exp_captured_ren ren e)
-  | Sil.Anpred (a, e) ->
-      Sil.Anpred (a, exp_captured_ren ren e)
+  | Sil.Apred (a, es) ->
+      Sil.Apred (a, IList.map (fun e -> exp_captured_ren ren e) es)
+  | Sil.Anpred (a, es) ->
+      Sil.Anpred (a, IList.map (fun e -> exp_captured_ren ren e) es)
 
 let rec strexp_captured_ren ren = function
   | Sil.Eexp (e, inst) ->
diff --git a/infer/src/backend/prop.mli b/infer/src/backend/prop.mli
index b58065cf4..c5a728433 100644
--- a/infer/src/backend/prop.mli
+++ b/infer/src/backend/prop.mli
@@ -223,10 +223,10 @@ val mk_neq : exp -> exp -> atom
 val mk_eq : exp -> exp -> atom
 
 (** Construct a positive pred. *)
-val mk_pred : attribute -> exp -> atom
+val mk_pred : attribute -> exp list -> atom
 
 (** Construct a negative pred. *)
-val mk_npred : attribute -> exp -> atom
+val mk_npred : attribute -> exp list -> atom
 
 (** create a strexp of the given type, populating the structures if [expand_structs] is true *)
 val create_strexp_of_type :
@@ -285,10 +285,10 @@ val atom_is_attribute : atom -> bool
 val attribute_map_resource : normal t -> (Sil.exp -> Sil.res_action -> Sil.res_action) -> normal t
 
 (** Return the exp and attribute marked in the atom if any, and return None otherwise *)
-val atom_get_exp_attribute : atom -> atom option
+val atom_get_attribute : atom -> atom option
 
 (** Get the attributes associated to the expression, if any *)
-val get_exp_attributes : 'a t -> exp -> atom list
+val get_attributes : 'a t -> exp -> atom list
 
 (** Get the undef attribute associated to the expression, if any *)
 val get_undef_attribute : 'a t -> exp -> atom option
@@ -319,15 +319,15 @@ val get_all_attributes : 'a t -> atom list
 
 val has_dangling_uninit_attribute : 'a t -> exp -> bool
 
-(** Set an attribute associated to the expression *)
-val set_exp_attribute : ?footprint: bool -> ?polarity: bool ->
-  normal t -> attribute -> exp -> normal t
+(** Set an attribute associated to the argument expressions *)
+val set_attribute : ?footprint: bool -> ?polarity: bool ->
+  normal t -> attribute -> exp list -> normal t
 
-val add_or_replace_exp_attribute_check_changed :
+val add_or_replace_attribute_check_changed :
   (Sil.attribute -> Sil.attribute -> unit) -> normal t -> atom -> normal t
 
 (** Replace an attribute associated to the expression *)
-val add_or_replace_exp_attribute : normal t -> atom -> normal t
+val add_or_replace_attribute : normal t -> atom -> normal t
 
 (** mark Sil.Var's or Sil.Lvar's as undefined *)
 val mark_vars_as_undefined : normal t -> Sil.exp list -> Procname.t -> Typ.item_annotation ->
@@ -347,8 +347,8 @@ val nullify_exp_with_objc_null : normal t -> exp -> normal t
 (** Remove an attribute from an exp in the heap *)
 val remove_attribute_from_exp : 'a t -> atom -> normal t
 
-(** Retireve all the atoms in the heap that contain a specific attribute *)
-val get_atoms_with_attribute : Sil.attribute -> 'a t -> Sil.exp list
+(** Retrieve all the atoms that contain a specific attribute *)
+val get_atoms_with_attribute : 'a t -> Sil.attribute -> Sil.atom list
 
 (** Return the sub part of [prop]. *)
 val get_sub : 'a t -> subst
diff --git a/infer/src/backend/propgraph.ml b/infer/src/backend/propgraph.ml
index 1d3bdf540..542d359c7 100644
--- a/infer/src/backend/propgraph.ml
+++ b/infer/src/backend/propgraph.ml
@@ -44,13 +44,14 @@ let edge_is_hpred = function
 
 (** Return the source of the edge *)
 let edge_get_source = function
-  | Ehpred (Sil.Hpointsto(e, _, _)) -> e
-  | Ehpred (Sil.Hlseg(_, _, e, _, _)) -> e
-  | Ehpred (Sil.Hdllseg(_, _, e1, _, _, _, _)) -> e1 (* only one direction supported for now *)
-  | Eatom (Sil.Aeq (e1, _)) -> e1
-  | Eatom (Sil.Aneq (e1, _)) -> e1
-  | Eatom (Sil.Apred (_, e) | Anpred (_, e)) -> e
-  | Esub_entry (x, _) -> Sil.Var x
+  | Ehpred (Sil.Hpointsto(e, _, _)) -> Some e
+  | Ehpred (Sil.Hlseg(_, _, e, _, _)) -> Some e
+  | Ehpred (Sil.Hdllseg(_, _, e1, _, _, _, _)) -> Some e1 (* only one direction supported for now *)
+  | Eatom (Sil.Aeq (e1, _)) -> Some e1
+  | Eatom (Sil.Aneq (e1, _)) -> Some e1
+  | Eatom (Sil.Apred (_, e :: _) | Anpred (_, e :: _)) -> Some e
+  | Eatom (Sil.Apred (_, []) | Anpred (_, [])) -> None
+  | Esub_entry (x, _) -> Some (Sil.Var x)
 
 (** Return the successor nodes of the edge *)
 let edge_get_succs = function
@@ -74,7 +75,11 @@ let edge_from_source g n footprint_part is_hpred =
     if is_hpred
     then IList.map (fun hpred -> Ehpred hpred ) (get_sigma footprint_part g)
     else IList.map (fun a -> Eatom a) (get_pi footprint_part g) @ IList.map (fun entry -> Esub_entry entry) (get_subl footprint_part g) in
-  match IList.filter (fun hpred -> Sil.exp_equal n (edge_get_source hpred)) edges with
+  let starts_from hpred =
+    match edge_get_source hpred with
+    | Some e -> Sil.exp_equal n e
+    | None -> false in
+  match IList.filter starts_from edges with
   | [] -> None
   | edge:: _ -> Some edge
 
@@ -159,10 +164,9 @@ let compute_edge_diff (oldedge: edge) (newedge: edge) : Obj.t list = match olded
       compute_exp_diff e1 e2
   | Eatom (Sil.Aneq (_, e1)), Eatom (Sil.Aneq (_, e2)) ->
       compute_exp_diff e1 e2
-  | Eatom (Sil.Apred (_, e1)), Eatom (Sil.Apred (_, e2)) ->
-      compute_exp_diff e1 e2
-  | Eatom (Sil.Anpred (_, e1)), Eatom (Sil.Anpred (_, e2)) ->
-      compute_exp_diff e1 e2
+  | Eatom (Sil.Apred (_, es1)), Eatom (Sil.Apred (_, es2))
+  | Eatom (Sil.Anpred (_, es1)), Eatom (Sil.Anpred (_, es2)) ->
+      IList.flatten (try IList.map2 compute_exp_diff es1 es2 with IList.Fail -> [])
   | Esub_entry (_, e1), Esub_entry (_, e2) ->
       compute_exp_diff e1 e2
   | _ -> [Obj.repr newedge]
@@ -173,16 +177,20 @@ let compute_diff default_color oldgraph newgraph : diff =
     let newedges = get_edges footprint_part newgraph in
     let changed = ref [] in
     let build_changed edge =
-      if not (contains_edge footprint_part oldgraph edge) then begin
-        match edge_from_source oldgraph (edge_get_source edge) footprint_part (edge_is_hpred edge) with
+      if not (contains_edge footprint_part oldgraph edge) then
+        match edge_get_source edge with
+        | Some source -> (
+            match edge_from_source oldgraph source footprint_part (edge_is_hpred edge) with
+            | None ->
+                let changed_obj = match edge with
+                  | Ehpred hpred -> Obj.repr hpred
+                  | Eatom a -> Obj.repr a
+                  | Esub_entry entry -> Obj.repr entry in
+                changed := changed_obj :: !changed
+            | Some oldedge -> changed := compute_edge_diff oldedge edge @ !changed
+          )
         | None ->
-            let changed_obj = match edge with
-              | Ehpred hpred -> Obj.repr hpred
-              | Eatom a -> Obj.repr a
-              | Esub_entry entry -> Obj.repr entry in
-            changed := changed_obj :: !changed
-        | Some oldedge -> changed := compute_edge_diff oldedge edge @ !changed
-      end in
+            () in
     IList.iter build_changed newedges;
     let colormap (o: Obj.t) =
       if IList.exists (fun x -> x == o) !changed then Red
diff --git a/infer/src/backend/propgraph.mli b/infer/src/backend/propgraph.mli
index dd8a7daad..58d366794 100644
--- a/infer/src/backend/propgraph.mli
+++ b/infer/src/backend/propgraph.mli
@@ -28,7 +28,7 @@ val is_root : node -> bool
 val nodes_connected : node -> node -> bool
 
 (** Return the source of the edge *)
-val edge_get_source : edge -> node
+val edge_get_source : edge -> node option
 
 (** Return the successor nodes of the edge *)
 val edge_get_succs : edge -> node list
diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml
index 71d0526da..7c07d9076 100644
--- a/infer/src/backend/prover.ml
+++ b/infer/src/backend/prover.ml
@@ -2109,14 +2109,12 @@ let rec pre_check_pure_implication calc_missing subs pi1 pi2 =
              imply_atom calc_missing subs prop_for_impl (Sil.Aeq (e2_in, f2_in));
              pre_check_pure_implication calc_missing subs pi1 pi2'
         )
-  | Sil.Aeq _ :: pi2' -> (* must be an inequality *)
+  | (Sil.Aneq (e, _) | Apred (_, e :: _) | Anpred (_, e :: _)) :: _
+    when not calc_missing && (match e with Var v -> not (Ident.is_primed v) | _ -> true) ->
+      raise (IMPL_EXC ("ineq e2=f2 in rhs with e2 not primed var",
+                       (Sil.sub_empty, Sil.sub_empty), EXC_FALSE))
+  | (Sil.Aeq _ | Aneq _ | Apred _ | Anpred _) :: pi2' ->
       pre_check_pure_implication calc_missing subs pi1 pi2'
-  | (Sil.Aneq (e, _) | Apred (_, e) | Anpred (_, e)) :: pi2' ->
-      if calc_missing || (match e with Var v -> Ident.is_primed v | _ -> false) then
-        pre_check_pure_implication calc_missing subs pi1 pi2'
-      else
-        raise (IMPL_EXC ("ineq e2=f2 in rhs with e2 not primed var",
-                         (Sil.sub_empty, Sil.sub_empty), EXC_FALSE))
 
 (** Perform the array bound checks delayed (to instantiate variables) by the prover.
     If there is a provable violation of the array bounds, set the prover status to Bounds_check
diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml
index 491c65717..cec9f4f5b 100644
--- a/infer/src/backend/rearrange.ml
+++ b/infer/src/backend/rearrange.ml
@@ -746,7 +746,7 @@ let add_guarded_by_constraints prop lexp pdesc =
         (function
           | Sil.Apred (Alocked, _) -> true
           | _ -> false)
-        (Prop.get_exp_attributes prop guarded_by_exp) in
+        (Prop.get_attributes prop guarded_by_exp) in
     let should_warn pdesc =
       (* adding this check implements "by reference" semantics for guarded-by rather than "by value"
          semantics. if this access is through a local L or field V.f
@@ -793,7 +793,7 @@ let add_guarded_by_constraints prop lexp pdesc =
           end
         else
           (* private method. add locked proof obligation to [pdesc] *)
-          Prop.set_exp_attribute ~footprint:true prop Alocked guarded_by_exp
+          Prop.set_attribute ~footprint:true prop Alocked [guarded_by_exp]
     | _ ->
         if not (proc_has_matching_annot pdesc guarded_by_str
                 || is_synchronized_on_class guarded_by_str) && should_warn pdesc
@@ -1205,7 +1205,7 @@ let check_dereference_error pdesc (prop : Prop.normal Prop.t) lexp loc =
                        nullable_obj_str := Some (Procname.to_string pname);
                        true
                    | _ -> false in
-                 IList.exists is_nullable_attr (Prop.get_exp_attributes prop exp) in
+                 IList.exists is_nullable_attr (Prop.get_attributes prop exp) in
              (* it's ok for a non-nullable local to point to deref_exp *)
              is_nullable || Pvar.is_local pvar
          | Sil.Hpointsto (_, Sil.Estruct (flds, _), Sil.Sizeof (typ, _, _)) ->
diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml
index 27c85fb55..55964d033 100644
--- a/infer/src/backend/symExec.ml
+++ b/infer/src/backend/symExec.ml
@@ -476,11 +476,11 @@ let check_already_dereferenced pname cond prop =
     raising an exception in that case *)
 let check_deallocate_static_memory prop_after =
   let check_deallocated_attribute = function
-    | Sil.Apred (Aresource ({ ra_kind = Rrelease } as ra), Lvar pv)
+    | Sil.Apred (Aresource ({ ra_kind = Rrelease } as ra), [Lvar pv])
       when Pvar.is_local pv || Pvar.is_global pv ->
         let freed_desc = Errdesc.explain_deallocate_stack_var pv ra in
         raise (Exceptions.Deallocate_stack_variable freed_desc)
-    | Sil.Apred (Aresource ({ ra_kind = Rrelease } as ra), Const (Cstr s)) ->
+    | Sil.Apred (Aresource ({ ra_kind = Rrelease } as ra), [Const (Cstr s)]) ->
         let freed_desc = Errdesc.explain_deallocate_constant_string s ra in
         raise (Exceptions.Deallocate_static_memory freed_desc)
     | _ -> () in
@@ -738,7 +738,7 @@ let handle_objc_instance_method_call_or_skip actual_pars path callee_pname pre r
     | [ret_id] -> (
         match Prop.find_equal_formal_path receiver prop with
         | Some (v,fs) ->
-            Prop.add_or_replace_exp_attribute prop (Apred (Aobjc_null (v,fs), Var ret_id))
+            Prop.add_or_replace_attribute prop (Apred (Aobjc_null (v,fs), [Sil.Var ret_id]))
         | None ->
             Prop.conjoin_eq (Sil.Var ret_id) Sil.exp_zero prop
       )
@@ -843,7 +843,7 @@ let add_constraints_on_retval pdesc prop ret_exp ~has_nullable_annot typ callee_
         | Typ.Tptr _ -> Prop.conjoin_neq exp Sil.exp_zero prop
         | _ -> prop in
     let add_tainted_post ret_exp callee_pname prop =
-      Prop.add_or_replace_exp_attribute prop (Apred (Ataint callee_pname, ret_exp)) in
+      Prop.add_or_replace_attribute prop (Apred (Ataint callee_pname, [ret_exp])) in
 
     if Config.angelic_execution && not (is_rec_call callee_pname) then
       (* introduce a fresh program variable to allow abduction on the return value *)
@@ -872,7 +872,7 @@ let add_taint prop lhs_id rhs_exp pname tenv  =
     if Taint.has_taint_annotation fieldname struct_typ
     then
       let taint_info = { Sil.taint_source = pname; taint_kind = Tk_unknown; } in
-      Prop.add_or_replace_exp_attribute prop (Apred (Ataint taint_info, Var lhs_id))
+      Prop.add_or_replace_attribute prop (Apred (Ataint taint_info, [Sil.Var lhs_id]))
     else
       prop in
   match rhs_exp with
@@ -903,7 +903,7 @@ let execute_letderef ?(report_deref_errors=true) pname pdesc tenv id rhs_exp typ
           let prop' = Prop.prop_iter_to_prop iter' in
           let prop'' =
             if lookup_uninitialized then
-              Prop.add_or_replace_exp_attribute prop' (Apred (Adangling DAuninit, Var id))
+              Prop.add_or_replace_attribute prop' (Apred (Adangling DAuninit, [Sil.Var id]))
             else prop' in
           let prop''' =
             if Config.taint_analysis
@@ -936,7 +936,7 @@ let execute_letderef ?(report_deref_errors=true) pname pdesc tenv id rhs_exp typ
             match callee_opt, atom with
             | None, Sil.Apred (Aundef _, _) -> Some atom
             | _ -> callee_opt in
-          IList.fold_left fold_undef_pname None (Prop.get_exp_attributes prop exp) in
+          IList.fold_left fold_undef_pname None (Prop.get_attributes prop exp) in
         let prop' =
           if Config.angelic_execution then
             (* when we try to deref an undefined value, add it to the footprint *)
@@ -1375,12 +1375,12 @@ and check_untainted exp taint_kind caller_pname callee_pname prop =
         Exceptions.Tainted_value_reaching_sensitive_function
           (err_desc, __POS__) in
       Reporting.log_warning caller_pname exn;
-      Prop.add_or_replace_exp_attribute prop (Apred (Auntaint taint_info, exp))
+      Prop.add_or_replace_attribute prop (Apred (Auntaint taint_info, [exp]))
   | _ ->
       if !Config.footprint then
         let taint_info = { Sil.taint_source = callee_pname; taint_kind; } in
         (* add untained(n_lexp) to the footprint *)
-        Prop.set_exp_attribute ~footprint:true prop (Auntaint taint_info) exp
+        Prop.set_attribute ~footprint:true prop (Auntaint taint_info) [exp]
       else prop
 
 (** execute a call for an unknown or scan function *)
@@ -1393,7 +1393,7 @@ and unknown_or_scan_call ~is_scan ret_type_option ret_annots
         match atom with
         | Sil.Apred ((Aresource {ra_res = Rfile} as res), _) -> Prop.remove_attribute q res
         | _ -> q in
-      IList.fold_left do_attribute p (Prop.get_exp_attributes p e) in
+      IList.fold_left do_attribute p (Prop.get_attributes p e) in
     let filtered_args =
       match args, instr with
       | _:: other_args, Sil.Call (_, _, _, _, { CallFlags.cf_virtual }) when cf_virtual ->
diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml
index 5e2efcdae..75bfee619 100644
--- a/infer/src/backend/tabulation.ml
+++ b/infer/src/backend/tabulation.ml
@@ -362,7 +362,7 @@ let post_process_sigma (sigma: Sil.hpred list) loc : Sil.hpred list =
 let check_path_errors_in_post caller_pname post post_path =
   let check_attr atom =
     match atom with
-    | Sil.Apred (Adiv0 path_pos, e) ->
+    | Sil.Apred (Adiv0 path_pos, [e]) ->
         if Prover.check_zero e then
           let desc = Errdesc.explain_divide_by_zero e (State.get_node ()) (State.get_loc ()) in
           let new_path, path_pos_opt =
@@ -386,12 +386,12 @@ let post_process_post
     | Some (Apred (Aresource ({ ra_kind = Rrelease }), _)) -> true
     | _ -> false in
   let atom_update_alloc_attribute = function
-    | Sil.Apred (Aresource ra, e)
+    | Sil.Apred (Aresource ra, [e])
       when not (ra.Sil.ra_kind = Sil.Rrelease && actual_pre_has_freed_attribute e) ->
         (* unless it was already freed before the call *)
         let vpath, _ = Errdesc.vpath_find post e in
         let ra' = { ra with Sil.ra_pname = callee_pname; Sil.ra_loc = loc; Sil.ra_vpath = vpath } in
-        Sil.Apred (Aresource ra', e)
+        Sil.Apred (Aresource ra', [e])
     | a -> a in
   let prop' = Prop.replace_sigma (post_process_sigma (Prop.get_sigma post) loc) post in
   let pi' = IList.map atom_update_alloc_attribute (Prop.get_pi prop') in
@@ -603,10 +603,10 @@ let prop_copy_footprint_pure p1 p2 =
   let res_noattr = Prop.replace_pi (Prop.get_pure p1 @ pi2_noattr) p2' in
   let replace_attr prop atom = (* call replace_atom_attribute which deals with existing attibutes *)
     (* if [atom] represents an attribute [att], add the attribure to [prop] *)
-    match Prop.atom_get_exp_attribute atom with
+    match Prop.atom_get_attribute atom with
     | None -> prop
     | Some atom ->
-        Prop.add_or_replace_exp_attribute_check_changed check_attr_dealloc_mismatch prop atom in
+        Prop.add_or_replace_attribute_check_changed check_attr_dealloc_mismatch prop atom in
   IList.fold_left replace_attr (Prop.normalize res_noattr) pi2_attr
 
 (** check if an expression is an exception *)
@@ -884,7 +884,7 @@ let mk_posts ret_ids prop callee_pname callee_attrs posts =
         let last_call_ret_non_null =
           IList.exists
             (function
-              | Sil.Apred (Aretval (pname, _), exp) when Procname.equal callee_pname pname ->
+              | Sil.Apred (Aretval (pname, _), [exp]) when Procname.equal callee_pname pname ->
                   Prover.check_disequal prop exp Sil.exp_zero
               | _ -> false)
             (Prop.get_all_attributes prop) in
@@ -904,8 +904,8 @@ let mk_posts ret_ids prop callee_pname callee_attrs posts =
             let taint_retval (prop, path) =
               let prop_normal = Prop.normalize prop in
               let prop' =
-                Prop.add_or_replace_exp_attribute prop_normal
-                  (Apred (Ataint { taint_source = callee_pname; taint_kind; }, Var ret_id))
+                Prop.add_or_replace_attribute prop_normal
+                  (Apred (Ataint { taint_source = callee_pname; taint_kind; }, [Sil.Var ret_id]))
                 |> Prop.expose in
               (prop', path) in
             IList.map taint_retval posts
@@ -936,11 +936,11 @@ let do_taint_check caller_pname callee_pname calling_prop missing_pi sub actual_
   (* build a map from exp -> [taint attrs, untaint attrs], keeping only exprs with both kinds of
      attrs (we will flag errors on those exprs) *)
   let collect_taint_untaint_exprs acc_map atom =
-    match Prop.atom_get_exp_attribute atom with
-    | Some (Apred (Ataint _, e)) ->
+    match Prop.atom_get_attribute atom with
+    | Some (Apred (Ataint _, [e])) ->
         let taint_atoms, untaint_atoms = try Sil.ExpMap.find e acc_map with Not_found -> ([], []) in
         Sil.ExpMap.add e (atom :: taint_atoms, untaint_atoms) acc_map
-    | Some (Apred (Auntaint _, e)) ->
+    | Some (Apred (Auntaint _, [e])) ->
         let taint_atoms, untaint_atoms = try Sil.ExpMap.find e acc_map with Not_found -> ([], []) in
         Sil.ExpMap.add e (taint_atoms, atom :: untaint_atoms) acc_map
     | _ -> acc_map in
@@ -955,7 +955,7 @@ let do_taint_check caller_pname callee_pname calling_prop missing_pi sub actual_
      the untaint atoms *)
   let report_taint_errors e (taint_atoms, _untaint_atoms) =
     let report_one_error taint_atom =
-      let taint_info = match Prop.atom_get_exp_attribute taint_atom with
+      let taint_info = match Prop.atom_get_attribute taint_atom with
         | Some (Apred (Ataint taint_info, _)) -> taint_info
         | _ -> failwith "Expected to get taint attr on atom" in
       report_taint_error e taint_info callee_pname caller_pname calling_prop in
@@ -1262,7 +1262,7 @@ let exe_call_postprocess ret_ids trace_call callee_pname callee_attrs loc result
       let ret_var = Sil.Var ret_id in
       let mark_id_as_retval (p, path) =
         let att_retval = Sil.Aretval (callee_pname, ret_annot) in
-        Prop.set_exp_attribute p att_retval ret_var, path in
+        Prop.set_attribute p att_retval [ret_var], path in
       IList.map mark_id_as_retval res
   | _ -> res
 
diff --git a/infer/src/backend/taint.ml b/infer/src/backend/taint.ml
index eb0e55148..b5cbc2776 100644
--- a/infer/src/backend/taint.ml
+++ b/infer/src/backend/taint.ml
@@ -379,6 +379,6 @@ let add_tainting_attribute att pvar_param prop =
          when Pvar.equal pvar pvar_param ->
            L.d_strln ("TAINT ANALYSIS: setting taint/untaint attribute of parameter " ^
                       (Pvar.to_string pvar));
-           Prop.add_or_replace_exp_attribute prop_acc (Apred (att, rhs))
+           Prop.add_or_replace_attribute prop_acc (Apred (att, [rhs]))
        | _ -> prop_acc)
     prop (Prop.get_sigma prop)