diff --git a/infer/src/IR/Binop.ml b/infer/src/IR/Binop.ml
index 96baf3772..5cc5a71ec 100644
--- a/infer/src/IR/Binop.ml
+++ b/infer/src/IR/Binop.ml
@@ -9,14 +9,18 @@
 (** The Smallfoot Intermediate Language: Binary Operators *)
 open! IStd
 
+type ikind_option_for_binop = Typ.ikind option
+
+let compare_ikind_option_for_binop _ _ = 0
+
 (** Binary operations *)
 type t =
-  | PlusA  (** arithmetic + *)
+  | PlusA of ikind_option_for_binop  (** arithmetic + *)
   | PlusPI  (** pointer + integer *)
-  | MinusA  (** arithmetic - *)
+  | MinusA of ikind_option_for_binop  (** arithmetic - *)
   | MinusPI  (** pointer - integer *)
   | MinusPP  (** pointer - pointer *)
-  | Mult  (** * *)
+  | Mult of ikind_option_for_binop  (** * *)
   | Div  (** / *)
   | Mod  (** % *)
   | Shiftlt  (** shift left *)
@@ -39,22 +43,22 @@ let equal = [%compare.equal: t]
 (** This function returns true if the operation is injective
     wrt. each argument: op(e,-) and op(-, e) is injective for all e.
     The return value false means "don't know". *)
-let injective = function PlusA | PlusPI | MinusA | MinusPI | MinusPP -> true | _ -> false
+let injective = function PlusA _ | PlusPI | MinusA _ | MinusPI | MinusPP -> true | _ -> false
 
 (** This function returns true if 0 is the right unit of [binop].
     The return value false means "don't know". *)
-let is_zero_runit = function PlusA | PlusPI | MinusA | MinusPI | MinusPP -> true | _ -> false
+let is_zero_runit = function PlusA _ | PlusPI | MinusA _ | MinusPI | MinusPP -> true | _ -> false
 
 let text = function
-  | PlusA ->
+  | PlusA _ ->
       "+"
   | PlusPI ->
       "+"
-  | MinusA | MinusPP ->
+  | MinusA _ | MinusPP ->
       "-"
   | MinusPI ->
       "-"
-  | Mult ->
+  | Mult _ ->
       "*"
   | Div ->
       "/"
diff --git a/infer/src/IR/Binop.mli b/infer/src/IR/Binop.mli
index 16b7b4302..cb677c3c2 100644
--- a/infer/src/IR/Binop.mli
+++ b/infer/src/IR/Binop.mli
@@ -11,12 +11,12 @@ open! IStd
 
 (** Binary operations *)
 type t =
-  | PlusA  (** arithmetic + *)
+  | PlusA of Typ.ikind option  (** arithmetic + *)
   | PlusPI  (** pointer + integer *)
-  | MinusA  (** arithmetic - *)
+  | MinusA of Typ.ikind option  (** arithmetic - *)
   | MinusPI  (** pointer - integer *)
   | MinusPP  (** pointer - pointer *)
-  | Mult  (** * *)
+  | Mult of Typ.ikind option  (** * *)
   | Div  (** / *)
   | Mod  (** % *)
   | Shiftlt  (** shift left *)
diff --git a/infer/src/IR/Exp.ml b/infer/src/IR/Exp.ml
index bbdec60b0..86fb2ab8c 100644
--- a/infer/src/IR/Exp.ml
+++ b/infer/src/IR/Exp.ml
@@ -192,7 +192,7 @@ let rec pp_ pe pp_t f e =
   let pp_exp = pp_ pe pp_t in
   let print_binop_stm_output e1 op e2 =
     match (op : Binop.t) with
-    | Eq | Ne | PlusA | Mult ->
+    | Eq | Ne | PlusA _ | Mult _ ->
         F.fprintf f "(%a %s %a)" pp_exp e2 (Binop.str pe op) pp_exp e1
     | Lt ->
         F.fprintf f "(%a %s %a)" pp_exp e2 (Binop.str pe Gt) pp_exp e1
diff --git a/infer/src/IR/HilExp.ml b/infer/src/IR/HilExp.ml
index d78e873d7..1269b02ee 100644
--- a/infer/src/IR/HilExp.ml
+++ b/infer/src/IR/HilExp.ml
@@ -215,13 +215,13 @@ and eval = function
       Some c
   | BinaryOperator (Binop.Div, e1, e2) -> (
     try eval_arithmetic_binop IntLit.div e1 e2 with Division_by_zero -> None )
-  | BinaryOperator (Binop.MinusA, e1, e2) ->
+  | BinaryOperator (Binop.MinusA _, e1, e2) ->
       eval_arithmetic_binop IntLit.sub e1 e2
   | BinaryOperator (Binop.Mod, e1, e2) ->
       eval_arithmetic_binop IntLit.rem e1 e2
-  | BinaryOperator (Binop.Mult, e1, e2) ->
+  | BinaryOperator (Binop.Mult _, e1, e2) ->
       eval_arithmetic_binop IntLit.mul e1 e2
-  | BinaryOperator (Binop.PlusA, e1, e2) ->
+  | BinaryOperator (Binop.PlusA _, e1, e2) ->
       eval_arithmetic_binop IntLit.add e1 e2
   | _ ->
       (* TODO: handle bitshifting cases, port eval_binop from RacerD.ml *)
diff --git a/infer/src/IR/Typ.ml b/infer/src/IR/Typ.ml
index 47d7b6a38..206ff4b2e 100644
--- a/infer/src/IR/Typ.ml
+++ b/infer/src/IR/Typ.ml
@@ -184,6 +184,11 @@ let void = mk Tvoid
 
 let void_star = mk (Tptr (mk Tvoid, Pk_pointer))
 
+let get_ikind_opt {desc} = match desc with Tint ikind -> Some ikind | _ -> None
+
+(* TODO: size_t should be implementation-dependent. *)
+let size_t = IULong
+
 let escape pe = if Pp.equal_print_kind pe.Pp.kind Pp.HTML then Escape.escape_xml else ident
 
 (** Pretty print a type with all the details, using the C syntax. *)
diff --git a/infer/src/IR/Typ.mli b/infer/src/IR/Typ.mli
index 997632c54..e24802bc0 100644
--- a/infer/src/IR/Typ.mli
+++ b/infer/src/IR/Typ.mli
@@ -120,6 +120,12 @@ val void : t
 val void_star : t
 (** void* type *)
 
+val get_ikind_opt : t -> ikind option
+(** Get ikind if the type is integer. *)
+
+val size_t : ikind
+(** ikind of size_t *)
+
 module Name : sig
   (** Named types. *)
   type t = name [@@deriving compare]
diff --git a/infer/src/biabduction/Absarray.ml b/infer/src/biabduction/Absarray.ml
index f3c3fde5d..116917254 100644
--- a/infer/src/biabduction/Absarray.ml
+++ b/infer/src/biabduction/Absarray.ml
@@ -405,7 +405,7 @@ let generic_strexp_abstract tenv (abstraction_name : string) (p_in : Prop.normal
 let index_is_pointed_to tenv (p : Prop.normal Prop.t) (path : StrexpMatch.path) (index : Exp.t) :
     bool =
   let indices =
-    let index_plus_one = Exp.BinOp (Binop.PlusA, index, Exp.one) in
+    let index_plus_one = Exp.BinOp (Binop.PlusA None, index, Exp.one) in
     [index; index_plus_one]
   in
   let add_index_to_paths =
@@ -448,8 +448,8 @@ let blur_array_index tenv (p : Prop.normal Prop.t) (path : StrexpMatch.path) (in
       Prop.set p2 ~sigma:sigma'
     in
     let p4 =
-      let index_next = Exp.BinOp (Binop.PlusA, index, Exp.one) in
-      let fresh_index_next = Exp.BinOp (Binop.PlusA, fresh_index, Exp.one) in
+      let index_next = Exp.BinOp (Binop.PlusA None, index, Exp.one) in
+      let fresh_index_next = Exp.BinOp (Binop.PlusA None, fresh_index, Exp.one) in
       let map = [(index, fresh_index); (index_next, fresh_index_next)] in
       prop_replace_path_index tenv p3 path map
     in
diff --git a/infer/src/biabduction/Dom.ml b/infer/src/biabduction/Dom.ml
index b829d861e..ada2cf845 100644
--- a/infer/src/biabduction/Dom.ml
+++ b/infer/src/biabduction/Dom.ml
@@ -455,7 +455,7 @@ end = struct
           false
     in
     let add_and_gen_eq e e' n =
-      let e_plus_n = Exp.BinOp (Binop.PlusA, e, Exp.int n) in
+      let e_plus_n = Exp.BinOp (Binop.PlusA None, e, Exp.int n) in
       Prop.mk_eq tenv e_plus_n e'
     in
     let rec f_eqs_entry ((e1, e2, e) as entry) eqs_acc t_seen = function
@@ -562,7 +562,7 @@ end = struct
         match e with
         | Exp.Const _ ->
             []
-        | Exp.Lvar _ | Exp.Var _ | Exp.BinOp (Binop.PlusA, Exp.Var _, _) ->
+        | Exp.Lvar _ | Exp.Var _ | Exp.BinOp (Binop.PlusA _, Exp.Var _, _) ->
             let is_same_e (e1, e2, _) = Exp.equal e (select side e1 e2) in
             let assoc = List.filter ~f:is_same_e !tbl in
             List.map ~f:(fun (e1, e2, _) -> select side_op e1 e2) assoc
@@ -588,15 +588,19 @@ end = struct
     let res = ref [] in
     let f v =
       match (v, side) with
-      | (Exp.BinOp (Binop.PlusA, e1', Exp.Const (Const.Cint i)), e2, e'), Lhs when Exp.equal e e1'
-        ->
+      | (Exp.BinOp (Binop.PlusA _, e1', Exp.Const (Const.Cint i)), e2, e'), Lhs
+        when Exp.equal e e1' ->
           let c' = Exp.int (IntLit.neg i) in
-          let v' = (e1', Exp.BinOp (Binop.PlusA, e2, c'), Exp.BinOp (Binop.PlusA, e', c')) in
+          let v' =
+            (e1', Exp.BinOp (Binop.PlusA None, e2, c'), Exp.BinOp (Binop.PlusA None, e', c'))
+          in
           res := v' :: !res
-      | (e1, Exp.BinOp (Binop.PlusA, e2', Exp.Const (Const.Cint i)), e'), Rhs when Exp.equal e e2'
-        ->
+      | (e1, Exp.BinOp (Binop.PlusA _, e2', Exp.Const (Const.Cint i)), e'), Rhs
+        when Exp.equal e e2' ->
           let c' = Exp.int (IntLit.neg i) in
-          let v' = (Exp.BinOp (Binop.PlusA, e1, c'), e2', Exp.BinOp (Binop.PlusA, e', c')) in
+          let v' =
+            (Exp.BinOp (Binop.PlusA None, e1, c'), e2', Exp.BinOp (Binop.PlusA None, e', c'))
+          in
           res := v' :: !res
       | _ ->
           ()
@@ -943,20 +947,20 @@ let rec exp_partial_join (e1 : Exp.t) (e2 : Exp.t) : Exp.t =
   | Exp.Var id, Exp.Lvar _ | Exp.Lvar _, Exp.Var id ->
       if Ident.is_normal id then ( L.d_strln "failure reason 21" ; raise Sil.JoinFail )
       else Rename.extend e1 e2 Rename.ExtFresh
-  | Exp.BinOp (Binop.PlusA, Exp.Var id1, Exp.Const _), Exp.Var id2
-  | Exp.Var id1, Exp.BinOp (Binop.PlusA, Exp.Var id2, Exp.Const _)
+  | Exp.BinOp (Binop.PlusA _, Exp.Var id1, Exp.Const _), Exp.Var id2
+  | Exp.Var id1, Exp.BinOp (Binop.PlusA _, Exp.Var id2, Exp.Const _)
     when ident_same_kind_primed_footprint id1 id2 ->
       Rename.extend e1 e2 Rename.ExtFresh
-  | Exp.BinOp (Binop.PlusA, Exp.Var id1, Exp.Const (Const.Cint c1)), Exp.Const (Const.Cint c2)
+  | Exp.BinOp (Binop.PlusA _, Exp.Var id1, Exp.Const (Const.Cint c1)), Exp.Const (Const.Cint c2)
     when can_rename id1 ->
       let c2' = c2 -- c1 in
       let e_res = Rename.extend (Exp.Var id1) (Exp.int c2') Rename.ExtFresh in
-      Exp.BinOp (Binop.PlusA, e_res, Exp.int c1)
-  | Exp.Const (Const.Cint c1), Exp.BinOp (Binop.PlusA, Exp.Var id2, Exp.Const (Const.Cint c2))
+      Exp.BinOp (Binop.PlusA None, e_res, Exp.int c1)
+  | Exp.Const (Const.Cint c1), Exp.BinOp (Binop.PlusA _, Exp.Var id2, Exp.Const (Const.Cint c2))
     when can_rename id2 ->
       let c1' = c1 -- c2 in
       let e_res = Rename.extend (Exp.int c1') (Exp.Var id2) Rename.ExtFresh in
-      Exp.BinOp (Binop.PlusA, e_res, Exp.int c2)
+      Exp.BinOp (Binop.PlusA None, e_res, Exp.int c2)
   | Exp.Cast (t1, e1), Exp.Cast (t2, e2) ->
       if not (Typ.equal t1 t2) then ( L.d_strln "failure reason 22" ; raise Sil.JoinFail )
       else
@@ -1011,11 +1015,11 @@ let rec exp_partial_join (e1 : Exp.t) (e2 : Exp.t) : Exp.t =
 
 and length_partial_join len1 len2 =
   match (len1, len2) with
-  | Exp.BinOp (Binop.PlusA, e1, Exp.Const c1), Exp.BinOp (Binop.PlusA, e2, Exp.Const c2) ->
+  | Exp.BinOp (Binop.PlusA _, e1, Exp.Const c1), Exp.BinOp (Binop.PlusA _, e2, Exp.Const c2) ->
       let e' = exp_partial_join e1 e2 in
       let c' = exp_partial_join (Exp.Const c1) (Exp.Const c2) in
-      Exp.BinOp (Binop.PlusA, e', c')
-  | Exp.BinOp (Binop.PlusA, _, _), Exp.BinOp (Binop.PlusA, _, _) ->
+      Exp.BinOp (Binop.PlusA None, e', c')
+  | Exp.BinOp (Binop.PlusA _, _, _), Exp.BinOp (Binop.PlusA _, _, _) ->
       Rename.extend len1 len2 Rename.ExtFresh
   | Exp.Var id1, Exp.Var id2 when Ident.equal id1 id2 ->
       len1
diff --git a/infer/src/biabduction/Prop.ml b/infer/src/biabduction/Prop.ml
index 8fe6c7980..225f563e6 100644
--- a/infer/src/biabduction/Prop.ml
+++ b/infer/src/biabduction/Prop.ml
@@ -543,7 +543,7 @@ let exp_collapse_consecutive_indices_prop (typ : Typ.t) exp =
   let rec exp_remove (e0 : Exp.t) =
     match e0 with
     | Lindex (Lindex (base, e1), e2) ->
-        let e0' : Exp.t = Lindex (base, BinOp (PlusA, e1, e2)) in
+        let e0' : Exp.t = Lindex (base, BinOp (PlusA None, e1, e2)) in
         exp_remove e0'
     | _ ->
         e0
@@ -712,7 +712,7 @@ module Normalize = struct
             Exp.bool (IntLit.leq n m)
         | Const (Cfloat v), Const (Cfloat w) ->
             Exp.bool (v <= w)
-        | BinOp (PlusA, e3, Const (Cint n)), Const (Cint m) ->
+        | BinOp (PlusA _, e3, Const (Cint n)), Const (Cint m) ->
             BinOp (Le, e3, Exp.int (m -- n))
         | e1', e2' ->
             Exp.le e1' e2' )
@@ -722,11 +722,11 @@ module Normalize = struct
             Exp.bool (IntLit.lt n m)
         | Const (Cfloat v), Const (Cfloat w) ->
             Exp.bool (v < w)
-        | Const (Cint n), BinOp (MinusA, f1, f2) ->
-            BinOp (Le, BinOp (MinusA, f2, f1), Exp.int (IntLit.minus_one -- n))
-        | BinOp (MinusA, f1, f2), Const (Cint n) ->
-            Exp.le (BinOp (MinusA, f1, f2)) (Exp.int (n -- IntLit.one))
-        | BinOp (PlusA, e3, Const (Cint n)), Const (Cint m) ->
+        | Const (Cint n), BinOp ((MinusA _ as ominus), f1, f2) ->
+            BinOp (Le, BinOp (ominus, f2, f1), Exp.int (IntLit.minus_one -- n))
+        | BinOp ((MinusA _ as ominus), f1, f2), Const (Cint n) ->
+            Exp.le (BinOp (ominus, f1, f2)) (Exp.int (n -- IntLit.one))
+        | BinOp (PlusA _, e3, Const (Cint n)), Const (Cint m) ->
             BinOp (Lt, e3, Exp.int (m -- n))
         | e1', e2' ->
             Exp.lt e1' e2' )
@@ -788,18 +788,23 @@ module Normalize = struct
               BinOp (LOr, e1', e2') )
       | BinOp (PlusPI, Lindex (ep, e1), e2) ->
           (* array access with pointer arithmetic *)
-          let e' : Exp.t = BinOp (PlusA, e1, e2) in
+          let e' : Exp.t = BinOp (PlusA None, e1, e2) in
           eval (Exp.Lindex (ep, e'))
       | BinOp (PlusPI, BinOp (PlusPI, e11, e12), e2) ->
           (* take care of pattern ((ptr + off1) + off2) *)
           (* progress: convert inner +I to +A *)
-          let e2' : Exp.t = BinOp (PlusA, e12, e2) in
+          let e2' : Exp.t = BinOp (PlusA None, e12, e2) in
           eval (Exp.BinOp (PlusPI, e11, e2'))
-      | BinOp ((PlusA as oplus), e1, e2) | BinOp ((PlusPI as oplus), e1, e2) -> (
+      | BinOp ((PlusA _ as oplus), e1, e2) | BinOp ((PlusPI as oplus), e1, e2) -> (
           let e1' = eval e1 in
           let e2' = eval e2 in
-          let isPlusA = Binop.equal oplus Binop.PlusA in
-          let ominus = if isPlusA then Binop.MinusA else Binop.MinusPI in
+          let isPlusA, ominus =
+            match oplus with
+            | Binop.PlusA topt ->
+                (true, Binop.MinusA topt)
+            | _ ->
+                (false, Binop.MinusPI)
+          in
           let ( +++ ) (x : Exp.t) (y : Exp.t) : Exp.t =
             match (x, y) with
             | _, Const (Cint i) when IntLit.iszero i ->
@@ -827,7 +832,7 @@ module Normalize = struct
           (* pattern for arrays and extensible structs:
                sizeof(struct s {... t[l]}) + k * sizeof(t)) = sizeof(struct s {... t[l + k]}) *)
           | ( Sizeof ({typ; dynamic_length= len1_opt} as sizeof_data)
-            , BinOp (Mult, len2, Sizeof {typ= elt; dynamic_length= None}) )
+            , BinOp (Mult _, len2, Sizeof {typ= elt; dynamic_length= None}) )
             when isPlusA && extensible_array_element_typ_equal elt typ ->
               let len = match len1_opt with Some len1 -> len1 +++ len2 | None -> len2 in
               Sizeof {sizeof_data with dynamic_length= Some len}
@@ -841,15 +846,15 @@ module Normalize = struct
               Exp.float (v +. w)
           | UnOp (Neg, f1, _), f2 | f2, UnOp (Neg, f1, _) ->
               BinOp (ominus, f2, f1)
-          | BinOp (PlusA, e, Const (Cint n1)), Const (Cint n2)
+          | BinOp (PlusA _, e, Const (Cint n1)), Const (Cint n2)
           | BinOp (PlusPI, e, Const (Cint n1)), Const (Cint n2)
-          | Const (Cint n2), BinOp (PlusA, e, Const (Cint n1))
+          | Const (Cint n2), BinOp (PlusA _, e, Const (Cint n1))
           | Const (Cint n2), BinOp (PlusPI, e, Const (Cint n1)) ->
               e +++ Exp.int (n1 ++ n2)
-          | BinOp (MinusA, Const (Cint n1), e), Const (Cint n2)
-          | Const (Cint n2), BinOp (MinusA, Const (Cint n1), e) ->
+          | BinOp (MinusA _, Const (Cint n1), e), Const (Cint n2)
+          | Const (Cint n2), BinOp (MinusA _, Const (Cint n1), e) ->
               Exp.int (n1 ++ n2) --- e
-          | BinOp (MinusA, e1, e2), e3 ->
+          | BinOp (MinusA _, e1, e2), e3 ->
               (* (e1-e2)+e3 --> e1 + (e3-e2) *)
               (* progress: brings + to the outside *)
               eval (e1 +++ (e3 --- e2))
@@ -863,11 +868,12 @@ module Normalize = struct
               if abs && isPlusA then Exp.get_undefined false
               else if abs && not isPlusA then e1' +++ Exp.get_undefined false
               else e1' +++ e2' )
-      | BinOp ((MinusA as ominus), e1, e2) | BinOp ((MinusPI as ominus), e1, e2) -> (
+      | BinOp ((MinusA _ as ominus), e1, e2) | BinOp ((MinusPI as ominus), e1, e2) -> (
           let e1' = eval e1 in
           let e2' = eval e2 in
-          let isMinusA = Binop.equal ominus Binop.MinusA in
-          let oplus = if isMinusA then Binop.PlusA else Binop.PlusPI in
+          let oplus =
+            match ominus with Binop.MinusA topt -> Binop.PlusA topt | _ -> Binop.PlusPI
+          in
           let ( +++ ) x y : Exp.t = BinOp (oplus, x, y) in
           let ( --- ) x y : Exp.t = BinOp (ominus, x, y) in
           if Exp.equal e1' e2' then Exp.zero
@@ -893,7 +899,7 @@ module Normalize = struct
                 if abs then Exp.get_undefined false else e1' --- e2' )
       | BinOp (MinusPP, e1, e2) ->
           if abs then Exp.get_undefined false else BinOp (MinusPP, eval e1, eval e2)
-      | BinOp (Mult, e1, e2) -> (
+      | BinOp ((Mult _ as omult), e1, e2) -> (
           let e1' = eval e1 in
           let e2' = eval e2 in
           match (e1', e2') with
@@ -914,11 +920,11 @@ module Normalize = struct
           | Const (Cfloat v), Const (Cfloat w) ->
               Exp.float (v *. w)
           | Var _, Var _ ->
-              BinOp (Mult, e1', e2')
+              BinOp (omult, e1', e2')
           | _, Sizeof _ | Sizeof _, _ ->
-              BinOp (Mult, e1', e2')
+              BinOp (omult, e1', e2')
           | _, _ ->
-              if abs then Exp.get_undefined false else BinOp (Mult, e1', e2') )
+              if abs then Exp.get_undefined false else BinOp (omult, e1', e2') )
       | BinOp (Div, e1, e2) -> (
           let e1' = eval e1 in
           let e2' = eval e2 in
@@ -969,7 +975,7 @@ module Normalize = struct
             | _, Const (Cint m) when IntLit.iszero m ->
                 eval e1
             | _, Const (Cint m) when IntLit.isone m ->
-                eval (Exp.BinOp (PlusA, e1, e1))
+                eval (Exp.BinOp (PlusA None, e1, e1))
             | Const (Cint m), _ when IntLit.iszero m ->
                 e1
             | _ ->
@@ -1036,7 +1042,7 @@ module Normalize = struct
           eval (Exp.BinOp (PlusPI, Lvar pv, e2))
       | Lindex (BinOp (PlusPI, ep, e1), e2) ->
           (* array access with pointer arithmetic *)
-          let e' : Exp.t = BinOp (PlusA, e1, e2) in
+          let e' : Exp.t = BinOp (PlusA None, e1, e2) in
           eval (Exp.Lindex (ep, e'))
       | Lindex (e1, e2) ->
           let e1' = eval e1 in
@@ -1077,19 +1083,19 @@ module Normalize = struct
         (* base <= n case *)
         let nbase = exp_normalize_noabs tenv Sil.sub_empty base in
         match nbase with
-        | BinOp (PlusA, base', Const (Cint n')) ->
+        | BinOp (PlusA _, base', Const (Cint n')) ->
             let new_offset = Exp.int (n -- n') in
             let new_e : Exp.t = BinOp (Le, base', new_offset) in
             Aeq (new_e, Exp.one)
-        | BinOp (PlusA, Const (Cint n'), base') ->
+        | BinOp (PlusA _, Const (Cint n'), base') ->
             let new_offset = Exp.int (n -- n') in
             let new_e : Exp.t = BinOp (Le, base', new_offset) in
             Aeq (new_e, Exp.one)
-        | BinOp (MinusA, base', Const (Cint n')) ->
+        | BinOp (MinusA _, base', Const (Cint n')) ->
             let new_offset = Exp.int (n ++ n') in
             let new_e : Exp.t = BinOp (Le, base', new_offset) in
             Aeq (new_e, Exp.one)
-        | BinOp (MinusA, Const (Cint n'), base') ->
+        | BinOp (MinusA _, Const (Cint n'), base') ->
             let new_offset = Exp.int (n' -- n -- IntLit.one) in
             let new_e : Exp.t = BinOp (Lt, new_offset, base') in
             Aeq (new_e, Exp.one)
@@ -1104,19 +1110,19 @@ module Normalize = struct
         (* n < base case *)
         let nbase = exp_normalize_noabs tenv Sil.sub_empty base in
         match nbase with
-        | BinOp (PlusA, base', Const (Cint n')) ->
+        | BinOp (PlusA _, base', Const (Cint n')) ->
             let new_offset = Exp.int (n -- n') in
             let new_e : Exp.t = BinOp (Lt, new_offset, base') in
             Aeq (new_e, Exp.one)
-        | BinOp (PlusA, Const (Const.Cint n'), base') ->
+        | BinOp (PlusA _, Const (Const.Cint n'), base') ->
             let new_offset = Exp.int (n -- n') in
             let new_e : Exp.t = BinOp (Lt, new_offset, base') in
             Aeq (new_e, Exp.one)
-        | BinOp (MinusA, base', Const (Cint n')) ->
+        | BinOp (MinusA _, base', Const (Cint n')) ->
             let new_offset = Exp.int (n ++ n') in
             let new_e : Exp.t = BinOp (Lt, new_offset, base') in
             Aeq (new_e, Exp.one)
-        | BinOp (MinusA, Const (Cint n'), base') ->
+        | BinOp (MinusA _, Const (Cint n'), base') ->
             let new_offset = Exp.int (n' -- n -- IntLit.one) in
             let new_e : Exp.t = BinOp (Le, base', new_offset) in
             Aeq (new_e, Exp.one)
@@ -1139,11 +1145,11 @@ module Normalize = struct
       match e with
       | Const (Cint n) ->
           ([], [], n)
-      | BinOp (PlusA, e1, e2) | BinOp (PlusPI, e1, e2) ->
+      | BinOp (PlusA _, e1, e2) | BinOp (PlusPI, e1, e2) ->
           let pos1, neg1, n1 = exp_to_posnegoff e1 in
           let pos2, neg2, n2 = exp_to_posnegoff e2 in
           (pos1 @ pos2, neg1 @ neg2, n1 ++ n2)
-      | BinOp (MinusA, e1, e2) | BinOp (MinusPI, e1, e2) | BinOp (MinusPP, e1, e2) ->
+      | BinOp (MinusA _, e1, e2) | BinOp (MinusPI, e1, e2) | BinOp (MinusPP, e1, e2) ->
           let pos1, neg1, n1 = exp_to_posnegoff e1 in
           let pos2, neg2, n2 = exp_to_posnegoff e2 in
           (pos1 @ neg2, neg1 @ pos2, n1 -- n2)
@@ -1179,7 +1185,7 @@ module Normalize = struct
       | [e] ->
           e
       | e :: el ->
-          BinOp (PlusA, e, exp_list_to_sum el)
+          BinOp (PlusA None, e, exp_list_to_sum el)
     in
     let norm_from_exp e : Exp.t =
       match normalize_posnegoff (exp_to_posnegoff e) with
@@ -1190,7 +1196,7 @@ module Normalize = struct
       | pos, [], n ->
           BinOp (Le, exp_list_to_sum pos, Exp.int (IntLit.zero -- n))
       | pos, neg, n ->
-          let lhs_e : Exp.t = BinOp (MinusA, exp_list_to_sum pos, exp_list_to_sum neg) in
+          let lhs_e : Exp.t = BinOp (MinusA None, exp_list_to_sum pos, exp_list_to_sum neg) in
           BinOp (Le, lhs_e, Exp.int (IntLit.zero -- n))
     in
     let ineq =
@@ -1198,10 +1204,10 @@ module Normalize = struct
     in
     match ineq with
     | BinOp (Le, e1, e2) ->
-        let e : Exp.t = BinOp (MinusA, e1, e2) in
+        let e : Exp.t = BinOp (MinusA None, e1, e2) in
         mk_inequality tenv (norm_from_exp e)
     | BinOp (Lt, e1, e2) ->
-        let e : Exp.t = BinOp (MinusA, BinOp (MinusA, e1, e2), Exp.minus_one) in
+        let e : Exp.t = BinOp (MinusA None, BinOp (MinusA None, e1, e2), Exp.minus_one) in
         mk_inequality tenv (norm_from_exp e)
     | _ ->
         a
@@ -1214,15 +1220,15 @@ module Normalize = struct
     let a = Sil.atom_sub sub a0 in
     let rec normalize_eq (eq : Exp.t * Exp.t) =
       match eq with
-      | BinOp (PlusA, e1, Const (Cint n1)), Const (Cint n2)
+      | BinOp (PlusA _, e1, Const (Cint n1)), Const (Cint n2)
       (* e1+n1==n2 ---> e1==n2-n1 *)
       | BinOp (PlusPI, e1, Const (Cint n1)), Const (Cint n2) ->
           (e1, Exp.int (n2 -- n1))
-      | BinOp (MinusA, e1, Const (Cint n1)), Const (Cint n2)
+      | BinOp (MinusA _, e1, Const (Cint n1)), Const (Cint n2)
       (* e1-n1==n2 ---> e1==n1+n2 *)
       | BinOp (MinusPI, e1, Const (Cint n1)), Const (Cint n2) ->
           (e1, Exp.int (n1 ++ n2))
-      | BinOp (MinusA, Const (Cint n1), e1), Const (Cint n2) ->
+      | BinOp (MinusA _, Const (Cint n1), e1), Const (Cint n2) ->
           (* n1-e1 == n2 -> e1==n1-n2 *)
           (e1, Exp.int (n1 -- n2))
       | Lfield (e1', fld1, _), Lfield (e2', fld2, _) ->
@@ -1231,13 +1237,13 @@ module Normalize = struct
           if Exp.equal idx1 idx2 then normalize_eq (e1', e2')
           else if Exp.equal e1' e2' then normalize_eq (idx1, idx2)
           else eq
-      | BinOp ((PlusA | PlusPI | MinusA | MinusPI), e1, e2), e1' when Exp.equal e1 e1' ->
+      | BinOp ((PlusA _ | PlusPI | MinusA _ | MinusPI), e1, e2), e1' when Exp.equal e1 e1' ->
           (e2, Exp.int IntLit.zero)
-      | BinOp ((PlusA | PlusPI), e2, e1), e1' when Exp.equal e1 e1' ->
+      | BinOp ((PlusA _ | PlusPI), e2, e1), e1' when Exp.equal e1 e1' ->
           (e2, Exp.int IntLit.zero)
-      | e1', BinOp ((PlusA | PlusPI | MinusA | MinusPI), e1, e2) when Exp.equal e1 e1' ->
+      | e1', BinOp ((PlusA _ | PlusPI | MinusA _ | MinusPI), e1, e2) when Exp.equal e1 e1' ->
           (e2, Exp.int IntLit.zero)
-      | e1', BinOp ((PlusA | PlusPI), e2, e1) when Exp.equal e1 e1' ->
+      | e1', BinOp ((PlusA _ | PlusPI), e2, e1) when Exp.equal e1 e1' ->
           (e2, Exp.int IntLit.zero)
       | _ ->
           eq
@@ -1454,32 +1460,44 @@ module Normalize = struct
             let hpred' = mk_ptsto_exp tenv Fld_init (root, size, None) inst in
             replace_hpred hpred'
         | ( Earray
-              (BinOp (Mult, Sizeof {typ= t; dynamic_length= None; subtype= st1}, x), esel, inst)
+              (BinOp (Mult _, Sizeof {typ= t; dynamic_length= None; subtype= st1}, x), esel, inst)
           , Sizeof {typ= {desc= Tarray {elt}} as arr} )
           when Typ.equal t elt ->
             let dynamic_length = Some x in
             let sizeof_data = {Exp.typ= arr; nbytes= None; dynamic_length; subtype= st1} in
             let hpred' = mk_ptsto_exp tenv Fld_init (root, Sizeof sizeof_data, None) inst in
             replace_hpred (replace_array_contents hpred' esel)
-        | ( Earray (BinOp (Mult, x, Sizeof {typ; dynamic_length= None; subtype}), esel, inst)
+        | ( Earray (BinOp (Mult _, x, Sizeof {typ; dynamic_length= None; subtype}), esel, inst)
           , Sizeof {typ= {desc= Tarray {elt}} as arr} )
           when Typ.equal typ elt ->
             let sizeof_data = {Exp.typ= arr; nbytes= None; dynamic_length= Some x; subtype} in
             let hpred' = mk_ptsto_exp tenv Fld_init (root, Sizeof sizeof_data, None) inst in
             replace_hpred (replace_array_contents hpred' esel)
-        | ( Earray (BinOp (Mult, Sizeof {typ; dynamic_length= Some len; subtype}, x), esel, inst)
+        | ( Earray
+              ( BinOp ((Mult _ as omult), Sizeof {typ; dynamic_length= Some len; subtype}, x)
+              , esel
+              , inst )
           , Sizeof {typ= {desc= Tarray {elt}} as arr} )
           when Typ.equal typ elt ->
             let sizeof_data =
-              {Exp.typ= arr; nbytes= None; dynamic_length= Some (Exp.BinOp (Mult, x, len)); subtype}
+              { Exp.typ= arr
+              ; nbytes= None
+              ; dynamic_length= Some (Exp.BinOp (omult, x, len))
+              ; subtype }
             in
             let hpred' = mk_ptsto_exp tenv Fld_init (root, Sizeof sizeof_data, None) inst in
             replace_hpred (replace_array_contents hpred' esel)
-        | ( Earray (BinOp (Mult, x, Sizeof {typ; dynamic_length= Some len; subtype}), esel, inst)
+        | ( Earray
+              ( BinOp ((Mult _ as omult), x, Sizeof {typ; dynamic_length= Some len; subtype})
+              , esel
+              , inst )
           , Sizeof {typ= {desc= Tarray {elt}} as arr} )
           when Typ.equal typ elt ->
             let sizeof_data =
-              {Exp.typ= arr; nbytes= None; dynamic_length= Some (Exp.BinOp (Mult, x, len)); subtype}
+              { Exp.typ= arr
+              ; nbytes= None
+              ; dynamic_length= Some (Exp.BinOp (omult, x, len))
+              ; subtype }
             in
             let hpred' = mk_ptsto_exp tenv Fld_init (root, Sizeof sizeof_data, None) inst in
             replace_hpred (replace_array_contents hpred' esel)
@@ -1957,7 +1975,7 @@ let sigma_get_array_indices sigma =
 let compute_reindexing_from_indices list =
   let get_id_offset (e : Exp.t) =
     match e with
-    | BinOp (PlusA, Var id, Const (Cint offset)) ->
+    | BinOp (PlusA _, Var id, Const (Cint offset)) ->
         if Ident.is_primed id then Some (id, offset) else None
     | _ ->
         None
@@ -1984,7 +2002,7 @@ let compute_reindexing_from_indices list =
     let id, offset = match get_id_offset x with None -> assert false | Some io -> io in
     let base_new : Exp.t = Var (Ident.create_fresh Ident.kprimed) in
     let offset_new = Exp.int (IntLit.neg offset) in
-    let exp_new : Exp.t = BinOp (PlusA, base_new, offset_new) in
+    let exp_new : Exp.t = BinOp (PlusA None, base_new, offset_new) in
     (id, exp_new)
   in
   let reindexing = List.map ~f:transform list_passed in
@@ -2016,7 +2034,7 @@ let prop_rename_array_indices tenv prop =
     let indices = sigma_get_array_indices prop.sigma in
     let not_same_base_lt_offsets (e1 : Exp.t) (e2 : Exp.t) =
       match (e1, e2) with
-      | BinOp (PlusA, e1', Const (Cint n1')), BinOp (PlusA, e2', Const (Cint n2')) ->
+      | BinOp (PlusA _, e1', Const (Cint n1')), BinOp (PlusA _, e2', Const (Cint n2')) ->
           not (Exp.equal e1' e2' && IntLit.lt n1' n2')
       | _ ->
           true
diff --git a/infer/src/biabduction/Prover.ml b/infer/src/biabduction/Prover.ml
index 857515587..0b4507df0 100644
--- a/infer/src/biabduction/Prover.ml
+++ b/infer/src/biabduction/Prover.ml
@@ -87,17 +87,17 @@ end = struct
 
   let equal = [%compare.equal: t]
 
-  let to_leq (e1, e2, n) = (Exp.BinOp (Binop.MinusA, e1, e2), Exp.int n)
+  let to_leq (e1, e2, n) = (Exp.BinOp (Binop.MinusA None, e1, e2), Exp.int n)
 
   let to_lt (e1, e2, n) =
-    (Exp.int (IntLit.zero -- n -- IntLit.one), Exp.BinOp (Binop.MinusA, e2, e1))
+    (Exp.int (IntLit.zero -- n -- IntLit.one), Exp.BinOp (Binop.MinusA None, e2, e1))
 
 
   let to_triple entry = entry
 
   let from_leq acc (e1, e2) =
     match (e1, e2) with
-    | ( Exp.BinOp (Binop.MinusA, (Exp.Var id11 as e11), (Exp.Var id12 as e12))
+    | ( Exp.BinOp (Binop.MinusA _, (Exp.Var id11 as e11), (Exp.Var id12 as e12))
       , Exp.Const (Const.Cint n) )
       when not (Ident.equal id11 id12) -> (
       match IntLit.to_signed n with
@@ -112,7 +112,7 @@ end = struct
   let from_lt acc (e1, e2) =
     match (e1, e2) with
     | ( Exp.Const (Const.Cint n)
-      , Exp.BinOp (Binop.MinusA, (Exp.Var id21 as e21), (Exp.Var id22 as e22)) )
+      , Exp.BinOp (Binop.MinusA _, (Exp.Var id21 as e21), (Exp.Var id22 as e22)) )
       when not (Ident.equal id21 id22) -> (
       match IntLit.to_signed n with
       | None ->
@@ -496,11 +496,11 @@ end = struct
     match (e1, e2) with
     | Exp.Const (Const.Cint n1), Exp.Const (Const.Cint n2) ->
         IntLit.leq n1 n2
-    | ( Exp.BinOp (Binop.MinusA, Exp.Sizeof {nbytes= Some nb1}, Exp.Sizeof {nbytes= Some nb2})
+    | ( Exp.BinOp (Binop.MinusA _, Exp.Sizeof {nbytes= Some nb1}, Exp.Sizeof {nbytes= Some nb2})
       , Exp.Const (Const.Cint n2) ) ->
         (* [ sizeof(t1) - sizeof(t2) <= n2 ] *)
         IntLit.(leq (sub (of_int nb1) (of_int nb2)) n2)
-    | ( Exp.BinOp (Binop.MinusA, Exp.Sizeof {typ= t1}, Exp.Sizeof {typ= t2})
+    | ( Exp.BinOp (Binop.MinusA _, Exp.Sizeof {typ= t1}, Exp.Sizeof {typ= t2})
       , Exp.Const (Const.Cint n2) )
       when IntLit.isminusone n2 && type_size_comparable t1 t2 ->
         (* [ sizeof(t1) - sizeof(t2) <= -1 ] *)
@@ -639,8 +639,8 @@ let check_equal tenv prop e1_0 e2_0 =
   let check_equal () = Exp.equal n_e1 n_e2 in
   let check_equal_const () =
     match (n_e1, n_e2) with
-    | Exp.BinOp (Binop.PlusA, e1, Exp.Const (Const.Cint d)), e2
-    | e2, Exp.BinOp (Binop.PlusA, e1, Exp.Const (Const.Cint d)) ->
+    | Exp.BinOp (Binop.PlusA _, e1, Exp.Const (Const.Cint d)), e2
+    | e2, Exp.BinOp (Binop.PlusA _, e1, Exp.Const (Const.Cint d)) ->
         if Exp.equal e1 e2 then IntLit.iszero d else false
     | Exp.Const c1, Exp.Lindex (Exp.Const c2, Exp.Const (Const.Cint i)) when IntLit.iszero i ->
         Const.equal c1 c2
@@ -693,9 +693,9 @@ let get_bounds tenv prop e0 =
   let e_norm = Prop.exp_normalize_prop ~destructive:true tenv prop e0 in
   let e_root, off =
     match e_norm with
-    | Exp.BinOp (Binop.PlusA, e, Exp.Const (Const.Cint n1)) ->
+    | Exp.BinOp (Binop.PlusA _, e, Exp.Const (Const.Cint n1)) ->
         (e, IntLit.neg n1)
-    | Exp.BinOp (Binop.MinusA, e, Exp.Const (Const.Cint n1)) ->
+    | Exp.BinOp (Binop.MinusA _, e, Exp.Const (Const.Cint n1)) ->
         (e, n1)
     | _ ->
         (e_norm, IntLit.zero)
@@ -719,20 +719,20 @@ let check_disequal tenv prop e1 e2 =
     | Exp.Const c1, Exp.Lindex (Exp.Const c2, Exp.Const (Const.Cint d)) ->
         if IntLit.iszero d then not (Const.equal c1 c2) (* offset=0 is no offset *)
         else Const.equal c1 c2 (* same base, different offsets *)
-    | ( Exp.BinOp (Binop.PlusA, e1, Exp.Const (Const.Cint d1))
-      , Exp.BinOp (Binop.PlusA, e2, Exp.Const (Const.Cint d2)) ) ->
+    | ( Exp.BinOp (Binop.PlusA _, e1, Exp.Const (Const.Cint d1))
+      , Exp.BinOp (Binop.PlusA _, e2, Exp.Const (Const.Cint d2)) ) ->
         if Exp.equal e1 e2 then IntLit.neq d1 d2 else false
-    | Exp.BinOp (Binop.PlusA, e1, Exp.Const (Const.Cint d)), e2
-    | e2, Exp.BinOp (Binop.PlusA, e1, Exp.Const (Const.Cint d)) ->
+    | Exp.BinOp (Binop.PlusA _, e1, Exp.Const (Const.Cint d)), e2
+    | e2, Exp.BinOp (Binop.PlusA _, e1, Exp.Const (Const.Cint d)) ->
         if Exp.equal e1 e2 then not (IntLit.iszero d) else false
     | Exp.Lindex (Exp.Const c1, Exp.Const (Const.Cint d)), Exp.Const c2 ->
         if IntLit.iszero d then not (Const.equal c1 c2) else Const.equal c1 c2
     | Exp.Lindex (Exp.Const c1, Exp.Const d1), Exp.Lindex (Exp.Const c2, Exp.Const d2) ->
         Const.equal c1 c2 && not (Const.equal d1 d2)
-    | Exp.Const (Const.Cint n), Exp.BinOp (Binop.Mult, Exp.Sizeof _, e21)
-    | Exp.Const (Const.Cint n), Exp.BinOp (Binop.Mult, e21, Sizeof _)
-    | Exp.BinOp (Binop.Mult, Exp.Sizeof _, e21), Exp.Const (Const.Cint n)
-    | Exp.BinOp (Binop.Mult, e21, Exp.Sizeof _), Exp.Const (Const.Cint n) ->
+    | Exp.Const (Const.Cint n), Exp.BinOp (Binop.Mult _, Exp.Sizeof _, e21)
+    | Exp.Const (Const.Cint n), Exp.BinOp (Binop.Mult _, e21, Sizeof _)
+    | Exp.BinOp (Binop.Mult _, Exp.Sizeof _, e21), Exp.Const (Const.Cint n)
+    | Exp.BinOp (Binop.Mult _, e21, Exp.Sizeof _), Exp.Const (Const.Cint n) ->
         IntLit.iszero n && not (Exp.is_zero e21)
     | Exp.Lvar pv0, Exp.Lvar pv1 ->
         (* Addresses of any two local vars must be different *)
@@ -831,7 +831,7 @@ let check_le_normalized tenv prop e1 e2 =
   (* L.d_str "check_le_normalized "; Sil.d_exp e1; L.d_str " "; Sil.d_exp e2; L.d_ln (); *)
   let eL, eR, off =
     match (e1, e2) with
-    | Exp.BinOp (Binop.MinusA, f1, f2), Exp.Const (Const.Cint n) ->
+    | Exp.BinOp (Binop.MinusA _, f1, f2), Exp.Const (Const.Cint n) ->
         if Exp.equal f1 f2 then (Exp.zero, Exp.zero, n) else (f1, f2, n)
     | _ ->
         (e1, e2, IntLit.zero)
@@ -1354,10 +1354,10 @@ let exp_imply tenv calc_missing (subs : subst2) e1_in e2_in : subst2 =
     match (e1, e2) with
     | Exp.Var v1, Exp.Var v2 ->
         var_imply subs v1 v2
-    | Exp.BinOp ((PlusA | PlusPI | MinusA | MinusPI), Exp.Var v1, e2), Exp.Var v2
+    | Exp.BinOp ((PlusA _ | PlusPI | MinusA _ | MinusPI), Exp.Var v1, e2), Exp.Var v2
       when Ident.equal v1 v2 ->
         do_imply subs e2 Exp.zero
-    | Exp.BinOp ((PlusA | PlusPI), e2, Exp.Var v1), Exp.Var v2 when Ident.equal v1 v2 ->
+    | Exp.BinOp ((PlusA _ | PlusPI), e2, Exp.Var v1), Exp.Var v2 when Ident.equal v1 v2 ->
         do_imply subs e2 Exp.zero
     | e1, Exp.Var v2 ->
         let occurs_check v e =
@@ -1372,16 +1372,16 @@ let exp_imply tenv calc_missing (subs : subst2) e1_in e2_in : subst2 =
           let sub2' = extend_sub (snd subs) v2 e1 in
           (fst subs, sub2')
         else raise (IMPL_EXC ("expressions not equal", subs, EXC_FALSE_EXPS (e1, e2)))
-    | e1, Exp.BinOp (Binop.PlusA, (Exp.Var v2 as e2), e2')
+    | e1, Exp.BinOp (Binop.PlusA _, (Exp.Var v2 as e2), e2')
       when Ident.is_primed v2 || Ident.is_footprint v2 ->
         (* here e2' could also be a variable that we could try to substitute (as in the next match
            case), but we ignore that to avoid backtracking *)
-        let e' = Exp.BinOp (Binop.MinusA, e1, e2') in
+        let e' = Exp.BinOp (Binop.MinusA None, e1, e2') in
         do_imply subs (Prop.exp_normalize_noabs tenv Sil.sub_empty e') e2
-    | e1, Exp.BinOp (Binop.PlusA, e2, (Exp.Var v2 as e2'))
+    | e1, Exp.BinOp (Binop.PlusA _, e2, (Exp.Var v2 as e2'))
       when Ident.is_primed v2 || Ident.is_footprint v2 ->
         (* symmetric of above case *)
-        let e' = Exp.BinOp (Binop.MinusA, e1, e2') in
+        let e' = Exp.BinOp (Binop.MinusA None, e1, e2') in
         do_imply subs (Prop.exp_normalize_noabs tenv Sil.sub_empty e') e2
     | Exp.Var id, Exp.Lvar pv when Ident.is_footprint id && Pvar.is_local pv ->
         (* Footprint var could never be the same as local address *)
@@ -1405,14 +1405,14 @@ let exp_imply tenv calc_missing (subs : subst2) e1_in e2_in : subst2 =
     | Exp.Const (Const.Cint _), Exp.BinOp (Binop.PlusPI, _, _) ->
         raise
           (IMPL_EXC ("pointer+index cannot evaluate to a constant", subs, EXC_FALSE_EXPS (e1, e2)))
-    | Exp.Const (Const.Cint n1), Exp.BinOp (Binop.PlusA, f1, Exp.Const (Const.Cint n2)) ->
+    | Exp.Const (Const.Cint n1), Exp.BinOp (Binop.PlusA _, f1, Exp.Const (Const.Cint n2)) ->
         do_imply subs (Exp.int (n1 -- n2)) f1
     | Exp.BinOp (op1, e1, f1), Exp.BinOp (op2, e2, f2) when Binop.equal op1 op2 ->
         do_imply (do_imply subs e1 e2) f1 f2
-    | Exp.BinOp (Binop.PlusA, Exp.Var v1, e1), e2 ->
-        do_imply subs (Exp.Var v1) (Exp.BinOp (Binop.MinusA, e2, e1))
+    | Exp.BinOp (Binop.PlusA _, Exp.Var v1, e1), e2 ->
+        do_imply subs (Exp.Var v1) (Exp.BinOp (Binop.MinusA None, e2, e1))
     | Exp.BinOp (Binop.PlusPI, Exp.Lvar pv1, e1), e2 ->
-        do_imply subs (Exp.Lvar pv1) (Exp.BinOp (Binop.MinusA, e2, e1))
+        do_imply subs (Exp.Lvar pv1) (Exp.BinOp (Binop.MinusA None, e2, e1))
     | ( Exp.Sizeof {typ= t1; dynamic_length= None; subtype= st1}
       , Exp.Sizeof {typ= t2; dynamic_length= None; subtype= st2} )
       when Typ.equal t1 t2 && Subtype.equal_modulo_flag st1 st2 ->
@@ -1479,9 +1479,9 @@ let path_to_id path =
 let array_len_imply tenv calc_missing subs len1 len2 indices2 =
   match (len1, len2) with
   | _, Exp.Var _
-  | _, Exp.BinOp (Binop.PlusA, Exp.Var _, _)
-  | _, Exp.BinOp (Binop.PlusA, _, Exp.Var _)
-  | Exp.BinOp (Binop.Mult, _, _), _ -> (
+  | _, Exp.BinOp (Binop.PlusA _, Exp.Var _, _)
+  | _, Exp.BinOp (Binop.PlusA _, _, Exp.Var _)
+  | Exp.BinOp (Binop.Mult _, _, _), _ -> (
     try exp_imply tenv calc_missing subs len1 len2 with IMPL_EXC (s, subs', x) ->
       raise (IMPL_EXC ("array len:" ^ s, subs', x)) )
   | _ ->
@@ -1806,7 +1806,7 @@ let expand_hpred_pointer =
           let hpred' = Sil.Hpointsto (e, Sil.Earray (len, [(ind, se)], Sil.inst_none), t') in
           expand true true hpred'
       | Sil.Hpointsto (Exp.BinOp (Binop.PlusPI, e1, e2), Sil.Earray (len, esel, inst), t) ->
-          let shift_exp e = Exp.BinOp (Binop.PlusA, e, e2) in
+          let shift_exp e = Exp.BinOp (Binop.PlusA None, e, e2) in
           let len' = shift_exp len in
           let esel' = List.map ~f:(fun (e, se) -> (shift_exp e, se)) esel in
           let hpred' = Sil.Hpointsto (e1, Sil.Earray (len', esel', inst), t) in
@@ -2520,7 +2520,7 @@ let check_array_bounds tenv (sub1, sub2) prop =
         (* L.d_strln_color Orange "check_bound ";
            Sil.d_exp len1; L.d_str " "; Sil.d_exp len2; L.d_ln(); *)
         let indices_to_check =
-          [Exp.BinOp (Binop.PlusA, len2, Exp.minus_one)]
+          [Exp.BinOp (Binop.PlusA None, len2, Exp.minus_one)]
           (* only check len *)
         in
         List.iter ~f:(fail_if_le len1) indices_to_check
diff --git a/infer/src/biabduction/Rearrange.ml b/infer/src/biabduction/Rearrange.ml
index f0331d2a5..d1be87330 100644
--- a/infer/src/biabduction/Rearrange.ml
+++ b/infer/src/biabduction/Rearrange.ml
@@ -37,7 +37,7 @@ let check_bad_index tenv pname p len index loc =
     Prover.check_atom tenv p index_too_large || Prover.check_atom tenv p index_negative
   in
   let index_provably_in_bound () =
-    let len_minus_one = Exp.BinOp (Binop.PlusA, len, Exp.minus_one) in
+    let len_minus_one = Exp.BinOp (Binop.PlusA None, len, Exp.minus_one) in
     let index_not_too_large =
       Prop.mk_inequality tenv (Exp.BinOp (Binop.Le, index, len_minus_one))
     in
@@ -457,11 +457,7 @@ let mk_ptsto_exp_footprint pname tenv orig_prop (lexp, typ) max_stamp inst :
       raise (Exceptions.Dangling_pointer_dereference (None, err_desc, __POS__)) ) ;
   let off_foot, eqs = laundry_offset_for_footprint max_stamp off in
   let subtype =
-    match !Language.curr_language with
-    | Clang ->
-        Subtype.exact
-    | Java ->
-        Subtype.subtypes
+    match !Language.curr_language with Clang -> Subtype.exact | Java -> Subtype.subtypes
   in
   let create_ptsto footprint_part off0 =
     match (root, off0, typ.Typ.desc) with
@@ -1600,7 +1596,7 @@ let check_dereference_error tenv pdesc (prop : Prop.normal Prop.t) lexp loc =
         (* try to remove an offset if any, and find the attribute there *)
         let root_no_offset =
           match root with
-          | Exp.BinOp ((Binop.PlusPI | Binop.PlusA | Binop.MinusPI | Binop.MinusA), base, _) ->
+          | Exp.BinOp ((Binop.PlusPI | Binop.PlusA _ | Binop.MinusPI | Binop.MinusA _), base, _) ->
               base
           | _ ->
               root
diff --git a/infer/src/bufferoverrun/bufferOverrunDomainRelation.ml b/infer/src/bufferoverrun/bufferOverrunDomainRelation.ml
index 6b0e9bf5c..3c227b3f1 100644
--- a/infer/src/bufferoverrun/bufferOverrunDomainRelation.ml
+++ b/infer/src/bufferoverrun/bufferOverrunDomainRelation.ml
@@ -677,11 +677,11 @@ module Make (Manager : Manager_S) = struct
           match (raw_of_exp' e1, raw_of_exp' e2) with
           | Some re1, Some re2 -> (
             match bop with
-            | Binop.PlusA ->
+            | Binop.PlusA _ ->
                 Some (raw_bop_make Texpr1.Add re1 re2)
-            | Binop.MinusA ->
+            | Binop.MinusA _ ->
                 Some (raw_bop_make Texpr1.Sub re1 re2)
-            | Binop.Mult ->
+            | Binop.Mult _ ->
                 Some (raw_bop_make Texpr1.Mul re1 re2)
             | _ ->
                 try_get_sym_f e )
diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml
index ea0e29ab6..b45b25028 100644
--- a/infer/src/bufferoverrun/bufferOverrunModels.ml
+++ b/infer/src/bufferoverrun/bufferOverrunModels.ml
@@ -65,8 +65,8 @@ let no_check _model_env _mem cond_set = cond_set
      - array size
      - flexible array size *)
 let get_malloc_info : Exp.t -> Typ.t * Int.t option * Exp.t * Exp.t option = function
-  | Exp.BinOp (Binop.Mult, Exp.Sizeof {typ; nbytes}, length)
-  | Exp.BinOp (Binop.Mult, length, Exp.Sizeof {typ; nbytes}) ->
+  | Exp.BinOp (Binop.Mult _, Exp.Sizeof {typ; nbytes}, length)
+  | Exp.BinOp (Binop.Mult _, length, Exp.Sizeof {typ; nbytes}) ->
       (typ, nbytes, length, None)
   (* In Java all arrays are dynamically allocated *)
   | Exp.Sizeof {typ; nbytes; dynamic_length= Some arr_length} when Language.curr_language_is Java
@@ -128,7 +128,7 @@ let malloc size_exp =
 
 
 let calloc size_exp stride_exp =
-  let byte_size_exp = Exp.BinOp (Binop.Mult, size_exp, stride_exp) in
+  let byte_size_exp = Exp.BinOp (Binop.Mult (Some Typ.size_t), size_exp, stride_exp) in
   malloc byte_size_exp
 
 
@@ -171,7 +171,7 @@ let realloc src_exp size_exp =
 let placement_new size_exp (src_exp1, t1) src_arg2_opt =
   match (t1.Typ.desc, src_arg2_opt) with
   | Tint _, None | Tint _, Some (_, {Typ.desc= Tint _}) ->
-      malloc (Exp.BinOp (Binop.PlusA, size_exp, src_exp1))
+      malloc (Exp.BinOp (Binop.PlusA (Some Typ.size_t), size_exp, src_exp1))
   | Tstruct (CppClass (name, _)), None
     when [%compare.equal: string list] (QualifiedCppName.to_list name) ["std"; "nothrow_t"] ->
       malloc size_exp
diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml
index b9799c0a4..cb6a12286 100644
--- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml
+++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml
@@ -198,17 +198,17 @@ and eval_binop : Binop.t -> Exp.t -> Exp.t -> Mem.astate -> Val.t =
   let v1 = eval e1 mem in
   let v2 = eval e2 mem in
   match binop with
-  | Binop.PlusA ->
+  | Binop.PlusA _ ->
       Val.plus_a v1 v2
   | Binop.PlusPI ->
       Val.plus_pi v1 v2
-  | Binop.MinusA ->
+  | Binop.MinusA _ ->
       Val.minus_a v1 v2
   | Binop.MinusPI ->
       Val.minus_pi v1 v2
   | Binop.MinusPP ->
       Val.minus_pp v1 v2
-  | Binop.Mult ->
+  | Binop.Mult _ ->
       Val.mult v1 v2
   | Binop.Div ->
       Val.div v1 v2
diff --git a/infer/src/clang/cArithmetic_trans.ml b/infer/src/clang/cArithmetic_trans.ml
index f7d8cbfae..a67e38269 100644
--- a/infer/src/clang/cArithmetic_trans.ml
+++ b/infer/src/clang/cArithmetic_trans.ml
@@ -19,11 +19,11 @@ let compound_assignment_binary_operation_instruction boi_kind (e1, t1) typ e2 lo
     let bop =
       match boi_kind with
       | `AddAssign ->
-          if Typ.is_pointer t1 then Binop.PlusPI else Binop.PlusA
+          if Typ.is_pointer t1 then Binop.PlusPI else Binop.PlusA (Typ.get_ikind_opt typ)
       | `SubAssign ->
-          if Typ.is_pointer t1 then Binop.MinusPI else Binop.MinusA
+          if Typ.is_pointer t1 then Binop.MinusPI else Binop.MinusA (Typ.get_ikind_opt typ)
       | `MulAssign ->
-          Binop.Mult
+          Binop.Mult (Typ.get_ikind_opt typ)
       | `DivAssign ->
           Binop.Div
       | `ShlAssign ->
@@ -66,9 +66,9 @@ let binary_operation_instruction source_range boi ((e1, t1) as e1_with_typ) typ
   | `Add ->
       if Typ.is_pointer t1 then (binop_exp Binop.PlusPI, [])
       else if Typ.is_pointer t2 then (binop_exp ~change_order:true Binop.PlusPI, [])
-      else (binop_exp Binop.PlusA, [])
+      else (binop_exp (Binop.PlusA (Typ.get_ikind_opt typ)), [])
   | `Mul ->
-      (binop_exp Binop.Mult, [])
+      (binop_exp (Binop.Mult (Typ.get_ikind_opt typ)), [])
   | `Div ->
       (binop_exp Binop.Div, [])
   | `Rem ->
@@ -76,7 +76,7 @@ let binary_operation_instruction source_range boi ((e1, t1) as e1_with_typ) typ
   | `Sub ->
       if Typ.is_pointer t1 then
         if Typ.is_pointer t2 then (binop_exp Binop.MinusPP, []) else (binop_exp Binop.MinusPI, [])
-      else (binop_exp Binop.MinusA, [])
+      else (binop_exp (Binop.MinusA (Typ.get_ikind_opt typ)), [])
   | `Shl ->
       (binop_exp Binop.Shiftlt, [])
   | `Shr ->
@@ -129,13 +129,13 @@ let unary_operation_instruction translation_unit_context uoi e typ loc =
   | `PostInc ->
       let id = Ident.create_fresh Ident.knormal in
       let instr1 = Sil.Load (id, e, typ, loc) in
-      let bop = if Typ.is_pointer typ then Binop.PlusPI else Binop.PlusA in
+      let bop = if Typ.is_pointer typ then Binop.PlusPI else Binop.PlusA (Typ.get_ikind_opt typ) in
       let e_plus_1 = Exp.BinOp (bop, Exp.Var id, Exp.Const (Const.Cint IntLit.one)) in
       (Exp.Var id, [instr1; Sil.Store (e, typ, e_plus_1, loc)])
   | `PreInc ->
       let id = Ident.create_fresh Ident.knormal in
       let instr1 = Sil.Load (id, e, typ, loc) in
-      let bop = if Typ.is_pointer typ then Binop.PlusPI else Binop.PlusA in
+      let bop = if Typ.is_pointer typ then Binop.PlusPI else Binop.PlusA (Typ.get_ikind_opt typ) in
       let e_plus_1 = Exp.BinOp (bop, Exp.Var id, Exp.Const (Const.Cint IntLit.one)) in
       let exp =
         if CGeneral_utils.is_cpp_translation translation_unit_context then e else e_plus_1
@@ -144,13 +144,17 @@ let unary_operation_instruction translation_unit_context uoi e typ loc =
   | `PostDec ->
       let id = Ident.create_fresh Ident.knormal in
       let instr1 = Sil.Load (id, e, typ, loc) in
-      let bop = if Typ.is_pointer typ then Binop.MinusPI else Binop.MinusA in
+      let bop =
+        if Typ.is_pointer typ then Binop.MinusPI else Binop.MinusA (Typ.get_ikind_opt typ)
+      in
       let e_minus_1 = Exp.BinOp (bop, Exp.Var id, Exp.Const (Const.Cint IntLit.one)) in
       (Exp.Var id, [instr1; Sil.Store (e, typ, e_minus_1, loc)])
   | `PreDec ->
       let id = Ident.create_fresh Ident.knormal in
       let instr1 = Sil.Load (id, e, typ, loc) in
-      let bop = if Typ.is_pointer typ then Binop.MinusPI else Binop.MinusA in
+      let bop =
+        if Typ.is_pointer typ then Binop.MinusPI else Binop.MinusA (Typ.get_ikind_opt typ)
+      in
       let e_minus_1 = Exp.BinOp (bop, Exp.Var id, Exp.Const (Const.Cint IntLit.one)) in
       let exp =
         if CGeneral_utils.is_cpp_translation translation_unit_context then e else e_minus_1
@@ -254,4 +258,4 @@ let sil_const_plus_one const =
   | Exp.Const (Const.Cint n) ->
       Exp.Const (Const.Cint (IntLit.add n IntLit.one))
   | _ ->
-      Exp.BinOp (Binop.PlusA, const, Exp.Const (Const.Cint IntLit.one))
+      Exp.BinOp (Binop.PlusA None, const, Exp.Const (Const.Cint IntLit.one))
diff --git a/infer/src/clang/cTrans_utils.ml b/infer/src/clang/cTrans_utils.ml
index bdb70fea2..4625125b4 100644
--- a/infer/src/clang/cTrans_utils.ml
+++ b/infer/src/clang/cTrans_utils.ml
@@ -345,7 +345,7 @@ let create_alloc_instrs ~alloc_builtin ?size_exp ?placement_args_exps sil_loc fu
     let sizeof_exp =
       match size_exp with
       | Some exp ->
-          Exp.BinOp (Binop.Mult, sizeof_exp_, exp)
+          Exp.BinOp (Binop.Mult (Some Typ.size_t), sizeof_exp_, exp)
       | None ->
           sizeof_exp_
     in
diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml
index cdaed6930..90c18fa40 100644
--- a/infer/src/java/jTrans.ml
+++ b/infer/src/java/jTrans.ml
@@ -177,14 +177,14 @@ let get_constant (c : JBir.const) =
       Const.Cstr (JBasics.jstr_pp jstr)
 
 
-let get_binop binop =
+let get_binop typ binop =
   match binop with
   | JBir.Add _ ->
-      Binop.PlusA
+      Binop.PlusA (Typ.get_ikind_opt typ)
   | JBir.Sub _ ->
-      Binop.MinusA
+      Binop.MinusA (Typ.get_ikind_opt typ)
   | JBir.Mult _ ->
-      Binop.Mult
+      Binop.Mult (Typ.get_ikind_opt typ)
   | JBir.Div _ ->
       Binop.Div
   | JBir.Rem _ ->
@@ -543,7 +543,7 @@ let rec expression (context : JContext.t) pc expr =
           let instrs = (instrs1 @ (deref_array_instr :: instrs2)) @ [load_instr] in
           (instrs, Exp.Var id, type_of_expr)
       | other_binop ->
-          let sil_binop = get_binop other_binop in
+          let sil_binop = get_binop type_of_expr other_binop in
           let sil_expr = Exp.BinOp (sil_binop, sil_ex1, sil_ex2) in
           (instrs1 @ instrs2, sil_expr, type_of_expr) )
   | JBir.Field (ex, cn, fs) ->