diff --git a/src/cdomain/value/cdomains/int/bitfieldDomain.ml b/src/cdomain/value/cdomains/int/bitfieldDomain.ml
index c6de18b9d5..928c4a876d 100644
--- a/src/cdomain/value/cdomains/int/bitfieldDomain.ml
+++ b/src/cdomain/value/cdomains/int/bitfieldDomain.ml
@@ -193,7 +193,7 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): Bitfield_SOverflow with type in
   (* bot = all bits are invalid *)
   let bot () = (BArith.zero_mask, BArith.zero_mask)
 
-  let top_of ik =
+  let top_of ?bitfield ik = (* TODO: use bitfield *)
     if GoblintCil.isSigned ik then top ()
     else (BArith.one_mask, Ints_t.of_bigint (snd (Size.range ik)))
 
diff --git a/src/cdomain/value/cdomains/int/congruenceDomain.ml b/src/cdomain/value/cdomains/int/congruenceDomain.ml
index 843949c254..178481089c 100644
--- a/src/cdomain/value/cdomains/int/congruenceDomain.ml
+++ b/src/cdomain/value/cdomains/int/congruenceDomain.ml
@@ -44,7 +44,7 @@ struct
   let range ik = Size.range ik
 
   let top () = Some (Z.zero, Z.one)
-  let top_of ik = Some (Z.zero, Z.one)
+  let top_of ?bitfield ik = Some (Z.zero, Z.one)
   let bot () = None
   let bot_of ik = bot ()
 
diff --git a/src/cdomain/value/cdomains/int/defExcDomain.ml b/src/cdomain/value/cdomains/int/defExcDomain.ml
index 00edc185cd..5fb96403a2 100644
--- a/src/cdomain/value/cdomains/int/defExcDomain.ml
+++ b/src/cdomain/value/cdomains/int/defExcDomain.ml
@@ -84,9 +84,14 @@ struct
   let overflow_range = R.of_interval range_ikind (-999L, 999L) (* Since there is no top ikind we use a range that includes both IInt128 [-127,127] and IUInt128 [0,128]. Only needed for intermediate range computation on longs. Correct range is set by cast. *)
   let top_overflow () = `Excluded (S.empty (), overflow_range)
   let bot () = `Bot
-  let top_of ik = `Excluded (S.empty (), size ik)
+  let top_of ?bitfield ik = match bitfield with
+    | Some b when b <= Z.numbits (Size.range ik |> snd) ->
+      let range = match Cil.isSigned ik with
+        | true ->  R.of_interval range_ikind (Int64.of_int @@ -(b-1), Int64.of_int b)
+        | false -> R.of_interval range_ikind (Int64.of_int 0, Int64.of_int b) in
+      `Excluded (S.empty (), range)
+    | _ -> `Excluded (S.empty (), size ik)
   let bot_of ik = bot ()
-
   let show x =
     let short_size x = "("^R.show x^")" in
     match x with
@@ -447,20 +452,47 @@ struct
 
   let ge ik x y = le ik y x
 
-  let lognot = lift1 Z.lognot
+  let lognot ik x = norm ik @@ match x with
+    | `Excluded (s,r) ->
+      let s' = S.map Z.lognot s in
+      let r' = match R.minimal r, R.maximal r with
+        | Some min, Some max when (Int64.compare (Int64.neg max) Int64.zero <= 0 ) && (Int64.compare (Int64.neg min) Int64.zero > 0) -> 
+          R.of_interval range_ikind (Int64.neg max, Int64.neg min)  
+        | _ -> apply_range Z.lognot r
+      in
+      `Excluded (s', r')
+    | `Definite x -> `Definite (Z.lognot x)
+    | `Bot -> `Bot
 
   let logand ik x y = norm ik (match x,y with
-      (* We don't bother with exclusion sets: *)
-      | `Excluded _, `Definite i ->
-        (* Except in two special cases *)
+      | `Excluded (_, r), `Definite i
+      | `Definite i, `Excluded (_, r) ->
         if Z.equal i Z.zero then
           `Definite Z.zero
         else if Z.equal i Z.one then
           of_interval IBool (Z.zero, Z.one)
         else
-          top_of ik
-      | `Definite _, `Excluded _
-      | `Excluded _, `Excluded _ -> top_of ik
+          (match (R.minimal r, R.maximal r) with
+           | (None, _) | (_, None) -> top_of ik
+           | (Some r1, Some r2) ->
+             match Z.compare i Z.zero >= 0, Int64.compare r1 Int64.zero >= 0 with
+             | true, true ->`Excluded (S.empty (), R.of_interval range_ikind (Int64.zero, Int64.min r2 (Int64.of_int @@ Z.numbits i)))
+             | true, _ -> `Excluded (S.empty (), R.of_interval range_ikind (Int64.zero, Int64.of_int @@ Z.numbits i))
+             | _, true -> `Excluded (S.empty (), R.of_interval range_ikind (Int64.zero, r2))
+             | _, _ -> let b = Int64.max (Int64.of_int @@ Z.numbits i) (Int64.max (Int64.abs r1) (Int64.abs r2)) in
+               `Excluded (S.empty (), R.of_interval range_ikind (Int64.neg b, b))               
+          )
+      | `Excluded (_, p), `Excluded (_, r) -> begin
+          match R.minimal p, R.maximal p, R.minimal r, R.maximal r with
+          | Some p1, Some p2, Some r1, Some r2 -> begin
+              match Int64.compare p1 Int64.zero >= 0, Int64.compare r1 Int64.zero >= 0 with
+              | true, true -> `Excluded (S.empty (), R.of_interval range_ikind (Int64.zero, Int64.min p2 r2))
+              | true, _ -> `Excluded (S.empty (), R.of_interval range_ikind (Int64.zero, p2))
+              | _, true -> `Excluded (S.empty (), R.of_interval range_ikind (Int64.zero, r2))
+              | _ -> `Excluded (S.empty (), R.join p r)            
+            end
+          | _ -> top_of ik
+        end
       (* The good case: *)
       | `Definite x, `Definite y ->
         (try `Definite (Z.logand x y) with | Division_by_zero -> top_of ik)
@@ -469,9 +501,52 @@ struct
         (* If only one of them is bottom, we raise an exception that eval_rv will catch *)
         raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y))))
 
+  let logor ik x y = norm ik (match x,y with
+      | `Excluded (_, r), `Definite i
+      | `Definite i, `Excluded (_, r) ->
+        if Z.compare i Z.zero >= 0 then
+          `Excluded (S.empty (), R.join r (R.of_interval range_ikind (Int64.zero, Int64.of_int @@ Z.numbits i)))
+        else
+          (match R.minimal r, R.maximal r with
+           | None, _ | _, None -> top_of ik
+           | Some r1, Some r2 -> let b = Int64.max (Int64.of_int @@ Z.numbits i) (Int64.max (Int64.abs r1) (Int64.abs r2)) in
+             `Excluded (S.empty (), R.of_interval range_ikind (Int64.neg b, b))
+          )
+      | `Excluded (_, r1), `Excluded (_, r2) -> `Excluded (S.empty (), R.join r1 r2)
+      | `Definite x, `Definite y ->
+        (try `Definite (Z.logor x y) with | Division_by_zero -> top_of ik)
+      | `Bot, `Bot -> `Bot
+      | _ ->
+        (* If only one of them is bottom, we raise an exception that eval_rv will catch *)
+        raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y))))
 
-  let logor  = lift2 Z.logor
-  let logxor = lift2 Z.logxor
+  let logxor ik x y = norm ik (match x,y with
+      | `Definite i, `Excluded (_, r)
+      | `Excluded (_, r), `Definite i -> begin
+          match R.minimal r, R.maximal r with
+          | None, _ | _, None -> top_of ik
+          | Some r1, Some r2 -> let b = Int64.max (Int64.of_int @@ Z.numbits i) (Int64.max (Int64.abs r1) (Int64.abs r2)) in
+            if Int64.compare r1 Int64.zero >= 0 && Z.compare i Z.zero >= 0 then
+              `Excluded (S.empty (), R.of_interval range_ikind (Int64.zero, b))
+            else 
+              `Excluded (S.empty (), R.of_interval range_ikind (Int64.neg b, b))
+        end
+      | `Excluded (_, p), `Excluded (_, r) -> begin
+          match R.minimal p, R.maximal p, R.minimal r, R.maximal r with
+          | Some p1, Some p2, Some r1, Some r2 -> let b = List.fold_left Int64.max Int64.zero (List.map Int64.abs [p1;p2;r1;r2]) in
+            if Int64.compare p1 Int64.zero >= 0 && Int64.compare r1 Int64.zero >= 0 then 
+              `Excluded (S.empty (), R.of_interval range_ikind (Int64.zero, Int64.max p2 r2))
+            else
+              `Excluded (S.empty (), R.of_interval range_ikind (Int64.neg b, b))
+          | _ -> top_of ik
+        end
+      (* The good case: *)
+      | `Definite x, `Definite y ->
+        (try `Definite (Z.logxor x y) with | Division_by_zero -> top_of ik)
+      | `Bot, `Bot -> `Bot
+      | _ ->
+        (* If only one of them is bottom, we raise an exception that eval_rv will catch *)
+        raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y))))
 
   let shift (shift_op: int_t -> int -> int_t) (ik: Cil.ikind) (x: t) (y: t) =
     (* BigInt only accepts int as second argument for shifts; perform conversion here *)
diff --git a/src/cdomain/value/cdomains/int/enumsDomain.ml b/src/cdomain/value/cdomains/int/enumsDomain.ml
index 8a681d7e7f..fb44f34e0d 100644
--- a/src/cdomain/value/cdomains/int/enumsDomain.ml
+++ b/src/cdomain/value/cdomains/int/enumsDomain.ml
@@ -21,10 +21,17 @@ module Enums : S with type int_t = Z.t = struct
   let bot () = failwith "bot () not implemented for Enums"
   let bot_of ik = Inc (BISet.empty ())
   let top_bool = Inc (BISet.of_list [Z.zero; Z.one])
-  let top_of ik =
+
+  let top_of ?bitfield ik =
     match ik with
     | IBool -> top_bool
-    | _ -> Exc (BISet.empty (), size ik)
+    | _ -> match bitfield with 
+      | Some b when b <= Z.numbits(Size.range ik |> snd) -> 
+        Exc (BISet.empty (), match Cil.isSigned ik with
+          | true -> R.of_interval range_ikind (Int64.of_int @@ -(b-1), Int64.of_int b)
+          | false -> R.of_interval range_ikind (Int64.of_int 0, Int64.of_int b)
+          )
+      | _ -> Exc (BISet.empty (), size ik)
 
   let range ik = Size.range ik
 
@@ -209,10 +216,102 @@ module Enums : S with type int_t = Z.t = struct
 
   let rem = lift2 Z.rem
 
-  let lognot = lift1 Z.lognot
-  let logand = lift2 Z.logand
-  let logor  = lift2 Z.logor
-  let logxor = lift2 Z.logxor
+  let apply_range f r = (* apply f to the min/max of the old range r to get a new range *)
+    (* If the Int64 might overflow on us during computation, we instead go to top_range *)
+    match R.minimal r, R.maximal r with
+    | _ ->
+      let rf m = (size % Size.min_for % f) (m r) in
+      let r1, r2 = rf Exclusion.min_of_range, rf Exclusion.max_of_range in
+      R.join r1 r2
+
+  let lognot ikind v = norm ikind @@ match v with
+    | Inc x when BISet.is_empty x -> v 
+    | Inc x when BISet.is_singleton x -> Inc (BISet.singleton (Z.lognot (BISet.choose x)))
+    | Inc x -> Inc (BISet.map Z.lognot x)
+    | Exc (s,r) -> 
+      let s' = BISet.map Z.lognot s in
+      let r' = match R.minimal r, R.maximal r with
+        | Some min, Some max -> R.of_interval range_ikind (Int64.neg max, Int64.neg min) 
+        | _ -> apply_range Z.lognot r
+      in
+      Exc (s', r')
+
+  let logand ikind u v = 
+    handle_bot u v (fun () ->
+        norm ikind @@ match u, v with
+        | Inc x,Inc y when BISet.is_singleton x && BISet.is_singleton y -> Inc (BISet.singleton (Z.logand (BISet.choose x) (BISet.choose y)))
+        | Inc x, Exc (s,r)
+        | Exc (s,r), Inc x -> 
+          let f = fun i -> 
+            (match (R.minimal r, R.maximal r) with
+             | (None, _) | (_, None) -> R.top_of ikind
+             | (Some r1, Some r2) ->
+               match Z.compare i Z.zero >= 0, Int64.compare r1 Int64.zero >= 0 with
+               | true, true -> R.of_interval range_ikind (Int64.zero, Int64.min r2 (Int64.of_int @@ Z.numbits i))
+               | true, _ -> R.of_interval range_ikind (Int64.zero, Int64.of_int @@ Z.numbits i)
+               | _, true -> R.of_interval range_ikind (Int64.zero, r2)
+               | _, _ -> let b = Int64.max (Int64.of_int @@ Z.numbits i) (Int64.max (Int64.abs r1) (Int64.abs r2)) in
+                 R.of_interval range_ikind (Int64.neg b, b)             
+            ) in 
+          let r' = BISet.fold (fun i acc -> R.join (f i) acc) x (R.bot ()) in 
+          Exc (BISet.empty (), r')
+        | Exc (_, p), Exc (_, r) -> 
+          (match R.minimal p, R.maximal p, R.minimal r, R.maximal r with
+           | Some p1, Some p2, Some r1, Some r2 -> begin
+               match Int64.compare p1 Int64.zero >= 0, Int64.compare r1 Int64.zero >= 0 with
+               | true, true -> Exc (BISet.empty (), R.of_interval range_ikind (Int64.zero, Int64.min p2 r2))
+               | true, _ -> Exc (BISet.empty (), R.of_interval range_ikind (Int64.zero, p2))
+               | _, true -> Exc (BISet.empty (), R.of_interval range_ikind (Int64.zero, r2))
+               | _ -> Exc (BISet.empty (), R.join p r)            
+             end
+           | _ -> top_of ikind)
+        | _,_ -> top_of ikind)
+
+  let logor ikind u v = handle_bot u v (fun () -> 
+      norm ikind @@ match u, v with
+      | Inc x,Inc y when BISet.is_singleton x && BISet.is_singleton y -> Inc (BISet.singleton (Z.logor (BISet.choose x) (BISet.choose y)))
+      | Inc x, Exc (_,r)
+      | Exc (_,r), Inc x ->
+        let f = fun i -> 
+          if Z.compare i Z.zero >= 0 then
+            R.join r (R.of_interval range_ikind (Int64.zero, Int64.of_int @@ Z.numbits i))
+          else
+            (match R.minimal r, R.maximal r with
+             | None, _ | _, None -> R.top_of ikind
+             | Some r1, Some r2 -> let b = Int64.max (Int64.of_int @@ Z.numbits i) (Int64.max (Int64.abs r1) (Int64.abs r2)) in
+               R.of_interval range_ikind (Int64.neg b, b)
+            ) in 
+        let r' = BISet.fold (fun i acc -> R.join (f i) acc) x (R.bot ()) in
+        Exc (BISet.empty (), r')
+      | Exc (_, r1), Exc (_, r2) -> Exc (BISet.empty (), R.join r1 r2)
+      | _ -> top_of ikind)
+
+  let logxor ikind u v = handle_bot u v (fun () ->
+      norm ikind @@ match u, v with
+      | Inc x,Inc y when BISet.is_singleton x && BISet.is_singleton y -> Inc (BISet.singleton (Z.logxor (BISet.choose x) (BISet.choose y)))
+      | Inc x, Exc (_,r)
+      | Exc (_,r), Inc x -> 
+        let f = fun i -> 
+          match R.minimal r, R.maximal r with
+          | None, _ | _, None -> R.top_of ikind 
+          | Some r1, Some r2 -> let b = Int64.max (Int64.of_int @@ Z.numbits i) (Int64.max (Int64.abs r1) (Int64.abs r2)) in
+            if Int64.compare r1 Int64.zero >= 0 && Z.compare i Z.zero >= 0 then
+              R.of_interval range_ikind (Int64.zero, b)
+            else 
+              R.of_interval range_ikind (Int64.neg b, b)
+        in 
+        let r' = BISet.fold (fun i acc -> R.join (f i) acc) x (R.bot ()) in 
+        Exc (BISet.empty (), r')
+      | Exc (_, p), Exc (_, r) -> begin
+          match R.minimal p, R.maximal p, R.minimal r, R.maximal r with
+          | Some p1, Some p2, Some r1, Some r2 -> let b = List.fold_left Int64.max Int64.zero (List.map Int64.abs [p1;p2;r1;r2]) in
+            if Int64.compare p1 Int64.zero >= 0 && Int64.compare r1 Int64.zero >= 0 then 
+              Exc (BISet.empty (), R.of_interval range_ikind (Int64.zero, Int64.max p2 r2))
+            else
+              Exc (BISet.empty (), R.of_interval range_ikind (Int64.neg b, b))
+          | _ -> top_of ikind
+        end
+      | _ -> top_of ikind)
 
   let shift (shift_op: int_t -> int -> int_t) (ik: Cil.ikind) (x: t) (y: t) =
     handle_bot x y (fun () ->
diff --git a/src/cdomain/value/cdomains/int/intDomTuple.ml b/src/cdomain/value/cdomains/int/intDomTuple.ml
index 64f251de46..249d9457ff 100644
--- a/src/cdomain/value/cdomains/int/intDomTuple.ml
+++ b/src/cdomain/value/cdomains/int/intDomTuple.ml
@@ -38,6 +38,7 @@ module IntDomTupleImpl = struct
 
   (* only first-order polymorphism on functions -> use records to get around monomorphism restriction on arguments *)
   type 'b poly_in  = { fi  : 'a. 'a m -> 'b -> 'a } [@@unboxed] (* inject *)
+  type 'b poly_in_bitfield  = { fi_bitfield  : 'a. 'a m ->  ?bitfield:int -> 'b -> 'a } [@@unboxed] (* inject *)
   type 'b poly2_in  = { fi2  : 'a. 'a m2 -> 'b -> 'a } [@@unboxed] (* inject for functions that depend on int_t *)
   type 'b poly2_in_ovc  = { fi2_ovc  : 'a. 'a m2 -> 'b -> 'a * overflow_info} [@@unboxed] (* inject for functions that depend on int_t *)
 
@@ -115,7 +116,7 @@ module IntDomTupleImpl = struct
 
   (* f0: constructors *)
   let bot () = create { fi = fun (type a) (module I:SOverflow with type t = a) -> I.bot } ()
-  let top_of = create { fi = fun (type a) (module I:SOverflow with type t = a) -> I.top_of }
+  let top_of ?bitfield = create { fi = fun (type a) (module I:SOverflow with type t = a) -> I.top_of ?bitfield }
   let bot_of = create { fi = fun (type a) (module I:SOverflow with type t = a) -> I.bot_of }
   let of_bool ik = create { fi = fun (type a) (module I:SOverflow with type t = a) -> I.of_bool ik }
   let of_excl_list ik = create2 { fi2 = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.of_excl_list ik}
diff --git a/src/cdomain/value/cdomains/int/intervalDomain.ml b/src/cdomain/value/cdomains/int/intervalDomain.ml
index 78dcec85ca..e98650436f 100644
--- a/src/cdomain/value/cdomains/int/intervalDomain.ml
+++ b/src/cdomain/value/cdomains/int/intervalDomain.ml
@@ -1,4 +1,5 @@
 open IntDomain0
+open GoblintCil
 
 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
@@ -9,7 +10,16 @@ struct
 
   let range ik = BatTuple.Tuple2.mapn Ints_t.of_bigint (Size.range ik)
 
-  let top_of ik = Some (range ik)
+  let top_of ?bitfield ik = match bitfield with
+    | Some b when b <= Ints_t.to_int (range ik |> snd) -> begin
+        let signed_lower_bound = Ints_t.neg @@ Ints_t.shift_left Ints_t.one (b-1) in
+        let unsigned_upper_bound = Ints_t.sub (Ints_t.shift_left Ints_t.one b) Ints_t.one in
+        match Cil.isSigned ik with
+        (* An "int" can also store unsigned int values in a bit-field. Goblint doesn't differentiate between implicit and explicit signed ints.*)
+        | true -> Some (signed_lower_bound, unsigned_upper_bound)
+        | false -> Some (Ints_t.zero, unsigned_upper_bound)
+      end
+    | _ -> Some (range ik)
   let bot () = None
   let bot_of ik = bot () (* TODO: improve *)
 
@@ -214,32 +224,107 @@ struct
       | Some x, Some y -> (try of_int ik (f ik x y) with Division_by_zero | Invalid_argument _ -> (top_of ik,{underflow=false; overflow=false}))
       | _              -> (top_of ik,{underflow=true; overflow=true})
 
-  let logxor = bit (fun _ik -> Ints_t.logxor)
+  let min_val_bit_constrained n = 
+    if Ints_t.equal n Ints_t.zero then 
+      Ints_t.neg Ints_t.one 
+    else 
+      Ints_t.neg @@ Ints_t.shift_left Ints_t.one (Z.numbits (Z.sub (Z.abs @@ Ints_t.to_bigint n) Z.one)) 
+
+  let max_val_bit_constrained n = 
+    let x = if Ints_t.compare n Ints_t.zero < 0 then Ints_t.sub (Ints_t.neg n) Ints_t.one else n in
+    Ints_t.sub (Ints_t.shift_left Ints_t.one (Z.numbits @@ Z.abs @@ Ints_t.to_bigint x)) Ints_t.one
+
+  let logxor ik i1 i2 =
+    match bit (fun _ik -> Ints_t.logxor) ik i1 i2 with
+    | result when result <> top_of ik && result <> bot_of ik -> result
+    | _ ->
+      match i1, i2 with
+      | Some (x1, x2), Some (y1, y2) ->
+        let is_nonneg x = Ints_t.compare x Ints_t.zero >= 0 in
+        (match is_nonneg x1, is_nonneg x2, is_nonneg y1, is_nonneg y2 with
+         | true, _, true, _ ->
+           of_interval ik (Ints_t.zero, max_val_bit_constrained @@ Ints_t.max x2 y2) |> fst
+         | _, false, _, false ->
+           let upper = max_val_bit_constrained @@ Ints_t.min x1 y1 in
+           of_interval ik (Ints_t.zero, upper) |> fst
+         | true, _, _, false | _, false, true, _ ->
+           let lower = List.fold_left Ints_t.min Ints_t.zero 
+               (List.append (List.map min_val_bit_constrained [x1; y1]) 
+                  (List.map (fun i -> Ints_t.neg @@ Ints_t.add (max_val_bit_constrained i) Ints_t.one) [x2; y2])) in 
+           of_interval ik (lower, Ints_t.zero) |> fst
+         | _ -> let lower = List.fold_left Ints_t.min Ints_t.zero 
+                    (List.append (List.map min_val_bit_constrained [x1; y1]) 
+                       (List.map (fun i -> Ints_t.neg @@ Ints_t.add (max_val_bit_constrained i) Ints_t.one) [x2; y2])) in 
+           let upper = List.fold_left Ints_t.max Ints_t.zero (List.map max_val_bit_constrained [x1;x2;y1;y2]) in
+           of_interval ik (lower, upper) |> fst)
+      | _ -> top_of ik
 
   let logand ik i1 i2 =
-    match is_bot i1, is_bot i2 with
-    | true, true -> bot_of ik
-    | true, _
-    | _   , true -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show i1) (show i2)))
+    match bit (fun _ik -> Ints_t.logand) ik i1 i2 with
+    | result when result <> top_of ik && result <> bot_of ik -> result
     | _ ->
-      match to_int i1, to_int i2 with
-      | Some x, Some y -> (try of_int ik (Ints_t.logand x y) |> fst with Division_by_zero -> top_of ik)
-      | _, Some y when Ints_t.equal y Ints_t.zero -> of_int ik Ints_t.zero |> fst
-      | _, Some y when Ints_t.equal y Ints_t.one -> of_interval ik (Ints_t.zero, Ints_t.one) |> fst
+      match i1, i2 with
+      | Some (x1, x2), Some (y1, y2) ->
+        let is_nonneg x = Ints_t.compare x Ints_t.zero >= 0 in
+        (match is_nonneg x1, is_nonneg x2, is_nonneg y1, is_nonneg y2 with
+         | true, _, true, _ ->
+           of_interval ik (Ints_t.zero, Ints_t.min x2 y2) |> fst
+         | _, false, _, false ->
+           of_interval ik (min_val_bit_constrained @@ Ints_t.min x1 y1, Ints_t.zero) |> fst
+         | true, _, _, _ -> of_interval ik (Ints_t.zero, x2) |> fst
+         | _, _, true, _ -> of_interval ik (Ints_t.zero, y2) |> fst
+         | _ ->
+           let lower = min_val_bit_constrained @@ Ints_t.min x1 y1 in
+           let upper = Ints_t.max x2 y2 in
+           of_interval ik (lower, upper) |> fst)
       | _ -> top_of ik
 
-  let logor  = bit (fun _ik -> Ints_t.logor)
+  let logor ik i1 i2 =
+    match bit (fun _ik -> Ints_t.logor) ik i1 i2 with
+    | result when result <> top_of ik && result <> bot_of ik -> result
+    | _ ->
+      match i1, i2 with
+      | Some (x1, x2), Some (y1, y2) ->
+        let is_nonneg x = Ints_t.compare x Ints_t.zero >= 0 in
+        (match is_nonneg x1, is_nonneg x2, is_nonneg y1, is_nonneg y2 with
+         | true, _, true, _ -> of_interval ik (Ints_t.max x1 y1, max_val_bit_constrained (Ints_t.max x2 y2)) |> fst
+         | _, false, _, false -> of_interval ik (Ints_t.max x1 y1, Ints_t.zero) |> fst
+         | _, false, _, _ -> of_interval ik (x1, Ints_t.zero) |> fst
+         | _, _, _, false -> of_interval ik (y1, Ints_t.zero) |> fst
+         |_ ->
+           let lower = Ints_t.min x1 y1 in
+           let upper = max_val_bit_constrained @@ Ints_t.max x2 y2 in
+           of_interval ik (lower, upper) |> fst)
+      | _ -> top_of ik
 
-  let bit1 f ik i1 =
+  let bit1 f ik i1 f' =
     if is_bot i1 then
       bot_of ik
     else
       match to_int i1 with
       | Some x -> of_int ik (f ik x) |> fst
-      | _      -> top_of ik
+      | _      -> f' ()
 
-  let lognot = bit1 (fun _ik -> Ints_t.lognot)
-  let shift_right = bitcomp (fun _ik x y -> Ints_t.shift_right x (Ints_t.to_int y))
+  let lognot ik i1 =
+    bit1 (fun _ik -> Ints_t.lognot) ik i1 (fun () ->
+        match i1 with
+        | Some (x1, x2) -> of_interval ik (Ints_t.lognot x2, Ints_t.lognot x1) |> fst
+        | _ -> top_of ik)
+
+  let shift_right ik i1 i2 =
+    match is_bot i1, is_bot i2 with
+    | true, true -> (bot_of ik,{underflow=false; overflow=false})
+    | true, _
+    | _   , true -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show i1) (show i2)))
+    | _ ->
+      match to_int i1, to_int i2 with
+      | Some x, Some y -> (try of_int ik (Ints_t.shift_right x (Ints_t.to_int y)) with Division_by_zero | Invalid_argument _ -> (top_of ik,{underflow=false; overflow=false}))
+      | _              ->
+        let is_nonneg x = Ints_t.compare x Ints_t.zero >= 0 in
+        match i1, i2 with
+        | Some (x1, x2), Some (y1,y2) when is_nonneg x1 && is_nonneg y1 ->
+          of_interval ik (Ints_t.zero, Ints_t.div x2 (Ints_t.shift_left Ints_t.one (Ints_t.to_int y1)))
+        | _ -> (top_of ik,{underflow=false; overflow=false})
 
   let neg ?no_ov ik = function None -> (None,{underflow=false; overflow=false}) | Some x -> norm ik @@ Some (IArith.neg x)
 
diff --git a/src/cdomain/value/cdomains/int/intervalSetDomain.ml b/src/cdomain/value/cdomains/int/intervalSetDomain.ml
index e4f74b0f7a..57c5dbb31e 100644
--- a/src/cdomain/value/cdomains/int/intervalSetDomain.ml
+++ b/src/cdomain/value/cdomains/int/intervalSetDomain.ml
@@ -31,7 +31,13 @@ struct
 
   let range ik = BatTuple.Tuple2.mapn Ints_t.of_bigint (Size.range ik)
 
-  let top_of ik = [range ik]
+  let top_of ?bitfield ik = [match bitfield with
+      | None -> range ik
+      | Some b -> let signed_lower_bound = Ints_t.neg @@ Ints_t.shift_left Ints_t.one (b-1) in
+        let unsigned_upper_bound = Ints_t.sub (Ints_t.shift_left Ints_t.one b) Ints_t.one in
+        match Cil.isSigned ik with
+        | true -> (signed_lower_bound, unsigned_upper_bound)
+        | false -> (Ints_t.zero, unsigned_upper_bound)]
 
   let bot () = []
 
@@ -307,23 +313,85 @@ struct
     | Some x, Some y -> (try of_int ik (f x y) with Division_by_zero | Invalid_argument _ -> (top_of ik,{overflow=false; underflow=false}))
     | _, _ -> (top_of ik,{overflow=false; underflow=false})
 
-  let logand ik x y =
-    let interval_logand = bit Ints_t.logand ik in
-    binop x y interval_logand
+  let min_val_bit_constrained n = 
+    if Ints_t.equal n Ints_t.zero then 
+      Ints_t.neg Ints_t.one 
+    else 
+      Ints_t.neg @@ Ints_t.shift_left Ints_t.one (Z.numbits (Z.sub (Z.abs @@ Ints_t.to_bigint n) Z.one)) 
 
-  let logor ik x y =
-    let interval_logor = bit Ints_t.logor ik in
-    binop x y interval_logor
+  let max_val_bit_constrained n = 
+    let x = if Ints_t.compare n Ints_t.zero < 0 then Ints_t.sub (Ints_t.neg n) Ints_t.one else n in
+    Ints_t.sub (Ints_t.shift_left Ints_t.one (Z.numbits @@ Z.abs @@ Ints_t.to_bigint x)) Ints_t.one
 
-  let logxor ik x y =
-    let interval_logxor = bit Ints_t.logxor ik in
-    binop x y interval_logxor
+  let interval_logand ik (i1, i2) =
+    match bit Ints_t.logand ik (i1,i2) with
+    | result when result <> top_of ik -> result
+    | _ ->
+      let (x1, x2), (y1, y2) = i1, i2 in
+      let is_nonneg x = Ints_t.compare x Ints_t.zero >= 0 in
+      match is_nonneg x1, is_nonneg x2, is_nonneg y1, is_nonneg y2 with
+      | true, _, true, _ ->
+        of_interval ik (Ints_t.zero, Ints_t.min x2 y2) |> fst
+      | _, false, _, false ->
+        of_interval ik (min_val_bit_constrained @@ Ints_t.min x1 y1, Ints_t.zero) |> fst
+      | true, _, _, _ -> of_interval ik (Ints_t.zero, x2) |> fst
+      | _, _, true, _ -> of_interval ik (Ints_t.zero, y2) |> fst
+      | _ ->
+        let lower = min_val_bit_constrained @@ Ints_t.min x1 y1 in
+        let upper = Ints_t.max x2 y2 in
+        of_interval ik (lower, upper) |> fst
+
+  let logand ik x y = binop x y (interval_logand ik)
+
+  let interval_logor ik (i1, i2) =
+    match bit Ints_t.logor ik (i1, i2) with
+    | result when result <> top_of ik -> result
+    | _ ->
+      let (x1, x2), (y1, y2) = i1, i2 in
+      let is_nonneg x = Ints_t.compare x Ints_t.zero >= 0 in
+      match is_nonneg x1, is_nonneg x2, is_nonneg y1, is_nonneg y2 with
+      | true, _, true, _ -> of_interval ik (Ints_t.max x1 y1, max_val_bit_constrained (Ints_t.max x2 y2)) |> fst
+      | _, false, _, false -> of_interval ik (Ints_t.max x1 y1, Ints_t.zero) |> fst
+      | _, false, _, _ -> of_interval ik (x1, Ints_t.zero) |> fst
+      | _, _, _, false -> of_interval ik (y1, Ints_t.zero) |> fst
+      |_ ->
+        let lower = Ints_t.min x1 y1 in
+        let upper = max_val_bit_constrained @@ Ints_t.max x2 y2 in
+        of_interval ik (lower, upper) |> fst
+
+  let logor ik x y = binop x y (interval_logor ik)
+
+  let interval_logxor ik (i1, i2) =
+    match bit Ints_t.logxor ik (i1, i2) with
+    | result when result <> top_of ik && result <> bot_of ik -> result
+    | _ ->
+      let (x1, x2), (y1, y2) = i1, i2 in
+      let is_nonneg x = Ints_t.compare x Ints_t.zero >= 0 in
+      match is_nonneg x1, is_nonneg x2, is_nonneg y1, is_nonneg y2 with
+      | true, _, true, _ ->
+        of_interval ik (Ints_t.zero, max_val_bit_constrained @@ Ints_t.max x2 y2) |> fst
+      | _, false, _, false ->
+        let upper = max_val_bit_constrained @@ Ints_t.min x1 y1 in
+        of_interval ik (Ints_t.zero, upper) |> fst
+      | true, _, _, false | _, false, true, _ ->
+        let lower = List.fold_left Ints_t.min Ints_t.zero 
+            (List.append (List.map min_val_bit_constrained [x1; y1]) 
+               (List.map (fun i -> Ints_t.neg @@ Ints_t.add (max_val_bit_constrained i) Ints_t.one) [x2; y2])) in  
+        of_interval ik (lower, Ints_t.zero) |> fst
+      | _ -> let lower = List.fold_left Ints_t.min Ints_t.zero 
+                 (List.append (List.map min_val_bit_constrained [x1; y1]) 
+                    (List.map (fun i -> Ints_t.neg @@ Ints_t.add (max_val_bit_constrained i) Ints_t.one) [x2; y2])) in 
+        let upper = List.fold_left Ints_t.max Ints_t.zero (List.map max_val_bit_constrained [x1;x2;y1;y2]) in
+        of_interval ik (lower, upper) |> fst
+
+  let logxor ik x y = binop x y (interval_logxor ik)
 
   let lognot ik x =
     let interval_lognot i =
       match interval_to_int i with
       | Some x -> of_int ik (Ints_t.lognot x) |> fst
-      | _ -> top_of ik
+      | _ ->
+        let (x1, x2) = i in of_interval ik (Ints_t.lognot x2, Ints_t.lognot x1) |> fst
     in
     unop x interval_lognot
 
@@ -331,9 +399,18 @@ struct
     let interval_shiftleft = bitcomp (fun x y -> Ints_t.shift_left x (Ints_t.to_int y)) ik in
     binary_op_with_ovc x y interval_shiftleft
 
-  let shift_right ik x y =
-    let interval_shiftright = bitcomp (fun x y -> Ints_t.shift_right x (Ints_t.to_int y)) ik in
-    binary_op_with_ovc x y interval_shiftright
+  let interval_shiftright ik (i1, i2) =
+    match (interval_to_int i1, interval_to_int i2) with
+    | Some x, Some y -> (try of_int ik (Ints_t.shift_right x (Ints_t.to_int y)) with Division_by_zero | Invalid_argument _ ->
+        (top_of ik,{overflow=false; underflow=false}))
+    | _ ->
+      let is_nonneg x = Ints_t.compare x Ints_t.zero >= 0 in
+      match i1, i2 with
+      | (x1, x2), (y1,y2) when is_nonneg x1 && is_nonneg y1 ->
+        of_interval ik (Ints_t.zero, Ints_t.div x2 (Ints_t.shift_left Ints_t.one (Ints_t.to_int y1)))
+      | _ -> (top_of ik,{underflow=false; overflow=false})
+
+  let shift_right ik x y = binary_op_with_ovc x y (interval_shiftright ik)
 
   let c_lognot ik x =
     let log1 f ik i1 =
diff --git a/src/cdomain/value/cdomains/intDomain0.ml b/src/cdomain/value/cdomains/intDomain0.ml
index ed9e6ea549..cf18846e90 100644
--- a/src/cdomain/value/cdomains/intDomain0.ml
+++ b/src/cdomain/value/cdomains/intDomain0.ml
@@ -129,7 +129,7 @@ struct
   let bot_of ikind = { v = I.bot_of ikind; ikind}
   let bot () = failwith "bot () is not implemented for IntDomLifter."
   let is_bot x = I.is_bot x.v
-  let top_of ikind = { v = I.top_of ikind; ikind}
+  let top_of ?bitfield ikind = { v = I.top_of ?bitfield ikind; ikind}
   let top () = failwith "top () is not implemented for IntDomLifter."
   let is_top _ = failwith "is_top is not implemented for IntDomLifter."
 
@@ -301,7 +301,7 @@ module Size = struct (* size in bits as int, range as int64 *)
 end
 
 
-module StdTop (B: sig type t val top_of: Cil.ikind -> t end) = struct
+module StdTop (B: sig type t val top_of: ?bitfield:int -> Cil.ikind -> t end) = struct
   open B
   (* these should be overwritten for better precision if possible: *)
   let to_excl_list    x = None
@@ -320,7 +320,7 @@ end
 module Std (B: sig
     type t
     val name: unit -> string
-    val top_of: Cil.ikind -> t
+    val top_of: ?bitfield:int -> Cil.ikind -> t
     val bot_of: Cil.ikind -> t
     val show: t -> string
     val equal: t -> t -> bool
@@ -503,7 +503,7 @@ struct
   type int_t = Ints_t.t
   let top () = raise Unknown
   let bot () = raise Error
-  let top_of ik = top ()
+  let top_of ?bitfield ik = top ()
   let bot_of ik = bot ()
   let show (x: Ints_t.t) = Ints_t.to_string x
 
@@ -571,7 +571,7 @@ struct
       let bot_name = "Error int"
     end) (Base)
 
-  let top_of ik = top ()
+  let top_of ?bitfield ik = top ()
   let bot_of ik = bot ()
 
 
@@ -652,7 +652,7 @@ struct
       let bot_name = "MinInt"
     end) (Base)
   type int_t = Base.int_t
-  let top_of ik = top ()
+  let top_of ?bitfield ik = top ()
   let bot_of ik = bot ()
   include StdTop (struct type nonrec t = t let top_of = top_of end)
 
diff --git a/src/cdomain/value/cdomains/valueDomain.ml b/src/cdomain/value/cdomains/valueDomain.ml
index 0fca1a49b9..78c1456276 100644
--- a/src/cdomain/value/cdomains/valueDomain.ml
+++ b/src/cdomain/value/cdomains/valueDomain.ml
@@ -34,7 +34,7 @@ sig
   val is_mutex_type: typ -> bool
   val bot_value: ?varAttr:attributes -> typ -> t
   val is_bot_value: t -> bool
-  val init_value: ?varAttr:attributes -> typ -> t
+  val init_value: ?bitfield:(int option) -> ?varAttr:attributes -> typ -> t
   val top_value: ?varAttr:attributes -> typ -> t
   val is_top_value: t -> typ -> bool
   val zero_init_value: ?varAttr:attributes -> typ -> t
@@ -187,16 +187,16 @@ struct
     | Bot -> true
     | Top -> false
 
-  let rec init_value ?(varAttr=[]) (t: typ): t = (* top_value is not used here because structs, blob etc will not contain the right members *)
+  let rec init_value ?(bitfield:int option=None) ?(varAttr=[]) (t: typ): t = (* top_value is not used here because structs, blob etc will not contain the right members *)
     match t with
     | t when is_mutex_type t -> Mutex
     | t when is_jmp_buf_type t -> JmpBuf (JmpBufs.top ())
     | t when is_mutexattr_type t -> MutexAttr (MutexAttrDomain.top ())
-    | TInt (ik,_) -> Int (ID.top_of ik)
+    | TInt (ik,_) -> Int (ID.top_of ?bitfield ik)
     (* TODO: TEnum? *)
     | TFloat (fkind, _) when not (Cilfacade.isComplexFKind fkind) -> Float (FD.top_of fkind)
     | TPtr _ -> Address AD.top_ptr
-    | TComp ({cstruct=true; _} as ci,_) -> Struct (Structs.create (fun fd -> init_value ~varAttr:fd.fattr fd.ftype) ci)
+    | TComp ({cstruct=true; _} as ci,_) -> Struct (Structs.create (fun fd -> init_value ~bitfield:fd.fbitfield ~varAttr:fd.fattr fd.ftype) ci)
     | TComp ({cstruct=false; _},_) -> Union (Unions.top ())
     | TArray (ai, length, _) ->
       let typAttr = typeAttrs ai in
@@ -979,7 +979,7 @@ struct
     do_eval_offset ask f x offs exp l o v t
 
   let update_offset ?(blob_destructive=false) (ask: VDQ.t) (x:t) (offs:offs) (value:t) (exp:exp option) (v:lval) (t:typ): t =
-    let rec do_update_offset (ask:VDQ.t) (x:t) (offs:offs) (value:t) (exp:exp option) (l:lval option) (o:offset option) (v:lval) (t:typ):t =
+    let rec do_update_offset ?(bitfield:int option=None) (ask:VDQ.t) (x:t) (offs:offs) (value:t) (exp:exp option) (l:lval option) (o:offset option) (v:lval) (t:typ):t =
       if M.tracing then M.traceli "update_offset" "do_update_offset %a %a (%a) %a" pretty x Offs.pretty offs (Pretty.docOpt (CilType.Exp.pretty ())) exp pretty value;
       let mu = function Blob (Blob (y, s', zeroinit), s, _) -> Blob (y, ID.join s s', zeroinit) | x -> x in
       let r =
@@ -1070,7 +1070,12 @@ struct
             | `NoOffset -> begin
                 match value with
                 | Blob (y, s, zeroinit) -> mu (Blob (join x y, s, zeroinit))
-                | Int _ -> cast t value
+                | Int i -> begin
+                  match bitfield with
+                  | Some b when not @@ ID.leq i (ID.top_of ~bitfield:b (ID.ikind i)) ->
+                    Messages.warn ~category:Analyzer "Assigned value %a exceeds the representable range of a %d-bit bit-field." pretty value b; Top
+                  | _ -> cast t value
+                end
                 | _ -> value
               end
             | `Field (fld, offs) when fld.fcomp.cstruct -> begin
@@ -1079,7 +1084,7 @@ struct
                 | Struct str ->
                   begin
                     let l', o' = shift_one_over l o in
-                    let value' = do_update_offset ask (Structs.get str fld) offs value exp l' o' v t in
+                    let value' = do_update_offset ~bitfield:fld.fbitfield ask (Structs.get str fld) offs value exp l' o' v t in
                     Struct (Structs.replace str fld value')
                   end
                 | Bot ->
diff --git a/tests/regression/98-bitwise-operations/01-logand.c b/tests/regression/98-bitwise-operations/01-logand.c
new file mode 100644
index 0000000000..3af350437d
--- /dev/null
+++ b/tests/regression/98-bitwise-operations/01-logand.c
@@ -0,0 +1,212 @@
+// PARAM: --enable ana.int.interval
+#include <goblint.h>
+
+int main() {
+  int res;
+  unsigned int unsigned_x;
+  unsigned int unsigned_y;
+
+  if (unsigned_x > 14) {
+    unsigned_x = 0;
+  } 
+
+  if (unsigned_y > 30) {
+    unsigned_y = 0;
+  }
+
+  res = unsigned_x & unsigned_y;
+  __goblint_check(res >= 0);
+  __goblint_check(res <= 14);
+
+  int both_pos_x;
+  int both_pos_y;
+
+  if (both_pos_x < 0 ||both_pos_x > 62) {
+    both_pos_x = 0;
+  }
+
+  if (both_pos_y < 0 || both_pos_y > 30) {
+    both_pos_y = 0;
+  }
+
+  res = both_pos_x & both_pos_y;
+
+  __goblint_check(res >= 0);
+  __goblint_check(res <= 30);
+
+  int both_neg_x;
+  int both_neg_y;
+
+  if (both_neg_x < -61 || both_neg_x > -1) {
+    both_neg_x = -61;
+  }
+  
+  if (both_neg_y < -30 || both_neg_y > -1) {
+    both_neg_y = -30;
+  }
+
+  res = both_neg_x & both_neg_y;
+  __goblint_check(res <= 0);
+  __goblint_check(res >= -64);
+
+  int both_neg_x2;
+  int both_neg_y2;
+
+  if (both_neg_x2 < -64 || both_neg_x2 > -1) {
+    both_neg_x2 = -64;
+  }
+
+  if (both_neg_y2 < -30 || both_neg_y2 > -1) {
+    both_neg_y2 = -30;
+  }
+
+  res = both_neg_x2 & both_neg_y2;
+  __goblint_check(res <= 0);
+  __goblint_check(res >= -64);
+
+  int both_neg_x3;
+  int both_neg_y3;
+
+  if (both_neg_x3 < -65 || both_neg_x3 > -1) {
+    both_neg_x3 = -65;
+  }
+
+  if (both_neg_y3 < -30 || both_neg_y3 > -1) {
+    both_neg_y3 = -30;
+  }
+
+  res = both_neg_x3 & both_neg_y3;
+  __goblint_check(res <= 0);
+  __goblint_check(res >= -128); 
+
+  int one_pos_x;
+  int one_pos_y;
+
+  if (one_pos_x < -64 || one_pos_x > -1) {
+    one_pos_x = -64;
+  }
+
+  if (one_pos_y > 30 || one_pos_y < 0) {
+    one_pos_y = 30;
+  }
+
+  res = one_pos_x & one_pos_y;
+  __goblint_check(res >= 0);
+  __goblint_check(res <= 30);
+
+  int one_pos_x2;
+  int one_pos_y2;
+
+  if (one_pos_x2 < -65 || one_pos_x2 > 40) {
+    one_pos_x2 = -65;
+  }
+
+  if (one_pos_y2 > 30 || one_pos_y2 < 0) {
+    one_pos_y2 = 30;
+  }
+
+  res = one_pos_x2 & one_pos_y2;
+  __goblint_check(res >= 0);
+  __goblint_check(res <= 30); 
+
+  int one_pos_x3;
+  int one_pos_y3;
+
+  if (one_pos_x3 < -65 || one_pos_x3 > 10) {
+    one_pos_x3 = 0;
+  }
+
+  if (one_pos_y3 > 30 || one_pos_y3 < 0) {
+    one_pos_y3 = 0;
+  }
+
+  res = one_pos_x3 & one_pos_y3;
+  __goblint_check(res >= 0);
+  __goblint_check(res <= 30);
+
+  int otherwise_x;
+  int otherwise_y;
+
+  if (otherwise_x < -64 || otherwise_x > 20) {
+    otherwise_x = 0;
+  }
+
+  if (otherwise_y < -10 || otherwise_y > 63) {
+    otherwise_y = 0;
+  }
+
+  res = otherwise_x & otherwise_y;
+  __goblint_check(res >= -64);
+  __goblint_check(res <= 63);
+
+  int x_otherwise2;
+  int y_otherwise2;
+
+  if (x_otherwise2 < -64 || x_otherwise2 > 30) {
+    x_otherwise2 = 0;
+  }
+
+  if (y_otherwise2 < -20 || y_otherwise2 > 64) {
+    y_otherwise2 = 0;
+  }
+  res = x_otherwise2 & y_otherwise2;
+  __goblint_check(res >= -128);
+  __goblint_check(res <= 127);
+
+  int x_otherwise3;
+  int y_otherwise3;
+
+  if (x_otherwise3 < -1 || x_otherwise3 > 1) {
+    x_otherwise3 = 0;
+  }
+
+  if (y_otherwise3 < -1 || y_otherwise3 > 1) {
+    y_otherwise3 = 0;
+  }
+
+  res = x_otherwise3 & y_otherwise3;
+  __goblint_check(res >= -2);
+  __goblint_check(res <= 1);
+
+  long long ll_res;
+  long long ll_int_x;
+  long long ll_int_y;
+
+  if (ll_int_x < -__INT_MAX__ - 1 || ll_int_x > __INT_MAX__ ) {
+    ll_int_x = 0;
+  }
+
+  if (ll_int_y < -__INT_MAX__ - 1 || ll_int_y > __INT_MAX__ ) {
+    ll_int_y = 0;
+  }
+
+  ll_res = ll_int_x & ll_int_y;
+  __goblint_check(ll_res >= -__INT_MAX__ - 1);
+  __goblint_check(ll_res <= __INT_MAX__);
+
+  long long ll_large_x;
+  long long ll_large_y;
+
+  if (ll_large_x < -__LONG_LONG_MAX__ + 100 || ll_large_x > __LONG_LONG_MAX__ - 100) {
+    ll_large_x = 0;
+  }
+
+  if (ll_large_y < -100 || ll_large_y > 100) {
+    ll_large_y = 0;
+  }
+
+  ll_res = ll_large_x & ll_large_y;
+  __goblint_check(ll_res >= -__LONG_LONG_MAX__ - 1);
+  __goblint_check(ll_res <= __LONG_LONG_MAX__);
+
+  long long ll_max_x;
+  long long ll_max_y;
+
+  if (ll_max_y < -100 || ll_max_y > 100) {
+    ll_max_y = 0;
+  }
+  ll_res = ll_max_x & ll_max_y;
+  __goblint_check(ll_res >= -__LONG_LONG_MAX__ - 1);
+  __goblint_check(ll_res <= __LONG_LONG_MAX__);
+
+}
\ No newline at end of file
diff --git a/tests/regression/98-bitwise-operations/02-logor.c b/tests/regression/98-bitwise-operations/02-logor.c
new file mode 100644
index 0000000000..a8ce399437
--- /dev/null
+++ b/tests/regression/98-bitwise-operations/02-logor.c
@@ -0,0 +1,200 @@
+// PARAM: --enable ana.int.interval
+#include <goblint.h>
+
+int main() {
+  unsigned int u_res;
+  unsigned int unsigned_x;
+  unsigned int unsigned_y;
+
+  if (unsigned_x < 14 ) {
+    unsigned_x = 14;
+  }
+
+  if (unsigned_y < 35 || unsigned_y > 60) {
+    unsigned_y = 60;
+  }
+
+  u_res = unsigned_x | unsigned_y;
+  __goblint_check(u_res >= 35);
+  __goblint_check(u_res <= __UINT32_MAX__);
+  
+  int res;
+  int both_pos_x;
+  int both_pos_y;
+
+  if (both_pos_x < 0 ||both_pos_x > 64) {
+    both_pos_x = 0;
+  }
+
+  if (both_pos_y < 10 || both_pos_y > 30) {
+    both_pos_y = 30;
+  }
+
+  res = both_pos_x | both_pos_y;
+  __goblint_check(res >= 10);
+  __goblint_check(res <= 127);
+
+  int both_neg_x;
+  int both_neg_y;
+
+  if (both_neg_x < -64 || both_neg_x > -1) {
+    both_neg_x = -64;
+  }
+
+  if (both_neg_y < -30 || both_neg_y > -1) {
+    both_neg_y = -30;
+  }
+
+  res = both_neg_x | both_neg_y;
+  __goblint_check(res <= 0);
+  __goblint_check(res >= -30);
+
+  int one_neg_x;
+  int one_neg_y;
+
+  if (one_neg_x < -64 || one_neg_x > -1) {
+    one_neg_x = -64;
+  }
+
+  if (one_neg_y > 63 || one_neg_y < 0) {
+    one_neg_y = 63;
+  }
+
+  res = one_neg_x | one_neg_y;
+  __goblint_check(res <= 0);
+  __goblint_check(res >= -64);
+
+  int one_neg_x2;
+  int one_neg_y2;
+
+  if (one_neg_x2 < -20 || one_neg_x2 > -1) {
+    one_neg_x2 = -20;
+  }
+
+  if (one_neg_y2 > 30 || one_neg_y2 < 0) {
+    one_neg_y2 = 30;
+  }
+
+  res = one_neg_x2 | one_neg_y2;
+  __goblint_check(res <= 0);
+  __goblint_check(res >= -20); 
+
+  int one_neg_x3;
+  int one_neg_y3;
+
+  if (one_neg_x3 < -10 || one_neg_x3 > -1) {
+    one_neg_x3 = -10;
+  }
+
+  if (one_neg_y3 > 64 || one_neg_y3 < -64) {
+    one_neg_y3 = 64;
+  }
+
+  res = one_neg_x3 | one_neg_y3;
+  __goblint_check(res <= 0);
+  __goblint_check(res >= -10);
+
+  int one_neg_x4;
+  int one_neg_y4;
+
+  if (one_neg_x4 < -30 || one_neg_x4 > -1) {
+    one_neg_x4 = -30;
+  }
+
+  if (one_neg_y4 > 10 || one_neg_y4 < -10) {
+    one_neg_y4 = 10;
+  }
+
+  res = one_neg_x4 | one_neg_y4;
+  __goblint_check(res <= 0);
+  __goblint_check(res >= -30);
+
+  int otherwise_x;
+  int otherwise_y;
+
+  if (otherwise_x < -63 || otherwise_x > 20) {
+    otherwise_x = 0;
+  }
+
+  if (otherwise_y < -10 || otherwise_y > 63) {
+    otherwise_y = 0;
+  }
+  res = otherwise_x | otherwise_y;
+  __goblint_check(res >= -63);
+  __goblint_check(res <= 63);
+
+  int x_otherwise2;
+  int y_otherwise2;
+
+  if (x_otherwise2 < -64 || x_otherwise2 > 30) {
+    x_otherwise2 = 0;
+  }
+
+  if (y_otherwise2 < -20 || y_otherwise2 > 64) {
+    y_otherwise2 = 0;
+  }
+
+  res = x_otherwise2 | y_otherwise2;
+  __goblint_check(res >= -64);
+  __goblint_check(res <= 127);
+
+  int x_otherwise3;
+  int y_otherwise3;
+
+  if (x_otherwise3 < -1 || x_otherwise3 > 1) {
+    x_otherwise3 = 0;
+  }
+
+  if (y_otherwise3 < -1 || y_otherwise3 > 1) {
+    y_otherwise3 = 0;
+  }
+
+  res = x_otherwise3 | y_otherwise3;
+  __goblint_check(res >= -1);
+  __goblint_check(res <= 1);
+
+
+  long long ll_res;
+  long long ll_int_x;
+  long long ll_int_y;
+
+  if (ll_int_x < -__INT_MAX__ - 1 || ll_int_x > __INT_MAX__ ) {
+    ll_int_x = 0;
+  }
+
+  if (ll_int_y < -__INT_MAX__ - 1 || ll_int_y > __INT_MAX__ ) {
+    ll_int_y = 0;
+  }
+
+  ll_res = ll_int_x | ll_int_y;
+  __goblint_check(ll_res >= -__INT_MAX__ - 1);
+  __goblint_check(ll_res <= __INT_MAX__);
+
+  long long ll_large_x;
+  long long ll_large_y;
+
+  if (ll_large_x < -__LONG_LONG_MAX__ + 100 || ll_large_x > __LONG_LONG_MAX__ - 100) {
+    ll_large_x = 0;
+  }
+
+  if (ll_large_y < -100 || ll_large_y > 100) {
+    ll_large_y = 0;
+  }
+
+  ll_res = ll_large_x | ll_large_y;
+  __goblint_check(ll_res >= -__LONG_LONG_MAX__ - 1);
+  __goblint_check(ll_res <= __LONG_LONG_MAX__);
+
+  long long ll_max_x;
+  long long ll_max_y;
+
+  if (ll_max_y < -100 || ll_max_y > 100) {
+    ll_max_y = 0;
+  }
+
+  ll_res = ll_max_x | ll_max_y;
+  __goblint_check(ll_res >= -__LONG_LONG_MAX__ - 1);
+  __goblint_check(ll_res <= __LONG_LONG_MAX__);
+
+  return 0;
+}
\ No newline at end of file
diff --git a/tests/regression/98-bitwise-operations/03-logxor.c b/tests/regression/98-bitwise-operations/03-logxor.c
new file mode 100644
index 0000000000..0bbfeeeffe
--- /dev/null
+++ b/tests/regression/98-bitwise-operations/03-logxor.c
@@ -0,0 +1,253 @@
+// PARAM: --enable ana.int.interval
+#include <goblint.h>
+
+int main() {
+
+  unsigned int u_res;
+  unsigned int unsigned_x;
+  unsigned int unsigned_y;
+
+  if (unsigned_x > 14) {
+    unsigned_x = 0;
+  } 
+  
+  if (unsigned_y > 30) {
+    unsigned_y = 0;
+  }
+
+  u_res = unsigned_x ^ unsigned_y;
+  __goblint_check(u_res <= 31);
+
+  int res;
+  int zero_x = 0;
+  int zero_y = 0;
+
+  res = zero_x ^ zero_y;
+  __goblint_check(res >= 0);
+  __goblint_check(res <= 0);
+  
+  int both_pos_x;
+  int both_pos_y;
+
+  if (both_pos_x < 0 ||both_pos_x > 63) {
+    both_pos_x = 0;
+  }
+
+  if (both_pos_y < 0 || both_pos_y > 30) {
+    both_pos_y = 0;
+  }
+
+  res = both_pos_x ^ both_pos_y;
+  __goblint_check(res >= 0);
+  __goblint_check(res <= 63);
+
+  int both_pos_x2;
+  int both_pos_y2;
+
+  if (both_pos_x2 < 0 || both_pos_x2 > 64) {
+    both_pos_x2 = 0;
+  }
+
+  if (both_pos_y2 < 0 || both_pos_y2 > 30) {
+    both_pos_y2 = 0;
+  }
+
+  res = both_pos_x2 ^ both_pos_y2;
+  __goblint_check(res >= 0);
+  __goblint_check(res <= 127);
+
+  int both_pos_x3;
+  int both_pos_y3;
+  if (both_pos_x3 < 0 || both_pos_x3 > 1) {
+    both_pos_x3 = 0;
+  }
+
+  if (both_pos_y3 < 0 || both_pos_y3 > 1) {
+    both_pos_y3 = 0;
+  }
+
+  res = both_pos_x3 ^ both_pos_y3;
+  __goblint_check(res >= 0);
+  __goblint_check(res <= 1);
+
+  int both_neg_x;
+  int both_neg_y;
+
+  if (both_neg_x < -64 || both_neg_x > -1) {
+    both_neg_x = -64;
+  }
+
+  if (both_neg_y < -64 || both_neg_y > -1) {
+    both_neg_y = -64;
+  }
+
+  res = both_neg_x ^ both_neg_y;
+  __goblint_check(res >= 0);
+  __goblint_check(res <= 63);
+
+  int both_neg_x2 = -1;
+  int both_neg_y2 = -1;
+
+  res = both_neg_x2 ^ both_neg_y2;
+  __goblint_check(res >= 0);
+  __goblint_check(res <= 0);
+
+  int both_neg_x3;
+  int both_neg_y3;
+
+  if (both_neg_x3 < -65 || both_neg_x3 > -1) {
+    both_neg_x3 = -65;
+  }
+
+  if (both_neg_y3 < -30 || both_neg_y3 > -1) {
+    both_neg_y3 = -30;
+  }
+
+  res = both_neg_x3 ^ both_neg_y3;
+  __goblint_check(res >= 0);
+  __goblint_check(res <= 127);
+
+  int neg_pos_x;
+  int neg_pos_y;
+
+  if (neg_pos_x < -64 || neg_pos_x > -1) {
+    neg_pos_x = -64;
+  }
+
+  if (neg_pos_y > 64 || neg_pos_y < 0) {
+    neg_pos_y = 64;
+  }
+
+  res = neg_pos_x ^ neg_pos_y;
+  __goblint_check(res <= 0);
+  __goblint_check(res >= -128);
+
+  int neg_pos_x2;
+  int neg_pos_y2;
+
+  if (neg_pos_x2 < -65 || neg_pos_x2 > -1) {
+    neg_pos_x2 = -65;
+  }
+
+  if (neg_pos_y2 > 65 || neg_pos_y2 < 0) {
+    neg_pos_y2 = 65;
+  }
+
+  res = neg_pos_x2 ^ neg_pos_y2;
+  __goblint_check(res <= 0);
+  __goblint_check(res >= -128);
+
+  int neg_pos_x3 = -1;
+  int neg_pos_y3;
+
+  if (neg_pos_y3 > 1 || neg_pos_y3 < 0) { 
+    neg_pos_y3 = 1;
+  }
+  
+  res = neg_pos_x3 ^ neg_pos_y3;
+  __goblint_check(res <= 0);
+  __goblint_check(res >= -2);
+
+  int neg_pos_x4;
+  int neg_pos_y4;
+
+  if (neg_pos_x4 < -63 || neg_pos_x4 > -1) {
+    neg_pos_x4 = -63;
+  }
+
+  if (neg_pos_y4 < 0 || neg_pos_y4 > 30) {
+    neg_pos_y4 = 0;
+  }
+
+  res = neg_pos_x4 ^ neg_pos_y4;
+  __goblint_check(res <= 0);
+  __goblint_check(res >= -64);
+
+  int otherwise_x;
+  int otherwise_y;
+
+  if (otherwise_x < -63 || otherwise_x > 20) {
+    otherwise_x = 0;
+  }
+
+  if (otherwise_y < -10 || otherwise_y > 63) {
+    otherwise_y = 0;
+  }
+
+  res = otherwise_x ^ otherwise_y;
+  __goblint_check(res >= -64);
+  __goblint_check(res <= 63);
+
+  int x_otherwise2;
+  int y_otherwise2;
+
+  if (x_otherwise2 < -64 || x_otherwise2 > 30) {
+    x_otherwise2 = 0;
+  }
+
+  if (y_otherwise2 < -20 || y_otherwise2 > 64) {
+    y_otherwise2 = 0;
+  }
+
+  res = x_otherwise2 ^ y_otherwise2;
+  __goblint_check(res >= -128);
+  __goblint_check(res <= 127);
+
+  int x_otherwise3;
+  int y_otherwise3;
+
+  if (x_otherwise3 < -1 || x_otherwise3 > 1) {
+    x_otherwise3 = 0;
+  }
+
+  if (y_otherwise3 < -1 || y_otherwise3 > 1) {
+    y_otherwise3 = 0;
+  }
+
+  res = x_otherwise3 ^ y_otherwise3;
+  __goblint_check(res >= -2);
+  __goblint_check(res <= 1);
+
+  long long ll_res;
+  long long ll_int_x;
+  long long ll_int_y;
+
+  if (ll_int_x < -__INT_MAX__ - 1 || ll_int_x > __INT_MAX__ ) {
+    ll_int_x = 0;
+  }
+
+  if (ll_int_y < -__INT_MAX__ - 1 || ll_int_y > __INT_MAX__ ) {
+    ll_int_y = 0;
+  }
+
+  ll_res = ll_int_x ^ ll_int_y;
+  __goblint_check(ll_res >= -__INT_MAX__ - 1);
+  __goblint_check(ll_res <= __INT_MAX__);
+  
+  long long ll_large_x;
+  long long ll_large_y;
+
+  if (ll_large_x < -__LONG_LONG_MAX__ + 100 || ll_large_x > __LONG_LONG_MAX__ - 100) {
+    ll_large_x = 0;
+  }
+
+  if (ll_large_y < -100 || ll_large_y > 100) {
+    ll_large_y = 0;
+  }
+
+  ll_res = ll_large_x ^ ll_large_y;
+  __goblint_check(ll_res >= -__LONG_LONG_MAX__ - 1);
+  __goblint_check(ll_res <= __LONG_LONG_MAX__);
+
+  long long ll_max_x;
+  long long ll_max_y;
+
+  if (ll_max_y < -100 || ll_max_y > 100) {
+    ll_max_y = 0;
+  }
+
+  ll_res = ll_max_x ^ ll_max_y;
+  __goblint_check(ll_res >= -__LONG_LONG_MAX__ - 1);
+  __goblint_check(ll_res <= __LONG_LONG_MAX__);
+  return 0;
+}
diff --git a/tests/regression/98-bitwise-operations/04-shift.c b/tests/regression/98-bitwise-operations/04-shift.c
new file mode 100644
index 0000000000..d7655ba308
--- /dev/null
+++ b/tests/regression/98-bitwise-operations/04-shift.c
@@ -0,0 +1,56 @@
+// PARAM: --enable ana.int.interval
+#include <goblint.h>
+
+int main() {
+  unsigned int x;
+
+  if (x > 10) {
+    x = 10;
+  }
+
+  unsigned int u_res = x >> 0;
+
+  __goblint_check(u_res >= 0);
+  __goblint_check(u_res <= 10); 
+
+  u_res = x >> 1;
+
+  __goblint_check(u_res >= 0);
+  __goblint_check(u_res <= 5); 
+
+  u_res = x >> 2;
+
+  __goblint_check(u_res >= 0);
+  __goblint_check(u_res <= 2); 
+
+  int x;
+
+  if (x < 0) {
+    x = 0;
+  }
+
+  int res = x >> 0;
+
+  __goblint_check(res >= 0);
+  __goblint_check(res <= __INT_MAX__);
+
+
+  res = x >> 1;
+
+  __goblint_check(res >= 0);
+  __goblint_check(res <= (__INT_MAX__ / 2));
+
+
+  long long ll_x = __LONG_LONG_MAX__;
+  long long ll_res = ll_x >> 0;
+
+  __goblint_check(ll_res >= 0);
+  __goblint_check(ll_res <= __LONG_LONG_MAX__);
+
+
+  ll_res = ll_x >> 2;
+
+  __goblint_check(ll_res >= 0);
+  __goblint_check(ll_res <= (__LONG_LONG_MAX__ / 4));
+  return 0;
+}
\ No newline at end of file
diff --git a/tests/regression/98-bitwise-operations/05-lognot.c b/tests/regression/98-bitwise-operations/05-lognot.c
new file mode 100644
index 0000000000..de968027dd
--- /dev/null
+++ b/tests/regression/98-bitwise-operations/05-lognot.c
@@ -0,0 +1,84 @@
+// PARAM: --enable ana.int.interval
+#include <goblint.h>
+
+int main() {
+  int res;
+  int pos_x;
+
+  if (pos_x < 0 || pos_x > 30) {
+    pos_x = 0;
+  }
+
+  res = ~pos_x;
+  __goblint_check(res <= 0);
+  __goblint_check(res >= -31);
+
+  int pos_x2;
+
+  if (pos_x2 < 20 || pos_x2 > 70) {
+    pos_x2 = 70;
+  }
+
+  res = ~pos_x2;
+  __goblint_check(res <= -21);
+  __goblint_check(res >= -71);
+
+  int neg_x;
+
+  if (neg_x < -30 || neg_x > -1) {
+    neg_x = -1;
+  }
+
+  res = ~neg_x;
+  __goblint_check(res >= 0);
+  __goblint_check(res <= 29);
+
+  int neg_x2;
+
+  if (neg_x2 < -70 || neg_x2 > -20) {
+    neg_x2 = -70;
+  }
+
+  res = ~neg_x2;
+  __goblint_check(res <= 69);
+  __goblint_check(res >= 19);
+
+  int other_x;
+
+  if (other_x < -63 || other_x > 20) {
+    other_x = 0;
+  }
+
+  res = ~other_x;
+  __goblint_check(res <= 62);
+  __goblint_check(res >= -21);
+
+  int other_x2;
+
+  if (other_x2 < -1 || other_x2 > 32) {
+    other_x2 = 0;
+  }
+
+  res = ~other_x2;
+  __goblint_check(res >= -33);
+  __goblint_check(res <= 0);
+
+  long long ll_res;
+  long long ll_large_x;
+
+  if (ll_large_x < -__LONG_LONG_MAX__ + 100 || ll_large_x > __LONG_LONG_MAX__ - 100) {
+    ll_large_x = 0;
+  }
+
+  ll_res = ~ll_large_x;
+  __goblint_check(ll_res <= __LONG_LONG_MAX__ - 101);
+  __goblint_check(ll_res >= -__LONG_LONG_MAX__ + 99);
+
+  long long ll_max_x;
+
+  ll_res = ~ll_max_x;
+  __goblint_check(ll_res <= __LONG_LONG_MAX__);
+  __goblint_check(ll_res >= -__LONG_LONG_MAX__ - 1);
+
+  return 0;
+}
\ No newline at end of file
diff --git a/tests/regression/98-bitwise-operations/06-bitfield.c b/tests/regression/98-bitwise-operations/06-bitfield.c
new file mode 100644
index 0000000000..a1cf8a5c7a
--- /dev/null
+++ b/tests/regression/98-bitwise-operations/06-bitfield.c
@@ -0,0 +1,38 @@
+// PARAM: --enable ana.int.interval
+
+#include <stdio.h>
+#include <goblint.h>
+ 
+struct S
+{
+    int a: 3;
+    unsigned int b : 3;  
+};
+ 
+int main(void)
+{
+    int x;
+    unsigned int y;
+    struct S s;
+
+    if (x < -30 || x > 30) {
+        x = 0;
+    }
+    y = y & 5;
+    
+    __goblint_check(s.a <= 7);
+    __goblint_check(s.a >= -4);
+    __goblint_check(s.b <= 7);
+    __goblint_check(s.b >= 0);
+    
+    s.a = 1; // NOWARN
+    s.b = 1; // NOWARN
+    s.b = y; // NOWARN
+
+    s.a = 8; // WARN
+    s.a = -5; // WARN
+    s.b = 8; // WARN
+    s.a = x; // WARN
+
+    return 0; 
+}
\ No newline at end of file
diff --git a/tests/unit/cdomains/intDomainTest.ml b/tests/unit/cdomains/intDomainTest.ml
index e001582203..212a7c8021 100644
--- a/tests/unit/cdomains/intDomainTest.ml
+++ b/tests/unit/cdomains/intDomainTest.ml
@@ -253,10 +253,14 @@ struct
     assert_equal i_minus_one_zero narrowed;
     assert_equal widened narrowed2
 
+  let test_interval_logand _ =
+    assert_equal (I.of_interval ik (Z.zero, Z.of_int 4)) (I.logand ik (I.of_interval ik (Z.of_int (-4), Z.of_int (-2))) (I.of_int ik (Z.of_int 4)))
+
   let test () = [
     "test_interval_rem" >:: test_interval_rem;
     "test_interval_widen" >:: test_interval_widen;
     "test_interval_narrow" >:: test_interval_narrow;
+    "test_interval_logand" >:: test_interval_logand;
   ]
 end