diff --git a/goblint.opam b/goblint.opam
index a5f2207d73..d3d707265b 100644
--- a/goblint.opam
+++ b/goblint.opam
@@ -101,7 +101,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 x-maintenance-intent: ["(latest)" "(latest).(latest-1)"] # also keep previous minor version (with two releases per year, always keep a SV-COMP release)
 available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
 pin-depends: [
-  [ "goblint-cil.2.0.9" "git+https://github.com/goblint/cil.git#1b48fc0ce4f3576a51618305251121ffedd0bf1e" ]
+  [ "goblint-cil.2.0.9" "git+https://github.com/goblint/cil.git#6360600542d9c297b87e41db92991209f52f5176" ]
   # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release
   [ "apron.v0.9.15" "git+https://github.com/antoinemine/apron.git#418a217c7a70dae3f422678f3aaba38ae374d91a" ]
 ]
diff --git a/goblint.opam.locked b/goblint.opam.locked
index 41873ff95b..f5154643d0 100644
--- a/goblint.opam.locked
+++ b/goblint.opam.locked
@@ -147,7 +147,7 @@ post-messages: [
 pin-depends: [
   [
     "goblint-cil.2.0.9"
-    "git+https://github.com/goblint/cil.git#1b48fc0ce4f3576a51618305251121ffedd0bf1e"
+    "git+https://github.com/goblint/cil.git#6360600542d9c297b87e41db92991209f52f5176"
   ]
   [
     "apron.v0.9.15"
diff --git a/goblint.opam.template b/goblint.opam.template
index 218447f9a3..35fb86fc74 100644
--- a/goblint.opam.template
+++ b/goblint.opam.template
@@ -3,7 +3,7 @@
 x-maintenance-intent: ["(latest)" "(latest).(latest-1)"] # also keep previous minor version (with two releases per year, always keep a SV-COMP release)
 available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
 pin-depends: [
-  [ "goblint-cil.2.0.9" "git+https://github.com/goblint/cil.git#1b48fc0ce4f3576a51618305251121ffedd0bf1e" ]
+  [ "goblint-cil.2.0.9" "git+https://github.com/goblint/cil.git#6360600542d9c297b87e41db92991209f52f5176" ]
   # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release
   [ "apron.v0.9.15" "git+https://github.com/antoinemine/apron.git#418a217c7a70dae3f422678f3aaba38ae374d91a" ]
 ]
diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml
index 0dcf7cfb45..5d66659b43 100644
--- a/src/analyses/apron/relationAnalysis.apron.ml
+++ b/src/analyses/apron/relationAnalysis.apron.ml
@@ -216,7 +216,7 @@ struct
       | Const x -> e
       | UnOp (unop, e, typ) -> UnOp(unop, inner e, typ)
       | BinOp (binop, e1, e2, typ) -> BinOp (binop, inner e1, inner e2, typ)
-      | CastE (t,e) -> CastE (t, inner e)
+      | CastE (k,t,e) -> CastE (k, t, inner e)
       | Lval (Var v, off) -> Lval (Var v, off)
       | Lval (Mem e, NoOffset) ->
         begin match ask (Queries.MayPointTo e) with
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index ab0d61a874..077eb76ade 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -167,7 +167,7 @@ struct
    * Abstract evaluation functions
    **************************************************************************)
 
-  let iDtoIdx x = ID.cast_to (Cilfacade.ptrdiff_ikind ()) x
+  let iDtoIdx x = ID.cast_to ~kind:Unknown (Cilfacade.ptrdiff_ikind ()) x (* TODO: proper castkind *)
 
   let unop_ID = function
     | Neg  -> ID.neg
@@ -182,7 +182,7 @@ struct
 
   (* Evaluating Cil's unary operators. *)
   let evalunop op typ: value -> value = function
-    | Int v1 -> Int (ID.cast_to (Cilfacade.get_ikind typ) (unop_ID op v1))
+    | Int v1 -> Int (ID.cast_to ~kind:Unknown (Cilfacade.get_ikind typ) (unop_ID op v1)) (* TODO: proper castkind *)
     | Float v -> unop_FD op v
     | Address a when op = LNot ->
       if AD.is_null a then
@@ -326,7 +326,7 @@ struct
       (* Pointer subtracted by a value (e-i) is very similar *)
       (* Cast n to the (signed) ptrdiff_ikind, then add the its negated value. *)
       | MinusPI ->
-        let n = ID.neg (ID.cast_to (Cilfacade.ptrdiff_ikind ()) n) in
+        let n = ID.neg (ID.cast_to ~kind:Unknown (Cilfacade.ptrdiff_ikind ()) n) in (* TODO: proper castkind *)
         Address (ad_concat_map (addToAddr n) p)
       | Mod -> Int (ID.top_of (Cilfacade.ptrdiff_ikind ())) (* we assume that address is actually casted to int first*)
       | _ -> Address AD.top_ptr
@@ -336,11 +336,11 @@ struct
     (* For the integer values, we apply the int domain operator *)
     | Int v1, Int v2 ->
       let result_ik = Cilfacade.get_ikind t in
-      Int (ID.cast_to result_ik (binop_ID result_ik op v1 v2))
+      Int (ID.cast_to ~kind:Unknown result_ik (binop_ID result_ik op v1 v2)) (* TODO: proper castkind *)
     (* For the float values, we apply the float domain operators *)
     | Float v1, Float v2 when is_int_returning_binop_FD op ->
       let result_ik = Cilfacade.get_ikind t in
-      Int (ID.cast_to result_ik (int_returning_binop_FD op v1 v2))
+      Int (ID.cast_to ~kind:Unknown result_ik (int_returning_binop_FD op v1 v2)) (* TODO: proper castkind *)
     | Float v1, Float v2 -> Float (binop_FD (Cilfacade.get_fkind t) op v1 v2)
     (* For address +/- value, we try to do some elementary ptr arithmetic *)
     | Address p, Int n
@@ -522,7 +522,7 @@ struct
         | Int _ ->
           let at = AD.type_of addrs in
           if Cil.isArithmeticType at then
-            VD.cast at x
+            VD.cast ~kind:Unknown at x (* TODO: proper castkind *)
           else
             x
         | _ -> x
@@ -819,7 +819,7 @@ struct
         eval_rv_base_lval ~eval_lv ~man st exp lv
       (* Binary operators *)
       (* Eq/Ne when both values are equal and casted to the same type *)
-      | BinOp ((Eq | Ne) as op, (CastE (t1, e1) as c1), (CastE (t2, e2) as c2), typ) when typeSig t1 = typeSig t2 ->
+      | BinOp ((Eq | Ne) as op, (CastE (_, t1, e1) as c1), (CastE (_, t2, e2) as c2), typ) when typeSig t1 = typeSig t2 ->
         let a1 = eval_rv ~man st e1 in
         let a2 = eval_rv ~man st e2 in
         let extra_is_safe =
@@ -836,7 +836,7 @@ struct
         (* split nested LOr Eqs to equality pairs, if possible *)
         let rec split = function
           (* copied from above to support pointer equalities with implicit casts inserted *)
-          | BinOp (Eq, (CastE (t1, e1) as c1), (CastE (t2, e2) as c2), typ) when typeSig t1 = typeSig t2 ->
+          | BinOp (Eq, (CastE (_, t1, e1) as c1), (CastE (_, t2, e2) as c2), typ) when typeSig t1 = typeSig t2 ->
             Some [binop_remove_same_casts ~extra_is_safe:false ~e1 ~e2 ~t1 ~t2 ~c1 ~c2]
           | BinOp (Eq, arg1, arg2, _) ->
             Some [(arg1, arg2)]
@@ -921,13 +921,13 @@ struct
         let array_ofs = `Index (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) Z.zero, `NoOffset) in
         let array_start = add_offset_varinfo array_ofs in
         Address (AD.map array_start (eval_lv ~man st lval))
-      | CastE (t, Const (CStr (x,e))) -> (* VD.top () *) eval_rv ~man st (Const (CStr (x,e))) (* TODO safe? *)
-      | CastE  (t, exp) ->
+      | CastE (_, t, Const (CStr (x,e))) -> (* VD.top () *) eval_rv ~man st (Const (CStr (x,e))) (* TODO safe? *)
+      | CastE (kind, t, exp) ->
         (let v = eval_rv ~man st exp in
          try
-           VD.cast ~torg:(Cilfacade.typeOf exp) t v
+           VD.cast ~kind ~torg:(Cilfacade.typeOf exp) t v
          with Cilfacade.TypeOfError _  ->
-           VD.cast t v)
+           VD.cast ~kind t v)
       | SizeOf _
       | Real _
       | Imag _
@@ -993,7 +993,7 @@ struct
           else
             VD.top () (* upcasts not! *)
         in
-        let v' = VD.cast t v in (* cast to the expected type (the abstract type might be something other than t since we don't change addresses upon casts!) *)
+        let v' = VD.cast ~kind:Unknown t v in (* cast to the expected type (the abstract type might be something other than t since we don't change addresses upon casts!) *) (* TODO: proper castkind *)
         if M.tracing then M.tracel "cast" "Ptr-Deref: cast %a to %a = %a!" VD.pretty v d_type t VD.pretty v';
         let v' = VD.eval_offset (Queries.to_value_domain_ask (Analyses.ask_of_man man)) (fun x -> get ~man st x (Some exp)) v' (convert_offset ~man st ofs) (Some exp) None t in (* handle offset *)
         v'
@@ -1066,7 +1066,7 @@ struct
     match ofs with
     | NoOffset -> `NoOffset
     | Field (fld, ofs) -> `Field (fld, convert_offset ~man st ofs)
-    | Index (exp, ofs) when CilType.Exp.equal exp (Lazy.force Offset.Index.Exp.any) -> (* special offset added by convertToQueryLval *)
+    | Index (exp, ofs) when Offset.Index.Exp.is_any exp -> (* special offset added by convertToQueryLval *)
       `Index (IdxDom.top (), convert_offset ~man st ofs)
     | Index (exp, ofs) ->
       match eval_rv ~man st exp with
@@ -1383,7 +1383,7 @@ struct
         | Imag e
         | SizeOfE e
         | AlignOfE e
-        | CastE (_, e) -> exp_may_signed_overflow man e
+        | CastE (_, _, e) -> exp_may_signed_overflow man e
         | UnOp (unop, e, _) ->
           (* check if the current operation causes a signed overflow *)
           begin match unop with
@@ -2048,7 +2048,7 @@ struct
           | `Lifted tid when ThreadReturn.is_current ask ->
             (* Evaluate exp and cast the resulting value to the void-pointer-type.
                 Casting to the right type here avoids precision loss on joins. *)
-            let rv = VD.cast ~torg:(Cilfacade.typeOf exp) Cil.voidPtrType rv in
+            let rv = VD.cast ~kind:Unknown ~torg:(Cilfacade.typeOf exp) Cil.voidPtrType rv in (* TODO: proper castkind *)
             man.sideg (V.thread tid) (G.create_thread rv);
             Priv.thread_return ask (priv_getg man.global) (priv_sideg man.sideg) tid st'
           | _ -> st'
@@ -2302,7 +2302,7 @@ struct
                   let item_typ_size_in_bytes = size_of_type_in_bytes item_typ in
                   begin match man.ask (Queries.EvalLength ptr) with
                     | `Lifted arr_len ->
-                      let arr_len_casted = ID.cast_to (Cilfacade.ptrdiff_ikind ()) arr_len in
+                      let arr_len_casted = ID.cast_to ~kind:Unknown (Cilfacade.ptrdiff_ikind ()) arr_len in (* TODO: proper castkind *)
                       begin
                         try `Lifted (ID.mul item_typ_size_in_bytes arr_len_casted)
                         with IntDomain.ArithmeticOnIntegerBot _ -> `Bot
@@ -2352,8 +2352,8 @@ struct
       let dest_size_equal_n =
         match dest_size, n_intdom with
         | `Lifted ds, `Lifted n ->
-          let casted_ds = ID.cast_to (Cilfacade.ptrdiff_ikind ()) ds in
-          let casted_n = ID.cast_to (Cilfacade.ptrdiff_ikind ()) n in
+          let casted_ds = ID.cast_to ~kind:Unknown (Cilfacade.ptrdiff_ikind ()) ds in (* TODO: proper castkind *)
+          let casted_n = ID.cast_to ~kind:Unknown (Cilfacade.ptrdiff_ikind ()) n in (* TODO: proper castkind *)
           let ds_eq_n =
             begin try ID.eq casted_ds casted_n
               with IntDomain.ArithmeticOnIntegerBot _ -> ID.top_of @@ Cilfacade.ptrdiff_ikind ()
@@ -2368,7 +2368,7 @@ struct
                     |> AD.type_of in
       (* when src and destination type coincide, take value from the source, otherwise use top *)
       let value = if (typeSig dest_typ = typeSig src_typ) && dest_size_equal_n then
-          let src_cast_lval = mkMem ~addr:(Cilfacade.mkCast ~e:src ~newt:(TPtr (dest_typ, []))) ~off:NoOffset in
+          let src_cast_lval = mkMem ~addr:(Cilfacade.mkCast ~kind:Unknown ~e:src ~newt:(TPtr (dest_typ, []))) ~off:NoOffset in
           eval_rv ~man st (Lval src_cast_lval)
         else
           VD.top_value (unrollType dest_typ)
@@ -2445,7 +2445,7 @@ struct
           let ptrdiff_ik = Cilfacade.ptrdiff_ikind () in
           let size = man.ask (Q.BlobSize {exp = s1; base_address = false}) in
           let s_id =
-            try ValueDomainQueries.ID.unlift (ID.cast_to ptrdiff_ik) size
+            try ValueDomainQueries.ID.unlift (ID.cast_to ~kind:Unknown ptrdiff_ik) size (* TODO: proper castkind *)
             with Failure _ -> ID.top_of ptrdiff_ik in
           let empty_array = CArrays.make s_id (Int (ID.top_of IChar)) in
           set ~man st lv_a lv_typ (op_array empty_array array_s2)
@@ -2454,7 +2454,7 @@ struct
           let ptrdiff_ik = Cilfacade.ptrdiff_ikind () in
           let size = man.ask (Q.BlobSize {exp = s1; base_address = false}) in
           let s_id =
-            try ValueDomainQueries.ID.unlift (ID.cast_to ptrdiff_ik) size
+            try ValueDomainQueries.ID.unlift (ID.cast_to ~kind:Unknown ptrdiff_ik) size (* TODO: proper castkind *)
             with Failure _ -> ID.top_of ptrdiff_ik in
           let empty_array = CArrays.make s_id (Int (ID.top_of IChar)) in
           let s2_null_bytes = List.map CArrays.to_null_byte_domain (AD.to_string s2_a) in
@@ -2618,7 +2618,7 @@ struct
         let eval_x = eval_rv ~man st x in
         begin match eval_x with
           | Int int_x ->
-            let xcast = ID.cast_to ik int_x in
+            let xcast = ID.cast_to ~kind:Unknown ik int_x in (* TODO: proper castkind *)
             (* the absolute value of the most-negative value is out of range for 2'complement types *)
             (match (ID.minimal xcast), (ID.minimal (ID.top_of ik)) with
              | _, None
@@ -2637,11 +2637,11 @@ struct
           | Nan (fk, str) when Cil.isPointerType (Cilfacade.typeOf str) -> Float (FD.nan_of fk)
           | Nan _ -> failwith ("non-pointer argument in call to function "^f.vname)
           | Inf fk -> Float (FD.inf_of fk)
-          | Isfinite x -> Int (ID.cast_to IInt (apply_unary FDouble FD.isfinite x))
-          | Isinf x -> Int (ID.cast_to IInt (apply_unary FDouble FD.isinf x))
-          | Isnan x -> Int (ID.cast_to IInt (apply_unary FDouble FD.isnan x))
-          | Isnormal x -> Int (ID.cast_to IInt (apply_unary FDouble FD.isnormal x))
-          | Signbit x -> Int (ID.cast_to IInt (apply_unary FDouble FD.signbit x))
+          | Isfinite x -> Int (ID.cast_to ~kind:Unknown IInt (apply_unary FDouble FD.isfinite x)) (* TODO: proper castkind *)
+          | Isinf x -> Int (ID.cast_to ~kind:Unknown IInt (apply_unary FDouble FD.isinf x)) (* TODO: proper castkind *)
+          | Isnan x -> Int (ID.cast_to ~kind:Unknown IInt (apply_unary FDouble FD.isnan x)) (* TODO: proper castkind *)
+          | Isnormal x -> Int (ID.cast_to ~kind:Unknown IInt (apply_unary FDouble FD.isnormal x)) (* TODO: proper castkind *)
+          | Signbit x -> Int (ID.cast_to ~kind:Unknown IInt (apply_unary FDouble FD.signbit x)) (* TODO: proper castkind *)
           | Ceil (fk,x) -> Float (apply_unary fk FD.ceil x)
           | Floor (fk,x) -> Float (apply_unary fk FD.floor x)
           | Fabs (fk, x) -> Float (apply_unary fk FD.fabs x)
@@ -2652,16 +2652,16 @@ struct
           | Cos (fk, x) -> Float (apply_unary fk FD.cos x)
           | Sin (fk, x) -> Float (apply_unary fk FD.sin x)
           | Tan (fk, x) -> Float (apply_unary fk FD.tan x)
-          | Isgreater (x,y) -> Int(ID.cast_to IInt (apply_binary FDouble FD.gt x y))
-          | Isgreaterequal (x,y) -> Int(ID.cast_to IInt (apply_binary FDouble FD.ge x y))
-          | Isless (x,y) -> Int(ID.cast_to IInt (apply_binary FDouble FD.lt x y))
-          | Islessequal (x,y) -> Int(ID.cast_to IInt (apply_binary FDouble FD.le x y))
-          | Islessgreater (x,y) -> Int(ID.c_logor (ID.cast_to IInt (apply_binary FDouble FD.lt x y)) (ID.cast_to IInt (apply_binary FDouble FD.gt x y)))
-          | Isunordered (x,y) -> Int(ID.cast_to IInt (apply_binary FDouble FD.unordered x y))
+          | Isgreater (x,y) -> Int(ID.cast_to ~kind:Unknown IInt (apply_binary FDouble FD.gt x y)) (* TODO: proper castkind *)
+          | Isgreaterequal (x,y) -> Int(ID.cast_to ~kind:Unknown IInt (apply_binary FDouble FD.ge x y)) (* TODO: proper castkind *)
+          | Isless (x,y) -> Int(ID.cast_to ~kind:Unknown IInt (apply_binary FDouble FD.lt x y)) (* TODO: proper castkind *)
+          | Islessequal (x,y) -> Int(ID.cast_to ~kind:Unknown IInt (apply_binary FDouble FD.le x y)) (* TODO: proper castkind *)
+          | Islessgreater (x,y) -> Int(ID.c_logor (ID.cast_to ~kind:Unknown IInt (apply_binary FDouble FD.lt x y)) (ID.cast_to ~kind:Unknown IInt (apply_binary FDouble FD.gt x y))) (* TODO: proper castkind *)
+          | Isunordered (x,y) -> Int(ID.cast_to ~kind:Unknown IInt (apply_binary FDouble FD.unordered x y)) (* TODO: proper castkind *)
           | Fmax (fd, x ,y) -> Float (apply_binary fd FD.fmax x y)
           | Fmin (fd, x ,y) -> Float (apply_binary fd FD.fmin x y)
           | Sqrt (fk, x) -> Float (apply_unary fk FD.sqrt x)
-          | Abs (ik, x) -> Int (ID.cast_to ik (apply_abs ik x))
+          | Abs (ik, x) -> Int (ID.cast_to ~kind:Unknown ik (apply_abs ik x)) (* TODO: proper castkind *)
         end
       in
       Option.map_default (fun lv -> set ~man st (eval_lv ~man st lv) (Cilfacade.typeOfLval lv) result) st lv
@@ -2724,7 +2724,7 @@ struct
             let blob_set = Option.map_default (fun heap_var -> [heap_var, TVoid [], VD.Blob (VD.bot (), sizeval, ZeroInit.calloc)]) [] heap_var in
             set_many ~man st ((eval_lv ~man st lv, (Cilfacade.typeOfLval lv), Address addr):: blob_set)
           else
-            let blobsize = ID.mul (ID.cast_to ik @@ sizeval) (ID.cast_to ik @@ countval) in
+            let blobsize = ID.mul (ID.cast_to ~kind:Unknown ik @@ sizeval) (ID.cast_to ~kind:Unknown ik @@ countval) in (* TODO: proper castkind *)
             let offset = `Index (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) Z.zero, `NoOffset) in
             (* the heap_var is the base address of the allocated memory, but we need to keep track of the offset for the blob *)
             let addr_offset = AD.map (fun a -> Addr.add_offset a offset) addr in
diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml
index 08ad447b5a..6abcd42d56 100644
--- a/src/analyses/baseInvariant.ml
+++ b/src/analyses/baseInvariant.ml
@@ -125,7 +125,7 @@ struct
                 let st = set' lv lval_a st in
                 let orig = AD.Addr.add_offset base_a original_offset in
                 let old_val = get ~man st (AD.singleton orig) None in
-                let old_val = VD.cast (Cilfacade.typeOfLval x) old_val in (* needed as the type of this pointer may be different *)
+                let old_val = VD.cast ~kind:Unknown (Cilfacade.typeOfLval x) old_val in (* needed as the type of this pointer may be different *) (* TODO: proper castkind *)
                 (* this what I would originally have liked to do, but eval_rv_lval_refine uses queries and thus stale values *)
                 (* let old_val = eval_rv_lval_refine ~man st exp x in *)
                 let old_val = map_oldval old_val (Cilfacade.typeOfLval x) in
@@ -157,7 +157,7 @@ struct
         (match value with
          | Int n ->
            let ikind = Cilfacade.get_ikind_exp (Lval lval) in
-           `Refine (x, Int (ID.cast_to ikind n))
+           `Refine (x, Int (ID.cast_to ~kind:Unknown ikind n)) (* TODO: proper castkind *)
          | _ -> `Refine (x, value))
       (* The false-branch for x == value: *)
       | Eq, x, value, false -> begin
@@ -194,7 +194,7 @@ struct
           match value with
           | Int n -> begin
               let ikind = Cilfacade.get_ikind_exp (Lval lval) in
-              let n = ID.cast_to ikind n in
+              let n = ID.cast_to ~kind:Unknown ikind n in (* TODO: proper castkind *)
               let range_from x = if tv then ID.ending ikind (Z.pred x) else ID.starting ikind x in
               let limit_from = if tv then ID.maximal else ID.minimal in
               match limit_from n with
@@ -209,7 +209,7 @@ struct
           match value with
           | Int n -> begin
               let ikind = Cilfacade.get_ikind_exp (Lval lval) in
-              let n = ID.cast_to ikind n in
+              let n = ID.cast_to ~kind:Unknown ikind n in (* TODO: proper castkind *)
               let range_from x = if tv then ID.ending ikind x else ID.starting ikind (Z.succ x) in
               let limit_from = if tv then ID.maximal else ID.minimal in
               match limit_from n with
@@ -241,13 +241,13 @@ struct
         let v = eval_rv ~man st rval in
         let x_type = Cilfacade.typeOfLval x in
         if VD.is_dynamically_safe_cast x_type (Cilfacade.typeOf rval) v then
-          helper op x (VD.cast x_type v) tv
+          helper op x (VD.cast ~kind:Unknown x_type v) tv (* TODO: proper castkind *)
         else
           `NotUnderstood
       | BinOp(op, rval, Lval x, typ) -> derived_invariant (BinOp(switchedOp op, Lval x, rval, typ)) tv
-      | BinOp(op, CastE (t1, c1), CastE (t2, c2), t) when (op = Eq || op = Ne) && typeSig t1 = typeSig t2 && VD.is_statically_safe_cast t1 (Cilfacade.typeOf c1) && VD.is_statically_safe_cast t2 (Cilfacade.typeOf c2)
+      | BinOp(op, CastE (_, t1, c1), CastE (_, t2, c2), t) when (op = Eq || op = Ne) && typeSig t1 = typeSig t2 && VD.is_statically_safe_cast t1 (Cilfacade.typeOf c1) && VD.is_statically_safe_cast t2 (Cilfacade.typeOf c2)
         -> derived_invariant (BinOp (op, c1, c2, t)) tv
-      | BinOp(op, CastE (t1, Lval x), rval, typ) when Cil.isIntegralType t1 ->
+      | BinOp(op, CastE (_, t1, Lval x), rval, typ) when Cil.isIntegralType t1 ->
         begin match eval_rv ~man st (Lval x) with
           | Int v ->
             if VD.is_dynamically_safe_cast t1 (Cilfacade.typeOfLval x) (Int v) then
@@ -256,8 +256,8 @@ struct
               `NotUnderstood
           | _ -> `NotUnderstood
         end
-      | BinOp(op, rval, CastE (ti, Lval x), typ) when Cil.isIntegralType ti ->
-        derived_invariant (BinOp (switchedOp op, CastE(ti, Lval x), rval, typ)) tv
+      | BinOp(op, rval, CastE (k, ti, Lval x), typ) when Cil.isIntegralType ti ->
+        derived_invariant (BinOp (switchedOp op, CastE(k, ti, Lval x), rval, typ)) tv
       | BinOp(op, (Const _ | AddrOf _), rval, typ) ->
         (* This is last such that we never reach here with rval being Lval (it is swapped around). *)
         `NothingToRefine
@@ -647,7 +647,7 @@ struct
         | UnOp (Neg, e, _), Float c -> inv_exp (unop_FD Neg c) e st
         | UnOp ((BNot|Neg) as op, e, _), Int c -> inv_exp (Int (unop_ID op c)) e st
         (* no equivalent for Float, as VD.is_statically_safe_cast fails for all float types anyways *)
-        | BinOp((Eq | Ne) as op, CastE (t1, e1), CastE (t2, e2), t), Int c when typeSig (Cilfacade.typeOf e1) = typeSig (Cilfacade.typeOf e2) && VD.is_statically_safe_cast t1 (Cilfacade.typeOf e1) && VD.is_statically_safe_cast t2 (Cilfacade.typeOf e2) ->
+        | BinOp((Eq | Ne) as op, CastE (_, t1, e1), CastE (_, t2, e2), t), Int c when typeSig (Cilfacade.typeOf e1) = typeSig (Cilfacade.typeOf e2) && VD.is_statically_safe_cast t1 (Cilfacade.typeOf e1) && VD.is_statically_safe_cast t2 (Cilfacade.typeOf e2) ->
           inv_exp (Int c) (BinOp (op, e1, e2, t)) st
         | BinOp (LOr, arg1, arg2, typ) as exp, Int c ->
           (* copied & modified from eval_rv_base... *)
@@ -655,7 +655,7 @@ struct
           (* split nested LOr Eqs to equality pairs, if possible *)
           let rec split = function
             (* copied from above to support pointer equalities with implicit casts inserted *)
-            | BinOp (Eq, CastE (t1, e1), CastE (t2, e2), typ) when typeSig (Cilfacade.typeOf e1) = typeSig (Cilfacade.typeOf e2) && VD.is_statically_safe_cast t1 (Cilfacade.typeOf e1) && VD.is_statically_safe_cast t2 (Cilfacade.typeOf e2) -> (* slightly different from eval_rv_base... *)
+            | BinOp (Eq, CastE (_, t1, e1), CastE (_, t2, e2), typ) when typeSig (Cilfacade.typeOf e1) = typeSig (Cilfacade.typeOf e2) && VD.is_statically_safe_cast t1 (Cilfacade.typeOf e1) && VD.is_statically_safe_cast t2 (Cilfacade.typeOf e2) -> (* slightly different from eval_rv_base... *)
               Some [(e1, e2)]
             | BinOp (Eq, arg1, arg2, _) ->
               Some [(arg1, arg2)]
@@ -757,7 +757,7 @@ struct
              | a1, a2 -> fallback (fun () -> Pretty.dprintf "binop: got abstract values that are not Int: %a and %a" VD.pretty a1 VD.pretty a2) st)
             (* use closures to avoid unused casts *)
           in (match c_typed with
-              | Int c -> invert_binary_op c ID.pretty (fun ik -> ID.cast_to ik c) (fun fk -> FD.of_int fk c)
+              | Int c -> invert_binary_op c ID.pretty (fun ik -> ID.cast_to ~kind:Unknown ik c) (fun fk -> FD.of_int fk c) (* TODO: proper castkind *)
               | Float c -> invert_binary_op c FD.pretty (fun ik -> FD.to_int ik c) (fun fk -> FD.cast_to fk c)
               | _ -> failwith "unreachable")
         | Lval x, (Int _ | Float _ | Address _) -> (* meet x with c *)
@@ -769,7 +769,7 @@ struct
               let c' = match t with
                 | TPtr _ -> VD.Address (AD.of_int c)
                 | TInt (ik, _)
-                | TEnum ({ekind = ik; _}, _) -> Int (ID.cast_to ik c)
+                | TEnum ({ekind = ik; _}, _) -> Int (ID.cast_to ~kind:Unknown ik c) (* TODO: proper castkind *)
                 | TFloat (fk, _) -> Float (FD.of_int fk c)
                 | _ -> Int c
               in
@@ -781,7 +781,7 @@ struct
                   if M.tracing then M.trace "invSpecial" "qry Result: %a" Queries.ML.pretty tmpSpecial;
                   begin match tmpSpecial with
                     | `Lifted (Abs (ik, xInt)) ->
-                      let c' = ID.cast_to ik c in (* different ik! *)
+                      let c' = ID.cast_to ~kind:Unknown ik c in (* different ik! *) (* TODO: proper castkind *)
                       inv_exp (Int (ID.join c' (ID.neg c'))) xInt st
                     | tmpSpecial ->
                       BatOption.map_default_delayed (fun tv ->
@@ -833,7 +833,7 @@ struct
             | _ -> assert false
           end
         | Const _ , _ -> st (* nothing to do *)
-        | CastE (t, e), c_typed ->
+        | CastE (k, t, e), c_typed ->
           begin match Cil.unrollType t, c_typed with
             | TFloat (_, _), Float c ->
               (match unrollType (Cilfacade.typeOf e), FD.get_fkind c with
@@ -854,15 +854,15 @@ struct
                     if VD.is_dynamically_safe_cast t t' (Int i) then
                       (* let c' = ID.cast_to ik_e c in *)
                       (* Suppressing overflow warnings as this is not a computation that comes from the program *)
-                      let res_range = (ID.cast_to ~suppress_ovwarn:true ik (ID.top_of ik_e)) in
-                      let c' = ID.cast_to ik_e (ID.meet c res_range) in (* TODO: cast without overflow, is this right for normal invariant? *)
+                      let res_range = (ID.cast_to ~suppress_ovwarn:true ~kind:Unknown ik (ID.top_of ik_e)) in (* TODO: proper castkind *)
+                      let c' = ID.cast_to ~kind:Unknown ik_e (ID.meet c res_range) in (* TODO: cast without overflow, is this right for normal invariant? *) (* TODO: proper castkind *)
                       if M.tracing then M.tracel "inv" "cast: %a from %a to %a: i = %a; cast c = %a to %a = %a" d_exp e d_ikind ik_e d_ikind ik ID.pretty i ID.pretty c d_ikind ik_e ID.pretty c';
                       inv_exp (Int c') e st
                     else
                       fallback (fun () -> Pretty.dprintf "CastE: %a evaluates to %a which is bigger than the type it is cast to which is %a" d_plainexp e ID.pretty i CilType.Typ.pretty t) st
                   | x -> fallback (fun () -> Pretty.dprintf "CastE: e did evaluate to Int, but the type did not match %a" CilType.Typ.pretty t) st)
                | v -> fallback (fun () -> Pretty.dprintf "CastE: e did not evaluate to Int, but %a" VD.pretty v) st)
-            | _, _ -> fallback (fun () -> Pretty.dprintf "CastE: %a not implemented" d_plainexp (CastE (t, e))) st
+            | _, _ -> fallback (fun () -> Pretty.dprintf "CastE: %a not implemented" d_plainexp (CastE (k, t, e))) st
           end
         | e, _ -> fallback (fun () -> Pretty.dprintf "%a not implemented" d_plainexp e) st
     in
diff --git a/src/analyses/condVars.ml b/src/analyses/condVars.ml
index fbfb2199f2..b504750a85 100644
--- a/src/analyses/condVars.ml
+++ b/src/analyses/condVars.ml
@@ -18,7 +18,7 @@ module Domain = struct
   and var_in_expr p = function
     | Const _ | SizeOf _ | SizeOfStr _ | AlignOf _ -> true
     | Lval l | AddrOf l | StartOf l -> var_in_lval p l
-    | SizeOfE e | AlignOfE e | UnOp (_,e,_) | CastE (_,e) | Imag e | Real e -> var_in_expr p e
+    | SizeOfE e | AlignOfE e | UnOp (_,e,_) | CastE (_,_,e) | Imag e | Real e -> var_in_expr p e
     | BinOp (_,e1,e2,_) -> var_in_expr p e1 && var_in_expr p e2
     | Question (c,t,e,_) -> var_in_expr p c && var_in_expr p t && var_in_expr p e
     | AddrOfLabel _ -> true
diff --git a/src/analyses/malloc_null.ml b/src/analyses/malloc_null.ml
index 8ef1718895..ec99978bf2 100644
--- a/src/analyses/malloc_null.ml
+++ b/src/analyses/malloc_null.ml
@@ -70,7 +70,7 @@ struct
 
   let get_concrete_exp (exp:exp) gl (st:D.t) =
     match constFold true exp with
-    | CastE (_,Lval (Var v, offs))
+    | CastE (_,_,Lval (Var v, offs))
     | Lval (Var v, offs) -> Some (Var v,offs)
     | _ -> None
 
diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml
index 72daac3a51..4c25e95b11 100644
--- a/src/analyses/memOutOfBounds.ml
+++ b/src/analyses/memOutOfBounds.ml
@@ -46,7 +46,7 @@ struct
     | SizeOfE e
     | AlignOfE e
     | UnOp (_, e, _)
-    | CastE (_, e) -> exp_contains_a_ptr e
+    | CastE (_, _, e) -> exp_contains_a_ptr e
     | BinOp (_, e1, e2, _) ->
       exp_contains_a_ptr e1 || exp_contains_a_ptr e2
     | Question (e1, e2, e3, _) ->
@@ -97,7 +97,7 @@ struct
                   let item_typ_size_in_bytes = size_of_type_in_bytes item_typ in
                   begin match man.ask (Queries.EvalLength ptr) with
                     | `Lifted arr_len ->
-                      let arr_len_casted = ID.cast_to (Cilfacade.ptrdiff_ikind ()) arr_len in
+                      let arr_len_casted = ID.cast_to ~kind:Unknown (Cilfacade.ptrdiff_ikind ()) arr_len in (* TODO: proper castkind *)
                       begin
                         try `Lifted (ID.mul item_typ_size_in_bytes arr_len_casted)
                         with IntDomain.ArithmeticOnIntegerBot _ -> `Bot
@@ -135,7 +135,7 @@ struct
     let ptr_contents_typ_size_in_bytes = size_of_type_in_bytes ptr_contents_typ in
     match eval_offset with
     | `Lifted eo ->
-      let casted_eo = ID.cast_to (Cilfacade.ptrdiff_ikind ()) eo in
+      let casted_eo = ID.cast_to ~kind:Unknown (Cilfacade.ptrdiff_ikind ()) eo in (* TODO: proper castkind *)
       begin
         try `Lifted (ID.mul casted_eo ptr_contents_typ_size_in_bytes)
         with IntDomain.ArithmeticOnIntegerBot _ -> `Bot
@@ -170,11 +170,11 @@ struct
       match ofs with
       | NoOffset -> `NoOffset
       | Field (fld, ofs) -> `Field (fld, convert_offset ofs)
-      | Index (exp, ofs) when CilType.Exp.equal exp (Lazy.force Offset.Index.Exp.any) -> (* special offset added by convertToQueryLval *)
+      | Index (exp, ofs) when Offset.Index.Exp.is_any exp -> (* special offset added by convertToQueryLval *)
         `Index (ID.top (), convert_offset ofs)
       | Index (exp, ofs) ->
         let i = match man.ask (Queries.EvalInt exp) with
-          | `Lifted x -> ID.cast_to (Cilfacade.ptrdiff_ikind ()) x
+          | `Lifted x -> ID.cast_to ~kind:Unknown (Cilfacade.ptrdiff_ikind ()) x (* TODO: proper castkind *)
           | _ -> ID.top_of @@ Cilfacade.ptrdiff_ikind ()
         in
         `Index (i, convert_offset ofs)
@@ -277,8 +277,8 @@ struct
             (set_mem_safety_flag InvalidDeref;
              M.warn "Size of lval dereference expression %a is bot. Out-of-bounds memory access may occur" d_exp e)
           | `Lifted es ->
-            let casted_es = ID.cast_to (Cilfacade.ptrdiff_ikind ()) es in
-            let casted_offs = ID.cast_to (Cilfacade.ptrdiff_ikind ()) offs_intdom in
+            let casted_es = ID.cast_to ~kind:Unknown (Cilfacade.ptrdiff_ikind ()) es in (* TODO: proper castkind *)
+            let casted_offs = ID.cast_to ~kind:Unknown (Cilfacade.ptrdiff_ikind ()) offs_intdom in (* TODO: proper castkind *)
             let ptr_size_lt_offs =
               let one = intdom_of_int 1 in
               let casted_es = ID.sub casted_es one in
@@ -325,8 +325,8 @@ struct
           set_mem_safety_flag InvalidDeref;
           M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Size of pointer %a is bot. Memory out-of-bounds access might occur due to pointer arithmetic" d_exp lval_exp
         | `Lifted ps, ao ->
-          let casted_ps = ID.cast_to (Cilfacade.ptrdiff_ikind ()) ps in
-          let casted_ao = ID.cast_to (Cilfacade.ptrdiff_ikind ()) ao in
+          let casted_ps = ID.cast_to ~kind:Unknown (Cilfacade.ptrdiff_ikind ()) ps in (* TODO: proper castkind *)
+          let casted_ao = ID.cast_to ~kind:Unknown (Cilfacade.ptrdiff_ikind ()) ao in (* TODO: proper castkind *)
           let ptr_size_lt_offs = ID.lt casted_ps casted_ao in
           begin match ID.to_bool ptr_size_lt_offs with
             | Some true ->
@@ -352,7 +352,7 @@ struct
     | SizeOfE e
     | AlignOfE e
     | UnOp (_, e, _)
-    | CastE (_, e) -> check_exp_for_oob_access man ~is_implicitly_derefed e
+    | CastE (_, _, e) -> check_exp_for_oob_access man ~is_implicitly_derefed e
     | BinOp (bop, e1, e2, t) ->
       check_exp_for_oob_access man ~is_implicitly_derefed e1;
       check_exp_for_oob_access man ~is_implicitly_derefed e2
@@ -383,8 +383,8 @@ struct
           (* Make sure to add the address offset to the binop offset *)
           let offset_size_with_addr_size = match offset_size with
             | `Lifted os ->
-              let casted_os = ID.cast_to (Cilfacade.ptrdiff_ikind ()) os in
-              let casted_ao = ID.cast_to (Cilfacade.ptrdiff_ikind ()) addr_offs in
+              let casted_os = ID.cast_to ~kind:Unknown (Cilfacade.ptrdiff_ikind ()) os in (* TODO: proper castkind *)
+              let casted_ao = ID.cast_to ~kind:Unknown (Cilfacade.ptrdiff_ikind ()) addr_offs in (* TODO: proper castkind *)
               begin
                 try `Lifted (ID.add casted_os casted_ao)
                 with IntDomain.ArithmeticOnIntegerBot _ -> `Bot
@@ -406,8 +406,8 @@ struct
               set_mem_safety_flag InvalidDeref;
               M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Operand value for pointer arithmetic in expression %a is bottom. Memory out-of-bounds access might occur" d_exp binopexp
             | `Lifted ps, `Lifted o ->
-              let casted_ps = ID.cast_to (Cilfacade.ptrdiff_ikind ()) ps in
-              let casted_o = ID.cast_to (Cilfacade.ptrdiff_ikind ()) o in
+              let casted_ps = ID.cast_to ~kind:Unknown (Cilfacade.ptrdiff_ikind ()) ps in (* TODO: proper castkind *)
+              let casted_o = ID.cast_to ~kind:Unknown (Cilfacade.ptrdiff_ikind ()) o in (* TODO: proper castkind *)
               let ptr_size_lt_offs = ID.lt casted_ps casted_o in
               begin match ID.to_bool ptr_size_lt_offs with
                 | Some true ->
@@ -444,9 +444,9 @@ struct
       set_mem_safety_flag InvalidDeref;
       M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Count parameter, passed to function %s is bottom" fun_name
     | `Lifted ds, `Lifted en ->
-      let casted_ds = ID.cast_to (Cilfacade.ptrdiff_ikind ()) ds in
-      let casted_en = ID.cast_to (Cilfacade.ptrdiff_ikind ()) en in
-      let casted_ao = ID.cast_to (Cilfacade.ptrdiff_ikind ()) addr_offs in
+      let casted_ds = ID.cast_to ~kind:Unknown (Cilfacade.ptrdiff_ikind ()) ds in (* TODO: proper castkind *)
+      let casted_en = ID.cast_to ~kind:Unknown (Cilfacade.ptrdiff_ikind ()) en in (* TODO: proper castkind *)
+      let casted_ao = ID.cast_to ~kind:Unknown (Cilfacade.ptrdiff_ikind ()) addr_offs in (* TODO: proper castkind *)
       let dest_size_lt_count = ID.lt casted_ds (ID.add casted_en casted_ao) in
       begin match ID.to_bool dest_size_lt_count with
         | Some true ->
diff --git a/src/analyses/tutorials/taint.ml b/src/analyses/tutorials/taint.ml
index 937f81584d..aadc2f91ea 100644
--- a/src/analyses/tutorials/taint.ml
+++ b/src/analyses/tutorials/taint.ml
@@ -45,7 +45,7 @@ struct
     | Imag e
     | SizeOfE e
     | AlignOfE e
-    | CastE (_,e)
+    | CastE (_,_,e)
     | UnOp (_,e,_) -> is_exp_tainted state e
     | SizeOf _ | SizeOfStr _ | Const _  | AlignOf _ | AddrOfLabel _ -> false
     | Question (b, t, f, _) -> is_exp_tainted state b || is_exp_tainted state t || is_exp_tainted state f
diff --git a/src/analyses/uninit.ml b/src/analyses/uninit.ml
index b3eb9f6f7a..de41be54f8 100644
--- a/src/analyses/uninit.ml
+++ b/src/analyses/uninit.ml
@@ -65,7 +65,7 @@ struct
     | AddrOf lval -> access_lv_byval a lval
     | StartOf lval -> access_lv_byval a lval
     (* Most casts are currently just ignored, that's probably not a good idea! *)
-    | CastE  (t, exp) -> access_one_byval a rw exp
+    | CastE  (_, t, exp) -> access_one_byval a rw exp
     | Question (b, t, f, _) ->
       access_one_byval a rw b @ access_one_byval a rw t @ access_one_byval a rw f
   (* Accesses during the evaluation of an lval, not the lval itself! *)
diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml
index 5597a67e9b..6d73d78a81 100644
--- a/src/analyses/varEq.ml
+++ b/src/analyses/varEq.ml
@@ -20,7 +20,7 @@ struct
     (* TODO: Should string constants not be added to D in the first place, rather than filtering them for witness invariants? *)
     let rec is_str_constant = function
       | Const (CStr _ | CWStr _) -> true
-      | CastE (_, e) -> is_str_constant e
+      | CastE (_, _, e) -> is_str_constant e
       | _ -> false
 
     let invariant ~scope ss =
@@ -97,7 +97,7 @@ struct
     | AddrOf  (Mem e,_)
     | StartOf (Mem e,_)
     | Lval    (Mem e,_)
-    | CastE (_,e)           -> interesting e
+    | CastE (_,_,e)           -> interesting e
 
   (* helper to decide equality *)
   let query_exp_equal ask e1 e2 g s =
@@ -138,7 +138,7 @@ struct
       | Lval (Mem e,o)
       | AddrOf (Mem e,o)
       | StartOf (Mem e,o) -> may_change_t_offset o || type_may_change_t e bt
-      | CastE (t,e) -> type_may_change_t e bt
+      | CastE (_,t,e) -> type_may_change_t e bt
       | Question (b, t, f, _) -> type_may_change_t b bt || type_may_change_t t bt || type_may_change_t f bt
     in
     let bt =  unrollTypeDeep (Cilfacade.typeOf b) in
@@ -174,7 +174,7 @@ struct
       | Lval (Mem e,o)
       | AddrOf (Mem e,o)
       | StartOf (Mem e,o) -> may_change_pt_offset o || lval_may_change_pt e bl
-      | CastE (t,e) -> lval_may_change_pt e bl
+      | CastE (_,t,e) -> lval_may_change_pt e bl
       | Question (b, t, f, _) -> lval_may_change_pt t bl || lval_may_change_pt t bl || lval_may_change_pt f bl
     in
     let bls = pt b in
@@ -235,7 +235,7 @@ struct
       | Lval (Mem e,o)    -> may_change_t_offset o || type_may_change_t true e
       | AddrOf (Mem e,o)  -> may_change_t_offset o || type_may_change_t false e
       | StartOf (Mem e,o) -> may_change_t_offset o || type_may_change_t false e
-      | CastE (t,e) -> type_may_change_t deref e
+      | CastE (_,t,e) -> type_may_change_t deref e
       | Question (b, t, f, _) -> type_may_change_t deref b || type_may_change_t deref t || type_may_change_t deref f
 
     and lval_may_change_pt a bl : bool =
@@ -253,7 +253,7 @@ struct
         | Lval    (Mem e,o) -> Some (AddrOf (Mem e, o))
         | AddrOf  (Mem e,o) -> (match addrOfExp e with Some e -> Some (AddrOf (Mem e, o)) | x -> x)
         | StartOf (Mem e,o) -> (match addrOfExp e with Some e -> Some (AddrOf (Mem e, o)) | x -> x)
-        | CastE   (t,e) -> addrOfExp e
+        | CastE   (_,t,e) -> addrOfExp e
         | _ -> None
       in
       let lval_is_not_disjoint (v,o) aad =
@@ -299,7 +299,7 @@ struct
            | Lval (Mem e,o)
            | AddrOf (Mem e,o)
            | StartOf (Mem e,o) -> may_change_pt_offset o || lval_may_change_pt e bl
-           | CastE (t,e) -> lval_may_change_pt e bl
+           | CastE (_,t,e) -> lval_may_change_pt e bl
            | Question (b, t, f, _) -> lval_may_change_pt b bl || lval_may_change_pt t bl || lval_may_change_pt f bl
     in
     let r =
@@ -361,7 +361,7 @@ struct
             ) ad)
         | _ -> Some true
       end
-    | CastE (t,e) -> is_global_var ask e
+    | CastE (_,t,e) -> is_global_var ask e
     | AddrOf (Var v,_) -> Some (ask.f (Queries.IsMultiple v)) (* Taking an address of a global is fine*)
     | AddrOf lv -> Some false (* TODO: sound?! *)
     | StartOf (Var v,_) ->  Some (ask.f (Queries.IsMultiple v)) (* Taking an address of a global is fine*)
@@ -545,7 +545,7 @@ struct
     | Some es ->
       let et = Cilfacade.typeOf e in
       let add x xs =
-        Queries.ES.add (CastE (et,x)) xs
+        Queries.ES.add (CastE (Unknown,et,x)) xs
       in
       D.B.fold add es (Queries.ES.empty ())
 
@@ -557,7 +557,7 @@ struct
         (* TODO: this applies eq_set_clos under the offset, unlike cases below; should generalize? *)
         Queries.ES.fold (fun e acc -> (* filter_map *)
             match e with
-            | CastE (_, StartOf a') -> (* eq_set adds casts *)
+            | CastE (_, _, StartOf a') -> (* eq_set adds casts *)
               let e' = AddrOf (Cil.addOffsetLval (Index (i, os)) a') in (* TODO: re-add cast? *)
               Queries.ES.add e' acc
             | _ -> acc
@@ -583,8 +583,8 @@ struct
         Queries.ES.map (fun e -> mkAddrOrStartOf (mkMem ~addr:e ~off:ofs)) (eq_set_clos e s)
       | Lval    (Mem e,ofs) ->
         Queries.ES.map (fun e -> Lval (mkMem ~addr:e ~off:ofs)) (eq_set_clos e s)
-      | CastE (t,e) ->
-        Queries.ES.map (fun e -> CastE (t,e)) (eq_set_clos e s)
+      | CastE (k,t,e) ->
+        Queries.ES.map (fun e -> CastE (k,t,e)) (eq_set_clos e s)
     in
     if M.tracing then M.traceu "var_eq" "eq_set_clos %a = %a" d_plainexp e Queries.ES.pretty r;
     r
diff --git a/src/autoTune.ml b/src/autoTune.ml
index 28c32e5d93..aaad118bdc 100644
--- a/src/autoTune.ml
+++ b/src/autoTune.ml
@@ -342,7 +342,7 @@ let isComparison = function
 
 let rec extractVar = function
   | UnOp (Neg, e, _)
-  | CastE (_, e) -> extractVar e
+  | CastE (_, _, e) -> extractVar e
   | Lval ((Var info),_) when OctagonTracked.varinfo_tracked info -> Some info
   | _ -> None
 
diff --git a/src/cdomain/value/cdomains/arrayDomain.ml b/src/cdomain/value/cdomains/arrayDomain.ml
index 46d602d774..f47a604a58 100644
--- a/src/cdomain/value/cdomains/arrayDomain.ml
+++ b/src/cdomain/value/cdomains/arrayDomain.ml
@@ -140,7 +140,7 @@ struct
   let get ?(checkBounds=true) (ask: VDQ.t) a i = a
   let set (ask: VDQ.t) a (ie, i) v =
     match ie with
-    | Some ie when CilType.Exp.equal ie (Lazy.force Offset.Index.Exp.all) ->
+    | Some ie when Offset.Index.Exp.is_all ie ->
       v
     | _ ->
       join a v
@@ -243,7 +243,7 @@ struct
     else ((update_unrolled_values min_i (Z.of_int ((factor ())-1))), (Val.join xr v))
   let set ask (xl, xr) (ie, i) v =
     match ie with
-    | Some ie when CilType.Exp.equal ie (Lazy.force Offset.Index.Exp.all) ->
+    | Some ie when Offset.Index.Exp.is_all ie ->
       (* TODO: Doesn't seem to work for unassume because unrolled elements are top-initialized, not bot-initialized. *)
       (BatList.make (factor ()) v, v)
     | _ ->
@@ -440,7 +440,7 @@ struct
       |	AlignOfE _ -> false
       | Question(e1, e2, e3, _) ->
         contains_array_access e1 || contains_array_access e2 || contains_array_access e3
-      |	CastE(_, e)
+      |	CastE(_, _, e)
       |	UnOp(_, e , _)
       | Real e
       | Imag e -> contains_array_access e
@@ -525,10 +525,10 @@ struct
   let set_with_length length (ask:VDQ.t) x (i,_) a =
     if M.tracing then M.trace "update_offset" "part array set_with_length %a %s %a" pretty x (BatOption.map_default Basetype.CilExp.show "None" i) Val.pretty a;
     match i with
-    | Some i when CilType.Exp.equal i (Lazy.force Offset.Index.Exp.all) ->
+    | Some i when Offset.Index.Exp.is_all i ->
       (* TODO: Doesn't seem to work for unassume. *)
       Joint a
-    | Some i when CilType.Exp.equal i (Lazy.force Offset.Index.Exp.any) ->
+    | Some i when Offset.Index.Exp.is_any i ->
       (assert !AnalysisState.global_initialization; (* just joining with xm here assumes that all values will be set, which is guaranteed during inits *)
        (* the join is needed here! see e.g 30/04 *)
        let o = match x with Partitioned (_, (_, xm, _)) -> xm | Joint v -> v in
diff --git a/src/cdomain/value/cdomains/int/bitfieldDomain.ml b/src/cdomain/value/cdomains/int/bitfieldDomain.ml
index 4557749a48..c1802acec4 100644
--- a/src/cdomain/value/cdomains/int/bitfieldDomain.ml
+++ b/src/cdomain/value/cdomains/int/bitfieldDomain.ml
@@ -281,7 +281,7 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): Bitfield_SOverflow with type in
     let overflow_info = {underflow; overflow} in
     (norm ~ov:(underflow || overflow) ik (z,o), overflow_info)
 
-  let cast_to ?torg ?(no_ov=false) ik (z,o) =
+  let cast_to ~kind ?torg ?(no_ov=false) ik (z,o) =
     if ik = GoblintCil.IBool then (
       let may_zero =
         if Ints_t.equal z BArith.one_mask then (* zero bit may be in every position (one_mask) *)
diff --git a/src/cdomain/value/cdomains/int/congruenceDomain.ml b/src/cdomain/value/cdomains/int/congruenceDomain.ml
index aef6b202d9..b310ffc28e 100644
--- a/src/cdomain/value/cdomains/int/congruenceDomain.ml
+++ b/src/cdomain/value/cdomains/int/congruenceDomain.ml
@@ -166,7 +166,7 @@ struct
     | _ -> None
 
   (* cast from original type to ikind, set to top if the value doesn't fit into the new type *)
-  let cast_to ?(suppress_ovwarn=false) ?torg ?(no_ov=false) t x =
+  let cast_to ?(suppress_ovwarn=false) ~kind ?torg ?(no_ov=false) t x =
     match x with
     | None -> None
     | Some (c, m) when m =: Z.zero ->
@@ -190,9 +190,9 @@ struct
       | _ -> top ()
 
 
-  let cast_to ?(suppress_ovwarn=false) ?torg ?no_ov (t : Cil.ikind) x =
+  let cast_to ?(suppress_ovwarn=false) ~kind ?torg ?no_ov (t : Cil.ikind) x =
     let pretty_bool _ x = Pretty.text (string_of_bool x) in
-    let res = cast_to ?torg ?no_ov t x in
+    let res = cast_to ~kind ?torg ?no_ov t x in
     if M.tracing then M.trace "cong-cast" "Cast %a to %a (no_ov: %a) = %a" pretty x Cil.d_ikind t (Pretty.docOpt (pretty_bool ())) no_ov pretty res;
     res
 
diff --git a/src/cdomain/value/cdomains/int/defExcDomain.ml b/src/cdomain/value/cdomains/int/defExcDomain.ml
index cec6a9f45e..6089deb8fc 100644
--- a/src/cdomain/value/cdomains/int/defExcDomain.ml
+++ b/src/cdomain/value/cdomains/int/defExcDomain.ml
@@ -132,7 +132,7 @@ struct
     | `Definite x -> if i = x then `Eq else `Neq
     | `Excluded (s,r) -> if S.mem i s then `Neq else `Top
 
-  let cast_to ?(suppress_ovwarn=false) ?torg ?no_ov ik = function
+  let cast_to ?(suppress_ovwarn=false) ~kind ?torg ?no_ov ik = function
     | `Excluded (s,r) ->
       let r' = size ik in
       if R.leq r r' then (* upcast -> no change *)
@@ -195,7 +195,7 @@ struct
       let min, max = Size.range ik in
       (* Perform a wrap-around for unsigned values and for signed values (if configured). *)
       if should_wrap ik then (
-        cast_to ik v
+        cast_to ~kind:Unknown ik v (* TODO: proper castkind *)
       )
       else if Z.compare min x <= 0 && Z.compare x max <= 0 then (
         v
diff --git a/src/cdomain/value/cdomains/int/enumsDomain.ml b/src/cdomain/value/cdomains/int/enumsDomain.ml
index 8d53723b86..c8afa558b3 100644
--- a/src/cdomain/value/cdomains/int/enumsDomain.ml
+++ b/src/cdomain/value/cdomains/int/enumsDomain.ml
@@ -97,7 +97,7 @@ module Enums : S with type int_t = Z.t = struct
       if BISet.mem i x then `Neq
       else `Top
 
-  let cast_to ?(suppress_ovwarn=false) ?torg ?no_ov ik v = norm ik @@ match v with
+  let cast_to ?(suppress_ovwarn=false) ~kind ?torg ?no_ov ik v = norm ik @@ match v with
     | Exc (s,r) ->
       let r' = size ik in
       if R.leq r r' then (* upcast -> no change *)
@@ -115,7 +115,7 @@ module Enums : S with type int_t = Z.t = struct
       then top_of ik (* When casting into a signed type and the result does not fit, the behavior is implementation-defined *)
       else Inc casted_xs
 
-  let of_int ikind x = cast_to ikind (Inc (BISet.singleton x))
+  let of_int ikind x = cast_to ~kind:Unknown ikind (Inc (BISet.singleton x)) (* TODO: proper castkind *)
 
   let of_interval ik (x, y) =
     if Z.compare x y = 0 then
diff --git a/src/cdomain/value/cdomains/int/intDomTuple.ml b/src/cdomain/value/cdomains/int/intDomTuple.ml
index 1c54f2905a..8addcefe5c 100644
--- a/src/cdomain/value/cdomains/int/intDomTuple.ml
+++ b/src/cdomain/value/cdomains/int/intDomTuple.ml
@@ -362,8 +362,8 @@ module IntDomTupleImpl = struct
   let c_lognot ik =
     map ik {f1 = (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.c_lognot ik)}
 
-  let cast_to ?(suppress_ovwarn=false) ?torg ?no_ov t =
-    mapovc ~suppress_ovwarn ~op:`Cast t {f1_ovc = (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.cast_to ?torg ?no_ov t)}
+  let cast_to ?(suppress_ovwarn=false) ~kind ?torg ?no_ov t =
+    mapovc ~suppress_ovwarn ~op:(`Cast kind) t {f1_ovc = (fun (type a) (module I : SOverflow with type t = a) ?no_ov -> I.cast_to ~kind ?torg ?no_ov t)}
 
   (* fp: projections *)
   let equal_to i x =
diff --git a/src/cdomain/value/cdomains/int/intervalDomain.ml b/src/cdomain/value/cdomains/int/intervalDomain.ml
index a488491cb4..1769878d72 100644
--- a/src/cdomain/value/cdomains/int/intervalDomain.ml
+++ b/src/cdomain/value/cdomains/int/intervalDomain.ml
@@ -138,7 +138,7 @@ struct
   let maximal = function None -> None | Some (x,y) -> Some y
   let minimal = function None -> None | Some (x,y) -> Some x
 
-  let cast_to ?torg ?no_ov t = norm ~cast:true t (* norm does all overflow handling *)
+  let cast_to ~kind ?torg ?no_ov t = norm ~cast:true t (* norm does all overflow handling *)
 
   let widen ik x y =
     match x, y with
diff --git a/src/cdomain/value/cdomains/int/intervalSetDomain.ml b/src/cdomain/value/cdomains/int/intervalSetDomain.ml
index 5f51be410e..6593400ad7 100644
--- a/src/cdomain/value/cdomains/int/intervalSetDomain.ml
+++ b/src/cdomain/value/cdomains/int/intervalSetDomain.ml
@@ -484,7 +484,7 @@ struct
     in
     binop x y interval_rem
 
-  let cast_to ?torg ?no_ov ik x = norm_intvs ~cast:true ik x
+  let cast_to ~kind ?torg ?no_ov ik x = norm_intvs ~cast:true ik x
 
   (*
       narrows down the extremeties of xs if they are equal to boundary values of the ikind with (possibly) narrower values from ys
diff --git a/src/cdomain/value/cdomains/intDomain0.ml b/src/cdomain/value/cdomains/intDomain0.ml
index 14fc7530bb..d9e6c4fbe1 100644
--- a/src/cdomain/value/cdomains/intDomain0.ml
+++ b/src/cdomain/value/cdomains/intDomain0.ml
@@ -71,7 +71,7 @@ let should_wrap ik = not (Cil.isSigned ik) || get_string "sem.int.signed_overflo
 let should_ignore_overflow ik = Cil.isSigned ik && get_string "sem.int.signed_overflow" = "assume_none"
 
 type overflow_info = IntDomain_intf.overflow_info = { overflow: bool; underflow: bool;}
-type overflow_op = [`Binop of binop | `Unop of unop | `Cast | `Internal]
+type overflow_op = [`Binop of binop | `Unop of unop | `Cast of castkind | `Internal]
 
 let set_overflow_flag ~(op:overflow_op) ~underflow ~overflow ik =
   if !AnalysisState.executing_speculative_computations then
@@ -79,14 +79,22 @@ let set_overflow_flag ~(op:overflow_op) ~underflow ~overflow ik =
     ()
   else
     let signed = Cil.isSigned ik in
-    if !AnalysisState.postsolving && signed && op <> `Cast then
+    if !AnalysisState.postsolving && signed && (match op with `Cast _ -> false | _ -> true) then
       AnalysisState.svcomp_may_overflow := true;
     let sign = if signed then "Signed" else "Unsigned" in
     let op =
       match op with
       | `Binop bop -> CilType.Binop.show bop
       | `Unop uop -> CilType.Unop.show uop
-      | `Cast -> "cast"
+      | `Cast Explicit -> "cast"
+      | `Cast IntegerPromotion -> "integer promotion"
+      | `Cast DefaultArgumentPromotion -> "default argument promotion"
+      | `Cast ArithmeticConversion -> "arithmethic conversion"
+      | `Cast ConditionalConversion -> "conditional conversion"
+      | `Cast PointerConversion -> "pointer conversion"
+      | `Cast Implicit -> "implicit conversion"
+      | `Cast Internal -> "internal cast"
+      | `Cast Unknown -> "unknown cast"
       | `Internal -> "internal operation"
     in
     match underflow, overflow with
@@ -169,7 +177,7 @@ struct
   let name () = "IntDomLifter(" ^ (I.name ()) ^ ")"
   let to_yojson x = I.to_yojson x.v
   let invariant e x =
-    let e' = Cilfacade.mkCast ~e ~newt:(TInt (x.ikind, [])) in
+    let e' = Cilfacade.mkCast ~kind:Unknown ~e ~newt:(TInt (x.ikind, [])) in
     I.invariant_ikind e' x.ikind x.v
   let tag x = I.tag x.v
   let arbitrary ik = failwith @@ "Arbitrary not implement for " ^ (name ()) ^ "."
@@ -214,7 +222,7 @@ struct
   let c_logand = lift2 I.c_logand
   let c_logor = lift2 I.c_logor
 
-  let cast_to ?(suppress_ovwarn=false) ?torg ikind x = {v = I.cast_to  ~suppress_ovwarn ~torg:(TInt(x.ikind,[])) ikind x.v; ikind}
+  let cast_to ?(suppress_ovwarn=false) ~kind ?torg ikind x = {v = I.cast_to  ~suppress_ovwarn ~kind ~torg:(TInt(x.ikind,[])) ikind x.v; ikind}
 
   let is_top_of ik x = ik = x.ikind && I.is_top_of ik x.v
 
@@ -517,7 +525,7 @@ module SOverflowUnlifter (D : SOverflow) : S2 with type int_t = D.int_t and type
 
   let neg ?no_ov ik x = fst @@ D.neg ?no_ov ik x
 
-  let cast_to ?suppress_ovwarn ?torg ?no_ov ik x = fst @@ D.cast_to ?torg ?no_ov ik x
+  let cast_to ?suppress_ovwarn ~kind ?torg ?no_ov ik x = fst @@ D.cast_to ~kind ?torg ?no_ov ik x
 
   let of_int ?suppress_ovwarn ik x = fst @@ D.of_int ik x
 
@@ -585,7 +593,7 @@ struct
   let c_lognot n1    = of_bool (not (to_bool' n1))
   let c_logand n1 n2 = of_bool ((to_bool' n1) && (to_bool' n2))
   let c_logor  n1 n2 = of_bool ((to_bool' n1) || (to_bool' n2))
-  let cast_to ?(suppress_ovwarn=false) ?torg t x =  failwith @@ "Cast_to not implemented for " ^ (name ()) ^ "."
+  let cast_to ?(suppress_ovwarn=false) ~kind ?torg t x =  failwith @@ "Cast_to not implemented for " ^ (name ()) ^ "."
   let arbitrary ik = QCheck.map ~rev:Ints_t.to_int64 Ints_t.of_int64 GobQCheck.Arbitrary.int64 (* TODO: use ikind *)
   let invariant _ _ = Invariant.none (* TODO *)
 end
@@ -615,8 +623,8 @@ struct
 
 
   let name () = "flat integers"
-  let cast_to ?(suppress_ovwarn=false) ?torg t = function
-    | `Lifted x -> `Lifted (Base.cast_to t x)
+  let cast_to ?(suppress_ovwarn=false) ~kind ?torg t = function
+    | `Lifted x -> `Lifted (Base.cast_to ~kind t x)
     | x -> x
 
   let equal_to i = function
@@ -696,8 +704,8 @@ struct
   include StdTop (struct type nonrec t = t let top_of = top_of end)
 
   let name () = "lifted integers"
-  let cast_to ?(suppress_ovwarn=false) ?torg t = function
-    | `Lifted x -> `Lifted (Base.cast_to t x)
+  let cast_to ?(suppress_ovwarn=false) ~kind ?torg t = function
+    | `Lifted x -> `Lifted (Base.cast_to ~kind t x)
     | x -> x
 
   let equal_to i = function
@@ -769,7 +777,7 @@ module SOverflowLifter (D : S) : SOverflow with type int_t = D.int_t and type t
 
   let neg ?no_ov ik x = lift @@ D.neg ?no_ov ik x
 
-  let cast_to ?torg ?no_ov ik x = lift @@ D.cast_to ?torg ?no_ov ik x
+  let cast_to ~kind ?torg ?no_ov ik x = lift @@ D.cast_to ~kind ?torg ?no_ov ik x
 
   let of_int ik x = lift @@ D.of_int ik x
 
diff --git a/src/cdomain/value/cdomains/intDomain_intf.ml b/src/cdomain/value/cdomains/intDomain_intf.ml
index 3d19a2c2ea..b47a20600f 100644
--- a/src/cdomain/value/cdomains/intDomain_intf.ml
+++ b/src/cdomain/value/cdomains/intDomain_intf.ml
@@ -199,7 +199,7 @@ sig
 
   (** {b Cast} *)
 
-  val cast_to: ?suppress_ovwarn:bool -> ?torg:Cil.typ -> Cil.ikind -> t -> t
+  val cast_to: ?suppress_ovwarn:bool -> kind:castkind -> ?torg:Cil.typ -> Cil.ikind -> t -> t
   (** Cast from original type [torg] to integer type [Cil.ikind]. Currently, [torg] is only present for actual casts. The function is also called to handle overflows/wrap around after operations. In these cases (where the type stays the same) [torg] is None. *)
 
 end
@@ -241,7 +241,7 @@ sig
   val mul : ?no_ov:bool -> Cil.ikind ->  t -> t -> t
   val div : ?no_ov:bool -> Cil.ikind ->  t -> t -> t
   val neg : ?no_ov:bool -> Cil.ikind ->  t -> t
-  val cast_to : ?suppress_ovwarn:bool -> ?torg:Cil.typ -> ?no_ov:bool -> Cil.ikind -> t -> t
+  val cast_to : ?suppress_ovwarn:bool -> kind:castkind -> ?torg:Cil.typ -> ?no_ov:bool -> Cil.ikind -> t -> t
   (** @param no_ov If true, assume no overflow can occur. *)
 
   val join: Cil.ikind -> t ->  t -> t
@@ -300,7 +300,7 @@ sig
 
   val neg : ?no_ov:bool -> Cil.ikind ->  t -> t * overflow_info
 
-  val cast_to : ?torg:Cil.typ -> ?no_ov:bool -> Cil.ikind -> t -> t * overflow_info
+  val cast_to : kind:castkind -> ?torg:Cil.typ -> ?no_ov:bool -> Cil.ikind -> t -> t * overflow_info
 
   val of_int : Cil.ikind -> int_t -> t * overflow_info
 
diff --git a/src/cdomain/value/cdomains/offset.ml b/src/cdomain/value/cdomains/offset.ml
index 2d51f60996..705c568d3e 100644
--- a/src/cdomain/value/cdomains/offset.ml
+++ b/src/cdomain/value/cdomains/offset.ml
@@ -23,7 +23,14 @@ struct
     let name () = "exp index"
 
     let any = Cilfacade.any_index_exp
-    let all = lazy (CastE (TInt (Cilfacade.ptrdiff_ikind (), []), mkString "all_index"))
+    let is_any = function
+      | CastE (_, TInt (ik, []), Const (CStr ("any_index", No_encoding))) when CilType.Ikind.equal ik (Cilfacade.ptrdiff_ikind ()) -> true
+      | _ -> false
+
+    let all = lazy (CastE (Internal, TInt (Cilfacade.ptrdiff_ikind (), []), mkString "all_index"))
+    let is_all = function
+      | CastE (_, TInt (ik, []), Const (CStr ("all_index", No_encoding))) when CilType.Ikind.equal ik (Cilfacade.ptrdiff_ikind ()) -> true
+      | _ -> false
 
     (* Override output *)
     let pretty () x =
diff --git a/src/cdomain/value/cdomains/offset_intf.ml b/src/cdomain/value/cdomains/offset_intf.ml
index e858f72214..a3fb705f4b 100644
--- a/src/cdomain/value/cdomains/offset_intf.ml
+++ b/src/cdomain/value/cdomains/offset_intf.ml
@@ -128,10 +128,16 @@ sig
           Used for [exp.fast_global_inits]. *)
       val any: GoblintCil.exp Lazy.t
 
+      (** [is_any e] is like [CilType.Exp.equal e any], except it ignores cast kind. *)
+      val is_any: GoblintCil.exp -> bool
+
       (** Special index expression for all indices.
           Strongly updates array in assignment.
           Used for Goblint-specific witness invariants. *)
       val all: GoblintCil.exp Lazy.t
+
+      (** [is_all e] is like [CilType.Exp.equal e all], except it ignores cast kind. *)
+      val is_all: GoblintCil.exp -> bool
     end
 
     module Z: Printable with type t = Z.t
diff --git a/src/cdomain/value/cdomains/unionDomain.ml b/src/cdomain/value/cdomains/unionDomain.ml
index 302875ea2e..a7a8edf243 100644
--- a/src/cdomain/value/cdomains/unionDomain.ml
+++ b/src/cdomain/value/cdomains/unionDomain.ml
@@ -5,7 +5,7 @@ open GoblintCil
 module type Arg =
 sig
   include Lattice.S
-  val cast: ?torg:typ -> typ -> t -> t
+  val cast: kind:castkind -> ?torg:typ -> typ -> t -> t
 end
 
 module type S =
@@ -54,7 +54,7 @@ struct
     | Field (f, offset) ->
       begin match lift_f with
         | `Lifted f' ->
-          let v = Values.cast ~torg:f'.ftype f.ftype v in
+          let v = Values.cast ~kind:Unknown ~torg:f'.ftype f.ftype v in (* TODO: proper castkind *)
           value_invariant ~offset ~lval v
         | `Top
         | `Bot ->
diff --git a/src/cdomain/value/cdomains/valueDomain.ml b/src/cdomain/value/cdomains/valueDomain.ml
index 6f234cce50..bc94967539 100644
--- a/src/cdomain/value/cdomains/valueDomain.ml
+++ b/src/cdomain/value/cdomains/valueDomain.ml
@@ -26,7 +26,7 @@ sig
   val invalidate_abstract_value: t -> t
   val is_statically_safe_cast: typ -> typ -> bool
   val is_dynamically_safe_cast: typ -> typ -> t -> bool
-  val cast: ?torg:typ -> typ -> t -> t
+  val cast: kind:castkind -> ?torg:typ -> typ -> t -> t
   val smart_join: (exp -> Z.t option) -> (exp -> Z.t option) -> t -> t ->  t
   val smart_widen: (exp -> Z.t option) -> (exp -> Z.t option) ->  t -> t -> t
   val smart_leq: (exp -> Z.t option) -> (exp -> Z.t option) -> t -> t -> bool
@@ -212,7 +212,7 @@ struct
     | _ when is_mutex_type t -> Mutex
     | t when is_jmp_buf_type t -> JmpBuf (JmpBufs.top ())
     | t when is_mutexattr_type t -> MutexAttr (MutexAttrDomain.top ())
-    | TInt (ik,_) -> Int (ID.(cast_to ik (top_of ik)))
+    | TInt (ik,_) -> Int (ID.(cast_to ~kind:Unknown ik (top_of ik))) (* TODO: proper castkind *)
     (* TODO: TEnum? *)
     | TFloat (fkind, _) when not (Cilfacade.isComplexFKind fkind) -> Float (FD.top_of fkind)
     | TPtr _ -> Address AD.top_ptr
@@ -476,7 +476,7 @@ struct
    * 1. normal casts
    * 2. dereferencing pointers (needed?)
   *)
-  let cast ?torg t v =
+  let cast ~kind ?torg t v =
     (*if v = Bot || (match torg with Some x -> is_safe_cast t x | None -> false) then v else*)
     match v with
     | Bot
@@ -490,7 +490,7 @@ struct
       let t = unrollType t in
       let v' = match t with
         | TInt (ik,_) ->
-          Int (ID.cast_to ?torg ik (match v with
+          Int (ID.cast_to ~kind ?torg ik (match v with
               | Int x -> x
               | Address x -> AD.to_int x
               | Float x -> FD.to_int ik x
@@ -507,14 +507,14 @@ struct
            | _ -> log_top __POS__; Top)
         | TFloat _ -> log_top __POS__; Top (*ignore complex numbers by going to top*)
         | TEnum ({ekind=ik; _},_) ->
-          Int (ID.cast_to ?torg ik (match v with
+          Int (ID.cast_to ~kind ?torg ik (match v with
               | Int x -> (* TODO warn if x is not in the constant values of ei.eitems? (which is totally valid (only ik is relevant for wrapping), but might be unintended) *) x
               | _ -> log_top __POS__; ID.top_of ik
             ))
         | TPtr (t,_) when isVoidType t || isVoidPtrType t ->
           (match v with
            | Address a -> v
-           | Int i -> Int(ID.cast_to ?torg (Cilfacade.ptr_ikind ()) i)
+           | Int i -> Int(ID.cast_to ~kind ?torg (Cilfacade.ptr_ikind ()) i)
            | _ -> v (* TODO: Does it make sense to have things here that are neither Address nor Int? *)
           )
         (* cast to voidPtr are ignored TODO what happens if our value does not fit? *)
@@ -707,7 +707,7 @@ struct
     | (x, Top) -> x
     | (Int x, Int y) -> Int (ID.meet x y)
     | (Float x, Float y) -> Float (FD.meet x y)
-    | (Int _, Address _) -> meet x (cast !GoblintCil.upointType y)
+    | (Int _, Address _) -> meet x (cast ~kind:Unknown !GoblintCil.upointType y) (* TODO: proper castkind *)
     | (Address x, Int y) -> Address (AD.meet x (AD.of_int y))
     | (Address x, Address y) -> Address (AD.meet x y)
     | (Struct x, Struct y) -> Struct (Structs.meet x y)
@@ -732,7 +732,7 @@ struct
     match (x,y) with
     | (Int x, Int y) -> Int (ID.narrow x y)
     | (Float x, Float y) -> Float (FD.narrow x y)
-    | (Int _, Address _) -> narrow x (cast !GoblintCil.upointType y)
+    | (Int _, Address _) -> narrow x (cast ~kind:Unknown !GoblintCil.upointType y) (* TODO: proper castkind *)
     | (Address x, Int y) -> Address (AD.narrow x (AD.of_int y))
     | (Address x, Address y) -> Address (AD.narrow x y)
     | (Struct x, Struct y) -> Struct (Structs.narrow x y)
@@ -827,7 +827,7 @@ struct
       |	AlignOfE _ -> false
       | Question(e1, e2, e3, _) ->
         (contains_pointer e1) || (contains_pointer e2) || (contains_pointer e3)
-      |	CastE(_, e)
+      |	CastE(_, _, e)
       |	UnOp(_, e , _)
       | Real e
       | Imag e -> contains_pointer e
@@ -952,7 +952,7 @@ struct
                  | Float _, t -> top_value t
                  | _, TFloat(fkind, _)  when not (Cilfacade.isComplexFKind fkind)-> Float (FD.top_of fkind)
                  | _ ->
-                   let x = cast ~torg:l_fld.ftype fld.ftype value in
+                   let x = cast ~kind:Unknown ~torg:l_fld.ftype fld.ftype value in (* TODO: proper castkind *)
                    let l', o' = shift_one_over l o in
                    do_eval_offset ask f x offs exp l' o' v t)
               | Union _ -> top ()
@@ -1079,7 +1079,7 @@ struct
                     match bitfield with
                     | Some b when not @@ ID.leq i (ID.top_of ~bitfield:b (ID.ikind i)) ->
                       Messages.warn ~category:Analyzer "Assigned value %a exceeds the representable range of a %d-bit bit-field." pretty value b; Top
-                    | _ -> cast t value
+                    | _ -> cast ~kind:Unknown t value (* TODO: proper castkind *)
                   end
                 | _ -> value
               end
@@ -1222,7 +1222,7 @@ struct
           | Some e ->
             begin
               match eval_exp e with
-              | Int x -> ID.cast_to (Cilfacade.ptrdiff_ikind ())  x
+              | Int x -> ID.cast_to ~kind:Unknown (Cilfacade.ptrdiff_ikind ())  x (* TODO: proper castkind *)
               | _ ->
                 M.debug ~category:Analyzer "Expression for size of VLA did not evaluate to Int at declaration";
                 ID.starting (Cilfacade.ptrdiff_ikind ()) Z.zero
@@ -1361,7 +1361,7 @@ struct
           let offset = Addr.Offs.to_cil offs in
 
           let cast_to_void_ptr e =
-            Cilfacade.mkCast ~e ~newt:(TPtr (TVoid [], []))
+            Cilfacade.mkCast ~kind:Unknown ~e ~newt:(TPtr (TVoid [], []))
           in
           let i =
             if InvariantCil.(exp_is_suitable ~scope c_exp && var_is_suitable ~scope vi && not (var_is_heap vi)) then
@@ -1384,7 +1384,7 @@ struct
               (* Address set for a void* variable contains pointers to values of non-void type,
                   so insert pointer cast to make invariant expression valid (no field/index on void). *)
               let newt = TPtr (typ, []) in
-              let c_exp = Cilfacade.mkCast ~e:c_exp ~newt in
+              let c_exp = Cilfacade.mkCast ~kind:Unknown ~e:c_exp ~newt in
               deref_invariant ~vs vi ~offset ~lval:(Mem c_exp, NoOffset)
             | exception Cilfacade.TypeOfError _ (* typeOffset: Index on a non-array on calloc-ed alloc variables *)
             | _ ->
diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml
index 5cf989452d..9aaa0f125e 100644
--- a/src/cdomains/apron/sharedFunctions.apron.ml
+++ b/src/cdomains/apron/sharedFunctions.apron.ml
@@ -160,7 +160,7 @@ struct
                 GobRef.wrap AnalysisState.executing_speculative_computations true @@ fun () ->
                 let ikind = try (Cilfacade.get_ikind_exp e) with Invalid_argument a -> raise (Unsupported_CilExp (Ikind_non_integer a))   in
                 let simp = query e ikind in
-                let const = IntDomain.IntDomTuple.to_int @@ IntDomain.IntDomTuple.cast_to ikind simp in
+                let const = IntDomain.IntDomTuple.to_int @@ IntDomain.IntDomTuple.cast_to ~kind:Unknown ikind simp in (* TODO: proper castkind *)
                 if M.tracing then M.trace "relation" "texpr1_expr_of_cil_exp/simplify: %a -> %a" d_plainexp e IntDomain.IntDomTuple.pretty simp;
                 BatOption.map_default (fun c -> Const (CInt (c, ikind, None))) e const
               in
@@ -174,7 +174,7 @@ struct
               | BinOp (Mod, e1, e2, _) -> bop_near Mod e1 e2
               | BinOp (Div, e1, e2, _) ->
                 Binop (Div, texpr1 e1, texpr1 e2, Int, Zero)
-              | CastE (t, e) when Cil.isIntegralType t ->
+              | CastE (_, t, e) when Cil.isIntegralType t ->
                 begin match  IntDomain.Size.is_cast_injective ~from_type:(Cilfacade.typeOf e) ~to_type:t with (* TODO: unnecessary cast check due to overflow check below? or maybe useful in general to also assume type bounds based on argument types? *)
                   | exception Invalid_argument a -> raise (Unsupported_CilExp (Ikind_non_integer a))
                   | true -> texpr1 e
@@ -185,7 +185,7 @@ struct
                       (* try to evaluate e by EvalInt Query *)
                       let res = try (query e @@ Cilfacade.get_ikind_exp e) with Invalid_argument a -> raise (Unsupported_CilExp (Ikind_non_integer a))  in
                       (* convert response to a constant *)
-                      IntDomain.IntDomTuple.to_int @@ IntDomain.IntDomTuple.cast_to t_ik res, res in
+                      IntDomain.IntDomTuple.to_int @@ IntDomain.IntDomTuple.cast_to ~kind:Unknown t_ik res, res in (* TODO: proper castkind *)
                     match const with
                     | Some c -> Cst (Coeff.s_of_z c) (* Got a constant value -> use it straight away *)
                     (* I gotten top, we can not guarantee injectivity *)
@@ -300,7 +300,7 @@ struct
   let cil_exp_of_linexpr1_term ~scalewith (c: Coeff.t) v =
     match V.to_cil_varinfo v with
     | Some vinfo when IntDomain.Size.is_cast_injective ~from_type:vinfo.vtype ~to_type:(TInt(ILongLong,[]))   ->
-      let var = Cilfacade.mkCast ~e:(Lval(Var vinfo,NoOffset)) ~newt:longlong in
+      let var = Cilfacade.mkCast ~kind:Unknown ~e:(Lval(Var vinfo,NoOffset)) ~newt:longlong in
       let i = int_of_coeff_warn ~scalewith c in
       if Z.equal i Z.one then
         false, var
diff --git a/src/cdomains/regionDomain.ml b/src/cdomains/regionDomain.ml
index cd9141876c..b3f4dfe694 100644
--- a/src/cdomains/regionDomain.ml
+++ b/src/cdomains/regionDomain.ml
@@ -126,7 +126,7 @@ struct
       match rval with
       | Lval lval -> BatOption.map (fun (deref, v, offs) -> (deref, v, `NoOffset)) (eval_lval deref lval)
       | AddrOf lval -> eval_lval deref lval
-      | CastE (typ, exp) -> eval_rval deref exp
+      | CastE (_, typ, exp) -> eval_rval deref exp
       | BinOp (MinusPI, p, i, typ)
       | BinOp (PlusPI, p, i, typ)
       | BinOp (IndexPI, p, i, typ) -> eval_rval deref p
diff --git a/src/cdomains/symbLocksDomain.ml b/src/cdomains/symbLocksDomain.ml
index 10ea70da1d..020ac9120e 100644
--- a/src/cdomains/symbLocksDomain.ml
+++ b/src/cdomains/symbLocksDomain.ml
@@ -30,7 +30,7 @@ struct
       | AddrOf  (Mem e,o)
       | StartOf (Mem e,o)
       | Lval    (Mem e,o) -> cv true e || offs_contains o
-      | CastE (_,e)           -> cv deref e
+      | CastE (_,_,e)           -> cv deref e
       | Lval    (Var v2,o) -> CilType.Varinfo.equal v v2 || offs_contains o
       | AddrOf  (Var v2,o)
       | StartOf (Var v2,o) ->
@@ -105,7 +105,7 @@ struct
     | AddrOf (Mem e,o)                     -> AddrOf (Mem (replace_base (v,offs) q e), o)
     | StartOf (Mem e,o) when simple_eq e q -> StartOf (Var v, addOffset o (Offset.Exp.to_cil offs))
     | StartOf (Mem e,o)                    -> StartOf (Mem (replace_base (v,offs) q e), o)
-    | CastE (t,e) -> CastE (t, replace_base (v,offs) q e)
+    | CastE (k,t,e) -> CastE (k, t, replace_base (v,offs) q e)
 
 
   let rec conc i =
@@ -157,7 +157,7 @@ struct
       end
     | AddrOf (Mem e, NoOffset) -> one_unknown_array_index e
     | StartOf (Mem e, NoOffset) -> one_unknown_array_index e
-    | CastE (t,e) -> one_unknown_array_index e
+    | CastE (_,t,e) -> one_unknown_array_index e
     | _ -> None
 end
 
@@ -221,7 +221,7 @@ struct
       | AddrOf (Mem e, os) -> helper e @ [EDeref] @ conv_o os @ [EAddr]
       | StartOf (Var v, os) -> EVar v :: conv_o os @ [EAddr]
       | StartOf (Mem e, os) -> helper e @ [EDeref] @ conv_o os @ [EAddr]
-      | CastE (_,e) -> helper e
+      | CastE (_,_,e) -> helper e
     in
     try helper exp
     with NotSimpleEnough -> []
@@ -350,7 +350,7 @@ struct
        | AddrOf  (Mem e,ofs) -> S.map (fun e -> AddrOf  (Mem e,ofs)) (eq_set ask e)
        | StartOf (Mem e,ofs) -> S.map (fun e -> StartOf (Mem e,ofs)) (eq_set ask e)
        | Lval    (Mem e,ofs) -> S.map (fun e -> Lval    (Mem e,ofs)) (eq_set ask e)
-       | CastE (_,e)           -> eq_set ask e
+       | CastE (_,_,e)           -> eq_set ask e
       )
 
   let add (ask: Queries.ask) e st =
diff --git a/src/cdomains/unionFind.ml b/src/cdomains/unionFind.ml
index 5dd999dfd1..d55052f300 100644
--- a/src/cdomains/unionFind.ml
+++ b/src/cdomains/unionFind.ml
@@ -158,7 +158,7 @@ module T = struct
     | ikind ->
       begin match ask.f (Queries.EvalInt exp) with
         | `Lifted i ->
-          let casted_i = IntDomain.IntDomTuple.cast_to ikind i in
+          let casted_i = IntDomain.IntDomTuple.cast_to ~kind:Unknown ikind i in (* TODO: proper castkind *)
           let maybe_i = IntDomain.IntDomTuple.to_int casted_i in
           begin match maybe_i with
             | Some i -> i
@@ -238,14 +238,14 @@ module T = struct
         `NoOffset
       | Field (fld, ofs) ->
         `Field (fld, convert_offset ofs)
-      | Index (exp, ofs) when CilType.Exp.equal exp (Lazy.force Offset.Index.Exp.any) -> (* special offset added by convertToQueryLval *)
+      | Index (exp, ofs) when Offset.Index.Exp.is_any exp -> (* special offset added by convertToQueryLval *)
         let exp_ikind = Cilfacade.get_ikind_exp exp in
         `Index (ValueDomain.ID.top_of exp_ikind, convert_offset ofs)
       | Index (exp, ofs) ->
         let ptr_diff_ikind = Cilfacade.ptrdiff_ikind () in
         let i = match ask.f (Queries.EvalInt exp) with
           | `Lifted x ->
-            IntDomain.IntDomTuple.cast_to ptr_diff_ikind x
+            IntDomain.IntDomTuple.cast_to ~kind:Unknown ptr_diff_ikind x (* TODO: proper castkind *)
           | _ ->
             ValueDomain.ID.top_of ptr_diff_ikind
         in
@@ -463,7 +463,7 @@ module T = struct
           | _ ->
             let void_ptr_type = TPtr(TVoid [], []) in
             let offset_plus_exp =  to_cil_sum offset exp in
-            Lval (Mem (CastE (void_ptr_type, offset_plus_exp)), NoOffset)
+            Lval (Mem (CastE (Unknown, void_ptr_type, offset_plus_exp)), NoOffset)
       in
       if check_valid_pointer res then
         res
@@ -537,14 +537,14 @@ module T = struct
         | _ ->
           raise (UnsupportedCilExpression "unsupported BinOp")
       end
-    | CastE (typ, exp)->
+    | CastE (kind, typ, exp)->
       begin match of_cil ask exp with
         | Some (Addr x), z ->
           Some (Addr x), z
         | Some (Aux (x, _)), z ->
-          Some (Aux (x, CastE (typ, exp))), z
+          Some (Aux (x, CastE (kind, typ, exp))), z
         | Some (Deref (x, z, _)), z' ->
-          Some (Deref (x, z, CastE (typ, exp))), z'
+          Some (Deref (x, z, CastE (kind, typ, exp))), z'
         | t, z -> t, z
       end
     | _ -> raise (UnsupportedCilExpression "unsupported Cil Expression")
diff --git a/src/common/cdomains/basetype.ml b/src/common/cdomains/basetype.ml
index bf832b1c3c..5ec9b22b44 100644
--- a/src/common/cdomains/basetype.ml
+++ b/src/common/cdomains/basetype.ml
@@ -60,7 +60,7 @@ struct
     | SizeOfE e
     | AlignOfE e -> occurs x e
     | BinOp (_,e1,e2,_) -> occurs x e1 || occurs x e2
-    | CastE (_,e) -> occurs x e
+    | CastE (_,_,e) -> occurs x e
     | Question (b, t, f, _) -> occurs x b || occurs x t || occurs x f
     | Const _
     | SizeOf _
@@ -86,7 +86,7 @@ struct
       | StartOf l -> StartOf (replace_lv l)
       | UnOp (op,e,t) -> UnOp (op, replace_rv e, t)
       | BinOp (op,e1,e2,t) -> BinOp (op, replace_rv e1, replace_rv e2, t)
-      | CastE (t,e) -> CastE(t, replace_rv e)
+      | CastE (k,t,e) -> CastE(k, t, replace_rv e)
       | Real e -> Real (replace_rv e)
       | Imag e -> Imag (replace_rv e)
       | SizeOfE e -> SizeOfE (replace_rv e)
@@ -113,7 +113,7 @@ struct
     | AddrOf _
     | StartOf _ -> [] (* TODO: return not empty, some may contain vars! *)
     | UnOp (_, e, _ )
-    | CastE (_, e)
+    | CastE (_, _, e)
     | Real e
     | Imag e -> get_vars e
     | BinOp (_, e1, e2, _) -> (get_vars e1)@(get_vars e2)
diff --git a/src/common/util/cilType.ml b/src/common/util/cilType.ml
index d50f288a43..1ecfc6fecc 100644
--- a/src/common/util/cilType.ml
+++ b/src/common/util/cilType.ml
@@ -250,6 +250,42 @@ struct
     )
 end
 
+module Castkind: S with type t = castkind =
+struct
+  include Std
+
+  (* Re-export constructors for monomorphization and deriving. *)
+  type t = castkind =
+    | Explicit
+    | IntegerPromotion
+    | DefaultArgumentPromotion
+    | ArithmeticConversion
+    | ConditionalConversion
+    | PointerConversion
+    | Implicit
+    | Internal
+    | Unknown
+  [@@deriving hash]
+  (* Hashtbl.hash doesn't monomorphize, so derive instead. *)
+
+  let name () = "castkind"
+
+  (* Identity *)
+  (* Enum type, so polymorphic identity is fine. *)
+  (* Monomorphize polymorphic operations for optimization. *)
+  let equal (x: t) (y: t) = x = y
+  let compare (x: t) (y: t) = Stdlib.compare x y
+
+  (* Output *)
+  let pretty () x = d_castkind () x
+  include Printable.SimplePretty (
+    struct
+      type nonrec t = t
+      let pretty = pretty
+    end
+    )
+end
+
 module Wstring_type: S with type t = wstring_type =
 struct
   include Std
@@ -652,7 +688,7 @@ struct
     | UnOp of Unop.t * t * Typ.t
     | BinOp of Binop.t * t * t * Typ.t
     | Question of t * t * t * Typ.t
-    | CastE of Typ.t * t
+    | CastE of Castkind.t * Typ.t * t
     | AddrOf of Lval.t
     | AddrOfLabel of Stmt.t ref
     | StartOf of Lval.t
diff --git a/src/common/util/cilfacade.ml b/src/common/util/cilfacade.ml
index 452d0297a5..16e43ba9ea 100644
--- a/src/common/util/cilfacade.ml
+++ b/src/common/util/cilfacade.ml
@@ -348,7 +348,7 @@ let rec typeOf (e: exp) : typ =
   | UnOp (_, _, t)
   | BinOp (_, _, _, t)
   | Question (_, _, _, t)
-  | CastE (t, _) -> t
+  | CastE (_, t, _) -> t
   | AddrOf (lv) -> TPtr(typeOfLval lv, [])
   | AddrOfLabel (lv) -> voidPtrType
   | StartOf (lv) -> begin
@@ -417,14 +417,14 @@ let bytesOffsetOnly t o =
 
 
 (** {!Cil.mkCast} using our {!typeOf}. *)
-let mkCast ~(e: exp) ~(newt: typ) =
+let mkCast ~kind ~(e: exp) ~(newt: typ) =
   let oldt =
     try
       typeOf e
     with TypeOfError _ -> (* e might involve alloc variables, weird offsets, etc *)
       Cil.voidType (* oldt is only used for avoiding duplicate cast, so this falls back to adding cast *)
   in
-  Cil.mkCastT ~e ~oldt ~newt
+  Cil.mkCastT ~kind ~e ~oldt ~newt
 
 (** @raise TypeOfError
     @raise Invalid_argument if not integral type. *)
@@ -805,4 +805,4 @@ let add_function_declarations (file: Cil.file): unit =
 (** Special index expression for some unknown index.
     Weakly updates array in assignment.
     Used for [exp.fast_global_inits]. *)
-let any_index_exp = lazy (CastE (TInt (ptrdiff_ikind (), []), mkString "any_index")) (* TODO: move back to Offset *)
+let any_index_exp = lazy (CastE (Internal, TInt (ptrdiff_ikind (), []), mkString "any_index")) (* TODO: move back to Offset *)
diff --git a/src/domains/access.ml b/src/domains/access.ml
index bc24cf2d31..823e1cd589 100644
--- a/src/domains/access.ml
+++ b/src/domains/access.ml
@@ -234,7 +234,7 @@ let rec get_type (fb: typ Lazy.t) : exp -> acc_typ = function
     `Type (uintType) (* TODO: Correct types from typeOf? *)
   | UnOp (_,_,t) -> `Type t
   | BinOp (_,_,_,t) -> `Type t
-  | CastE (t,e) ->
+  | CastE (_,t,e) ->
     begin match get_type fb e with
       | `Struct s -> `Struct s
       | _         -> `Type t
@@ -370,7 +370,7 @@ and distribute_access_exp f = function
     distribute_access_lval_addr f lval
 
   (* Most casts are currently just ignored, that's probably not a good idea! *)
-  | CastE  (t, exp) ->
+  | CastE (_, t, exp) ->
     distribute_access_exp f exp
   | Question (b,t,e,_) ->
     distribute_access_exp f b;
diff --git a/src/domains/queries.ml b/src/domains/queries.ml
index 31e93dd0b2..e3de5ef1d4 100644
--- a/src/domains/queries.ml
+++ b/src/domains/queries.ml
@@ -562,7 +562,7 @@ let may_be_equal = eval_int_binop (module MayBool) Eq
 let may_be_less = eval_int_binop (module MayBool) Lt
 
 let eval_bool (ask: ask) e: BoolDomain.FlatBool.t =
-  let e' = CastE (TInt (IBool, []), e) in
+  let e' = CastE (Unknown, TInt (IBool, []), e) in
   match ask.f (EvalInt e') with
   | v when ID.is_bot v || ID.is_bot_ikind v -> `Bot
   | v -> BatOption.map_default (fun b -> `Lifted b) `Top (ID.to_bool v)
diff --git a/src/incremental/compareAST.ml b/src/incremental/compareAST.ml
index 59adfe00be..4d01d7e166 100644
--- a/src/incremental/compareAST.ml
+++ b/src/incremental/compareAST.ml
@@ -93,7 +93,7 @@ and eq_exp (a: exp) (b: exp) ~(rename_mapping: rename_mapping) ~(acc: (typ * typ
   | UnOp (op1, exp1, typ1), UnOp (op2, exp2, typ2) ->
     (CilType.Unop.equal op1 op2, rename_mapping) &&>> eq_exp exp1 exp2 ~acc &&>> eq_typ_acc typ1 typ2 ~acc
   | BinOp (op1, left1, right1, typ1), BinOp (op2, left2, right2, typ2) ->  (op1 = op2, rename_mapping) &&>> eq_exp left1 left2 ~acc &&>> eq_exp right1 right2 ~acc &&>> eq_typ_acc typ1 typ2 ~acc
-  | CastE (typ1, exp1), CastE (typ2, exp2) -> eq_typ_acc typ1 typ2 ~rename_mapping ~acc &&>> eq_exp exp1 exp2 ~acc
+  | CastE (kind1, typ1, exp1), CastE (kind2, typ2, exp2) -> (CilType.Castkind.equal kind1 kind2, rename_mapping) &&>> eq_typ_acc typ1 typ2 ~acc &&>> eq_exp exp1 exp2 ~acc (* TODO: or should ignore cast kind? (changing explicit to implicit or vice versa) *)
   | AddrOf lv1, AddrOf lv2 -> eq_lval lv1 lv2 ~rename_mapping ~acc
   | StartOf lv1, StartOf lv2 -> eq_lval lv1 lv2 ~rename_mapping ~acc
   | Real exp1, Real exp2 -> eq_exp exp1 exp2 ~rename_mapping ~acc
diff --git a/src/util/library/libraryFunctions.ml b/src/util/library/libraryFunctions.ml
index ee663d4152..f6c21b7522 100644
--- a/src/util/library/libraryFunctions.ml
+++ b/src/util/library/libraryFunctions.ml
@@ -17,7 +17,7 @@ let intmax_t = lazy (
 )
 
 let stripOuterBoolCast = function
-  | CastE (TInt (IBool, _), e) -> e
+  | CastE (_, TInt (IBool, _), e) -> e (* TODO: keep explicit cast? *)
   | Const (CInt (b, IBool, s)) -> Const (CInt (b, IInt, s))
   | e -> e
 
diff --git a/tests/unit/cdomains/intDomainTest.ml b/tests/unit/cdomains/intDomainTest.ml
index af52b14abd..0f566df867 100644
--- a/tests/unit/cdomains/intDomainTest.ml
+++ b/tests/unit/cdomains/intDomainTest.ml
@@ -430,10 +430,10 @@ struct
   let test_cast_to _ =
     let b1 = I.of_int ik (of_int 1234) in
 
-    assert_equal (I.of_int IUChar (of_int (210))) (I.cast_to IUChar b1);
-    assert_equal (I.of_int IUChar (of_int (-46))) (I.cast_to IUChar b1);
+    assert_equal (I.of_int IUChar (of_int (210))) (I.cast_to ~kind:Unknown IUChar b1);
+    assert_equal (I.of_int IUChar (of_int (-46))) (I.cast_to ~kind:Unknown IUChar b1);
 
-    assert_equal (I.of_int IUInt128 (of_int 1234)) (I.cast_to IUInt128 b1)
+    assert_equal (I.of_int IUInt128 (of_int 1234)) (I.cast_to ~kind:Unknown IUInt128 b1)
 
   (* Bitwise  *)