diff --git a/scripts/goblint-lib-modules.py b/scripts/goblint-lib-modules.py
index 90537e57fe..0e0a0613a7 100755
--- a/scripts/goblint-lib-modules.py
+++ b/scripts/goblint-lib-modules.py
@@ -53,6 +53,7 @@
     "DefExcDomain", # included in IntDomain
     "EnumsDomain", # included in IntDomain
     "CongruenceDomain", # included in IntDomain
+    "BitfieldDomain", #included in IntDomain
     "IntDomTuple", # included in IntDomain
     "WitnessGhostVar", # included in WitnessGhost
 
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 2529398939..ac6cda5762 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -624,6 +624,8 @@ struct
 
   let drop_intervalSet = CPA.map (function Int x -> Int (ID.no_intervalSet x) | x -> x )
 
+  let drop_bitfield = CPA.map (function Int x -> Int (ID.no_bitfield x) | x -> x )
+
   let context man (fd: fundec) (st: store): store =
     let f keep drop_fn (st: store) = if keep then st else { st with cpa = drop_fn st.cpa} in
     st |>
@@ -634,6 +636,7 @@ struct
     %> f (ContextUtil.should_keep ~isAttr:GobContext ~keepOption:"ana.base.context.int" ~removeAttr:"base.no-int" ~keepAttr:"base.int" fd) drop_ints
     %> f (ContextUtil.should_keep ~isAttr:GobContext ~keepOption:"ana.base.context.interval" ~removeAttr:"base.no-interval" ~keepAttr:"base.interval" fd) drop_interval
     %> f (ContextUtil.should_keep ~isAttr:GobContext ~keepOption:"ana.base.context.interval_set" ~removeAttr:"base.no-interval_set" ~keepAttr:"base.interval_set" fd) drop_intervalSet
+    %> f (ContextUtil.should_keep ~isAttr:GobContext ~keepOption:"ana.base.context.bitfield" ~removeAttr:"base.no-bitfield" ~keepAttr:"base.bitfield" fd) drop_bitfield
 
 
   let reachable_top_pointers_types man (ps: AD.t) : Queries.TS.t =
diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml
index 19a9999ecf..485d8b62c9 100644
--- a/src/analyses/baseInvariant.ml
+++ b/src/analyses/baseInvariant.ml
@@ -395,27 +395,46 @@ struct
             | Le, Some false -> meet_bin (ID.starting ikind (Z.succ l2)) (ID.ending ikind (Z.pred u1))
             | _, _ -> a, b)
          | _ -> a, b)
-      | BOr | BXor as op->
-        if M.tracing then M.tracel "inv" "Unhandled operator %a" d_binop op;
+      | BOr ->      
+        (* Be careful: inv_exp performs a meet on both arguments of the BOr / BXor. *)        
+        if PrecisionUtil.get_bitfield () then
+          (* refinement based on the following idea: bit set to one in c and set to zero in b must be one in a and bit set to zero in c must be zero in a too (analogously for b) *)
+          let ((az, ao), (bz, bo)) = BitfieldDomain.Bitfield.refine_bor (ID.to_bitfield ikind a) (ID.to_bitfield ikind b) (ID.to_bitfield ikind c) in 
+          ID.meet a (ID.of_bitfield ikind (az, ao)), ID.meet b (ID.of_bitfield ikind (bz, bo))
+        else 
+          (if M.tracing then M.tracel "inv" "Unhandled operator %a" d_binop op;
+           (* Be careful: inv_exp performs a meet on both arguments of the BOr / BXor. *)
+           (a, b)
+          )
+      | BXor ->
         (* Be careful: inv_exp performs a meet on both arguments of the BOr / BXor. *)
-        a, b
+        meet_com ID.logxor
       | LAnd ->
         if ID.to_bool c = Some true then
           meet_bin c c
         else
           a, b
-      | BAnd as op ->
+      | BAnd ->
         (* we only attempt to refine a here *)
+        let b_int = ID.to_int b in 
         let a =
-          match ID.to_int b with
+          match b_int with
           | Some x when Z.equal x Z.one ->
             (match ID.to_bool c with
              | Some true -> ID.meet a (ID.of_congruence ikind (Z.one, Z.of_int 2))
              | Some false -> ID.meet a (ID.of_congruence ikind (Z.zero, Z.of_int 2))
-             | None -> if M.tracing then M.tracel "inv" "Unhandled case for operator x %a 1 = %a" d_binop op ID.pretty c; a)
-          | _ -> if M.tracing then M.tracel "inv" "Unhandled case for operator x %a %a = %a" d_binop op ID.pretty b ID.pretty c; a
+             | None -> a)
+          | _ -> a
         in
-        a, b
+        if PrecisionUtil.get_bitfield () then 
+          (* refinement based on the following idea: bit set to zero in c and set to one in b must be zero in a and bit set to one in c must be one in a too (analogously for b) *)
+          let ((az, ao), (bz, bo)) = BitfieldDomain.Bitfield.refine_band (ID.to_bitfield ikind a) (ID.to_bitfield ikind b) (ID.to_bitfield ikind c) in 
+          ID.meet a (ID.of_bitfield ikind (az, ao)), ID.meet b (ID.of_bitfield ikind (bz, bo))
+        else if b_int = None then 
+          (if M.tracing then M.tracel "inv" "Unhandled operator %a" d_binop op;
+           (a, b)
+          )
+        else a, b
       | op ->
         if M.tracing then M.tracel "inv" "Unhandled operator %a" d_binop op;
         a, b
diff --git a/src/cdomain/value/cdomains/int/bitfieldDomain.ml b/src/cdomain/value/cdomains/int/bitfieldDomain.ml
new file mode 100644
index 0000000000..d8fc66c8ba
--- /dev/null
+++ b/src/cdomain/value/cdomains/int/bitfieldDomain.ml
@@ -0,0 +1,712 @@
+open IntDomain0
+
+module InfixIntOps (Ints_t : IntOps.IntOps) = struct
+  let (&:) = Ints_t.logand
+  let (|:) = Ints_t.logor
+  let (^:) = Ints_t.logxor
+  let (!:) = Ints_t.lognot
+  let (<<:) = Ints_t.shift_left
+  let (>>:) = Ints_t.shift_right
+  let (<:) = fun a b -> Ints_t.compare a b < 0
+  let (=:) = fun a b -> Ints_t.compare a b = 0
+  let (>:) = fun a b -> Ints_t.compare a b > 0
+  let (<>:) = fun a b -> Ints_t.compare a b <> 0
+
+  let (+:) = Ints_t.add
+  let (-:) = Ints_t.sub
+  let ( *: ) = Ints_t.mul
+  let (/:) = Ints_t.div
+  let (%:) = Ints_t.rem
+
+  let (>>.) = fun a b -> a >>: b |: !:((Ints_t.one <<: b) -: Ints_t.one)
+end
+
+(*
+  Operations in the abstract domain mostly based on 
+
+  "Abstract Domains for Bit-Level Machine Integer and Floating-point Operations"
+  of Antoine Miné
+  https://doi.org/10.29007/b63g
+
+  and
+
+  the bachelor thesis "Integer Abstract Domains"
+  of Tomáš Brukner
+  https://is.muni.cz/th/kasap/thesis.pdf
+*)
+
+(* Bitfield arithmetic, without any overflow handling etc. *)
+module BitfieldArith (Ints_t : IntOps.IntOps) = struct
+
+  include InfixIntOps (Ints_t)
+
+  let zero_mask = Ints_t.zero
+
+  (* one_mask corresponds to (-1). It has an infinite amount of 1 bits *)
+  let one_mask = !:zero_mask
+
+  let of_int x = (!:x, x) 
+
+  let join (z1,o1) (z2,o2) = (z1 |: z2, o1 |: o2)
+  let meet (z1,o1) (z2,o2) = (z1 &: z2, o1 &: o2)
+
+  let one = of_int Ints_t.one
+  let zero = of_int Ints_t.zero
+  let top_bool = join one zero
+
+  let bits_known (z,o) = z ^: o
+  let bits_invalid (z,o) = !:(z |: o)
+
+  let is_const (z,o) = (z ^: o) =: one_mask
+
+  let is_invalid (z,o) =
+    not (!:(z |: o) = Ints_t.zero)
+
+  let nabla x y= if x =: (x |: y) then x else one_mask
+
+  let widen (z1,o1) (z2,o2) = (nabla z1 z2, nabla o1 o2)            
+
+  let lognot (z,o) = (o,z)
+
+  let logxor (z1,o1)  (z2,o2) = ((z1 &: z2) |: (o1 &: o2), 
+                                 (z1 &: o2) |: (o1 &: z2))
+
+  let logand (z1,o1) (z2,o2) = (z1 |: z2, o1 &: o2)
+
+  let logor (z1,o1)  (z2,o2) = (z1 &: z2, o1 |: o2)
+
+  let bitmask_up_to n = (Ints_t.one <<: n) -: Ints_t.one
+
+  let nth_bit p n = Ints_t.one &: (p >>: n) =: Ints_t.one
+
+  let min ik (z,o) = 
+    (* checking whether the MSB is set *)
+    let signBit = Ints_t.one <<: ((Size.bit ik) - 1) in 
+    let isNegative = signBit &: o <>: Ints_t.zero in
+    (* mask to set all bits outside of ik to 1 *)
+    let signMask = !: (Ints_t.of_bigint (snd (Size.range ik))) in    
+    if GoblintCil.isSigned ik && isNegative then 
+      (* maximal number of 0 with correct sign extension *)
+      Ints_t.to_bigint(signMask |: (!: z))
+    else 
+      (* maximal number of 0 with correct sign extension *)
+      Ints_t.to_bigint(!: z)
+
+  let max ik (z,o) =
+    (* checking whether the MSB is set *)
+    let signBit = Ints_t.one <<: ((Size.bit ik) - 1) in 
+    let isPositive = signBit &: z <>: Ints_t.zero in
+    (* mask to set all bits outside of ik to 1 *)
+    let signMask = Ints_t.of_bigint (snd (Size.range ik)) in        
+    if GoblintCil.isSigned ik && isPositive then 
+      (* maximal number of 1 with correct sign extension*)
+      Ints_t.to_bigint(signMask &: o)
+    else 
+      (* maximal number of 1 *)
+      Ints_t.to_bigint o 
+
+  (** [concretize bf] computes the set of all possible integer values represented by the bitfield [bf].
+
+      @param (z,o) The bitfield to concretize.
+
+      @info By default, the function generates all possible values that the bitfield can represent, 
+            which results in an exponential complexity of O(2^n) where [n] is the width of [ik].
+            It is recommended to constrain the number of bits that are concretized to avoid non-termination.
+  *)
+  let rec concretize (z,o) =
+    if is_const (z,o) then [o]
+    else
+      let bit = o &: Ints_t.one in
+      concretize (z >>. 1, o >>: 1)
+      |>
+      match nth_bit z 0, nth_bit o 0 with
+      | true, true -> List.concat_map (fun c -> [c <<: 1; (c <<: 1) |: Ints_t.one])
+      | false, false -> failwith "Should not have happened: Invalid bit during concretization of a bitfield."
+      | _ -> List.map (fun c -> c <<: 1 |: bit)
+
+  let concretize bf = List.map Ints_t.to_int (concretize bf)
+
+  let bit_width_of ik = snd @@ Size.bits ik
+
+  let constrain_to_bit_width_of ik (z,o) =
+    let mask = bitmask_up_to (Int.succ @@ Z.log2up @@ Z.of_int @@ bit_width_of ik) in
+    (z |: !:mask, o &: mask)
+
+  let shift_right ik (z,o) c =
+    let msb_pos = Int.max 0 (Size.bit ik - c) in
+    let sign_mask = !:(bitmask_up_to msb_pos) in
+    if GoblintCil.isSigned ik && o <: Ints_t.zero then
+      ((z >>: c) |: sign_mask, (o >>: c) |: sign_mask) (* sign extension in sar is impl. defined *)
+    else
+      ((z >>: c) |: sign_mask, o >>: c)
+
+  let shift_left _ (z,o) c =
+    let zero_mask = bitmask_up_to c in
+    ((z <<: c) |: zero_mask, o <<: c)
+
+  let join_shifts shift ik bf (z2,o2) =
+    match is_const (z2,o2) with
+    | true -> shift ik bf (Ints_t.to_int o2)
+    | false ->
+      (* Only values leq then inf_c {c | bf >> c = 0} are relevant. *)
+      let defined_shifts = constrain_to_bit_width_of ik (z2, o2) in
+      let shift_amounts = concretize defined_shifts in (* O(n) *)
+      List.fold_left (fun acc c ->
+          join acc @@ shift ik bf c
+        ) (zero_mask, zero_mask) shift_amounts
+
+  let shift_left = join_shifts shift_left
+
+  let shift_right = join_shifts shift_right
+
+  let nth_bit p n = if nth_bit p n then Ints_t.one else Ints_t.zero
+
+  let is_power_of_two x = (x &: (x -: Ints_t.one) = Ints_t.zero) 
+
+  let has_neg_values ik b = Z.compare (min ik b) Z.zero < 0
+
+  let has_only_neg_values ik b = Z.compare (max ik b) Z.zero < 0
+
+  let exceeds_bit_width_of ik b = Z.compare (min ik b) (Z.of_int @@ bit_width_of ik) > 0
+
+  let equals_bit_width_of ik b = Z.compare (min ik b) (Z.of_int @@ bit_width_of ik) = 0
+end
+
+module BitfieldFunctor (Ints_t : IntOps.IntOps): Bitfield_SOverflow with type int_t = Ints_t.t and type t = (Ints_t.t * Ints_t.t) = struct
+
+  include InfixIntOps (Ints_t)
+
+  let name () = "bitfield"
+  type int_t = Ints_t.t
+
+  (* the bitfield is represented as a tuple of two bitmasks zs and os. *)
+  (* zs is the mask of all bits that may be zero, os is the mask of all bits that may be one *)
+  (* Example: (zs, os) = (−1, 7) = (...1111,...0111) =...0??? represents the bitmask, *)
+  (* where the last three bits are unknown, and all other bits are known to be 0 *)
+  type t = (Ints_t.t * Ints_t.t) [@@deriving eq, ord, hash]
+
+  module BArith = BitfieldArith (Ints_t)
+
+  (* top = all bis are unknown*)
+  let top () = (BArith.one_mask, BArith.one_mask)
+
+  (* bot = all bits are invalid *)
+  let bot () = (BArith.zero_mask, BArith.zero_mask)
+
+  let top_of ik = 
+    if GoblintCil.isSigned ik then top () 
+    else (BArith.one_mask, Ints_t.of_bigint (snd (Size.range ik)))
+
+  let bot_of ik = bot ()
+
+  let to_pretty_bits (z,o) = 
+    let known_bitmask = BArith.bits_known (z,o) in
+    let invalid_bitmask = BArith.bits_invalid (z,o) in
+
+    (* converts the (zs,os) mask representation to a human readable string of the form 0b(0|1|?|⊥)...(0|1|?|⊥)+. *)
+    (* Example: 0b0...01? should mean that the last bit is unknown, while all other bits are exactly known *)
+    (* The ... (dots) are used to indicate an infinte repetition of the previous bit *)
+    let rec create_pretty_bf_string o_mask z_mask known_bitmask invalid_bitmask acc =
+      let current_bit_known = (known_bitmask &: Ints_t.one) = Ints_t.one in
+      let current_bit_invalid = (invalid_bitmask &: Ints_t.one) = Ints_t.one in
+      let bit_value = o_mask &: Ints_t.one in
+      let bit =
+        if current_bit_invalid then "⊥"
+        else if not current_bit_known then "?"
+        else Ints_t.to_string bit_value 
+      in
+      if (o_mask = Ints_t.of_int (-1) || o_mask = Ints_t.zero) && (z_mask = Ints_t.of_int (-1) || z_mask = Ints_t.zero) then
+        let prefix = bit ^ "..." ^ bit in
+        prefix ^ acc
+      else
+        create_pretty_bf_string (o_mask >>: 1) (z_mask >>: 1) (known_bitmask >>: 1) (invalid_bitmask >>: 1) (bit ^ acc)
+    in
+    "0b" ^ create_pretty_bf_string o z known_bitmask invalid_bitmask ""
+
+  let show t = 
+    if t = bot () then "⊥" else
+      let (z,o) = t in
+      if GobConfig.get_bool "dbg.full-output" then
+        Printf.sprintf "{%s, (zs:%s, os:%s)}" (to_pretty_bits t) (Ints_t.to_string z) (Ints_t.to_string o)
+      else
+        to_pretty_bits t
+
+  include Std (struct type nonrec t = t let name = name let top_of = top_of let bot_of = bot_of let show = show let equal = equal end)
+
+  let maximal (z,o) =     
+    if (z <: Ints_t.zero) <> (o <: Ints_t.zero) then Some o
+    else None
+
+  let minimal (z,o) =     
+    if (z <: Ints_t.zero) <> (o <: Ints_t.zero) then Some (!:z)
+    else None
+
+  (* setting all bits outside of the ik range to the correct sign bit *)
+  let wrap ik (z,o) = 
+    let (min_ik, max_ik) = Size.range ik in
+    if GoblintCil.isSigned ik then
+      let newz = (z &: (Ints_t.of_bigint max_ik)) |: ((Ints_t.of_bigint min_ik) *: (BArith.nth_bit z (Size.bit ik - 1))) in
+      let newo = (o &: (Ints_t.of_bigint max_ik)) |: ((Ints_t.of_bigint min_ik) *: (BArith.nth_bit o (Size.bit ik - 1))) in
+      (newz,newo)
+    else
+      let newz = z |: !:(Ints_t.of_bigint max_ik) in
+      let newo = o &: (Ints_t.of_bigint max_ik) in
+      (newz,newo)
+
+  let norm ?(suppress_ovwarn=false) ?(ov=false) ik (z,o) = 
+    if BArith.is_invalid (z,o) then 
+      bot ()
+    else         
+      let new_bitfield = wrap ik (z,o) in     
+      if not ov || should_wrap ik then
+        new_bitfield
+      else 
+        top_of ik
+
+  let cast_to ?(suppress_ovwarn=false) ?torg ?(no_ov=false) ik (z,o) = 
+    let (min_ik, max_ik) = Size.range ik in 
+    let (underflow, overflow) = match torg with   
+      | None -> (false, false) (* ik does not change *)
+      | Some (GoblintCil.Cil.TInt (old_ik, _)) ->         
+        let underflow = Z.compare (BArith.min old_ik (z,o)) min_ik < 0 in 
+        let overflow = Z.compare max_ik (BArith.max old_ik (z,o)) < 0 in 
+        (underflow, overflow)
+      | _ -> 
+        let isPos = z <: Ints_t.zero in 
+        let isNeg = o <: Ints_t.zero in
+        let underflow = if GoblintCil.isSigned ik then (((Ints_t.of_bigint min_ik) &: z) <>: Ints_t.zero) && isNeg else isNeg in
+        let overflow = (((!:(Ints_t.of_bigint max_ik)) &: o) <>: Ints_t.zero) && isPos in
+        (underflow, overflow)
+    in
+    let overflow_info = if suppress_ovwarn then {underflow=false; overflow=false} else {underflow=underflow; overflow=overflow} in      
+    (norm ~suppress_ovwarn:(suppress_ovwarn) ~ov:(underflow || overflow) ik (z,o), overflow_info)
+
+  let join ik b1 b2 = norm ik @@ (BArith.join b1 b2)
+
+  let meet ik x y = norm ik @@ (BArith.meet x y)
+
+  let leq (z1,o1) (z2,o2) =
+    (* If a bit can have a certain value in parameter 1, it must be able to have the same value in parameter 2. *)
+    (* This corresponds to bitwise implication. *)
+    let implies a b = Ints_t.equal (!:a |: b) BArith.one_mask in
+    implies z1 z2 && implies o1 o2
+
+  let widen ik x y = norm ik @@ BArith.widen x y
+
+  let narrow ik x y = meet ik x y
+
+  let of_int ik (x: int_t) = 
+    let (min_ik, max_ik) = Size.range ik in 
+    let y = Ints_t.to_bigint x in 
+    let underflow = Z.compare y min_ik < 0 in 
+    let overflow = Z.compare max_ik y < 0 in 
+    let overflow_info = {underflow=underflow; overflow=overflow} in    
+    (norm ~ov:(underflow || overflow) ik (BArith.of_int x), overflow_info) 
+
+  let to_int (z,o) = if is_bot (z,o) then None else
+    if BArith.is_const (z,o) then Some o
+    else None
+
+  let equal_to i bf = 
+    if BArith.of_int i = bf then `Eq
+    else if leq (BArith.of_int i) bf then `Top
+    else `Neq
+
+  (* Conversions *)
+
+  type bit_status = Zero | One | Top
+
+  let of_interval ?(suppress_ovwarn=false) ik (x,y) =
+    let (min_ik, max_ik) = Size.range ik in
+    let startv = Ints_t.max x (Ints_t.of_bigint min_ik) in
+    let endv= Ints_t.min y (Ints_t.of_bigint max_ik) in
+
+    (* constructs a bitfield of the interval: for each bit check if the smallest number that is greater than startv and has the bit flipped is still in the interval *)
+    (* If the flipped value is still in the interval, the bit can be 0 or 1 which means it must be described as top, otherwise the bit cant change and is the same as in startv *)
+    (* Runtime: O(bits) *)
+    let rec construct_bitfield pos (acc_z, acc_o) =
+      if pos < 0 then (acc_z, acc_o)
+      else
+        let position_mask = Ints_t.shift_left Ints_t.one pos in
+        let mask = Ints_t.sub position_mask Ints_t.one in
+        let remainder = Ints_t.logand startv mask in
+
+        let smallest_number_with_flipped_bit = Ints_t.add (Ints_t.sub startv remainder) position_mask in
+
+        let bit_status =
+          if Ints_t.compare smallest_number_with_flipped_bit endv <= 0 then
+            Top
+          else 
+            (* bit can't change inside the interval -> it's the same as in startv *)
+          if Ints_t.equal (Ints_t.logand (Ints_t.shift_right startv pos) Ints_t.one) Ints_t.one then
+            One
+          else
+            Zero
+        in
+
+        (* set bit in masks depending on bit_status *)
+        let new_acc = 
+          match bit_status with
+          | Top-> (Ints_t.logor position_mask acc_z, Ints_t.logor position_mask acc_o)
+          | One-> (Ints_t.logand (Ints_t.lognot position_mask) acc_z, Ints_t.logor position_mask acc_o)
+          | Zero-> (Ints_t.logor position_mask acc_z, Ints_t.logand (Ints_t.lognot position_mask) acc_o)
+        in 
+        construct_bitfield (pos - 1) new_acc
+    in      
+    let result = construct_bitfield (Size.bit ik - 1) (bot()) in
+    let casted = (Ints_t.of_bigint (Size.cast ik ((Ints_t.to_bigint (fst result)))), Ints_t.of_bigint (Size.cast ik ((Ints_t.to_bigint (snd result))))) 
+    in (wrap ik casted, {underflow=false; overflow=false})
+
+  let of_bool _ik = function true -> BArith.one | false -> BArith.zero
+
+  let to_bool d =
+    if not (leq BArith.zero d) then Some true
+    else if equal d BArith.zero then Some false
+    else None
+
+  let of_bitfield ik x = norm ik x
+
+  let to_bitfield ik x = norm ik x
+
+  let of_congruence ik (c,m) = 
+    if m = Ints_t.zero then 
+      of_int ik c |> fst
+    else if BArith.is_power_of_two m && Ints_t.one <>: m then 
+      let mod_mask = !:(m -: Ints_t.one) in 
+      let z = mod_mask |: (!: c) in 
+      let o = mod_mask |: c in 
+      norm ik (z,o)
+    else top_of ik
+
+  (* Logic *)
+
+  let log1 f ik i1 = match to_bool i1 with
+    | None -> top_of ik
+    | Some x -> of_bool ik (f x)
+
+  let log2 f ~annihilator ik i1 i2 = match to_bool i1, to_bool i2 with
+    | Some x, _ when x = annihilator -> of_bool ik annihilator
+    | _, Some y when y = annihilator -> of_bool ik annihilator
+    | Some x, Some y -> of_bool ik (f x y)
+    | _              -> top_of ik
+
+  let c_logor = log2 (||) ~annihilator:true
+
+  let c_logand = log2 (&&) ~annihilator:false
+
+  let c_lognot ik i1 = log1 not ik i1
+
+
+  (* Bitwise *)
+
+  let logxor ik i1 i2 = BArith.logxor i1 i2 |> norm ik
+
+  let logand ik i1 i2 = BArith.logand i1 i2 |> norm ik
+
+  let logor  ik i1 i2 = BArith.logor i1 i2 |> norm ik
+
+  let lognot ik i1 = BArith.lognot i1 |> norm ik
+
+  let top_on_undefined_shift ?(is_shift_left=false) ik a b do_shift =
+    let no_ov = {underflow=false; overflow=false} in
+    if BArith.exceeds_bit_width_of GoblintCil.ILongLong b || BArith.equals_bit_width_of GoblintCil.ILongLong b then
+      (top_of ik,
+       match is_shift_left, GoblintCil.isSigned ik && BArith.has_neg_values ik a with
+       | true, false -> {underflow=false; overflow=true}
+       | true, true when BArith.has_only_neg_values ik a -> {underflow=true; overflow=false}
+       | true, true -> {underflow=true; overflow=true}
+       | _ -> no_ov
+      )
+    else
+    if GoblintCil.isSigned ik && BArith.has_only_neg_values ik b then (top_of ik, no_ov) else do_shift ()
+
+  let shift_right ik a b = match is_bot a, is_bot b with
+    | true, true -> bot_of ik, {underflow=false; overflow=false}
+    | true,_ | _,true -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s >> %s" (show a) (show b)))
+    | _ ->
+      top_on_undefined_shift ik a b @@ fun () ->
+      (norm ik (BArith.shift_right ik a b), {underflow=false; overflow=false})
+
+  let shift_left ik a b = match is_bot a, is_bot b with
+    | true, true -> bot_of ik, {underflow=false; overflow=false}
+    | true,_ | _,true -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s << %s" (show a) (show b)))
+    | _ ->
+      top_on_undefined_shift ~is_shift_left:true ik a b @@ fun () ->
+      let max_shift = if Z.fits_int (BArith.max ik b) then Z.to_int (BArith.max ik b) else Int.max_int in 
+      let (min_ik, max_ik) = Size.range ik in 
+      let min_res = if max_shift < 0 then Z.pred min_ik else Z.shift_left (BArith.min ik a) max_shift in 
+      let max_res = if max_shift < 0 then Z.succ max_ik else Z.shift_left (BArith.max ik a) max_shift in 
+      let underflow = Z.compare min_res min_ik < 0 in 
+      let overflow = Z.compare max_ik max_res < 0 in 
+      (norm ~ov:(underflow || overflow) ik (BArith.shift_left ik a b), {underflow=underflow; overflow=overflow})
+
+  (* Arith *)
+
+  (*
+  add, sub and mul based on the paper 
+  "Sound, Precise, and Fast Abstract Interpretation with Tristate Numbers"
+  of Vishwanathan et al.
+  https://doi.org/10.1109/CGO53902.2022.9741267 
+  *)
+
+  let add_paper pv pm qv qm = 
+    let sv = pv +: qv in
+    let sm = pm +: qm in
+    let sigma = sv +: sm in
+    let chi = sigma ^: sv in
+    let mu = pm |: qm |: chi in
+    let rv = sv &: !:mu in
+    let rm = mu in 
+    (rv, rm)
+
+  let add ?no_ov ik (z1, o1) (z2, o2) =
+    let pv = o1 &: !:z1 in
+    let pm = o1 &: z1 in
+    let qv = o2 &: !:z2 in
+    let qm = o2 &: z2 in
+    let (rv, rm) = add_paper pv pm qv qm in 
+    let o3 = rv |: rm in 
+    let z3 = !:rv |: rm in
+    let (max1, max2) = (BArith.max ik (z1, o1), BArith.max ik (z2, o2)) in 
+    let (min1, min2) = (BArith.min ik (z1, o1), BArith.min ik (z2, o2)) in 
+    let (min_ik, max_ik) = Size.range ik in 
+    let underflow = Z.compare (Z.add min1 min2) min_ik < 0 in 
+    let overflow = Z.compare max_ik (Z.add max1 max2) < 0 in 
+    (norm ~ov:(overflow || underflow) ik (z3,o3), {underflow=underflow; overflow=overflow})
+
+  let sub ?no_ov ik (z1, o1) (z2, o2) =
+    let pv = o1 &: !:z1 in
+    let pm = o1 &: z1 in
+    let qv = o2 &: !:z2 in
+    let qm = o2 &: z2 in
+    let dv = pv -: qv in
+    let alpha = dv +: pm in
+    let beta = dv -: qm in
+    let chi = alpha ^: beta in
+    let mu = pm |: qm |: chi in
+    let rv = dv &: !:mu in
+    let rm = mu in 
+    let o3 = rv |: rm in 
+    let z3 = !:rv |: rm in   
+    let (max1, max2) = (BArith.max ik (z1, o1), BArith.max ik (z2, o2)) in 
+    let (min1, min2) = (BArith.min ik (z1, o1), BArith.min ik (z2, o2)) in 
+    let (min_ik, max_ik) = Size.range ik in 
+    let underflow = Z.compare (Z.sub min1 max2) min_ik < 0 in 
+    let overflow = Z.compare max_ik (Z.sub max1 min2) < 0 in 
+    (norm ~ov:(overflow || underflow) ik (z3, o3), {underflow=underflow; overflow=overflow})
+
+  let neg ?no_ov ik x =
+    if M.tracing then M.trace "bitfield" "neg";
+    sub ?no_ov ik BArith.zero x
+
+  let mul ?no_ov ik (z1, o1) (z2, o2) =
+    let pm = ref (z1 &: o1) in
+    let pv = ref (o1 &: !:z1) in 
+    let qm = ref (z2 &: o2) in
+    let qv = ref (o2 &: !:z2) in 
+    let accv = ref BArith.zero_mask in 
+    let accm = ref BArith.zero_mask in 
+    let size = if GoblintCil.isSigned ik then Size.bit ik - 1 else Size.bit ik in
+    let bitmask = Ints_t.of_bigint (fst (Size.range ik)) in
+    let signBitUndef1 = z1 &: o1 &: bitmask in
+    let signBitUndef2 = z2 &: o2 &: bitmask in
+    let signBitUndef = signBitUndef1 |: signBitUndef2 in
+    let signBitDefO = (o1 ^: o2) &: bitmask in
+    let signBitDefZ = !:(o1 ^: o2) &: bitmask in
+    for _ = size downto 0 do 
+      (if !pm &: Ints_t.one == Ints_t.one then 
+         accm := snd(add_paper Ints_t.zero !accm Ints_t.zero (!qv |: !qm))
+       else if !pv &: Ints_t.one == Ints_t.one then
+         accv := fst(add_paper !accv Ints_t.zero !qv Ints_t.zero);
+       accm := snd(add_paper Ints_t.zero !accm Ints_t.zero !qm));
+
+      pv := !pv >>: 1;
+      pm := !pm >>: 1;
+      qv := !qv <<: 1;
+      qm := !qm <<: 1;
+    done; 
+    let (rv, rm) = add_paper !accv Ints_t.zero Ints_t.zero !accm in 
+    let o3 = rv |: rm in 
+    let z3 = !:rv |: rm in
+    let (max1, max2) = (BArith.max ik (z1, o1), BArith.max ik (z2, o2)) in 
+    let (min1, min2) = (BArith.min ik (z1, o1), BArith.min ik (z2, o2)) in 
+    let (min_ik, max_ik) = Size.range ik in 
+    let min_res = Z.min (Z.mul min1 max2) (Z.mul max1 min2) in 
+    let max_res = Z.max (Z.mul min1 min2) (Z.mul max1 max2) in 
+    let underflow = Z.compare min_res min_ik < 0 in 
+    let overflow = Z.compare max_ik max_res < 0 in  
+    let z3 = if GoblintCil.isSigned ik then signBitUndef |: signBitDefZ |: z3 else z3 in 
+    let o3 = if GoblintCil.isSigned ik then signBitUndef |: signBitDefO |: o3 else o3 in 
+    (norm ~ov:(overflow || underflow) ik (z3, o3), {underflow=underflow; overflow=overflow})
+
+
+  let div ?no_ov ik (z1, o1) (z2, o2) =
+    if o2 = Ints_t.zero then 
+      (top_of ik, {underflow=false; overflow=false}) 
+    else
+      let res = 
+        if BArith.is_const (z1, o1) && BArith.is_const (z2, o2) then 
+          (let tmp = o1 /: o2 in (!:tmp, tmp)) 
+        else if BArith.is_const (z2, o2) && BArith.is_power_of_two o2 then           
+          let exp = Z.trailing_zeros (Ints_t.to_bigint o2) in 
+          (z1 >>: exp, o1 >>: exp)
+        else 
+          top_of ik 
+      in
+      let min_ik = Size.range ik |> fst |> Ints_t.of_bigint in    
+      (* div can only overflow for divisions like -(INT_MIN) / (-1) *)   
+      let overflow = GoblintCil.isSigned ik && leq (!: min_ik, min_ik) (z1, o1) && leq (Ints_t.zero, BArith.one_mask) (z2, o2) in
+      (norm ~ov:overflow ik res, {underflow=false; overflow=overflow})
+
+  let rem ik (z1, o1) (z2, o2) = 
+    if o2 = Ints_t.zero then top_of ik else
+    if BArith.is_const (z1, o1) && BArith.is_const (z2, o2) then
+      let tmp = o1 %: o2 in (!:tmp, tmp)       
+    else if BArith.is_const (z2, o2) && BArith.is_power_of_two o2 then 
+      let mask = Ints_t.sub o2 Ints_t.one in
+      let newz = Ints_t.logor z1 (Ints_t.lognot mask) in
+      let newo = Ints_t.logand o1 mask in
+      norm ik (newz, newo)
+    else 
+      top_of ik
+
+  let eq ik x y =
+    if Z.compare (BArith.max ik x) (BArith.min ik y) <= 0 && Z.compare (BArith.min ik x) (BArith.max ik y) >= 0 then 
+      of_bool ik true 
+    else if Z.compare (BArith.min ik x) (BArith.max ik y) > 0 || Z.compare (BArith.max ik x) (BArith.min ik y) < 0 then 
+      of_bool ik false 
+    else 
+      BArith.top_bool
+
+  let ne ik x y = match eq ik x y with
+    | t when t = of_bool ik true -> of_bool ik false
+    | t when t = of_bool ik false -> of_bool ik true
+    | _ -> BArith.top_bool
+
+  let le ik x y = 
+    if Z.compare (BArith.max ik x) (BArith.min ik y) <= 0 then 
+      of_bool ik true 
+    else if Z.compare (BArith.min ik x) (BArith.max ik y) > 0 then 
+      of_bool ik false 
+    else 
+      BArith.top_bool
+
+  let ge ik x y = le ik y x
+
+  let lt ik x y = 
+    if Z.compare (BArith.max ik x) (BArith.min ik y) < 0 then 
+      of_bool ik true 
+    else if Z.compare (BArith.min ik x) (BArith.max ik y) >= 0 then 
+      of_bool ik false 
+    else 
+      BArith.top_bool
+
+  let gt ik x y = lt ik y x
+
+  (* Invariant *)
+
+  let invariant_ikind e ik (z,o) = 
+    if z =: BArith.one_mask && o =: BArith.one_mask then 
+      Invariant.top ()
+    else if  BArith.is_invalid (z,o) then 
+      Invariant.none
+    else      
+      let open GoblintCil.Cil in
+      let def0 = z &: (!: o) in       
+      let def1 = o &: (!: z) in 
+      let (def0, def1) = BatTuple.Tuple2.mapn (kintegerCilint ik) (Ints_t.to_bigint def0, Ints_t.to_bigint def1) in
+      let exp0 = Invariant.of_exp (BinOp (Eq, (BinOp (BAnd, (UnOp (BNot, e, TInt(ik,[]))), def0, TInt(ik,[]))), def0, intType)) in 
+      let exp1 = Invariant.of_exp (BinOp (Eq, (BinOp (BAnd, e, def1, TInt(ik,[]))), def1, intType)) in 
+      Invariant.meet exp0 exp1
+
+  let starting ?(suppress_ovwarn=false) ik n = 
+    let (min_ik, max_ik) = Size.range ik in
+    of_interval ~suppress_ovwarn ik (n, Ints_t.of_bigint max_ik) 
+
+  let ending ?(suppress_ovwarn=false) ik n =
+    let (min_ik, max_ik) = Size.range ik in
+    of_interval ~suppress_ovwarn ik (Ints_t.of_bigint min_ik, n)
+
+  (* Refinements *)
+
+  let refine_with_congruence ik bf ((cong) : (int_t * int_t ) option) : t =
+    match cong with
+    | Some (c, m) -> meet ik bf (of_congruence ik (c,m))
+    | _ -> norm ik bf
+
+  let refine_with_interval ik t itv = 
+    match itv with
+    | None -> norm ik t
+    | Some (l, u) -> meet ik t (of_interval ik (l, u) |> fst)  
+
+  let refine_with_bitfield ik x y = meet ik x y
+
+  let refine_with_excl_list ik t (excl : (int_t list * (int64 * int64)) option) : t = norm ik t
+
+  let refine_with_incl_list ik t (incl : (int_t list) option) : t =
+    let joined =match incl with
+      | None -> top_of ik
+      | Some ls -> 
+        List.fold_left (fun acc i -> BArith.join acc (BArith.of_int i)) (bot_of ik) ls
+    in
+    meet ik t joined
+
+
+  let refine_bor (az, ao) (bz, bo) (cz, co) =     
+    let cDef0 = cz &: (!: co) in 
+    let cDef1 = co &: (!: cz) in         
+    let aDef0 = az &: (!: ao) in   
+    let bDef0 = bz &: (!: bo) in
+    (* if a bit is definitely 0 in b and definitely 1 in c, the same bit must be definitely 1 in a *)
+    (* example (with t for top): (tttt) | (t010) = (1011) *)
+    (* we can refine (tttt) to (ttt1) because the lowest 1 of c must come from a *)
+    let az = az &: (!: (bDef0 &: cDef1)) in 
+    let bz = bz &: (!: (aDef0 &: cDef1)) in
+    (* if a bit is definitely 0 in c, the same bit must be definitely 0 in a too *)
+    (* example (with t for top): (ttt1) | (t010) = (1011) *)
+    (* we can refine (ttt1) to (t0t1) because the second bit of a cannot be a 1 *)
+    let ao = ao &: (!: cDef0) in     
+    let bo = bo &: (!: cDef0) in 
+    ((az, ao), (bz, bo))
+
+  let refine_band (az, ao) (bz, bo) (cz, co) = 
+    let cDef0 = cz &: (!: co) in 
+    let cDef1 = co &: (!: cz) in 
+    let aDef1 = ao &: (!: az) in
+    let bDef1 = bo &: (!: bz) in
+    (* if a bit is definitely 1 in c, the same bit must be definitely 1 in a too *)
+    (* example (with t for top): (tttt) & (t010) = (1011) *)
+    (* we can refine (tttt) to (1t11) *)
+    let az = az &: (!: cDef1) in 
+    let bz = bz &: (!: cDef1) in 
+    (* if a bit is definitely 1 in b and definitely 0 in c, the same bit must be definitely 0 in a *)
+    (* example (with t for top): (tttt) & (t110) = (1011) *)
+    (* we can refine (tttt) to (t0tt) *)
+    let ao = ao &: (!: (bDef1 &: cDef0)) in     
+    let bo = bo &: (!: (aDef1 &: cDef0)) in
+    ((az, ao), (bz, bo))
+
+  let arbitrary ik = 
+    let open QCheck.Iter in
+    let int_arb = QCheck.map ~rev:Ints_t.to_int64 Ints_t.of_int64 GobQCheck.Arbitrary.int64 in
+    let pair_arb = QCheck.pair int_arb int_arb in
+    let shrink bf =
+      (GobQCheck.shrink pair_arb bf 
+       >|= (fun (zs, os) -> 
+           (* Shrinking works by setting some unsure bits to 0. This reduces the number of possible values, and makes the decimal representation of the masks smaller *)
+           let random_mask = Ints_t.of_int64 (Random.int64 (Int64.of_int (Size.bits ik |> snd))) in
+           let unsure_bitmask= zs &: os in
+           let pruned_bits= unsure_bitmask &: random_mask in
+           (* set the pruned bits to 1 in the zs-mask and to 0 in the os-mask *)
+           let flipped_z = zs |: pruned_bits in
+           let flipped_o = os &: !:pruned_bits in
+           norm ik (flipped_z, flipped_o)
+         ))
+    in
+    QCheck.(set_shrink shrink @@ set_print show @@ map (fun (i1,i2) -> norm ik (i1,i2)) pair_arb)
+
+  let project ik p t = t
+
+end
+
+module Bitfield = BitfieldFunctor (IntOps.BigIntOps)
\ No newline at end of file
diff --git a/src/cdomain/value/cdomains/int/congruenceDomain.ml b/src/cdomain/value/cdomains/int/congruenceDomain.ml
index 003e33a624..e61399210c 100644
--- a/src/cdomain/value/cdomains/int/congruenceDomain.ml
+++ b/src/cdomain/value/cdomains/int/congruenceDomain.ml
@@ -139,6 +139,23 @@ struct
 
   let of_congruence ik (c,m) = normalize ik @@ Some(c,m)
 
+  let of_bitfield ik (z,o) = 
+    match BitfieldDomain.Bitfield.to_int (z,o) with
+    | Some x -> normalize ik (Some (x, Z.zero))
+    | _ ->
+      (* get posiiton of first top bit *)
+      let tl_zeros = Z.trailing_zeros (Z.logand z o) in 
+      let ik_bits = Size.bit ik in 
+      let m = if tl_zeros > ik_bits then Z.one else Z.pow Z.one tl_zeros in 
+      let c = Z.logand o (m -: Z.one) in 
+      normalize ik (Some (c, m))
+
+  let to_bitfield ik x = 
+    let x = normalize ik x in 
+    match x with 
+    | None -> (Z.zero, Z.zero) 
+    | Some (c,m) -> BitfieldDomain.Bitfield.of_congruence ik (c,m)
+
   let maximal t = match t with
     | Some (x, y) when y =: Z.zero -> Some x
     | _ -> None
@@ -434,7 +451,6 @@ struct
 
   let gt ik x y = comparison ik (>:) x y
 
-
   let gt ik x y =
     let res = gt ik x y in
     if M.tracing then  M.trace "congruence" "greater than : %a %a -> %a " pretty x pretty y pretty res;
@@ -489,7 +505,13 @@ struct
     refn
 
   let refine_with_congruence ik a b = meet ik a b
+
+  let refine_with_bitfield ik a (z,o) = 
+    let a = normalize ik a in 
+    meet ik a (of_bitfield ik (z,o))
+
   let refine_with_excl_list ik a b = a
+
   let refine_with_incl_list ik a b = a
 
   let project ik p t = t
diff --git a/src/cdomain/value/cdomains/int/defExcDomain.ml b/src/cdomain/value/cdomains/int/defExcDomain.ml
index 89e4b399aa..467afe338b 100644
--- a/src/cdomain/value/cdomains/int/defExcDomain.ml
+++ b/src/cdomain/value/cdomains/int/defExcDomain.ml
@@ -299,6 +299,17 @@ struct
       let ex = if Z.gt x Z.zero || Z.lt y Z.zero then S.singleton Z.zero else  S.empty () in
       norm ik @@ (`Excluded (ex, r))
 
+  let to_bitfield ik x = 
+    match x with 
+    | `Definite c -> (Z.lognot c, c) 
+    | _ when Cil.isSigned ik -> 
+      let one_mask = Z.lognot Z.zero in 
+      (one_mask, one_mask)
+    | _ -> 
+      let one_mask = Z.lognot Z.zero in 
+      let ik_mask = snd (Size.range ik) in 
+      (one_mask, ik_mask)
+
   let starting ?(suppress_ovwarn=false) ikind x =
     let _,u_ik = Size.range ikind in
     of_interval ~suppress_ovwarn ikind (x, u_ik)
@@ -530,6 +541,14 @@ struct
     ] (* S TODO: decide frequencies *)
 
   let refine_with_congruence ik a b = a
+
+  let refine_with_bitfield ik x (z,o) = 
+    match BitfieldDomain.Bitfield.to_int (z,o) with 
+    | Some y ->
+      meet ik x (`Definite y)
+    | _ ->
+      x
+
   let refine_with_interval ik a b = match a, b with
     | x, Some(i) -> meet ik x (of_interval ik i)
     | _ -> a
diff --git a/src/cdomain/value/cdomains/int/enumsDomain.ml b/src/cdomain/value/cdomains/int/enumsDomain.ml
index e530c16f89..ac025c1a56 100644
--- a/src/cdomain/value/cdomains/int/enumsDomain.ml
+++ b/src/cdomain/value/cdomains/int/enumsDomain.ml
@@ -250,6 +250,19 @@ module Enums : S with type int_t = Z.t = struct
   let is_excl_list = BatOption.is_some % to_excl_list
   let to_incl_list = function Inc s when not (BISet.is_empty s) -> Some (BISet.elements s) | _ -> None
 
+  let to_bitfield ik x = 
+    let ik_mask = snd (Size.range ik) in 
+    let one_mask = Z.lognot Z.zero in
+    match x with 
+    | Inc i when BISet.is_empty i -> (Z.zero, Z.zero) 
+    | Inc i when BISet.is_singleton i ->       
+      let o = BISet.choose i in 
+      let o = if Cil.isSigned ik then o else Z.logand ik_mask o in 
+      (Z.lognot o, o) 
+    | Inc i -> BISet.fold (fun o (az, ao) -> (Z.logor (Z.lognot o) az, Z.logor (if Cil.isSigned ik then o else Z.logand ik_mask o) ao)) i (Z.zero, Z.zero) 
+    | _ when Cil.isSigned ik -> (one_mask, one_mask)
+    | _ -> (one_mask, ik_mask)
+
   let starting ?(suppress_ovwarn=false) ikind x =
     let _,u_ik = Size.range ikind in
     of_interval ~suppress_ovwarn ikind (x, u_ik)
@@ -362,6 +375,13 @@ module Enums : S with type int_t = Z.t = struct
     | Inc e, Some (c, m) -> Inc (BISet.filter (contains c m) e)
     | _ -> a
 
+  let refine_with_bitfield ik x (z,o) =
+    match x, BitfieldDomain.Bitfield.to_int (z,o) with 
+    | Inc _, Some y ->     
+      meet ik x (Inc (BISet.singleton y))
+    | _ ->
+      x
+
   let refine_with_interval ik a b =
     match a, b with
     | Inc _, None -> bot_of ik
diff --git a/src/cdomain/value/cdomains/int/intDomTuple.ml b/src/cdomain/value/cdomains/int/intDomTuple.ml
index faf251423c..bd46e8944c 100644
--- a/src/cdomain/value/cdomains/int/intDomTuple.ml
+++ b/src/cdomain/value/cdomains/int/intDomTuple.ml
@@ -4,11 +4,11 @@ open IntervalSetDomain
 open DefExcDomain
 open EnumsDomain
 open CongruenceDomain
+open BitfieldDomain
 open GoblintCil
 open Pretty
 open PrecisionUtil
 
-
 (* The old IntDomList had too much boilerplate since we had to edit every function in S when adding a new domain. With the following, we only have to edit the places where fn are applied, i.e., create, mapp, map, map2. You can search for I3 below to see where you need to extend. *)
 (* discussion: https://github.com/goblint/analyzer/pull/188#issuecomment-818928540 *)
 module IntDomTupleImpl = struct
@@ -21,15 +21,17 @@ module IntDomTupleImpl = struct
   module I3 = SOverflowLifter (Enums)
   module I4 = SOverflowLifter (Congruence)
   module I5 = IntervalSetFunctor (IntOps.BigIntOps)
+  module I6 = BitfieldFunctor (IntOps.BigIntOps)
 
-  type t = I1.t option * I2.t option * I3.t option * I4.t option * I5.t option
+  type t = I1.t option * I2.t option * I3.t option * I4.t option * I5.t option * I6.t option
   [@@deriving eq, ord, hash]
 
   let name () = "intdomtuple"
 
   (* The Interval domain can lead to too many contexts for recursive functions (top is [min,max]), but we don't want to drop all ints as with `ana.base.context.int`. TODO better solution? *)
-  let no_interval = Tuple5.map2 (const None)
-  let no_intervalSet = Tuple5.map5 (const None)
+  let no_interval = GobTuple.Tuple6.map2 (const None)
+  let no_intervalSet = GobTuple.Tuple6.map5 (const None)
+  let no_bitfield = GobTuple.Tuple6.map6 (const None)
 
   type 'a m = (module SOverflow with type t = 'a)
   type 'a m2 = (module SOverflow with type t = 'a and type int_t = int_t )
@@ -47,14 +49,14 @@ module IntDomTupleImpl = struct
   type poly2 = {f2: 'a. 'a m -> ?no_ov:bool -> 'a -> 'a -> 'a} [@@unboxed]
   type poly2_ovc = {f2_ovc: 'a. 'a m -> ?no_ov:bool -> 'a -> 'a -> 'a * overflow_info } [@@unboxed]
   type 'b poly3 = { f3: 'a. 'a m -> 'a option } [@@unboxed] (* used for projection to given precision *)
-  let create r x ((p1, p2, p3, p4, p5): int_precision) =
+  let create r x ((p1, p2, p3, p4, p5, p6): int_precision) =
     let f b g = if b then Some (g x) else None in
-    f p1 @@ r.fi (module I1), f p2 @@ r.fi (module I2), f p3 @@ r.fi (module I3), f p4 @@ r.fi (module I4), f p5 @@ r.fi (module I5)
+    f p1 @@ r.fi (module I1), f p2 @@ r.fi (module I2), f p3 @@ r.fi (module I3), f p4 @@ r.fi (module I4), f p5 @@ r.fi (module I5), f p6 @@ r.fi (module I6)
   let create r x = (* use where values are introduced *)
     create r x (int_precision_from_node_or_config ())
-  let create2 r x ((p1, p2, p3, p4, p5): int_precision) =
+  let create2 r x ((p1, p2, p3, p4, p5, p6): int_precision) =
     let f b g = if b then Some (g x) else None in
-    f p1 @@ r.fi2 (module I1), f p2 @@ r.fi2 (module I2), f p3 @@ r.fi2 (module I3), f p4 @@ r.fi2 (module I4), f p5 @@ r.fi2 (module I5)
+    f p1 @@ r.fi2 (module I1), f p2 @@ r.fi2 (module I2), f p3 @@ r.fi2 (module I3), f p4 @@ r.fi2 (module I4), f p5 @@ r.fi2 (module I5) , f p6 @@ r.fi2 (module I6)
   let create2 r x = (* use where values are introduced *)
     create2 r x (int_precision_from_node_or_config ())
 
@@ -62,24 +64,26 @@ module IntDomTupleImpl = struct
     | Some(_, {underflow; overflow}) -> not (underflow || overflow)
     | _ -> false
 
-  let check_ov ?(suppress_ovwarn = false) ~cast ik intv intv_set =
-    let no_ov = (no_overflow ik intv) || (no_overflow ik intv_set) in
-    if not no_ov && not suppress_ovwarn && ( BatOption.is_some intv || BatOption.is_some intv_set) then (
+  let check_ov ?(suppress_ovwarn = false) ~cast ik intv intv_set bf = 
+    let no_ov = (no_overflow ik intv) || (no_overflow ik intv_set) || (no_overflow ik bf) in
+    if not no_ov && not suppress_ovwarn && ( BatOption.is_some intv || BatOption.is_some intv_set || BatOption.is_some bf) then (
       let (_,{underflow=underflow_intv; overflow=overflow_intv}) = match intv with None -> (I2.bot (), {underflow= true; overflow = true}) | Some x -> x in
       let (_,{underflow=underflow_intv_set; overflow=overflow_intv_set}) = match intv_set with None -> (I5.bot (), {underflow= true; overflow = true}) | Some x -> x in
-      let underflow = underflow_intv && underflow_intv_set in
-      let overflow = overflow_intv && overflow_intv_set in
+      let (_,{underflow=underflow_bf; overflow=overflow_bf}) = match bf with None -> (I6.bot (), {underflow= true; overflow = true}) | Some x -> x in
+      let underflow = underflow_intv && underflow_intv_set && underflow_bf in
+      let overflow = overflow_intv && overflow_intv_set && overflow_bf in
       set_overflow_flag ~cast ~underflow ~overflow ik;
     );
     no_ov
 
-  let create2_ovc ik r x ((p1, p2, p3, p4, p5): int_precision) =
+  let create2_ovc ik r x ((p1, p2, p3, p4, p5, p6): int_precision) =
     let f b g = if b then Some (g x) else None in
     let map x = Option.map fst x in
     let intv =  f p2 @@ r.fi2_ovc (module I2) in
     let intv_set = f p5 @@ r.fi2_ovc (module I5) in
-    ignore (check_ov ~cast:false ik intv intv_set);
-    map @@ f p1 @@ r.fi2_ovc (module I1), map @@ f p2 @@ r.fi2_ovc (module I2), map @@ f p3 @@ r.fi2_ovc (module I3), map @@ f p4 @@ r.fi2_ovc (module I4), map @@ f p5 @@ r.fi2_ovc (module I5)
+    let bf = f p6 @@ r.fi2_ovc (module I6) in
+    ignore (check_ov ~cast:false ik intv intv_set bf);
+    map @@ f p1 @@ r.fi2_ovc (module I1), map @@ f p2 @@ r.fi2_ovc (module I2), map @@ f p3 @@ r.fi2_ovc (module I3), map @@ f p4 @@ r.fi2_ovc (module I4), map @@ f p5 @@ r.fi2_ovc (module I5) , map @@ f p6 @@ r.fi2_ovc (module I6)
 
   let create2_ovc ik r x = (* use where values are introduced *)
     create2_ovc ik r x (int_precision_from_node_or_config ())
@@ -88,28 +92,26 @@ module IntDomTupleImpl = struct
   let opt_map2 f ?no_ov =
     curry @@ function Some x, Some y -> Some (f ?no_ov x y) | _ -> None
 
-  let to_list x = Tuple5.enum x |> List.of_enum |> List.filter_map identity (* contains only the values of activated domains *)
+  let to_list x = GobTuple.Tuple6.enum x |> List.of_enum |> List.filter_map identity (* contains only the values of activated domains *)
   let to_list_some x = List.filter_map identity @@ to_list x (* contains only the Some-values of activated domains *)
 
   let exists = function
-    | (Some true, _, _, _, _)
-    | (_, Some true, _, _, _)
-    | (_, _, Some true, _, _)
-    | (_, _, _, Some true, _)
-    | (_, _, _, _, Some true) ->
-      true
-    | _ ->
-      false
+    | (Some true, _, _, _, _,_)
+    | (_, Some true, _, _, _,_)
+    | (_, _, Some true, _, _,_)
+    | (_, _, _, Some true, _,_)
+    | (_, _, _, _, Some true,_) 
+    | (_, _, _, _, _, Some true) -> true 
+    | _ -> false
 
   let for_all = function
-    | (Some false, _, _, _, _)
-    | (_, Some false, _, _, _)
-    | (_, _, Some false, _, _)
-    | (_, _, _, Some false, _)
-    | (_, _, _, _, Some false) ->
-      false
-    | _ ->
-      true
+    | (Some false, _, _, _, _,_)
+    | (_, Some false, _, _, _,_)
+    | (_, _, Some false, _, _,_)
+    | (_, _, _, Some false, _,_)
+    | (_, _, _, _, Some false,_) 
+    | (_, _, _, _, _, Some false) -> false
+    | _ -> true
 
   (* f0: constructors *)
   let top () = create { fi = fun (type a) (module I:SOverflow with type t = a) -> I.top } ()
@@ -123,8 +125,9 @@ module IntDomTupleImpl = struct
   let ending ?(suppress_ovwarn=false) ik = create2_ovc ik { fi2_ovc = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.ending ~suppress_ovwarn ik }
   let of_interval ?(suppress_ovwarn=false) ik = create2_ovc ik { fi2_ovc = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.of_interval ~suppress_ovwarn ik }
   let of_congruence ik = create2 { fi2 = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.of_congruence ik }
+  let of_bitfield ik = create2 { fi2 = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.of_bitfield ik }
 
-  let refine_with_congruence ik ((a, b, c, d, e) : t) (cong : (int_t * int_t) option) : t=
+  let refine_with_congruence ik ((a, b, c, d, e, f) : t) (cong : (int_t * int_t) option) : t=
     let opt f a =
       curry @@ function Some x, y -> Some (f a x y) | _ -> None
     in
@@ -132,9 +135,11 @@ module IntDomTupleImpl = struct
     , opt I2.refine_with_congruence ik b cong
     , opt I3.refine_with_congruence ik c cong
     , opt I4.refine_with_congruence ik d cong
-    , opt I5.refine_with_congruence ik e cong)
+    , opt I5.refine_with_congruence ik e cong
+    , opt I6.refine_with_congruence ik f cong 
+    )
 
-  let refine_with_interval ik (a, b, c, d, e) intv =
+  let refine_with_interval ik (a, b, c, d, e,f) intv =
     let opt f a =
       curry @@ function Some x, y -> Some (f a x y) | _ -> None
     in
@@ -142,9 +147,21 @@ module IntDomTupleImpl = struct
     , opt I2.refine_with_interval ik b intv
     , opt I3.refine_with_interval ik c intv
     , opt I4.refine_with_interval ik d intv
-    , opt I5.refine_with_interval ik e intv )
+    , opt I5.refine_with_interval ik e intv 
+    , opt I6.refine_with_interval ik f intv )
 
-  let refine_with_excl_list ik (a, b, c, d, e) excl =
+  let refine_with_bitfield ik (a, b, c, d, e,f) bf =
+    let opt f a =
+      curry @@ function Some x, y -> Some (f a x y) | _ -> None
+    in
+    ( opt I1.refine_with_bitfield ik a bf
+    , opt I2.refine_with_bitfield ik b bf
+    , opt I3.refine_with_bitfield ik c bf
+    , opt I4.refine_with_bitfield ik d bf
+    , opt I5.refine_with_bitfield ik e bf 
+    , opt I6.refine_with_bitfield ik f bf )
+
+  let refine_with_excl_list ik (a, b, c, d, e,f) excl =
     let opt f a =
       curry @@ function Some x, y -> Some (f a x y) | _ -> None
     in
@@ -152,9 +169,10 @@ module IntDomTupleImpl = struct
     , opt I2.refine_with_excl_list ik b excl
     , opt I3.refine_with_excl_list ik c excl
     , opt I4.refine_with_excl_list ik d excl
-    , opt I5.refine_with_excl_list ik e excl )
+    , opt I5.refine_with_excl_list ik e excl
+    , opt I6.refine_with_excl_list ik f excl )
 
-  let refine_with_incl_list ik (a, b, c, d, e) incl =
+  let refine_with_incl_list ik (a, b, c, d, e,f) incl =
     let opt f a =
       curry @@ function Some x, y -> Some (f a x y) | _ -> None
     in
@@ -162,25 +180,28 @@ module IntDomTupleImpl = struct
     , opt I2.refine_with_incl_list ik b incl
     , opt I3.refine_with_incl_list ik c incl
     , opt I4.refine_with_incl_list ik d incl
-    , opt I5.refine_with_incl_list ik e incl )
+    , opt I5.refine_with_incl_list ik e incl
+    , opt I6.refine_with_incl_list ik f incl )
 
 
-  let mapp r (a, b, c, d, e) =
+  let mapp r (a, b, c, d, e, f) =
     let map = BatOption.map in
     ( map (r.fp (module I1)) a
     , map (r.fp (module I2)) b
     , map (r.fp (module I3)) c
     , map (r.fp (module I4)) d
-    , map (r.fp (module I5)) e)
+    , map (r.fp (module I5)) e
+    , map (r.fp (module I6)) f)
 
 
-  let mapp2 r (a, b, c, d, e) =
+  let mapp2 r (a, b, c, d, e, f) =
     BatOption.
       ( map (r.fp2 (module I1)) a
       , map (r.fp2 (module I2)) b
       , map (r.fp2 (module I3)) c
       , map (r.fp2 (module I4)) d
-      , map (r.fp2 (module I5)) e)
+      , map (r.fp2 (module I5)) e
+      , map (r.fp2 (module I6)) f)
 
 
   (* exists/for_all *)
@@ -189,12 +210,13 @@ module IntDomTupleImpl = struct
   let is_top_of ik = for_all % mapp { fp = fun (type a) (module I:SOverflow with type t = a) -> I.is_top_of ik }
   let is_excl_list = exists % mapp { fp = fun (type a) (module I:SOverflow with type t = a) -> I.is_excl_list }
 
-  let map2p r (xa, xb, xc, xd, xe) (ya, yb, yc, yd, ye) =
+  let map2p r (xa, xb, xc, xd, xe, xf) (ya, yb, yc, yd, ye, yf) =
     ( opt_map2 (r.f2p (module I1)) xa ya
     , opt_map2 (r.f2p (module I2)) xb yb
     , opt_map2 (r.f2p (module I3)) xc yc
     , opt_map2 (r.f2p (module I4)) xd yd
-    , opt_map2 (r.f2p (module I5)) xe ye)
+    , opt_map2 (r.f2p (module I5)) xe ye
+    , opt_map2 (r.f2p (module I6)) xf yf)
 
   (* f2p: binary projections *)
   let (%%) f g x = f % (g x) (* composition for binary function g *)
@@ -222,6 +244,12 @@ module IntDomTupleImpl = struct
     in
     mapp2 { fp2 = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.to_incl_list } x |> flat merge
 
+  let to_bitfield ik x = 
+    let bf_meet (z1,o1) (z2,o2) = (Z.logand z1 z2, Z.logand o1 o2) in 
+    let bf_top = (Z.lognot Z.zero, Z.lognot Z.zero) in 
+    let res_tup = mapp2 { fp2 = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.to_bitfield ik } x
+    in List.fold bf_meet bf_top (to_list res_tup)
+
   let same show x = let xs = to_list_some x in let us = List.unique xs in let n = List.length us in
     if n = 1 then Some (List.hd xs)
     else (
@@ -248,13 +276,14 @@ module IntDomTupleImpl = struct
     let maybe reffun ik domtup dom =
       match dom with Some y -> reffun ik domtup y | _ -> domtup
     in
-    [(fun (a, b, c, d, e) -> refine_with_excl_list ik (a, b, c, d, e) (to_excl_list (a, b, c, d, e)));
-     (fun (a, b, c, d, e) -> refine_with_incl_list ik (a, b, c, d, e) (to_incl_list (a, b, c, d, e)));
-     (fun (a, b, c, d, e) -> maybe refine_with_interval ik (a, b, c, d, e) b); (* TODO: get interval across all domains with minimal and maximal *)
-     (fun (a, b, c, d, e) -> maybe refine_with_congruence ik (a, b, c, d, e) d)]
-
-  let refine ik ((a, b, c, d, e) : t ) : t =
-    let dt = ref (a, b, c, d, e) in
+    [(fun (a, b, c, d, e, f) -> refine_with_excl_list ik (a, b, c, d, e,f) (to_excl_list (a, b, c, d, e,f)));
+     (fun (a, b, c, d, e, f) -> refine_with_incl_list ik (a, b, c, d, e,f) (to_incl_list (a, b, c, d, e,f)));
+     (fun (a, b, c, d, e, f) -> maybe refine_with_interval ik (a, b, c, d, e, f) b); (* TODO: get interval across all domains with minimal and maximal *)
+     (fun (a, b, c, d, e, f) -> maybe refine_with_congruence ik (a, b, c, d, e, f) d);
+     (fun (a, b, c, d, e, f) -> maybe refine_with_bitfield ik (a, b, c, d, e, f) f)]
+
+  let refine ik ((a, b, c, d, e, f) : t ) : t =
+    let dt = ref (a, b, c, d, e, f) in
     (match get_refinement () with
      | "never" -> ()
      | "once" ->
@@ -273,48 +302,54 @@ module IntDomTupleImpl = struct
 
 
   (* map with overflow check *)
-  let mapovc ?(suppress_ovwarn=false) ?(cast=false) ik r (a, b, c, d, e) =
+  let mapovc ?(suppress_ovwarn=false) ?(cast=false) ik r (a, b, c, d, e, f) =
     let map f ?no_ov = function Some x -> Some (f ?no_ov x) | _ -> None  in
     let intv = map (r.f1_ovc (module I2)) b in
     let intv_set = map (r.f1_ovc (module I5)) e in
-    let no_ov = check_ov ~suppress_ovwarn ~cast ik intv intv_set in
+    let bf = map (r.f1_ovc (module I6)) f in
+    let no_ov = check_ov ~suppress_ovwarn ~cast ik intv intv_set bf in
     let no_ov = no_ov || should_ignore_overflow ik in
     refine ik
       ( map (fun ?no_ov x -> r.f1_ovc ?no_ov (module I1) x |> fst) a
       , BatOption.map fst intv
       , map (fun ?no_ov x -> r.f1_ovc ?no_ov (module I3) x |> fst) c
       , map (fun ?no_ov x -> r.f1_ovc ?no_ov (module I4) x |> fst) ~no_ov d
-      , BatOption.map fst intv_set )
+      , BatOption.map fst intv_set 
+      , BatOption.map fst bf)
 
   (* map2 with overflow check *)
-  let map2ovc ?(cast=false) ik r (xa, xb, xc, xd, xe) (ya, yb, yc, yd, ye) =
+  let map2ovc ?(cast=false) ik r (xa, xb, xc, xd, xe, xf) (ya, yb, yc, yd, ye, yf) =
     let intv = opt_map2 (r.f2_ovc (module I2)) xb yb in
     let intv_set = opt_map2 (r.f2_ovc (module I5)) xe ye in
-    let no_ov = check_ov ~cast ik intv intv_set in
+    let bf = opt_map2 (r.f2_ovc (module I6)) xf yf in
+    let no_ov = check_ov ~cast ik intv intv_set bf in
     let no_ov = no_ov || should_ignore_overflow ik in
     refine ik
       ( opt_map2 (fun ?no_ov x y -> r.f2_ovc ?no_ov (module I1) x y |> fst) xa ya
       , BatOption.map fst intv
       , opt_map2 (fun ?no_ov x y -> r.f2_ovc ?no_ov (module I3) x y |> fst) xc yc
       , opt_map2 (fun ?no_ov x y -> r.f2_ovc ?no_ov (module I4) x y |> fst) ~no_ov:no_ov xd yd
-      , BatOption.map fst intv_set )
+      , BatOption.map fst intv_set 
+      , BatOption.map fst bf)
 
-  let map ik r (a, b, c, d, e) =
+  let map ik r (a, b, c, d, e, f) =
     refine ik
       BatOption.
         ( map (r.f1 (module I1)) a
         , map (r.f1 (module I2)) b
         , map (r.f1 (module I3)) c
         , map (r.f1 (module I4)) d
-        , map (r.f1 (module I5)) e)
+        , map (r.f1 (module I5)) e
+        , map (r.f1 (module I6)) f)
 
-  let map2 ?(norefine=false) ik r (xa, xb, xc, xd, xe) (ya, yb, yc, yd, ye) =
+  let map2 ?(norefine=false) ik r (xa, xb, xc, xd, xe, xf) (ya, yb, yc, yd, ye, yf) =
     let r =
       ( opt_map2 (r.f2 (module I1)) xa ya
       , opt_map2 (r.f2 (module I2)) xb yb
       , opt_map2 (r.f2 (module I3)) xc yc
       , opt_map2 (r.f2 (module I4)) xd yd
-      , opt_map2 (r.f2 (module I5)) xe ye)
+      , opt_map2 (r.f2 (module I5)) xe ye
+      , opt_map2 (r.f2 (module I6)) xf yf)
     in
     if norefine then r else refine ik r
 
@@ -334,10 +369,10 @@ module IntDomTupleImpl = struct
 
   (* fp: projections *)
   let equal_to i x =
-    let xs = mapp2 { fp2 = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.equal_to i } x |> Tuple5.enum |> List.of_enum |> List.filter_map identity in
+    let xs = mapp2 { fp2 = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.equal_to i } x |> GobTuple.Tuple6.enum |> List.of_enum |> List.filter_map identity in
     if List.mem `Eq xs then `Eq else
     if List.mem `Neq xs then `Neq else
-      `Top
+      `Top 
 
   let to_bool = same string_of_bool % mapp { fp = fun (type a) (module I:SOverflow with type t = a) -> I.to_bool }
   let minimal = flat (List.max ~cmp:Z.compare) % mapp2 { fp2 = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.minimal }
@@ -354,12 +389,13 @@ module IntDomTupleImpl = struct
   (* `map/opt_map` are used by `project` *)
   let opt_map b f =
     curry @@ function None, true -> f | x, y when y || b -> x | _ -> None
-  let map ~keep r (i1, i2, i3, i4, i5) (b1, b2, b3, b4, b5) =
+  let map ~keep r (i1, i2, i3, i4, i5, i6) (b1, b2, b3, b4, b5, b6) =
     ( opt_map keep (r.f3 (module I1)) i1 b1
     , opt_map keep (r.f3 (module I2)) i2 b2
     , opt_map keep (r.f3 (module I3)) i3 b3
     , opt_map keep (r.f3 (module I4)) i4 b4
-    , opt_map keep (r.f3 (module I5)) i5 b5 )
+    , opt_map keep (r.f3 (module I5)) i5 b5
+    , opt_map keep (r.f3 (module I6)) i6 b6)
 
   (** Project tuple t to precision p
    * We have to deactivate IntDomains after the refinement, since we might
@@ -462,7 +498,7 @@ module IntDomTupleImpl = struct
     | Some v when not (GobConfig.get_bool "dbg.full-output") -> BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" (Z.to_string v)
     | _ -> BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" (show x)
 
-  let invariant_ikind e ik ((_, _, _, x_cong, x_intset) as x) =
+  let invariant_ikind e ik ((_, _, _, x_cong, x_intset, x_bf) as x) =
     (* TODO: do refinement before to ensure incl_list being more precise than intervals, etc (https://github.com/goblint/analyzer/pull/1517#discussion_r1693998515), requires refine functions to actually refine that *)
     let simplify_int fallback =
       match to_int x with
@@ -489,7 +525,8 @@ module IntDomTupleImpl = struct
           IntInvariant.of_interval_opt e ik (min, max) && (* Output best interval bounds once instead of multiple subdomains repeating them (or less precise ones). *)
           IntInvariant.of_excl_list e ik ns &&
           Option.map_default (I4.invariant_ikind e ik) Invariant.none x_cong && (* Output congruence as is. *)
-          Option.map_default (I5.invariant_ikind e ik) Invariant.none x_intset (* Output interval sets as is. *)
+          Option.map_default (I5.invariant_ikind e ik) Invariant.none x_intset && (* Output interval sets as is. *)
+          Option.map_default (I6.invariant_ikind e ik) Invariant.none x_bf (* Output bitmask as is. *)
         )
     in
     let simplify_none () =
@@ -504,10 +541,10 @@ module IntDomTupleImpl = struct
     | "all" -> simplify_int simplify_all
     | _ -> assert false
 
-  let arbitrary ik = QCheck.(set_print show @@ tup5 (option (I1.arbitrary ik)) (option (I2.arbitrary ik)) (option (I3.arbitrary ik)) (option (I4.arbitrary ik)) (option (I5.arbitrary ik)))
+  let arbitrary ik = QCheck.(set_print show @@ tup6 (option (I1.arbitrary ik)) (option (I2.arbitrary ik)) (option (I3.arbitrary ik)) (option (I4.arbitrary ik)) (option (I5.arbitrary ik)) (option (I6.arbitrary ik)))
 
-  let relift (a, b, c, d, e) =
-    (Option.map I1.relift a, Option.map I2.relift b, Option.map I3.relift c, Option.map I4.relift d, Option.map I5.relift e)
+  let relift (a, b, c, d, e, f) =
+    (Option.map I1.relift a, Option.map I2.relift b, Option.map I3.relift c, Option.map I4.relift d, Option.map I5.relift e, Option.map I6.relift f)
 end
 
 module IntDomTuple =
@@ -519,6 +556,8 @@ struct
   let no_interval (x: I.t) = {x with v = IntDomTupleImpl.no_interval x.v}
 
   let no_intervalSet (x: I.t) = {x with v = IntDomTupleImpl.no_intervalSet x.v}
+
+  let no_bitfield (x: I.t) = {x with v = IntDomTupleImpl.no_bitfield x.v}
 end
 
-let of_const (i, ik, str) = IntDomTuple.of_int ik i
+let of_const (i, ik, str) = IntDomTuple.of_int ik i
\ No newline at end of file
diff --git a/src/cdomain/value/cdomains/int/intervalDomain.ml b/src/cdomain/value/cdomains/int/intervalDomain.ml
index 7d7329e76a..7c7e17b54a 100644
--- a/src/cdomain/value/cdomains/int/intervalDomain.ml
+++ b/src/cdomain/value/cdomains/int/intervalDomain.ml
@@ -1,6 +1,5 @@
 open IntDomain0
 
-
 module IntervalFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Ints_t.t and type t = (Ints_t.t * Ints_t.t) option =
 struct
   let name () = "intervals"
@@ -79,11 +78,38 @@ struct
   (* TODO: change to_int signature so it returns a big_int *)
   let to_int x = Option.bind x (IArith.to_int)
   let of_interval ?(suppress_ovwarn=false) ik (x,y) = norm ~suppress_ovwarn ik @@ Some (x,y)
+
+  let of_bitfield ik x =     
+    let min ik (z,o) = 
+      let signBit = Ints_t.shift_left Ints_t.one ((Size.bit ik) - 1) in 
+      let signMask = Ints_t.lognot (Ints_t.of_bigint (snd (Size.range ik))) in
+      let isNegative = Ints_t.logand signBit o <> Ints_t.zero in
+      if GoblintCil.isSigned ik && isNegative then 
+        Ints_t.logor signMask (Ints_t.lognot z)
+      else 
+        Ints_t.lognot z
+    in let max ik (z,o) =
+         let signBit = Ints_t.shift_left Ints_t.one ((Size.bit ik) - 1) in 
+         let signMask = Ints_t.of_bigint (snd (Size.range ik)) in
+         let isPositive = Ints_t.logand signBit z <> Ints_t.zero in
+         if GoblintCil.isSigned ik && isPositive 
+          then Ints_t.logand signMask o
+         else 
+          o 
+    in fst (norm ik (Some (min ik x, max ik x)))
+
   let of_int ik (x: int_t) = of_interval ik (x,x)
   let zero = Some IArith.zero
   let one  = Some IArith.one
   let top_bool = Some IArith.top_bool
 
+  let to_bitfield ik z = 
+    match z with 
+    | None -> (Ints_t.lognot Ints_t.zero, Ints_t.lognot Ints_t.zero) 
+    | Some (x,y) ->
+      let (z,o) = fst(BitfieldDomain.Bitfield.of_interval ik (Ints_t.to_bigint x, Ints_t.to_bigint y)) in 
+      (Ints_t.of_bigint z, Ints_t.of_bigint o)
+
   let of_bool _ik = function true -> one | false -> zero
   let to_bool (a: t) = match a with
     | None -> None
@@ -381,6 +407,10 @@ struct
     if M.tracing then M.trace "refine" "int_refine_with_congruence %a %a -> %a" pretty x pretty y pretty refn;
     refn
 
+  let refine_with_bitfield ik a b = 
+    let interv = of_bitfield ik b in 
+    meet ik a interv
+
   let refine_with_interval ik a b = meet ik a b
 
   let refine_with_excl_list ik (intv : t) (excl : (int_t list * (int64 * int64)) option) : t =
diff --git a/src/cdomain/value/cdomains/int/intervalSetDomain.ml b/src/cdomain/value/cdomains/int/intervalSetDomain.ml
index 3e2bc847ee..1511802e51 100644
--- a/src/cdomain/value/cdomains/int/intervalSetDomain.ml
+++ b/src/cdomain/value/cdomains/int/intervalSetDomain.ml
@@ -236,6 +236,15 @@ struct
 
   let of_interval ?(suppress_ovwarn=false) ik (x,y) =  norm_interval  ~suppress_ovwarn ~cast:false ik (x,y)
 
+  let of_bitfield ik x = 
+    match Interval.of_bitfield ik x with 
+    | None -> []
+    | Some (a,b) -> norm_interval ik (a,b) |> fst
+
+  let to_bitfield ik x = 
+    let joinbf (z1,o1) (z2,o2) = (Ints_t.logor z1 z2, Ints_t.logor o1 o2) in 
+    List.fold_left (fun acc i -> joinbf acc (Interval.to_bitfield ik (Some i))) (Ints_t.zero, Ints_t.zero) x
+
   let of_int ik (x: int_t) = of_interval ik (x, x)
 
   let lt ik x y =
@@ -501,6 +510,10 @@ struct
 
   let refine_with_interval ik xs = function None -> [] | Some (a,b) -> meet ik xs [(a,b)]
 
+  let refine_with_bitfield ik x y = 
+    let interv = of_bitfield ik y in 
+    norm_intvs ik (meet ik x interv) |> fst
+    
   let refine_with_incl_list ik intvs  = function
     | None -> intvs
     | Some xs -> meet ik intvs (List.map (fun x -> (x,x)) xs)
diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index c53367d278..eeb2789004 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -5,4 +5,5 @@ include IntervalSetDomain
 include DefExcDomain
 include EnumsDomain
 include CongruenceDomain
-include IntDomTuple
+include BitfieldDomain
+include IntDomTuple
\ No newline at end of file
diff --git a/src/cdomain/value/cdomains/intDomain.mli b/src/cdomain/value/cdomains/intDomain.mli
index e7667c9b14..734f1b9452 100644
--- a/src/cdomain/value/cdomains/intDomain.mli
+++ b/src/cdomain/value/cdomains/intDomain.mli
@@ -228,6 +228,7 @@ sig
   val of_interval: ?suppress_ovwarn:bool -> Cil.ikind -> int_t * int_t -> t
 
   val of_congruence: Cil.ikind -> int_t * int_t -> t
+  val of_bitfield: Cil.ikind -> int_t * int_t -> t
   val arbitrary: unit -> t QCheck.arbitrary
   val invariant: Cil.exp -> t -> Invariant.t
 end
@@ -262,10 +263,13 @@ sig
 
   val of_interval: ?suppress_ovwarn:bool -> Cil.ikind -> int_t * int_t -> t
   val of_congruence: Cil.ikind -> int_t * int_t -> t
+  val of_bitfield: Cil.ikind -> int_t * int_t -> t
+  val to_bitfield: Cil.ikind -> t -> int_t * int_t
   val is_top_of: Cil.ikind -> t -> bool
   val invariant_ikind : Cil.exp -> Cil.ikind -> t -> Invariant.t
 
   val refine_with_congruence: Cil.ikind -> t -> (int_t * int_t) option -> t
+  val refine_with_bitfield: Cil.ikind -> t -> (int_t * int_t) -> t
   val refine_with_interval: Cil.ikind -> t -> (int_t * int_t) option -> t
   val refine_with_excl_list: Cil.ikind -> t -> (int_t list * (int64 * int64)) option -> t
   val refine_with_incl_list: Cil.ikind -> t -> int_t list option -> t
@@ -325,6 +329,9 @@ sig
 
   val of_congruence: Cil.ikind -> int_t * int_t -> t
 
+  val of_bitfield: Cil.ikind -> int_t * int_t -> t
+  val to_bitfield: Cil.ikind -> t -> int_t * int_t
+
   val starting   : ?suppress_ovwarn:bool -> Cil.ikind -> int_t -> t
   val ending     : ?suppress_ovwarn:bool -> Cil.ikind -> int_t -> t
 
@@ -354,6 +361,7 @@ module IntDomTuple : sig
   include Z
   val no_interval: t -> t
   val no_intervalSet: t -> t
+  val no_bitfield: t -> t
   val ikind: t -> ikind
 end
 
@@ -402,12 +410,16 @@ module Lifted : IkindUnawareS with type t = [`Top | `Lifted of int64 | `Bot] and
 
 module IntervalFunctor(Ints_t : IntOps.IntOps): SOverflow with type int_t = Ints_t.t and type t = (Ints_t.t * Ints_t.t) option
 
+module BitfieldFunctor(Ints_t : IntOps.IntOps): SOverflow with type int_t = Ints_t.t and type t = (Ints_t.t * Ints_t.t)
+
 module IntervalSetFunctor(Ints_t : IntOps.IntOps): SOverflow with type int_t = Ints_t.t and type t = (Ints_t.t * Ints_t.t) list
 
 module Interval32 :Y with (* type t = (IntOps.Int64Ops.t * IntOps.Int64Ops.t) option and *) type int_t = IntOps.Int64Ops.t
 
 module Interval : SOverflow with type int_t = Z.t
 
+module Bitfield : SOverflow with type int_t = Z.t
+
 module IntervalSet : SOverflow with type int_t = Z.t
 
 module Congruence : S with type int_t = Z.t
diff --git a/src/cdomain/value/cdomains/intDomain0.ml b/src/cdomain/value/cdomains/intDomain0.ml
index e88ddaa8ee..5ca7b5c49c 100644
--- a/src/cdomain/value/cdomains/intDomain0.ml
+++ b/src/cdomain/value/cdomains/intDomain0.ml
@@ -192,6 +192,7 @@ sig
   val of_bool: bool -> t
   val of_interval: ?suppress_ovwarn:bool -> Cil.ikind -> int_t * int_t -> t
   val of_congruence: Cil.ikind -> int_t * int_t -> t
+  val of_bitfield: Cil.ikind -> int_t * int_t -> t
   val arbitrary: unit -> t QCheck.arbitrary
   val invariant: Cil.exp -> t -> Invariant.t
 end
@@ -219,10 +220,13 @@ sig
   val of_bool: Cil.ikind -> bool -> t
   val of_interval: ?suppress_ovwarn:bool -> Cil.ikind -> int_t * int_t -> t
   val of_congruence: Cil.ikind -> int_t * int_t -> t
+  val of_bitfield: Cil.ikind -> int_t * int_t -> t
+  val to_bitfield: Cil.ikind -> t -> int_t * int_t
   val is_top_of: Cil.ikind -> t -> bool
   val invariant_ikind : Cil.exp -> Cil.ikind -> t -> Invariant.t
 
   val refine_with_congruence: Cil.ikind -> t -> (int_t * int_t) option -> t
+  val refine_with_bitfield: Cil.ikind -> t -> (int_t * int_t) -> t
   val refine_with_interval: Cil.ikind -> t -> (int_t * int_t) option -> t
   val refine_with_excl_list: Cil.ikind -> t -> (int_t list * (int64 * int64)) option -> t
   val refine_with_incl_list: Cil.ikind -> t -> int_t list option -> t
@@ -260,6 +264,17 @@ sig
   val shift_right : Cil.ikind -> t -> t -> t * overflow_info
 end
 
+module type Bitfield_SOverflow = 
+sig 
+
+  include SOverflow 
+
+  (* necessary for baseInvariant *)
+  val refine_bor : t -> t -> t -> t * t
+  val refine_band : t -> t -> t -> t * t
+
+end
+
 module type Y =
 sig
   (* include B *)
@@ -269,6 +284,8 @@ sig
   val of_bool: Cil.ikind -> bool -> t
   val of_interval: ?suppress_ovwarn:bool -> Cil.ikind -> int_t * int_t -> t
   val of_congruence: Cil.ikind -> int_t * int_t -> t
+  val of_bitfield: Cil.ikind -> int_t * int_t -> t
+  val to_bitfield: Cil.ikind -> t -> int_t * int_t
 
   val starting   : ?suppress_ovwarn:bool -> Cil.ikind -> int_t -> t
   val ending     : ?suppress_ovwarn:bool -> Cil.ikind -> int_t -> t
@@ -347,6 +364,9 @@ struct
   let to_incl_list x = I.to_incl_list x.v
   let of_interval ?(suppress_ovwarn=false) ikind (lb,ub) = {v = I.of_interval ~suppress_ovwarn ikind (lb,ub); ikind}
   let of_congruence ikind (c,m) = {v = I.of_congruence ikind (c,m); ikind}
+  let of_bitfield ikind (z,o) = {v = I.of_bitfield ikind (z,o); ikind}
+  let to_bitfield ikind x = I.to_bitfield ikind x.v
+
   let starting ?(suppress_ovwarn=false) ikind i = {v = I.starting ~suppress_ovwarn  ikind i; ikind}
   let ending ?(suppress_ovwarn=false) ikind i = {v = I.ending ~suppress_ovwarn ikind i; ikind}
   let maximal x = I.maximal x.v
@@ -481,6 +501,7 @@ module StdTop (B: sig type t val top_of: Cil.ikind -> t end) = struct
   let to_incl_list    x = None
   let of_interval ?(suppress_ovwarn=false) ik x = top_of ik
   let of_congruence ik x = top_of ik
+  let of_bitfield ik x = top_of ik
   let starting ?(suppress_ovwarn=false) ik x = top_of ik
   let ending ?(suppress_ovwarn=false)   ik x = top_of ik
   let maximal         x = None
@@ -772,6 +793,7 @@ struct
   let to_incl_list x = None
   let of_interval ?(suppress_ovwarn=false) ik x = top_of ik
   let of_congruence ik x = top_of ik
+  let of_bitfield ik x = top_of ik
   let starting ?(suppress_ovwarn=false) ikind x = top_of ikind
   let ending ?(suppress_ovwarn=false)   ikind x = top_of ikind
   let maximal      x = None
diff --git a/src/cdomain/value/util/precisionUtil.ml b/src/cdomain/value/util/precisionUtil.ml
index 047043b4aa..3ecd019356 100644
--- a/src/cdomain/value/util/precisionUtil.ml
+++ b/src/cdomain/value/util/precisionUtil.ml
@@ -1,8 +1,8 @@
 (** Integer and floating-point option and attribute handling. *)
 
 (* We define precision by the number of IntDomains activated.
- * We currently have 5 types: DefExc, Interval, Enums, Congruence, IntervalSet *)
-type int_precision = (bool * bool * bool * bool * bool)
+ * We currently have 6 types: DefExc, Interval, Enums, Congruence, IntervalSet, Bitfield*)
+type int_precision = (bool * bool * bool * bool * bool * bool)
 (* Same applies for FloatDomain
  * We currently have only an interval type analysis *)
 type float_precision = (bool)
@@ -12,6 +12,7 @@ let interval: bool option ref = ref None
 let enums: bool option ref = ref None
 let congruence: bool option ref = ref None
 let interval_set: bool option ref = ref None
+let bitfield: bool option ref = ref None
 
 let get_def_exc () =
   if !def_exc = None then
@@ -38,6 +39,11 @@ let get_interval_set () =
     interval_set := Some (GobConfig.get_bool "ana.int.interval_set");
   Option.get !interval_set
 
+let get_bitfield () =
+  if !bitfield = None then
+    bitfield := Some (GobConfig.get_bool "ana.int.bitfield");
+  Option.get !bitfield
+
 let annotation_int_enabled: bool option ref = ref None
 
 let get_annotation_int_enabled () =
@@ -51,17 +57,19 @@ let reset_lazy () =
   enums := None;
   congruence := None;
   interval_set := None;
+  bitfield := None;
   annotation_int_enabled := None
 
 (* Thus for maximum precision we activate all Domains *)
-let max_int_precision : int_precision = (true, true, true, true, true)
+let max_int_precision : int_precision = (true, true, true, true, true, true)
 let max_float_precision : float_precision = (true)
 let int_precision_from_fundec (fd: GoblintCil.fundec): int_precision =
   ((ContextUtil.should_keep_int_domain ~isAttr:GobPrecision ~keepOption:(get_def_exc ()) ~removeAttr:"no-def_exc" ~keepAttr:"def_exc" fd),
    (ContextUtil.should_keep_int_domain ~isAttr:GobPrecision ~keepOption:(get_interval ()) ~removeAttr:"no-interval" ~keepAttr:"interval" fd),
    (ContextUtil.should_keep_int_domain ~isAttr:GobPrecision ~keepOption:(get_enums ()) ~removeAttr:"no-enums" ~keepAttr:"enums" fd),
    (ContextUtil.should_keep_int_domain ~isAttr:GobPrecision ~keepOption:(get_congruence ()) ~removeAttr:"no-congruence" ~keepAttr:"congruence" fd),
-   (ContextUtil.should_keep_int_domain ~isAttr:GobPrecision ~keepOption:(get_interval_set ()) ~removeAttr:"no-interval_set" ~keepAttr:"interval_set" fd))
+   (ContextUtil.should_keep_int_domain ~isAttr:GobPrecision ~keepOption:(get_interval_set ()) ~removeAttr:"no-interval_set" ~keepAttr:"interval_set" fd),
+   (ContextUtil.should_keep_int_domain ~isAttr:GobPrecision ~keepOption:(get_bitfield ()) ~removeAttr:"no-bitfield" ~keepAttr:"bitfield" fd))
 
 let float_precision_from_fundec (fd: GoblintCil.fundec): float_precision =
   ((ContextUtil.should_keep ~isAttr:GobPrecision ~keepOption:"ana.float.interval" ~removeAttr:"no-float-interval" ~keepAttr:"float-interval" fd))
@@ -70,7 +78,7 @@ let int_precision_from_node (): int_precision =
   | Some n -> int_precision_from_fundec (Node.find_fundec n)
   | _ -> max_int_precision (* In case a Node is None we have to handle Globals, i.e. we activate all IntDomains (TODO: verify this assumption) *)
 
-let is_congruence_active (_, _, _, c,_: int_precision): bool = c
+let is_congruence_active (_, _, _, c,_,_: int_precision): bool = c
 
 let float_precision_from_node (): float_precision =
   match !MyCFG.current_node with
@@ -81,7 +89,7 @@ let int_precision_from_node_or_config (): int_precision =
   if get_annotation_int_enabled () then
     int_precision_from_node ()
   else
-    (get_def_exc (), get_interval (), get_enums (), get_congruence (), get_interval_set ())
+    (get_def_exc (), get_interval (), get_enums (), get_congruence (), get_interval_set (), get_bitfield ())
 
 let float_precision_from_node_or_config (): float_precision =
   if GobConfig.get_bool "annotation.float.enabled" then
diff --git a/src/config/options.schema.json b/src/config/options.schema.json
index 9b7010621a..ce0f398bee 100644
--- a/src/config/options.schema.json
+++ b/src/config/options.schema.json
@@ -414,6 +414,13 @@
               "type": "boolean",
               "default": false
             },
+            "bitfield": {
+              "title": "ana.int.bitfield",
+              "description":
+                "Use IntDomain.Bitfield: Bitfield domain for integers.",
+              "type": "boolean",
+              "default": false
+            },
             "congruence": {
               "title": "ana.int.congruence",
               "description":
@@ -641,6 +648,12 @@
                     "Integer values of the IntervalSet domain in function contexts.",
                   "type": "boolean",
                   "default": true
+                },
+                "bitfield": {
+                  "title": "ana.base.context.bitfield",
+                  "description": "Bitfield values in function contexts.",
+                  "type": "boolean",
+                  "default": true
                 }
               },
               "additionalProperties": false
@@ -1701,7 +1714,7 @@
             "type": "array",
             "items": {
               "type": "string",
-              "enum": ["base.no-non-ptr", "base.non-ptr", "base.no-int", "base.int", "base.no-interval", "base.no-interval_set","base.interval", "base.interval_set","relation.no-context", "relation.context", "no-widen", "widen"]
+              "enum": ["base.no-non-ptr", "base.non-ptr", "base.no-int", "base.int", "base.no-interval", "base.no-interval_set", "base.no-bitfield", "base.interval", "base.interval_set", "base.bitfield", "relation.no-context", "relation.context", "no-widen", "widen"]
             },
             "default": []
           }
diff --git a/src/util/std/gobTuple.ml b/src/util/std/gobTuple.ml
new file mode 100644
index 0000000000..1855d6ee2e
--- /dev/null
+++ b/src/util/std/gobTuple.ml
@@ -0,0 +1,20 @@
+(* Custom Tuple6 as Batteries only provides up to Tuple5 *)
+module Tuple6 = struct
+
+  let first (a,_,_,_,_, _) = a
+  let second (_,b,_,_,_, _) = b
+  let third (_,_,c,_,_, _) = c
+  let fourth (_,_,_,d,_, _) = d
+  let fifth (_,_,_,_,e, _) = e
+  let sixth (_,_,_,_,_, f) = f
+
+  let map1 fn (a, b, c, d, e, f) = (fn a, b, c, d, e, f)
+  let map2 fn (a, b, c, d, e, f) = (a, fn b, c, d, e, f)
+  let map3 fn (a, b, c, d, e, f) = (a, b, fn c, d, e, f)
+  let map4 fn (a, b, c, d, e, f) = (a, b, c, fn d, e, f)
+  let map5 fn (a, b, c, d, e, f) = (a, b, c, d, fn e, f)
+  let map6 fn (a, b, c, d, e, f) = (a, b, c, d, e, fn f)
+
+  let enum (a,b,c,d,e,f) = BatList.enum [a;b;c;d;e;f] (* Make efficient? *)
+
+end
\ No newline at end of file
diff --git a/src/util/std/goblint_std.ml b/src/util/std/goblint_std.ml
index 5b623ead30..98c8742c0c 100644
--- a/src/util/std/goblint_std.ml
+++ b/src/util/std/goblint_std.ml
@@ -13,6 +13,7 @@ module GobResult = GobResult
 module GobOption = GobOption
 module GobSys = GobSys
 module GobUnix = GobUnix
+module GobTuple = GobTuple
 
 (** {1 Other libraries}
 
diff --git a/tests/regression/83-bitfield/00-simple-demo.c b/tests/regression/83-bitfield/00-simple-demo.c
new file mode 100644
index 0000000000..e87fa63d79
--- /dev/null
+++ b/tests/regression/83-bitfield/00-simple-demo.c
@@ -0,0 +1,29 @@
+// PARAM: --enable ana.int.bitfield
+#include <assert.h>
+#include <stdio.h>
+#include <stdlib.h>
+
+#define ANY_ERROR 5  // 0b0101
+
+int main() {
+  int testvar = 235;
+
+  int state;
+  int r = rand() % 3;
+  switch (r) {
+    case 0:
+      state = 0; /* 0b000 */
+      testvar = 1;
+      break;
+    case 1:
+      state = 8; /* 0b1000 */
+      testvar = 1;
+      break;
+    default:
+      state = 10; /* 0b1010 */
+      testvar = 1;
+      break;
+  }
+
+  __goblint_check((state & ANY_ERROR) == 0);
+}
\ No newline at end of file
diff --git a/tests/regression/83-bitfield/01-simple-arith.c b/tests/regression/83-bitfield/01-simple-arith.c
new file mode 100644
index 0000000000..045c26e5d4
--- /dev/null
+++ b/tests/regression/83-bitfield/01-simple-arith.c
@@ -0,0 +1,13 @@
+// PARAM: --disable ana.int.interval --disable ana.int.def_exc --enable ana.int.bitfield
+#include <stdlib.h>
+
+int main() {
+  int a = 19;
+  int b = 23;
+
+  __goblint_check(a + b == 42);
+  __goblint_check(a - b == -4);
+  __goblint_check(a * b == 437);
+  __goblint_check(a / b == 0);
+  __goblint_check(a % b == 19);
+}
\ No newline at end of file
diff --git a/tests/regression/83-bitfield/02-complex-arith.c b/tests/regression/83-bitfield/02-complex-arith.c
new file mode 100644
index 0000000000..a1f718b86b
--- /dev/null
+++ b/tests/regression/83-bitfield/02-complex-arith.c
@@ -0,0 +1,63 @@
+// PARAM: --disable ana.int.interval --disable ana.int.def_exc --enable ana.int.bitfield
+#include <stdlib.h>
+#include <goblint.h>
+
+int main() {
+  int a;
+  int b = 23;
+
+  int r = rand() % 2;
+  switch (r) {
+    case 0:
+      a = 19;
+      printf("a = 19\n");
+      break;
+    default:
+      a = 17;
+      printf("a = 17\n");
+      break;
+  }
+
+  // PLUS
+
+  int c_add = a + b;
+
+  if (c_add == 40) {
+    __goblint_check(1);  // reachable
+  }
+  if (c_add == 42) {
+    __goblint_check(1);  // reachable
+  }
+  if (c_add > 42 || c_add < 40) {
+    __goblint_check(0);  // NOWARN (unreachable)
+  }
+
+  // MINUS
+
+  int c_minus = b - a;
+
+  if (c_minus == 6) {
+    __goblint_check(1);  // reachable
+  }
+  if (c_minus == 4) {
+    __goblint_check(1);  // reachable
+  }
+  if (c_minus > 6 || c_minus < 4) {
+    __goblint_check(0);  // NOWARN (unreachable)
+  }
+
+  // MULT
+
+  int c_mult = a * b;
+
+  if (c_mult == 391) {
+    __goblint_check(1);  // reachable
+  }
+  if (c_mult == 437) {
+    __goblint_check(1);  // reachable
+  }
+
+  // DIV
+
+  // Div on non-unique bitfields is not supported
+}
\ No newline at end of file
diff --git a/tests/regression/83-bitfield/03-simple-bitwise.c b/tests/regression/83-bitfield/03-simple-bitwise.c
new file mode 100644
index 0000000000..2e0ce3a57d
--- /dev/null
+++ b/tests/regression/83-bitfield/03-simple-bitwise.c
@@ -0,0 +1,14 @@
+// PARAM: --disable ana.int.interval --disable ana.int.def_exc --enable ana.int.bitfield
+#include <stdlib.h>
+
+int main() {
+  int a = 19;
+  int b = 14;
+
+  __goblint_check((a & b) == 2);
+  __goblint_check((a | b) == 31);
+  __goblint_check((a ^ b) == 29);
+  __goblint_check((~a) == -20);
+  __goblint_check((a << 2) == 76);
+  __goblint_check((a >> 2) == 4);
+}
\ No newline at end of file
diff --git a/tests/regression/83-bitfield/04-complex-bitwise.c b/tests/regression/83-bitfield/04-complex-bitwise.c
new file mode 100644
index 0000000000..393f759cb8
--- /dev/null
+++ b/tests/regression/83-bitfield/04-complex-bitwise.c
@@ -0,0 +1,87 @@
+// PARAM: --disable ana.int.interval --disable ana.int.def_exc --enable ana.int.bitfield
+#include <stdlib.h>
+
+int main() {
+  int a;
+  int b = 21;  // 10101 in binary
+
+  int r = rand() % 2;
+  switch (r) {
+    case 0:
+      a = 19;  // 10011 in binary
+      printf("a = 19\n");
+      break;
+    default:
+      a = 17;  // 10001 in binary
+      printf("a = 17\n");
+      break;
+  }
+
+  // AND
+  int c_and = a & b;
+
+  if (c_and == 17) {
+    __goblint_check(1);  // reachable (19 & 21 = 17, 17 & 21 = 17)
+  }
+  if (c_and != 17) {
+    __goblint_check(0);  // NOWARN (unreachable)
+  }
+
+  // OR
+  int c_or = a | b;
+
+  if (c_or == 23) {
+    __goblint_check(1);  // reachable (19|21 = 23)
+  }
+  if (c_or == 21) {
+    __goblint_check(1);  // reachable (17|21 = 21)
+  }
+  if (c_or > 23 || c_or < 21) {
+    __goblint_check(0);  // NOWARN (unreachable)
+  }
+
+  // XOR
+  int c_xor = a ^ b;
+
+  if (c_xor == 6) {
+    __goblint_check(1);  // reachable (19^21 = 6)
+  }
+  if (c_xor == 4) {
+    __goblint_check(1);  // reachable (17^21 = 4)
+  }
+  if (c_xor > 6 || c_xor < 4) {
+    __goblint_check(0);  // NOWARN (unreachable)
+  }
+
+  // Left shift
+  int c_lshift = a << 1;
+
+  if (c_lshift == 38) {
+    __goblint_check(1);  // reachable (19<<1 = 38)
+  }
+  if (c_lshift == 34) {
+    __goblint_check(1);  // reachable (17<<1 = 34)
+  }
+  if (c_lshift > 38 || c_lshift < 34) {
+    __goblint_check(0);  // NOWARN (unreachable)
+  }
+
+  // Right shift
+  int c_rshift = a >> 1;
+
+  if (c_rshift == 9) {
+    __goblint_check(1);  // reachable (19>>1 = 9)
+  }
+  if (c_rshift == 8) {
+    __goblint_check(1);  // reachable (17>>1 = 8)
+  }
+  if (c_rshift > 9 || c_rshift < 8) {
+    __goblint_check(0);  // NOWARN (unreachable)
+  }
+
+  // Check power of two formula
+  int a = 16;
+  __goblint_assert((a & (a - 1)) == 0);  // SUCCESS
+
+  return 0;
+}
\ No newline at end of file
diff --git a/tests/regression/83-bitfield/05-refine-with-congruence.c b/tests/regression/83-bitfield/05-refine-with-congruence.c
new file mode 100644
index 0000000000..828bdfdb9f
--- /dev/null
+++ b/tests/regression/83-bitfield/05-refine-with-congruence.c
@@ -0,0 +1,15 @@
+// PARAM: --disable ana.int.interval --disable ana.int.def_exc --enable ana.int.bitfield --set ana.int.refinement fixpoint --enable ana.int.congruence
+#include <assert.h>
+#include <stdio.h>
+#include <stdlib.h>
+
+int main() {
+  int a = rand();
+
+  __goblint_assume(a % 8 == 3);
+
+  __goblint_assert((a & 0x7) == 3); // SUCCESS
+
+}
+
+ 
\ No newline at end of file
diff --git a/tests/regression/83-bitfield/06-refine-with-incl-set.c b/tests/regression/83-bitfield/06-refine-with-incl-set.c
new file mode 100644
index 0000000000..6edd060c5c
--- /dev/null
+++ b/tests/regression/83-bitfield/06-refine-with-incl-set.c
@@ -0,0 +1,12 @@
+// PARAM: --disable ana.int.def_exc --enable ana.int.bitfield --set ana.int.refinement fixpoint --enable ana.int.enums
+#include <assert.h>
+#include <stdio.h>
+#include <stdlib.h>
+
+int main() {
+  int a = rand();
+
+  if (a == 9 || a == 11 || a == 15) {
+    __goblint_assert((a & 9) == 9); // SUCCESS
+  }
+}
diff --git a/tests/regression/83-bitfield/07-refine-with-interval.c b/tests/regression/83-bitfield/07-refine-with-interval.c
new file mode 100644
index 0000000000..3a4bc547fb
--- /dev/null
+++ b/tests/regression/83-bitfield/07-refine-with-interval.c
@@ -0,0 +1,25 @@
+// PARAM: --enable ana.int.interval --disable ana.int.def_exc --enable ana.int.bitfield --set ana.int.refinement fixpoint
+#include <assert.h>
+#include <stdio.h>
+#include <stdlib.h>
+
+int main() {
+  int a = rand();
+
+  if (a <= 4) {
+    __goblint_assert((a & 0x10) == 0); // SUCCESS
+
+    int b = ~0x7;
+    __goblint_assert((a & b) == 0);  // SUCCESS
+  }
+
+  if (a > 8 && a < 15) {
+    __goblint_assert((a & 8) == 8);  // SUCCESS
+  }
+
+  int b = rand() - 512;
+
+  if(-4 <= b && b <= -2) {
+    __goblint_assert((b & 4) == 4);  // SUCCESS
+  }
+}
diff --git a/tests/regression/83-bitfield/08-refine-with-bitfield.c b/tests/regression/83-bitfield/08-refine-with-bitfield.c
new file mode 100644
index 0000000000..d55b4cee46
--- /dev/null
+++ b/tests/regression/83-bitfield/08-refine-with-bitfield.c
@@ -0,0 +1,100 @@
+// PARAM: --enable ana.int.bitfield --set ana.int.refinement fixpoint
+#include <assert.h>
+#include <stdio.h>
+#include <stdlib.h>
+
+int main() {
+  int a = rand();
+
+  // Basic bitwise properties
+  __goblint_assert((a & 0) == 0);                    // Any number ANDed with 0 is 0
+  __goblint_assert((a | 0xFFFFFFFF) == 0xFFFFFFFF);  // Any number ORed with all 1s gives all 1s
+
+  // Testing alignment and divisibility with powers of 2
+  int ALIGN_8 = 0x7;  // 111 in binary
+  if ((a & ALIGN_8) == 0) {
+    __goblint_assert(a % 8 == 0);  // Number is aligned to 8
+  }
+
+  int ALIGN_32 = 0x1F;  // 11111 in binary
+  if ((a & ALIGN_32) == 0) {
+    __goblint_assert(a % 32 == 0);  // Number is divisible by 32
+  }
+
+  // Testing specific power of 2 patterns
+  int POW2_MASK = (1 << 4) - 1;  // 15 (0b1111)
+  if ((a & POW2_MASK) == 8) {
+    __goblint_assert((a & 0xf) == 8);  // Exactly bit 3 set in lower 4 bits
+    __goblint_assert((a & 12) == 8);   // Bits 2-3 must be 1000
+    __goblint_assert((a & 3) == 0);    // Bits 0-1 must be 0
+  }
+
+  // Testing specific bit patterns and masking
+  if ((a & 0x3) == 0x3) {
+    __goblint_assert(a % 4 >= 3);    // Last two bits are 1
+    __goblint_assert((a & 1) == 1);  // Least significant bit must be 1
+  }
+
+  if ((a & 0xC) == 0x8) {                // 1000 in binary
+    __goblint_assert((a & 0x4) == 0);    // Bit 2 must be 0
+    __goblint_assert((a & 0x8) == 0x8);  // Bit 3 must be 1
+  }
+
+  // Testing OR operations with patterns
+  int OR_MASK = 0x55;  // 01010101 in binary
+  if ((a | OR_MASK) == 0x55) {
+    __goblint_assert((a | 0xFF) == 0xFF);  // ORing with all 1s gives all 1s
+  }
+
+  if ((a | 0x6) == a) {
+    __goblint_assert((a & 0x6) == 0x6);  // Bits 1 and 2 must be set
+  }
+
+  // Testing XOR operations
+  int XOR_MASK = 0xAA;  // 10101010 in binary
+  if ((a ^ XOR_MASK) == 0) {
+    __goblint_assert(a == 0xAA);           // Must match the mask exactly
+    __goblint_assert((a & 0xAA) == 0xAA);  // All alternating bits must be 1
+  }
+
+  if ((a ^ 0xFF) == 0) {
+    __goblint_assert(a == 0xFF);  // Only possible if a is 0xFF
+  }
+
+  // Testing complex bit patterns
+  int COMPLEX_MASK = 0x33;  // 00110011 in binary
+  if ((a & COMPLEX_MASK) == 0x11) {
+    __goblint_assert((a & 0x22) == 0);     // Middle bits must be 0
+    __goblint_assert((a & 0x11) == 0x11);  // Outer bits must be 1
+  }
+
+  // Testing shifted masks and patterns
+  int SHIFT_MASK = 3 << 2;  // 1100 in binary
+  if ((a & SHIFT_MASK) == SHIFT_MASK) {
+    __goblint_assert((a & 12) == 12);         // Both bits must be set
+    __goblint_assert(((a >> 2) & 3) == 3);    // When shifted right, lowest bits must be 11
+  }
+
+  if (a == SHIFT_MASK) {
+    __goblint_assert(((a << 2) & 48) == 48);  // When shifted left, highest bits must be 11
+  }
+
+  int SHIFTED = 0x7 << 3;  // 111000 in binary
+  if ((a & SHIFTED) == 0) {
+    __goblint_assert((a & 0x38) == 0);  // Bits 3,4,5 must be 0
+  }
+
+  // Testing sign bits and negative numbers
+  if ((a & 0x80) == 0x80) {
+    __goblint_assert(a & 0x80);            // Highest bit must be set
+    __goblint_assert((a | 0x7F) >= 0x80);  // Result must be >= 128
+  }
+
+  // Testing bitwise complement
+  int COMP_MASK = ~0x0F;
+  if ((a & COMP_MASK) == 0x0F) {
+    __goblint_check(0);  // NOWARN (unreachable)
+  }
+
+  return 0;
+}
\ No newline at end of file
diff --git a/tests/regression/83-bitfield/09-refine-intervalA.c b/tests/regression/83-bitfield/09-refine-intervalA.c
new file mode 100644
index 0000000000..6cf8ca9b19
--- /dev/null
+++ b/tests/regression/83-bitfield/09-refine-intervalA.c
@@ -0,0 +1,22 @@
+// PARAM: --enable ana.int.bitfield --set ana.int.refinement fixpoint
+#include <assert.h>
+#include <stdio.h>
+#include <stdlib.h>
+
+int main() {
+  int a = rand();
+
+  int inv_mask = ~0xe;  // inv_mask = 0b1111.1111.1111.1111.1111.1111.1111.0001 in binary
+
+  if ((a & inv_mask) == 0) {
+    // a should get refined to 0b0000.0000.0000.0000.0000.0000.0000.???0 in binary
+    __goblint_check(a <= 14);  // SUCCESS
+    __goblint_check(a >= 0);   // SUCCESS
+
+    if (0 <= a && a <= 14) {
+      printf("a is in the interval [0, 14]\n");
+    } else {
+      __goblint_check(0);  // NOWARN (unreachable)
+    }
+  }
+}
\ No newline at end of file
diff --git a/tests/regression/83-bitfield/10-refine-intervalB.c b/tests/regression/83-bitfield/10-refine-intervalB.c
new file mode 100644
index 0000000000..77720a077d
--- /dev/null
+++ b/tests/regression/83-bitfield/10-refine-intervalB.c
@@ -0,0 +1,22 @@
+// PARAM: --enable ana.int.interval --enable ana.int.bitfield --set ana.int.refinement fixpoint
+#include <goblint.h>
+
+int main() {
+  unsigned char r; // non-neg rand
+  char x = r % 64;
+
+  if ((r | x) == 0) {
+    __goblint_check(r == 0); // SUCCESS
+    __goblint_check(x == 0); // SUCCESS
+  }
+
+  if ((r & x) == 63) {
+    __goblint_check((r & 63) == 63); // SUCCESS
+    __goblint_check(x == 63); // SUCCESS
+  }
+
+  if ((x ^ 3) == 5) {
+    __goblint_check(x == 6); // SUCCESS
+  }
+
+}
diff --git a/tests/regression/83-bitfield/11-refine-intervalC.c b/tests/regression/83-bitfield/11-refine-intervalC.c
new file mode 100644
index 0000000000..6dc63b2494
--- /dev/null
+++ b/tests/regression/83-bitfield/11-refine-intervalC.c
@@ -0,0 +1,17 @@
+// PARAM: --enable ana.int.interval --enable ana.int.bitfield --set ana.int.refinement fixpoint
+#include <goblint.h>
+
+int main() {
+  unsigned char r; // non-neg rand
+  char x = r % 64;
+
+  if ((x | 0) == 63) {
+    __goblint_check(x == 63); // SUCCESS
+  }
+
+  if ((x & 63) == 0) {
+    __goblint_check(x == 0); // SUCCESS
+  }
+
+
+}
diff --git a/tests/regression/83-bitfield/12-precision.c b/tests/regression/83-bitfield/12-precision.c
new file mode 100644
index 0000000000..01d44e95b4
--- /dev/null
+++ b/tests/regression/83-bitfield/12-precision.c
@@ -0,0 +1,47 @@
+// PARAM: --enable ana.int.bitfield --enable annotation.int.enabled
+#include <goblint.h>
+
+#define ANY_ERROR 5  // 0b0101
+void example1(void) __attribute__((goblint_precision("no-bitfield")));
+void example2(void) __attribute__((goblint_precision("bitfield")));
+
+int main() {
+  example1();
+  example2();
+}
+
+void example1() {
+  int state;
+  int r = rand() % 3;
+  switch (r) {
+    case 0:
+      state = 0; /* 0b0000 */
+      break;
+    case 1:
+      state = 8; /* 0b1000 */
+      break;
+    default:
+      state = 10; /* 0b1010 */
+      break;
+  }
+
+  __goblint_check((state & ANY_ERROR) == 0);  // UNKNOWN
+}
+
+void example2() {
+  int state;
+  int r = rand() % 3;
+  switch (r) {
+    case 0:
+      state = 0; /* 0b0000 */
+      break;
+    case 1:
+      state = 8; /* 0b1000 */
+      break;
+    default:
+      state = 10; /* 0b1010 */
+      break;
+  }
+
+  __goblint_check((state & ANY_ERROR) == 0);  // SUCCESS
+}
\ No newline at end of file
diff --git a/tests/regression/83-bitfield/13-join.c b/tests/regression/83-bitfield/13-join.c
new file mode 100644
index 0000000000..3711c13230
--- /dev/null
+++ b/tests/regression/83-bitfield/13-join.c
@@ -0,0 +1,63 @@
+// PARAM: --disable ana.int.interval --disable ana.int.def_exc --enable ana.int.bitfield
+#include <goblint.h>
+
+void basic_join() {
+  int a = 8;
+  int b = 10;
+
+  int c;
+  if (rand()) {
+    c = a;
+  } else {
+    c = b;
+  }
+  // c should be 0b0000.0000.0000.0000.0000.0000.0000.010?0
+
+  int definite_ones = 8;     // 0b0000.0000.0000.0000.0000.0000.0000.1000
+  int definite_zeros = -11;  // 0b1111.1111.1111.1111.1111.1111.1111.0101
+
+  __goblint_assert((c & definite_ones) == definite_ones);     // SUCCESS
+  __goblint_assert((~c & definite_zeros) == definite_zeros);  // SUCCESS
+}
+
+void join_with_cast() {
+  int a = 511;
+  char b = 10;
+
+  unsigned char c;
+  if (rand()) {
+    c = a;
+  } else {
+    c = b;
+  }
+  // c should be 0b????.1?1?
+
+  char definite_ones = 10;  // 0b0000.1010
+  char definite_zeros = 0;  // 0b0000.0000
+
+  __goblint_assert((c & definite_ones) == definite_ones);     // SUCCESS
+  __goblint_assert((~c & definite_zeros) == definite_zeros);  // SUCCESS
+}
+
+void join_loop() {
+  unsigned char a = 16;
+
+  while (a < 128) {
+    a *= 2;
+  }
+  // a should be 0b????.0000
+
+  char definite_ones = 0;    // 0b0000.0000
+  char definite_zeros = 15;  // 0b0000.1111
+
+  __goblint_assert((a & definite_ones) == definite_ones);     // SUCCESS
+  __goblint_assert((~a & definite_zeros) == definite_zeros);  // SUCCESS
+}
+
+int main() {
+  basic_join();
+  join_with_cast();
+  join_loop();
+
+  return 0;
+}
diff --git a/tests/unit/cdomains/intDomainTest.ml b/tests/unit/cdomains/intDomainTest.ml
index a60b7a6cb1..5d022d7ce2 100644
--- a/tests/unit/cdomains/intDomainTest.ml
+++ b/tests/unit/cdomains/intDomainTest.ml
@@ -250,7 +250,677 @@ struct
   ]
 end
 
+module BitfieldTest (I : IntDomain.SOverflow with type int_t = Z.t) =
+struct
+  module I_ = I
+  module I = IntDomain.SOverflowUnlifter (I)
+
+  let ik = Cil.IInt
+  let ik_lst = [Cil.IChar; Cil.IUChar; Cil.IShort; Cil.IUShort; ik; Cil.IUInt;]
+
+  let assert_equal x y =
+    OUnit.assert_equal ~printer:I.show x y
+
+  let test_of_int_to_int _ =
+    let b1 = I.of_int ik (of_int 17) in
+    OUnit.assert_equal 17 (I.to_int b1 |> Option.get |> to_int)
+
+  let test_to_int_of_int _ =
+    OUnit.assert_equal None (I.to_int (I.bot_of ik));
+    OUnit.assert_equal (of_int 13) (I.to_int (I.of_int ik (of_int 13)) |> Option.get);
+    OUnit.assert_equal None (I.to_int (I.top_of ik));
+    OUnit.assert_equal None (I.to_int (I.join ik (I.of_int ik (of_int 13)) (I.of_int ik (of_int 14))))
+
+  let test_equal_to _ =
+    let b1 = I.join ik (I.of_int ik (of_int 4)) (I.of_int ik (of_int 2)) in
+    OUnit.assert_equal `Top (I.equal_to (Z.of_int 4) b1);
+    OUnit.assert_equal `Top (I.equal_to (Z.of_int 2) b1);
+
+    OUnit.assert_equal `Top (I.equal_to (Z.of_int 0) b1);
+    OUnit.assert_equal `Top (I.equal_to (Z.of_int 6) b1);
+
+    OUnit.assert_equal `Neq (I.equal_to (Z.of_int 1) b1);
+    OUnit.assert_equal `Neq (I.equal_to (Z.of_int 3) b1);
+    OUnit.assert_equal `Neq (I.equal_to (Z.of_int 5) b1);
+
+    let b2 =I.of_int ik (of_int 123) in
+    OUnit.assert_equal `Eq (I.equal_to (Z.of_int 123) b2)
+
+  let test_join _ =
+    let b1 = I.of_int ik (of_int 9) in
+    let b2 = I.of_int ik (of_int 2) in
+    let bjoin = I.join ik b1 b2 in
+
+    assert_bool "num1 leq join" (I.leq b1 bjoin);
+    assert_bool "num2 leq join" (I.leq b2 bjoin);
+
+    OUnit.assert_equal `Top (I.equal_to (Z.of_int 9) bjoin);
+    OUnit.assert_equal `Top (I.equal_to (Z.of_int 2) bjoin);
+    OUnit.assert_equal `Top (I.equal_to (Z.of_int 11) bjoin)
+
+  let test_meet _ =
+    let b1 = I.of_int ik (of_int 5) in
+    let b2 = I.of_int ik (of_int 3) in
+    let bf12 = I.join ik b1 b2 in
+
+    let b3 = I.of_int ik (of_int 7) in
+    let b4 = I.of_int ik (of_int 4) in
+    let bf34 = I.join ik b3 b4 in
+
+    let bmeet2 = I.meet ik bf12 bf34 in
+
+    OUnit.assert_equal `Top (I.equal_to (Z.of_int 5) bmeet2);
+    OUnit.assert_equal `Top (I.equal_to (Z.of_int 7) bmeet2)
+
+  let test_leq_1 _ =
+    let b1 = I.of_int ik (of_int 13) in
+    let b2 = I.of_int ik (of_int 5) in
+
+    let bjoin = I.join ik b1 b2 in
+
+    OUnit.assert_bool "13 leq 13" (I.leq b1 b1);
+    OUnit.assert_bool "5 leq 5" (I.leq b2 b2);
+
+    OUnit.assert_bool "5 leq 13" (I.leq b2 bjoin);
+    OUnit.assert_bool "not 13 leq 5" (not (I.leq bjoin b2))
+
+  let test_leq_2 _ =
+    let b1 = I.of_int ik (of_int 7) in
+
+    OUnit.assert_bool "bot leq 7" (I.leq (I.bot_of ik) b1);
+    OUnit.assert_bool "7 leq top" (I.leq b1 (I.top_of ik))
+
+  let test_wrap_1 _ =
+    let z = of_int 31376 in
+    let b_uint8 = I.of_int IUChar z in
+    let b_sint8 = I.of_int IUChar z in
+    let b_uint16 = I.of_int IUShort z in
+    let b_sint16 = I.of_int IUShort z in
+
+    (* See https://www.simonv.fr/TypesConvert/?integers *)
+    assert_equal (I.of_int IUChar (of_int 144)) b_uint8;
+    assert_equal (I.of_int IUChar (of_int (-112))) b_sint8;
+    assert_equal (I.of_int IUShort (of_int 31376)) b_uint16;
+    assert_equal (I.of_int IUShort (of_int 31376)) b_sint16
+
+  let test_wrap_2 _ =
+    let z1 = of_int 30867 in
+    let z2 = of_int 30870 in
+    let join_cast_unsigned = I.join IUChar (I.of_int IUChar z1) (I.of_int IUChar z2) in
+
+    let expected_unsigned = I.join IUChar (I.of_int IUChar (of_int 147)) (I.of_int IUChar (of_int 150)) in
+
+    let expected_signed = I.join IUChar (I.of_int IUChar (of_int (-106))) (I.of_int IUChar (of_int (-109))) in
+
+    assert_equal expected_unsigned join_cast_unsigned;
+    assert_equal expected_signed join_cast_unsigned
+
+  let test_widen_1 _ =
+    let b1 = I.of_int ik (of_int 3) in
+    let b2 = I.of_int ik (of_int 17) in
+
+    (* widen both masks *)
+    assert_equal (I.top_of ik) (I.widen ik b1 b2);
+
+    (* no widening *)
+    let bjoin = I.join ik b1 b2 in
+    assert_equal bjoin (I.widen ik bjoin b1)
+
+
+  let test_widen_2 _ =
+    let b1 = I.of_int ik (of_int 123613) in
+    let b2 = I.of_int ik (of_int 613261) in
+
+    (* no widening needed *)
+    assert_bool "join leq widen" (I.leq (I.join ik b1 b2) (I.widen ik b1 b2))
+
+  let assert_of_interval lb ub =
+    let intvl = (of_int lb, of_int ub) in 
+    let bf = I.of_interval ik intvl in
+    let print_err_message i = "Missing value: " ^ string_of_int i ^ " in [" ^ string_of_int lb ^ ", " ^ string_of_int ub ^ "]" in
+    for i = lb to ub do
+      assert_bool (print_err_message i) (I.equal_to (of_int i) bf = `Top)
+    done
+
+  let test_of_interval _ =
+    assert_of_interval 3 17;
+    assert_of_interval (-17) (-3);
+    assert_of_interval (-3) 17;
+    assert_of_interval (-17) 3
+
+  let test_of_bool _ =
+    let b1 = I.of_bool ik true in
+    let b2 = I.of_bool ik false in
+
+    assert_bool "true" (I.equal_to (of_int 1) b1 = `Eq);
+    assert_bool "false" (I.equal_to (of_int 0) b2 = `Eq)
+
+  let test_to_bool _ =
+    let ik = IUInt in
+    let b1 = I.of_int ik (of_int 3) in
+    let b2 = I.of_int ik (of_int (-6)) in
+    let b3 = I.of_int ik (of_int 0) in
+
+    let b12 = I.join ik b1 b2 in
+    let b13 = I.join ik b1 b3 in
+    let b23 = I.join ik b2 b3 in
+
+    assert_bool "3" (I.to_bool b1 = Some true);
+    assert_bool "-6" (I.to_bool b2 = Some true);
+    assert_bool "0" (I.to_bool b3 = Some false);
+
+    assert_bool "3 | -6" (I.to_bool b12 = Some true);
+    assert_bool "3 | 0" (I.to_bool b13 = None);
+    assert_bool "-6 | 0" (I.to_bool b23 = None)
+
+  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 IUInt128 (of_int 1234)) (I.cast_to IUInt128 b1)
+
+  (* Bitwise  *)
+
+  let test_logxor _ =
+    let b1 = I.of_int ik (of_int 5) in
+    let b2 = I.of_int ik (of_int 17) in
+
+    assert_equal (I.of_int ik (of_int 20)) (I.logxor ik b1 b2);
+
+    let b12 = I.join ik b1 b2 in
+    let b3 = I.of_int ik (of_int 13) in
+    assert_bool "8 ?= 13 xor (5 | 17)" (I.equal_to (of_int 8) (I.logxor ik b12 b3) = `Top);
+    assert_bool "28 ?= 13 xor (5 | 17)" (I.equal_to (of_int 28) (I.logxor ik b12 b3) = `Top)
+
+  let test_logand _ =
+    let b1 = I.of_int ik (of_int 7) in
+    let b2 = I.of_int ik (of_int 13) in
+
+    assert_equal (I.of_int ik (of_int 5)) (I.logand ik b1 b2);
+
+    let b12 = I.join ik b1 b2 in
+    let b3 = I.of_int ik (of_int 12) in
+    assert_bool "4 ?= 12 and (7 | 12)" (I.equal_to (of_int 4) (I.logand ik b12 b3) = `Top);
+    assert_bool "12 ?= 12 and (7 | 12)" (I.equal_to (of_int 12) (I.logand ik b12 b3) = `Top)
+
+
+  let test_logor _ =
+    let b1 = I.of_int ik (of_int 5) in
+    let b2 = I.of_int ik (of_int 17) in
+
+    assert_equal (I.of_int ik (of_int 21)) (I.logor ik b1 b2);
+
+    let b12 = I.join ik b1 b2 in
+    let b3 = I.of_int ik (of_int 13) in
+    assert_bool "13 ?= 13 or (5 | 17)" (I.equal_to (of_int 13) (I.logor ik b12 b3) = `Top);
+    assert_bool "29 ?= 13 or (5 | 17)" (I.equal_to (of_int 29) (I.logor ik b12 b3) = `Top)
+
+  let test_lognot _ =
+    let b1 = I.of_int ik (of_int 4) in
+    let b2 = I.of_int ik (of_int 12) in
+
+    (* assumes two's complement *)
+    assert_equal (I.of_int ik (of_int (-5))) (I.lognot ik b1);
+
+    let b12= I.join ik b1 b2 in
+    assert_bool "-13 ?= not (4 | 12)" (I.equal_to (of_int (-13)) (I.lognot ik b12) = `Top);
+    assert_bool "-5 ?= not (4 | 12)" (I.equal_to (of_int (-5)) (I.lognot ik b12) = `Top)
+
+  let of_list ik is = List.fold_left (fun acc x -> I.join ik acc (I.of_int ik x)) (I.bot ()) is
+  let cart_op op a b = List.map (BatTuple.Tuple2.uncurry op) (BatList.cartesian_product a b)
+
+  let precision ik = snd @@ IntDomain.Size.bits ik
+  let over_precision ik = Int.succ @@ precision ik
+  let under_precision ik = Int.pred @@ precision ik
+
+  let assert_shift ?(rev_cond=false) ?(expected_ov_info=None) shift ik a b expected = 
+    let module I = I_ in
+    let symb, shift_op_bf, shift_op_int = match shift with
+      | `L -> "<<", I.shift_left ik, Int.shift_left
+      | `R -> ">>", I.shift_right ik, Int.shift_right
+    in
+    let of_list (is: int list) : I.t = of_list ik (List.map of_int is) in
+    let get_param x : I.t = match x with
+      | `B bf -> bf
+      | `I is -> of_list is
+    in
+    let string_of_param x = match x with
+      | `B bf -> I.show bf
+      | `I is -> Printf.sprintf "[%s]" (String.concat ", " @@ List.map string_of_int is)
+    in
+    let bf_a, bf_b, expected = get_param a, get_param b, get_param expected in
+    let result, ov_info = (shift_op_bf bf_a bf_b) in
+    let output_string = Printf.sprintf "test (%s) shift %s %s %s failed: was: %s but should%s be: %s"
+        (CilType.Ikind.show ik)
+        (string_of_param a) symb (string_of_param b)
+        (I.show result) (if rev_cond then " not" else "") (I.show expected)
+    in
+    let assertion = I.equal result expected in
+    let assertion = if rev_cond then not assertion else assertion in
+    assert_bool output_string assertion;
+    if Option.is_some expected_ov_info then
+      let ov_printer (ov_info : IntDomain.overflow_info) = Printf.sprintf "{underflow=%b; overflow=%b}" ov_info.underflow ov_info.overflow in
+      let err_msg = Printf.sprintf "In (%s) shift %s %s %s" (CilType.Ikind.show ik) (string_of_param a) symb (string_of_param b) in
+      OUnit.assert_equal ~msg:err_msg ~printer:ov_printer (Option.get expected_ov_info) ov_info
+
+
+  let assert_shift_left ?(rev_cond=false) ?(ov_info=None) = assert_shift ~rev_cond:rev_cond ~expected_ov_info:ov_info `L
+  let assert_shift_right ?(rev_cond=false) ?(ov_info=None) = assert_shift ~rev_cond:rev_cond ~expected_ov_info:ov_info `R
+
+  let gen_sized_set size_gen gen = 
+    let open QCheck2.Gen in
+    map (List.sort_uniq Int.compare) (list_size size_gen gen)
+
+  let test_shift ik name c_op a_op =
+    let shift_test_printer (a,b) = Printf.sprintf "a: [%s] b: [%s]"
+        (String.concat ", " (List.map string_of_int a))
+        (String.concat ", " (List.map string_of_int b))
+    in
+    let of_list ik is = of_list ik (List.map of_int is) in
+    let open QCheck2 in let open Gen in
+    let a_gen ik =
+      let min_ik, max_ik = Batteries.Tuple2.mapn Z.to_int (IntDomain.Size.range ik) in
+      gen_sized_set (1 -- precision ik) (min_ik -- max_ik)
+    in
+    let b_gen ik =
+      gen_sized_set (1 -- (Z.log2up @@ Z.of_int @@ precision ik)) (0 -- under_precision ik) (* only shifts that are smaller than precision *)
+    in
+    let test_case_gen = Gen.pair (a_gen ik) (b_gen ik)
+    in
+    Test.make ~name:name ~print:shift_test_printer
+      test_case_gen
+      (fun (a,b) ->
+         let expected_subset = cart_op c_op a b |> of_list ik in
+         let result = a_op ik (of_list ik a) (of_list ik b) in
+         I.leq expected_subset result
+      )
+
+  let test_shift_left = List.fold_left (fun acc ik -> test_shift ik
+                                           (Printf.sprintf "test_shift_left_ik_%s" (CilType.Ikind.show ik)) Int.shift_left I.shift_left :: acc
+                                       ) [] ik_lst |> QCheck_ounit.to_ounit2_test_list
+
+  let test_shift_right = List.fold_left (fun acc ik -> test_shift ik
+                                            (Printf.sprintf "test_shift_right_ik_%s" (CilType.Ikind.show ik)) Int.shift_right I.shift_right :: acc
+                                        ) [] ik_lst |> QCheck_ounit.to_ounit2_test_list
+
+  let bot = `B (I.bot ())
+  let top = `B (I.top ())
+
+  let isSigned = GoblintCil.Cil.isSigned
+
+  let max_of ik = Z.to_int @@ snd @@ IntDomain.Size.range ik
+  let min_of ik = Z.to_int @@ fst @@ IntDomain.Size.range ik
+
+  let ov_overflow : IntDomain.overflow_info option = Some ({underflow=false; overflow=true})
+  let ov_underflow : IntDomain.overflow_info option = Some ({underflow=true; overflow=false})
+  let no_ov : IntDomain.overflow_info option = Some ({underflow=false; overflow=false})
+
+  let one ik = I.of_int ik @@ Z.of_int 1
+
+  let test_shift_left =
+    let highest_bit_set ?(is_neg=false) ik =
+      let pos = Int.pred @@ snd @@ IntDomain.Size.bits ik in
+      (if isSigned ik && is_neg
+       then Z.neg @@ Z.shift_left Z.one pos
+       else Z.shift_left Z.one pos
+      ) |> Z.to_int
+    in
+    [
+      "property_test_shift_left" >::: test_shift_left;
+      "shift_left_edge_cases" >:: fun _ ->
+        assert_shift_left ik (`I [1]) (`I [1; 2]) (`I [1; 2; 4; 8]);
+        assert_shift_left ~ov_info:ov_underflow ik (`I [-1000]) (`I [64]) top;
+
+        List.iter (fun ik ->
+            assert_shift_left ik bot bot bot;
+
+            assert_shift_left ik (`I [0]) top (`I [0]);
+
+            if isSigned ik
+            then (
+              assert_shift_left ik (`I [1]) (`I [-1]) top; (* Negative shifts are undefined behavior *)
+              assert_shift_left ik (`I [-1]) top top;
+              assert_shift_left ik top (`I [-1]) top;
+
+              assert_shift_left ~ov_info:no_ov ik (`I [1]) (`I [under_precision ik]) (`I [highest_bit_set ik]);
+              assert_shift_left ~ov_info:ov_overflow ik (`I [1]) (`I [precision ik]) top;
+              assert_shift_left ~ov_info:ov_overflow ik (`I [1]) (`I [over_precision ik]) top;
+
+              assert_shift_left ~ov_info:no_ov ik (`I [-1]) (`I [under_precision ik]) (`I [highest_bit_set ~is_neg:true ik]);
+              assert_shift_left ~ov_info:no_ov ik (`I [-1]) (`I [precision ik]) (`I [Z.to_int @@ IntDomain.Size.cast ik @@ Z.shift_left Z.one (precision ik)]);
+              assert_shift_left ~ov_info:ov_underflow ik (`I [-1]) (`I [over_precision ik]) top;
+            ) else (
+              (* See C11 N2310 at 6.5.7 *)
+              assert_shift_left ~ov_info:no_ov ik (`I [1]) (`I [under_precision ik]) (`I [highest_bit_set ik]);
+              assert_shift_left ~ov_info:ov_overflow ik (`I [1]) (`I [precision ik]) (`I [0]);
+              assert_shift_left ~ov_info:ov_overflow ik (`I [1]) (`I [over_precision ik]) (`I [0]);
+            )
+
+          ) ik_lst
+    ]
+
+  let test_shift_right =
+    [
+      "property_test_shift_right" >::: test_shift_right;
+      "shift_right_edge_cases" >:: fun _ ->
+        assert_shift_right ik (`I [10]) (`I [1; 2]) (`I [10; 7; 5; 1]);
+
+        List.iter (fun ik ->
+            assert_shift_right ik bot bot bot;
+
+            assert_shift_right ik (`I [0]) top (`I [0]);
+
+            if isSigned ik
+            then (
+              assert_shift_right ~rev_cond:true ik (`I [max_of ik]) top top; (* the sign bit shouldn't be set with right shifts if its unset *)
+
+              assert_shift_right ik (`I [2]) (`I [-1]) top; (* Negative shifts are undefined behavior *)
+              assert_shift_right ik (`I [min_of ik]) top top; (* implementation-defined sign-bit handling *)
+
+              assert_shift_right ~ov_info:no_ov ik (`I [max_of ik]) (`I [under_precision ik]) (`I [1]);
+              assert_shift_right ~ov_info:no_ov ik (`I [max_of ik]) (`I [precision ik]) (`I [0]);
+              assert_shift_right ~ov_info:no_ov ik (`I [max_of ik]) (`I [over_precision ik]) (`I [0]);
+
+              assert_shift_right ~ov_info:no_ov ik ~rev_cond:true (`I [min_of ik]) (`I [under_precision ik]) top;
+              assert_shift_right ~ov_info:no_ov ik ~rev_cond:true (`I [min_of ik]) (`I [precision ik]) top;
+              assert_shift_right ~ov_info:no_ov ik (`I [min_of ik]) (`I [over_precision ik]) top;
+            ) else (
+              (* See C11 N2310 at 6.5.7 *)
+              assert_shift_right ~ov_info:no_ov ik (`I [max_of ik]) (`I [under_precision ik]) (`I [1]);
+              assert_shift_right ~ov_info:no_ov ik (`I [max_of ik]) (`I [precision ik]) (`I [0]);
+              assert_shift_right ~ov_info:no_ov ik (`I [max_of ik]) (`I [over_precision ik]) (`I [0]);
+            )
+
+          ) ik_lst
+
+    ]
+
+
+  (* Arith *)
+
+  let print_err_message bf1 bf2 bfr = 
+    I.show bfr ^ " on input " ^ I.show bf1 ^ " and " ^ I.show bf2
+
+  let ik_arithu = Cil.IUChar
+
+  let ik_ariths = Cil.IChar
+
+  let result_list op is1 is2 = List.concat (List.map (fun x -> List.map (op x) is2) is1)
+
+  let generate_test ?(debug=false) opc opa ik is1 is2 = 
+    let zs1 = List.map Z.of_int is1 in 
+    let zs2 = List.map Z.of_int is2 in 
+    let res = of_list ik (result_list opc zs1 zs2) in 
+    let bs1 = of_list ik zs1 in 
+    let bs2 = of_list ik zs2 in 
+    let bsr = opa ik bs1 bs2 in
+    OUnit2.assert_equal ~cmp:I.leq ~printer:(print_err_message bs1 bs2) res bsr
+
+  let c1 = [99]
+  let c2 = [186]
+  let c3 = [-64]
+  let c4 = [-104]
+
+  let is1 = [8; 45; 89; 128]
+  let is2 = [5; 69; 72; 192]
+  let is3 = [-11; -42; -99; -120]
+  let is4 = [-16; -64; -87; -111]
+  let is5 = [-64; -14; 22; 86]
+
+  let testsuite = [c1;c2;c3;c4;is1;is2;is3;is4]
+  let testsuite_unsigned = [c1;c2;is1;is2]
+
+  let arith_testsuite ?(debug=false) opc opa ts ik = 
+    List.iter (fun x -> List.iter (generate_test opc opa ik x) ts) ts
+
+  let test_add _ = 
+    let _ = arith_testsuite Z.add I.add testsuite ik_arithu in
+    let _ = arith_testsuite Z.add I.add testsuite ik_ariths in 
+    ()
+
+  let test_sub _ = 
+    let _ = arith_testsuite Z.sub I.sub testsuite ik_arithu in
+    let _ = arith_testsuite Z.sub I.sub testsuite ik_ariths in 
+    ()
+
+  let test_mul _ =     
+    let _ = arith_testsuite Z.mul I.mul testsuite ik_arithu in
+    let _ = arith_testsuite Z.mul I.mul testsuite ik_ariths in 
+    ()
+
+  let test_div _ = 
+    let _ = arith_testsuite Z.div I.div testsuite_unsigned ik_arithu in
+    let _ = arith_testsuite Z.div I.div testsuite IShort in 
+    ()
+
+  let test_rem _ = 
+    let _ = arith_testsuite Z.rem I.rem testsuite_unsigned ik_arithu in
+    let _ = arith_testsuite Z.rem I.rem testsuite IShort in 
+    ()
+
+  let test_neg _ = 
+    let print_neg_err_message bfi bfr = 
+      I.show bfr ^ " on input " ^ I.show bfi
+    in
+    let generate_test_neg opc opa ik is = 
+      let zs = List.map Z.of_int is in 
+      let res = of_list ik (List.map opc zs) in 
+      let bs = of_list ik zs in 
+      OUnit2.assert_equal ~cmp:I.leq ~printer:(print_neg_err_message bs) res (opa ik bs)
+    in 
+    let neg_testsuite opc opa ik = 
+      let testsuite = [c1;c2;c3;c4;is1;is2;is3;is4] in
+      List.map (generate_test_neg opc opa ik) testsuite
+    in
+    let _ = neg_testsuite Z.neg I.neg ik_arithu in
+    let _ = neg_testsuite Z.neg I.neg ik_ariths in 
+    ()
+
+  (* Comparisons *)
+
+  let test_eq _ =
+    let b1 = I.of_int ik (of_int 5) in
+    let b2 = I.of_int ik (of_int 17) in
+
+    assert_bool "5 == 5" (I.eq ik b1 b1 = I.of_bool ik true);
+    assert_bool "5 == 17" (I.eq ik b1 b2 = I.of_bool ik false);
+
+    let b12 = I.join ik b1 b2 in
+    assert_bool "5 == (5 | 17)" (I.eq ik b1 b12 = (I.join ik (I.of_bool ik true) (I.of_bool ik false)))
+
+  let test_ne _ =
+    let b1 = I.of_int ik (of_int 5) in
+    let b2 = I.of_int ik (of_int 17) in
+
+    assert_bool "5 != 5" (I.ne ik b1 b1 = I.of_bool ik false);
+    assert_bool "5 != 17" (I.ne ik b1 b2 = I.of_bool ik true);
+
+    let b12 = I.join ik b1 b2 in
+    assert_bool "5 != (5 | 17)" (I.ne ik b1 b12 = (I.join ik (I.of_bool ik false) (I.of_bool ik true)))
+
+  let test_le _ =
+    let b1 = I.of_int ik (of_int 5) in
+    let b2 = I.of_int ik (of_int 14) in
+
+    assert_bool "5 <= 5" (I.le ik b1 b1 = I.of_bool ik true);
+    assert_bool "5 <= 14" (I.le ik b1 b2 = I.of_bool ik true);
+    assert_bool "14 <= 5" (I.le ik b2 b1 = I.of_bool ik false);
+
+    let b12 = I.join ik b1 b2 in
+
+    let b3 = I.of_int ik (of_int 17) in
+    assert_bool "17 <= (5 | 14)" (I.le ik b3 b12 = I.of_bool ik false);
+
+    let b4 = I.of_int ik (of_int 13) in
+    assert_bool "13 <= (5 | 14)" (I.le ik b4 b12 = (I.join ik (I.of_bool ik false) (I.of_bool ik true)));
+
+    let b5 = I.of_int ik (of_int 5) in
+    assert_bool "5 <= (5 | 14)" (I.le ik b5 b12 = I.join ik (I.of_bool ik true) (I.of_bool ik false));
+
+    let b6 = I.of_int ik (of_int 4) in
+    assert_bool "4 <= (5 | 14)" (I.le ik b6 b12 = I.of_bool ik true)
+
+
+  let test_ge _ =
+    let b1 = I.of_int ik (of_int 5) in
+    let b2 = I.of_int ik (of_int 14) in
+
+    assert_bool "5 >= 5" (I.ge ik b1 b1 = I.of_bool ik true);
+    assert_bool "5 >= 14" (I.ge ik b1 b2 = I.of_bool ik false);
+    assert_bool "14 >= 5" (I.ge ik b2 b1 = I.of_bool ik true);
+
+    let b12 = I.join ik b1 b2 in
+
+    let b3 = I.of_int ik (of_int 2) in
+    assert_bool "2 >= (5 | 14)" (I.ge ik b3 b12 = I.of_bool ik false);
+
+    let b4 = I.of_int ik (of_int 13) in
+    assert_bool "13 >= (5 | 14)" (I.ge ik b4 b12 = (I.join ik (I.of_bool ik true) (I.of_bool ik false)));
+
+    let b6 = I.of_int ik (of_int 15) in
+    assert_bool "15 >= (5 | 14)" (I.ge ik b6 b12 = I.of_bool ik true)
+
+  let test_lt _ =
+    let b1 = I.of_int ik (of_int 7) in
+    let b2 = I.of_int ik (of_int 13) in
+
+    assert_bool "7 < 7" (I.lt ik b1 b1 = I.of_bool ik false);
+    assert_bool "7 < 13" (I.lt ik b1 b2 = I.of_bool ik true);
+
+    let b12 = I.join ik b1 b2 in
+    let b3 = I.of_int ik (of_int 4) in
+    assert_bool "4 < (7 | 13)" (I.lt ik b3 b12 = I.of_bool ik true);
+
+    let b4 = I.of_int ik (of_int 8) in
+    assert_bool "8 < (7 | 13)" (I.lt ik b4 b12 = I.join ik (I.of_bool ik false) (I.of_bool ik true))
+
+  let test_gt _ =
+    let b1 = I.of_int ik (of_int 5) in
+    let b2 = I.of_int ik (of_int 14) in
+
+    assert_bool "5 > 5" (I.gt ik b1 b1 = I.of_bool ik false);
+    assert_bool "5 > 14" (I.gt ik b1 b2 = I.of_bool ik false);
+    assert_bool "14 > 5" (I.gt ik b2 b1 = I.of_bool ik true);
+
+    let b12 = I.join ik b1 b2 in
+
+    let b3 = I.of_int ik (of_int 2) in
+    assert_bool "2 > (5 | 14)" (I.gt ik b3 b12 = I.of_bool ik false);
+
+    let b4 = I.of_int ik (of_int 13) in
+    assert_bool "13 > (5 | 14)" (I.gt ik b4 b12 = (I.join ik (I.of_bool ik false) (I.of_bool ik true)));
+
+    let b5 = I.of_int ik (of_int 5) in
+    assert_bool "5 > (5 | 14)" (I.gt ik b5 b12 = I.join ik (I.of_bool ik false) (I.of_bool ik true));
+
+    let b6 = I.of_int ik (of_int 4) in
+    assert_bool "4 > (5 | 14)" (I.gt ik b6 b12 = (I.of_bool ik false) )
+
+  let test_starting _ =
+    let bf1 = I.starting ik (of_int 17) in
+
+    assert_bool "17" (I.equal_to (of_int 17) bf1 = `Top);
+    assert_bool "18" (I.equal_to (of_int 18) bf1 = `Top);
+
+    assert_bool "-3" (I.equal_to (of_int (-3)) bf1 = `Neq);
+
+    let bf2 = I.starting ik (of_int (-17)) in
+
+    assert_bool "-16" (I.equal_to (of_int (-16)) bf2 = `Top);
+    assert_bool "-17" (I.equal_to (of_int (-17)) bf2 = `Top)
+
+
+  let test_ending _ =
+    let bf = I.ending ik (of_int 17) in
+
+    assert_bool "-4" (I.equal_to (of_int (-4)) bf = `Top);
+    assert_bool "16" (I.equal_to (of_int 16) bf = `Top);
+
+    let bf2 = I.ending ik (of_int (-17)) in
+
+    assert_bool "-16" (I.equal_to (of_int (-16)) bf2 = `Top);
+    assert_bool "-18" (I.equal_to (of_int (-18)) bf2 = `Top);
+
+    assert_bool "17" (I.equal_to (of_int 17) bf2 = `Neq)
+
+  let test_refine_with_congruence _ =
+    let bf = I.top_of ik in
+
+    let bf_refined1= I.refine_with_congruence ik bf (Some (Z.of_int 3, Z.of_int 4)) in
+    assert_bool "3" (I.equal_to (of_int 3) bf_refined1 = `Top);
+    let bf_refined3= I.refine_with_congruence ik bf (Some (Z.of_int 5, Z.of_int 0)) in
+    assert_bool "5" (I.equal_to (of_int 5) bf_refined3 = `Eq)
+
+  let test_refine_with_inclusion_list _ =
+    let bf = I.top_of ik in
+
+    let list = List.map of_int [-2;3;23; 26] in
+    let bf_refined = I.refine_with_incl_list ik bf (Some list) in
+
+    List.iter (fun i -> assert_bool (Z.to_string i) (I.equal_to i bf_refined = `Top)) list
+
+  (*
+  let test_refine_with_exclusion_list _ = failwith "TODO"
+  *)
+
+  let test () =[
+    "test_of_int_to_int" >:: test_of_int_to_int;
+    "test_to_int_of_int" >:: test_to_int_of_int;
+    "test_equal_to" >:: test_equal_to;
+
+    "test_join" >:: test_join;
+    "test_meet" >:: test_meet;
+
+    "test_leq_1" >:: test_leq_1;
+    "test_leq_2" >:: test_leq_2;
+
+    "test_wrap_1" >:: test_wrap_1;
+    "test_wrap_2" >:: test_wrap_2;
+
+    "test_widen_1" >:: test_widen_1;
+    "test_widen_2" >:: test_widen_2;
+
+
+    "test_of_interval" >:: test_of_interval;
+    "test_of_bool" >:: test_of_bool;
+    "test_to_bool" >:: test_to_bool;
+    "test_cast_to" >:: test_cast_to;
+
+    "test_logxor" >:: test_logxor;
+    "test_logand" >:: test_logand;
+    "test_logor" >:: test_logor;
+    "test_lognot" >:: test_lognot;
+
+    "test_shift_left" >::: test_shift_left;
+    "test_shift_right" >::: test_shift_right;
+
+    "test_add" >:: test_add;
+    "test_sub" >:: test_sub;
+    "test_mul" >:: test_mul;
+    "test_div" >:: test_div;
+    "test_rem" >:: test_rem;
+
+
+    "test_eq" >:: test_eq;
+    "test_ne" >:: test_ne;
+    "test_le" >:: test_le;
+    "test_ge" >:: test_ge;
+    "test_lt" >:: test_lt;
+    "test_gt" >:: test_gt;
+
+    "test_starting" >:: test_starting;
+    "test_ending" >:: test_ending;
+
+    "test_refine_with_congruence" >:: test_refine_with_congruence;
+    "test_refine_with_inclusion_list" >:: test_refine_with_inclusion_list;    
+  ]
+
+end
+
 module Interval    = IntervalTest (IntDomain.Interval)
+module Bitfield    = BitfieldTest (IntDomain.Bitfield)
 module IntervalSet = IntervalTest (IntDomain.IntervalSet)
 
 module Congruence =
@@ -320,6 +990,7 @@ struct
     ]
 end
 
+
 let test () =
   "intDomainTest" >::: [
     "int_Integers"  >::: A.test ();
@@ -330,6 +1001,7 @@ let test () =
     "test_meet"     >::  test_meet;
     "test_excl_list">::  test_ex_set;
     "interval" >::: Interval.test ();
+    "bitfield" >::: Bitfield.test ();
     "intervalSet" >::: IntervalSet.test ();
     "congruence" >::: Congruence.test ();
     "intDomTuple" >::: IntDomTuple.test ();
diff --git a/tests/unit/maindomaintest.ml b/tests/unit/maindomaintest.ml
index 4b379a252f..b6af01ff6f 100644
--- a/tests/unit/maindomaintest.ml
+++ b/tests/unit/maindomaintest.ml
@@ -46,6 +46,7 @@ let intDomains: (module IntDomainProperties.S) list = [
   (module IntDomain.Enums);
   (module IntDomain.Congruence);
   (module IntDomain.SOverflowUnlifter(IntDomain.IntervalSet));
+  (module IntDomain.SOverflowUnlifter(IntDomain.Bitfield));
   (* (module IntDomain.Flattened); *)
   (* (module IntDomain.Interval32); *)
   (* (module IntDomain.Booleans); *)