diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml
index b275f2f83..9a1ed8a8f 100644
--- a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml
+++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml
@@ -233,18 +233,8 @@ module TransferFunctions = struct
         in
         let mem =
           match PowLoc.is_singleton_or_more locs with
-          | IContainer.Singleton loc_v -> (
-              let pname = Summary.get_proc_name summary in
-              match Typ.Procname.get_method pname with
-              | "__inferbo_empty" when Loc.is_return loc_v -> (
-                match Procdesc.get_pvar_formals (Summary.get_proc_desc summary) with
-                | [(formal, _)] ->
-                    let formal_v = Dom.Mem.find (Loc.of_pvar formal) mem in
-                    Dom.Mem.store_empty_alias formal_v loc_v mem
-                | _ ->
-                    assert false )
-              | _ ->
-                  Dom.Mem.store_simple_alias loc_v exp2 mem )
+          | IContainer.Singleton loc_v ->
+              Dom.Mem.store_simple_alias loc_v exp2 mem
           | _ ->
               mem
         in
diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml
index 074033f8a..5f6ea6633 100644
--- a/infer/src/bufferoverrun/bufferOverrunDomain.ml
+++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml
@@ -189,8 +189,6 @@ module Val = struct
     of_itv (Itv.set_lb_zero (Itv.of_int max_char))
 
 
-  let modify_itv : Itv.t -> t -> t = fun i x -> {x with itv= i}
-
   let unknown_bit : t -> t = fun x -> {x with itv= Itv.top; sym= Relation.Sym.top}
 
   let neg : t -> t = fun x -> {x with itv= Itv.neg x.itv; sym= Relation.Sym.top}
@@ -697,7 +695,6 @@ module AliasTarget = struct
     | Empty of Loc.t
     | Size of Loc.t
     | Fgets of Loc.t
-    | Nullity of Loc.t
     | Top
   [@@deriving compare]
 
@@ -715,18 +712,14 @@ module AliasTarget = struct
         F.fprintf fmt "size(%a)" Loc.pp l
     | Fgets l ->
         F.fprintf fmt "fgets(%a)" Loc.pp l
-    | Nullity l ->
-        F.fprintf fmt "nullity(%a)" Loc.pp l
     | Top ->
         F.fprintf fmt "T"
 
 
   let fgets l = Fgets l
 
-  let nullity l = Nullity l
-
   let get_loc = function
-    | Simple l | SimplePlusA (l, _) | Empty l | Size l | Fgets l | Nullity l ->
+    | Simple l | SimplePlusA (l, _) | Empty l | Size l | Fgets l ->
         Some l
     | Top ->
         None
@@ -746,8 +739,6 @@ module AliasTarget = struct
         Option.map (f l) ~f:(fun l -> Size l)
     | Fgets l ->
         Option.map (f l) ~f:(fun l -> Fgets l)
-    | Nullity l ->
-        Option.map (f l) ~f:(fun l -> Nullity l)
     | Top ->
         Some Top
 
@@ -772,13 +763,7 @@ end
    "AliasTarget.Empty relation": For pruning vector.length with vector::empty() results, we adopt a
    specific relation between %r and v->elements, where %r=v.empty().  So, if %r!=0, v's array length
    ([v->elements->length]) is pruned by 0.  On the other hand, if %r==0, v's array length is pruned
-   by >=1.
-
-   "AliasTarget.Nullity relation": For pruning vector.length with vector::empty() results, we adopt
-   a specific relation between %r and i, where %r=v.empty() and i=v.length.  So, if %r!=0, i is
-   pruned by i=0.  On the other hand, if %r==0, i is pruned by i>=1.  This is similar to the
-   AliasTarget.Empty relation, but is used when there is a program variable [i] for the length of
-   the array. *)
+   by >=1. *)
 module AliasMap = struct
   module Key = struct
     type t = IdentKey of Ident.t | JavaTmp of Loc.t [@@deriving compare]
@@ -914,17 +899,6 @@ module Alias = struct
         a
 
 
-  let store_empty : Val.t -> Loc.t -> t -> t =
-   fun formal loc a ->
-    let a = lift_map (AliasMap.forget loc) a in
-    let locs = Val.get_all_locs formal in
-    match PowLoc.is_singleton_or_more locs with
-    | IContainer.Singleton loc ->
-        {a with ret= AliasRet.v (AliasTarget.nullity loc)}
-    | _ ->
-        a
-
-
   let fgets : Ident.t -> PowLoc.t -> t -> t =
    fun id locs a ->
     let a = PowLoc.fold (fun loc acc -> lift_map (AliasMap.forget loc) acc) locs a in
@@ -1429,12 +1403,7 @@ module MemReach = struct
         Some (l, None)
     | Some (AliasTarget.SimplePlusA (l, i)) ->
         Some (l, Some i)
-    | Some
-        ( AliasTarget.Empty _
-        | AliasTarget.Size _
-        | AliasTarget.Fgets _
-        | AliasTarget.Nullity _
-        | AliasTarget.Top )
+    | Some (AliasTarget.Empty _ | AliasTarget.Size _ | AliasTarget.Fgets _ | AliasTarget.Top)
     | None ->
         None
 
@@ -1453,10 +1422,6 @@ module MemReach = struct
    fun loc e m -> {m with alias= Alias.store_simple loc e m.alias}
 
 
-  let store_empty_alias : Val.t -> Loc.t -> t -> t =
-   fun formal loc m -> {m with alias= Alias.store_empty formal loc m.alias}
-
-
   let fgets_alias : Ident.t -> PowLoc.t -> t -> t =
    fun id locs m -> {m with alias= Alias.fgets id locs m.alias}
 
@@ -1777,10 +1742,6 @@ module Mem = struct
    fun loc e -> map ~f:(MemReach.store_simple_alias loc e)
 
 
-  let store_empty_alias : Val.t -> Loc.t -> t -> t =
-   fun formal loc -> map ~f:(MemReach.store_empty_alias formal loc)
-
-
   let fgets_alias : Ident.t -> PowLoc.t -> t -> t =
    fun id locs -> map ~f:(MemReach.fgets_alias id locs)
 
diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml
index 808edabbc..3101b73e1 100644
--- a/infer/src/bufferoverrun/bufferOverrunModels.ml
+++ b/infer/src/bufferoverrun/bufferOverrunModels.ml
@@ -331,30 +331,12 @@ let strndup src_exp length_exp =
   {exec; check= no_check}
 
 
-let inferbo_min e1 e2 =
-  let exec {integer_type_widths} ~ret:(id, _) mem =
-    let i1 = Sem.eval integer_type_widths e1 mem |> Dom.Val.get_itv in
-    let i2 = Sem.eval integer_type_widths e2 mem |> Dom.Val.get_itv in
-    let v = Itv.min_sem i1 i2 |> Dom.Val.of_itv in
-    mem |> Dom.Mem.add_stack (Loc.of_id id) v
-  in
-  {exec; check= no_check}
-
-
 let set_size {integer_type_widths; location} array_v size_exp mem =
   let locs = Dom.Val.get_pow_loc array_v in
   let length = Sem.eval integer_type_widths size_exp mem in
   Dom.Mem.transform_mem ~f:(Dom.Val.set_array_length location ~length) locs mem
 
 
-let inferbo_set_size src_exp size_exp =
-  let exec ({integer_type_widths} as model) ~ret:_ mem =
-    let src_v = Sem.eval integer_type_widths src_exp mem in
-    set_size model src_v size_exp mem
-  and check = check_alloc_size ~can_be_zero:true size_exp in
-  {exec; check}
-
-
 let model_by_value value id mem = Dom.Mem.add_stack (Loc.of_id id) value mem
 
 (** Given a string of length n, return itv [-1, n_u-1]. *)
@@ -1020,9 +1002,7 @@ module Call = struct
     let std_array2 = mk_std_array () in
     let char_ptr = Typ.mk (Typ.Tptr (Typ.mk (Typ.Tint Typ.IChar), Pk_pointer)) in
     make_dispatcher
-      [ -"__inferbo_min" <>$ capt_exp $+ capt_exp $!--> inferbo_min
-      ; -"__inferbo_set_size" <>$ capt_exp $+ capt_exp $!--> inferbo_set_size
-      ; -"__exit" <>--> bottom
+      [ -"__exit" <>--> bottom
       ; -"CFArrayCreate" <>$ any_arg $+ capt_exp $+ capt_exp $+...$--> CFArray.create_array
       ; -"CFArrayCreateCopy" <>$ any_arg $+ capt_exp $!--> create_copy_array
       ; -"MCFArrayGetCount" <>$ capt_exp $!--> CFArray.length
diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml
index 7691fac24..66b4230fc 100644
--- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml
+++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml
@@ -315,7 +315,6 @@ let rec eval_arr : Typ.IntegerWidths.t -> Exp.t -> Mem.t -> Val.t =
         | AliasTarget.Size _
         | AliasTarget.Empty _
         | AliasTarget.Fgets _
-        | AliasTarget.Nullity _
         | Top )
     | None ->
         Val.bot )
@@ -512,10 +511,6 @@ module Prune = struct
           let strlen_loc = Loc.of_c_strlen lv in
           let v' = Val.prune_ge_one (Mem.find strlen_loc mem) in
           update_mem_in_prune strlen_loc v' astate
-      | Some (AliasTarget.Nullity lv) ->
-          let v = Mem.find lv mem in
-          let v' = Val.prune_eq_zero v in
-          update_mem_in_prune lv v' astate
       | Some (AliasTarget.SimplePlusA _ | AliasTarget.Size _ | Top) | None ->
           astate )
     | Exp.UnOp (Unop.LNot, Exp.Var x, _) -> (
@@ -528,11 +523,6 @@ module Prune = struct
           let v = Mem.find lv mem in
           let v' = Val.prune_length_ge_one v in
           update_mem_in_prune lv v' astate
-      | Some (AliasTarget.Nullity lv) ->
-          let v = Mem.find lv mem in
-          let itv_v = Itv.prune_comp Binop.Ge (Val.get_itv v) Itv.one in
-          let v' = Val.modify_itv itv_v v in
-          update_mem_in_prune lv v' astate
       | Some (AliasTarget.SimplePlusA _ | AliasTarget.Size _ | AliasTarget.Fgets _ | Top) | None ->
           astate )
     | _ ->