diff --git a/infer/src/IR/Cfg.re b/infer/src/IR/Cfg.re
index e5cb7ec09..db94e0f70 100644
--- a/infer/src/IR/Cfg.re
+++ b/infer/src/IR/Cfg.re
@@ -897,7 +897,7 @@ let get_name_of_objc_block_locals p => {
   IList.flatten (IList.flatten vars_sigma)
 };
 
-let remove_abducted_retvars tenv p =>
+let remove_abduced_retvars tenv p =>
   /* compute the hpreds and pure atoms reachable from the set of seed expressions in [exps] */
   {
     let compute_reachable p seed_exps => {
@@ -967,31 +967,31 @@ let remove_abducted_retvars tenv p =>
       };
       (Sil.HpredSet.elements reach_hpreds, reach_pi)
     };
-    /* separate the abducted pvars from the normal ones, deallocate the abducted ones*/
-    let (abducteds, normal_pvars) =
+    /* separate the abduced pvars from the normal ones, deallocate the abduced ones*/
+    let (abduceds, normal_pvars) =
       IList.fold_left
         (
           fun pvars hpred =>
             switch hpred {
             | Sil.Hpointsto (Exp.Lvar pvar) _ _ =>
-              let (abducteds, normal_pvars) = pvars;
-              if (Pvar.is_abducted pvar) {
-                ([pvar, ...abducteds], normal_pvars)
+              let (abduceds, normal_pvars) = pvars;
+              if (Pvar.is_abduced pvar) {
+                ([pvar, ...abduceds], normal_pvars)
               } else {
-                (abducteds, [pvar, ...normal_pvars])
+                (abduceds, [pvar, ...normal_pvars])
               }
             | _ => pvars
             }
         )
         ([], [])
         p.Prop.sigma;
-    let (_, p') = Attribute.deallocate_stack_vars tenv p abducteds;
+    let (_, p') = Attribute.deallocate_stack_vars tenv p abduceds;
     let normal_pvar_set =
       IList.fold_left
         (fun normal_pvar_set pvar => Exp.Set.add (Exp.Lvar pvar) normal_pvar_set)
         Exp.Set.empty
         normal_pvars;
-    /* walk forward from non-abducted pvars, keep everything reachable. remove everything else */
+    /* walk forward from non-abduced pvars, keep everything reachable. remove everything else */
     let (sigma_reach, pi_reach) = compute_reachable p' normal_pvar_set;
     Prop.normalize tenv (Prop.set p' pi::pi_reach sigma::sigma_reach)
   };
@@ -1011,7 +1011,7 @@ let remove_locals tenv (curr_f: Procdesc.t) p => {
   (
     removed,
     if Config.angelic_execution {
-      remove_abducted_retvars tenv p'
+      remove_abduced_retvars tenv p'
     } else {
       p'
     }
diff --git a/infer/src/IR/Pvar.re b/infer/src/IR/Pvar.re
index aa9560fb5..ff0eb1f2e 100644
--- a/infer/src/IR/Pvar.re
+++ b/infer/src/IR/Pvar.re
@@ -24,8 +24,8 @@ let module F = Format;
 type pvar_kind =
   | Local_var of Procname.t /** local variable belonging to a function */
   | Callee_var of Procname.t /** local variable belonging to a callee */
-  | Abducted_retvar of Procname.t Location.t /** synthetic variable to represent return value */
-  | Abducted_ref_param of Procname.t t Location.t
+  | Abduced_retvar of Procname.t Location.t /** synthetic variable to represent return value */
+  | Abduced_ref_param of Procname.t t Location.t
   /** synthetic variable to represent param passed by reference */
   | Global_var /** gloval variable */
   | Seed_var /** variable used to store the initial value of formal parameters */
@@ -40,16 +40,16 @@ let rec pvar_kind_compare k1 k2 =>
   | (Callee_var n1, Callee_var n2) => Procname.compare n1 n2
   | (Callee_var _, _) => (-1)
   | (_, Callee_var _) => 1
-  | (Abducted_retvar p1 l1, Abducted_retvar p2 l2) =>
+  | (Abduced_retvar p1 l1, Abduced_retvar p2 l2) =>
     let n = Procname.compare p1 p2;
     if (n != 0) {
       n
     } else {
       Location.compare l1 l2
     }
-  | (Abducted_retvar _, _) => (-1)
-  | (_, Abducted_retvar _) => 1
-  | (Abducted_ref_param p1 pv1 l1, Abducted_ref_param p2 pv2 l2) =>
+  | (Abduced_retvar _, _) => (-1)
+  | (_, Abduced_retvar _) => 1
+  | (Abduced_ref_param p1 pv1 l1, Abduced_ref_param p2 pv2 l2) =>
     let n = Procname.compare p1 p2;
     if (n != 0) {
       n
@@ -61,8 +61,8 @@ let rec pvar_kind_compare k1 k2 =>
         Location.compare l1 l2
       }
     }
-  | (Abducted_ref_param _, _) => (-1)
-  | (_, Abducted_ref_param _) => 1
+  | (Abduced_ref_param _, _) => (-1)
+  | (_, Abduced_ref_param _) => 1
   | (Global_var, Global_var) => 0
   | (Global_var, _) => (-1)
   | (_, Global_var) => 1
@@ -94,17 +94,17 @@ let rec _pp f pv => {
     } else {
       F.fprintf f "%a$%a|callee" Procname.pp n Mangled.pp name
     }
-  | Abducted_retvar n l =>
+  | Abduced_retvar n l =>
     if !Config.pp_simple {
-      F.fprintf f "%a|abductedRetvar" Mangled.pp name
+      F.fprintf f "%a|abducedRetvar" Mangled.pp name
     } else {
-      F.fprintf f "%a$%a%a|abductedRetvar" Procname.pp n Location.pp l Mangled.pp name
+      F.fprintf f "%a$%a%a|abducedRetvar" Procname.pp n Location.pp l Mangled.pp name
     }
-  | Abducted_ref_param n pv l =>
+  | Abduced_ref_param n pv l =>
     if !Config.pp_simple {
-      F.fprintf f "%a|%a|abductedRefParam" _pp pv Mangled.pp name
+      F.fprintf f "%a|%a|abducedRefParam" _pp pv Mangled.pp name
     } else {
-      F.fprintf f "%a$%a%a|abductedRefParam" Procname.pp n Location.pp l Mangled.pp name
+      F.fprintf f "%a$%a%a|abducedRefParam" Procname.pp n Location.pp l Mangled.pp name
     }
   | Global_var => F.fprintf f "#GB$%a" Mangled.pp name
   | Seed_var => F.fprintf f "old_%a" Mangled.pp name
@@ -125,22 +125,22 @@ let pp_latex f pv => {
       (Mangled.to_string name)
       (Latex.pp_string Latex.Roman)
       "callee"
-  | Abducted_retvar _ =>
+  | Abduced_retvar _ =>
     F.fprintf
       f
       "%a_{%a}"
       (Latex.pp_string Latex.Roman)
       (Mangled.to_string name)
       (Latex.pp_string Latex.Roman)
-      "abductedRetvar"
-  | Abducted_ref_param _ =>
+      "abducedRetvar"
+  | Abduced_ref_param _ =>
     F.fprintf
       f
       "%a_{%a}"
       (Latex.pp_string Latex.Roman)
       (Mangled.to_string name)
       (Latex.pp_string Latex.Roman)
-      "abductedRefParam"
+      "abducedRefParam"
   | Global_var => Latex.pp_string Latex.Boldface f (Mangled.to_string name)
   | Seed_var =>
     F.fprintf
@@ -212,10 +212,10 @@ let get_simplified_name pv => {
 
 
 /** Check if the pvar is an abucted return var or param passed by ref */
-let is_abducted pv =>
+let is_abduced pv =>
   switch pv.pv_kind {
-  | Abducted_retvar _
-  | Abducted_ref_param _ => true
+  | Abduced_retvar _
+  | Abduced_ref_param _ => true
   | _ => false
   };
 
@@ -287,8 +287,8 @@ let to_callee pname pvar =>
   | Local_var _ => {...pvar, pv_kind: Callee_var pname}
   | Global_var => pvar
   | Callee_var _
-  | Abducted_retvar _
-  | Abducted_ref_param _
+  | Abduced_retvar _
+  | Abduced_ref_param _
   | Seed_var =>
     L.d_str "Cannot convert pvar to callee: ";
     d pvar;
@@ -326,13 +326,13 @@ let mk_tmp name pname => {
 };
 
 
-/** create an abducted return variable for a call to [proc_name] at [loc] */
-let mk_abducted_ret (proc_name: Procname.t) (loc: Location.t) :t => {
+/** create an abduced return variable for a call to [proc_name] at [loc] */
+let mk_abduced_ret (proc_name: Procname.t) (loc: Location.t) :t => {
   let name = Mangled.from_string ("$RET_" ^ Procname.to_unique_id proc_name);
-  {pv_name: name, pv_kind: Abducted_retvar proc_name loc}
+  {pv_name: name, pv_kind: Abduced_retvar proc_name loc}
 };
 
-let mk_abducted_ref_param (proc_name: Procname.t) (pv: t) (loc: Location.t) :t => {
+let mk_abduced_ref_param (proc_name: Procname.t) (pv: t) (loc: Location.t) :t => {
   let name = Mangled.from_string ("$REF_PARAM_" ^ Procname.to_unique_id proc_name);
-  {pv_name: name, pv_kind: Abducted_ref_param proc_name pv loc}
+  {pv_name: name, pv_kind: Abduced_ref_param proc_name pv loc}
 };
diff --git a/infer/src/IR/Pvar.rei b/infer/src/IR/Pvar.rei
index 3560df90c..ce9655ebd 100644
--- a/infer/src/IR/Pvar.rei
+++ b/infer/src/IR/Pvar.rei
@@ -55,8 +55,8 @@ let get_ret_pvar: Procname.t => t;
 let get_simplified_name: t => string;
 
 
-/** Check if the pvar is an abducted return var or param passed by ref */
-let is_abducted: t => bool;
+/** Check if the pvar is an abduced return var or param passed by ref */
+let is_abduced: t => bool;
 
 
 /** Check if the pvar is a callee var */
@@ -91,12 +91,12 @@ let is_frontend_tmp: t => bool;
 let mk: Mangled.t => Procname.t => t;
 
 
-/** create an abducted variable for a parameter passed by reference */
-let mk_abducted_ref_param: Procname.t => t => Location.t => t;
+/** create an abduced variable for a parameter passed by reference */
+let mk_abduced_ref_param: Procname.t => t => Location.t => t;
 
 
-/** create an abducted return variable for a call to [proc_name] at [loc] */
-let mk_abducted_ret: Procname.t => Location.t => t;
+/** create an abduced return variable for a call to [proc_name] at [loc] */
+let mk_abduced_ret: Procname.t => Location.t => t;
 
 
 /** [mk_callee name proc_name] creates a program var
diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml
index 61acfccf1..9a7b3bd62 100644
--- a/infer/src/backend/errdesc.ml
+++ b/infer/src/backend/errdesc.ml
@@ -981,7 +981,7 @@ let explain_nth_function_parameter tenv use_buckets deref_str prop n pvar_off =
 let find_with_exp prop exp =
   let res = ref None in
   let found_in_pvar pv =
-    if not (Pvar.is_abducted pv) && not (Pvar.is_this pv) then
+    if not (Pvar.is_abduced pv) && not (Pvar.is_this pv) then
       res := Some (pv, Fpvar) in
   let found_in_struct pv fld_lst = (* found_in_pvar has priority *)
     if !res = None then res := Some (pv, Fstruct (IList.rev fld_lst)) in
diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml
index e4d4f7219..318cc9a18 100644
--- a/infer/src/backend/interproc.ml
+++ b/infer/src/backend/interproc.ml
@@ -842,7 +842,7 @@ let collect_postconditions wl tenv pdesc : Paths.PathSet.t * Specs.Visitedset.t
 
 let create_seed_vars sigma =
   let hpred_add_seed sigma = function
-    | Sil.Hpointsto (Exp.Lvar pv, se, typ) when not (Pvar.is_abducted pv) ->
+    | Sil.Hpointsto (Exp.Lvar pv, se, typ) when not (Pvar.is_abduced pv) ->
         Sil.Hpointsto(Exp.Lvar (Pvar.to_seed pv), se, typ) :: sigma
     | _ -> sigma in
   IList.fold_left hpred_add_seed [] sigma
diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml
index 7ae275a3f..fe80049a9 100644
--- a/infer/src/backend/symExec.ml
+++ b/infer/src/backend/symExec.ml
@@ -789,27 +789,28 @@ let do_error_checks tenv node_opt instr pname pdesc = match node_opt with
   | None ->
       ()
 
-let add_strexp_to_footprint tenv strexp abducted_pv typ prop =
-  let abducted_lvar = Exp.Lvar abducted_pv in
+let add_strexp_to_footprint tenv strexp abduced_pv typ prop =
+  let abduced_lvar = Exp.Lvar abduced_pv in
   let lvar_pt_fpvar =
     let sizeof_exp = Exp.Sizeof (typ, None, Subtype.subtypes) in
-    Prop.mk_ptsto tenv abducted_lvar strexp sizeof_exp in
+    Prop.mk_ptsto tenv abduced_lvar strexp sizeof_exp in
   let sigma_fp = prop.Prop.sigma_fp in
   Prop.normalize tenv (Prop.set prop ~sigma_fp:(lvar_pt_fpvar :: sigma_fp))
 
-let add_to_footprint tenv abducted_pv typ prop =
+let add_to_footprint tenv abduced_pv typ prop =
   let fresh_fp_var = Exp.Var (Ident.create_fresh Ident.kfootprint) in
-  let prop' = add_strexp_to_footprint tenv (Sil.Eexp (fresh_fp_var, Sil.Inone)) abducted_pv typ prop in
+  let prop' =
+    add_strexp_to_footprint tenv (Sil.Eexp (fresh_fp_var, Sil.Inone)) abduced_pv typ prop in
   prop', fresh_fp_var
 
 (* the current abduction mechanism treats struct values differently than all other types. abduction
    on struct values adds a a struct whose fields are initialized to fresh footprint vars to the
    footprint. regular abduction just adds a fresh footprint value of the correct type to the
    footprint. we can get rid of this special case if we fix the abduction on struct values *)
-let add_struct_value_to_footprint tenv abducted_pv typ prop =
+let add_struct_value_to_footprint tenv abduced_pv typ prop =
   let struct_strexp =
     Prop.create_strexp_of_type tenv Prop.Fld_init typ None Sil.inst_none in
-  let prop' = add_strexp_to_footprint tenv struct_strexp abducted_pv typ prop in
+  let prop' = add_strexp_to_footprint tenv struct_strexp abduced_pv typ prop in
   prop', struct_strexp
 
 let add_constraints_on_retval tenv pdesc prop ret_exp ~has_nullable_annot typ callee_pname callee_loc=
@@ -817,17 +818,17 @@ let add_constraints_on_retval tenv pdesc prop ret_exp ~has_nullable_annot typ ca
   else
     let is_rec_call pname = (* TODO: (t7147096) extend this to detect mutual recursion *)
       Procname.equal pname (Cfg.Procdesc.get_proc_name pdesc) in
-    let already_has_abducted_retval p abducted_ret_pv =
+    let already_has_abduced_retval p abduced_ret_pv =
       IList.exists
         (fun hpred -> match hpred with
-           | Sil.Hpointsto (Exp.Lvar pv, _, _) -> Pvar.equal pv abducted_ret_pv
+           | Sil.Hpointsto (Exp.Lvar pv, _, _) -> Pvar.equal pv abduced_ret_pv
            | _ -> false)
         p.Prop.sigma_fp in
-    (* find an hpred [abducted] |-> A in [prop] and add [exp] = A to prop *)
-    let bind_exp_to_abducted_val exp_to_bind abducted prop =
+    (* find an hpred [abduced] |-> A in [prop] and add [exp] = A to prop *)
+    let bind_exp_to_abduced_val exp_to_bind abduced prop =
       let bind_exp prop = function
         | Sil.Hpointsto (Exp.Lvar pv, Sil.Eexp (rhs, _), _)
-          when Pvar.equal pv abducted ->
+          when Pvar.equal pv abduced ->
             Prop.conjoin_eq tenv exp_to_bind rhs prop
         | _ -> prop in
       IList.fold_left bind_exp prop prop.Prop.sigma in
@@ -845,17 +846,17 @@ let add_constraints_on_retval tenv pdesc prop ret_exp ~has_nullable_annot typ ca
 
     if Config.angelic_execution && not (is_rec_call callee_pname) then
       (* introduce a fresh program variable to allow abduction on the return value *)
-      let abducted_ret_pv = Pvar.mk_abducted_ret callee_pname callee_loc in
-      (* prevent introducing multiple abducted retvals for a single call site in a loop *)
-      if already_has_abducted_retval prop abducted_ret_pv then prop
+      let abduced_ret_pv = Pvar.mk_abduced_ret callee_pname callee_loc in
+      (* prevent introducing multiple abduced retvals for a single call site in a loop *)
+      if already_has_abduced_retval prop abduced_ret_pv then prop
       else
         let prop' =
           if !Config.footprint then
-            let (prop', fresh_fp_var) = add_to_footprint tenv abducted_ret_pv typ prop in
+            let (prop', fresh_fp_var) = add_to_footprint tenv abduced_ret_pv typ prop in
             Prop.conjoin_eq tenv ~footprint: true ret_exp fresh_fp_var prop'
           else
-            (* bind return id to the abducted value pointed to by the pvar we introduced *)
-            bind_exp_to_abducted_val ret_exp abducted_ret_pv prop in
+            (* bind return id to the abduced value pointed to by the pvar we introduced *)
+            bind_exp_to_abduced_val ret_exp abduced_ret_pv prop in
         let prop'' = add_ret_non_null ret_exp typ prop' in
         if Config.taint_analysis then
           match Taint.returns_tainted callee_pname None with
@@ -1291,27 +1292,27 @@ and add_constraints_on_actuals_by_ref tenv prop actuals_by_ref callee_pname call
     match actual with
     | Exp.Lvar actual_pv ->
         (* introduce a fresh program variable to allow abduction on the return value *)
-        let abducted_ref_pv =
-          Pvar.mk_abducted_ref_param callee_pname actual_pv callee_loc in
-        let already_has_abducted_retval p =
+        let abduced_ref_pv =
+          Pvar.mk_abduced_ref_param callee_pname actual_pv callee_loc in
+        let already_has_abduced_retval p =
           IList.exists
             (fun hpred -> match hpred with
-               | Sil.Hpointsto (Exp.Lvar pv, _, _) -> Pvar.equal pv abducted_ref_pv
+               | Sil.Hpointsto (Exp.Lvar pv, _, _) -> Pvar.equal pv abduced_ref_pv
                | _ -> false)
             p.Prop.sigma_fp in
-        (* prevent introducing multiple abducted retvals for a single call site in a loop *)
-        if already_has_abducted_retval prop then prop
+        (* prevent introducing multiple abduced retvals for a single call site in a loop *)
+        if already_has_abduced_retval prop then prop
         else
         if !Config.footprint then
           let prop', abduced_strexp = match actual_typ with
             | Typ.Tptr ((Typ.Tstruct _) as typ, _) ->
                 (* for struct types passed by reference, do abduction on the fields of the
                    struct *)
-                add_struct_value_to_footprint tenv abducted_ref_pv typ prop
+                add_struct_value_to_footprint tenv abduced_ref_pv typ prop
             | Typ.Tptr (typ, _) ->
                 (* for pointer types passed by reference, do abduction directly on the pointer *)
                 let (prop', fresh_fp_var) =
-                  add_to_footprint tenv abducted_ref_pv typ prop in
+                  add_to_footprint tenv abduced_ref_pv typ prop in
                 prop', Sil.Eexp (fresh_fp_var, Sil.Inone)
             | typ ->
                 failwith
@@ -1327,7 +1328,7 @@ and add_constraints_on_actuals_by_ref tenv prop actuals_by_ref callee_pname call
               prop'.Prop.sigma in
           Prop.normalize tenv (Prop.set prop' ~sigma:filtered_sigma)
         else
-          (* bind actual passed by ref to the abducted value pointed to by the synthetic pvar *)
+          (* bind actual passed by ref to the abduced value pointed to by the synthetic pvar *)
           let prop' =
             let filtered_sigma =
               IList.filter
@@ -1340,7 +1341,7 @@ and add_constraints_on_actuals_by_ref tenv prop actuals_by_ref callee_pname call
           IList.fold_left
             (fun p hpred ->
                match hpred with
-               | Sil.Hpointsto (Exp.Lvar pv, rhs, texp) when Pvar.equal pv abducted_ref_pv ->
+               | Sil.Hpointsto (Exp.Lvar pv, rhs, texp) when Pvar.equal pv abduced_ref_pv ->
                    let new_hpred = Sil.Hpointsto (actual, rhs, texp) in
                    Prop.normalize tenv (Prop.set p ~sigma:(new_hpred :: prop'.Prop.sigma))
                | _ -> p)