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/cdomain/value/cdomains/int/bitfieldDomain.ml b/src/cdomain/value/cdomains/int/bitfieldDomain.ml
index 30d371c512..d0c65284fd 100644
--- a/src/cdomain/value/cdomains/int/bitfieldDomain.ml
+++ b/src/cdomain/value/cdomains/int/bitfieldDomain.ml
@@ -21,6 +21,20 @@ module BitfieldInfixOps (Ints_t : IntOps.IntOps) = struct
   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
 
@@ -44,9 +58,9 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct
   let bits_invalid (z,o) = !:(z |: o)
 
   let is_const (z,o) = (z ^: o) =: one_mask
-  let is_invalid ik (z,o) = 
-    let mask = !:(Ints_t.of_bigint (snd (Size.range ik))) in
-    not ((!:(z |: o |: mask)) = Ints_t.zero)
+
+  let is_invalid (z,o) =
+    not (!:(z |: o) = Ints_t.zero)
 
   let nabla x y= if x =: (x |: y) then x else one_mask
 
@@ -61,12 +75,12 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct
 
   let logor (z1,o1)  (z2,o2) = (z1 &: z2, o1 |: o2)
 
-  let make_bitone_msk pos = Ints_t.one <<: pos
-  let make_lsb_bitmask pos =
-    let bitmsk = make_bitone_msk pos in
-    if bitmsk =: Ints_t.zero then Ints_t.zero
-    else Ints_t.sub bitmsk Ints_t.one
-  let make_msb_bitmask pos = !:(make_lsb_bitmask pos)
+  let bitmask_up_to pos =
+    let top_bit = Ints_t.one <<: pos in
+    if top_bit =: Ints_t.zero
+      then Ints_t.zero
+    else
+      Ints_t.sub top_bit Ints_t.one
 
   let get_bit bf pos = Ints_t.one &: (bf >>: pos)
 
@@ -84,71 +98,51 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct
     if isSigned ik && isPositive then Ints_t.to_bigint(signMask &: o)
     else Ints_t.to_bigint o 
 
-  (* Worst Case asymptotic runtime: O(2^n). *)
   let rec concretize (z,o) =
     if is_const (z,o) then [o]
     else
       let is_bit_unknown = not ((bits_unknown (z,o) &: Ints_t.one) =: Ints_t.zero) in
       let bit = o &: Ints_t.one in
-      let shifted_z, shifted_o = (z >>. 1, o >>: 1) in
-      if is_bit_unknown
-        then concretize (shifted_z, shifted_o) |> List.concat_map (fun c -> [c <<: 1; (c <<: 1) |: Ints_t.one])
-        else concretize (shifted_z, shifted_o) |> List.map (fun c -> c <<: 1 |: bit)
+      concretize (z >>. 1, o >>: 1) |>
+      if is_bit_unknown then
+        List.concat_map (fun c -> [c <<: 1; (c <<: 1) |: Ints_t.one])
+      else
+        List.map (fun c -> c <<: 1 |: bit)
 
   let concretize bf = List.map Ints_t.to_int (concretize bf)
 
-  let get_o (_,o) = Ints_t.to_int o
-
-  let shift_right_action ik (z,o) c =
-    let sign_msk = make_msb_bitmask (Size.bit ik - c) in
-    if (isSigned ik) && (o <: Ints_t.zero) then
-      (z >>: c, (o >>: c) |: sign_msk)
+  let shift_right ik (z,o) c =
+    let msb_pos = (Size.bit ik - c) in
+    let msb_pos = if msb_pos < 0 then 0 else msb_pos in
+    let sign_mask = !:(bitmask_up_to msb_pos) in
+    if isSigned ik && o <: Ints_t.zero then
+      (z >>: c, (o >>: c) |: sign_mask)
     else
-      ((z >>: c) |: sign_msk, o >>: c)
+      ((z >>: c) |: sign_mask, o >>: c)
 
   let shift_right ik (z1, o1) (z2, o2) = 
     if is_const (z2, o2) 
       then 
-        shift_right_action ik (z1, o1) (Ints_t.to_int o2)
+        shift_right ik (z1, o1) (Ints_t.to_int o2)
     else
-      let max_bit = Z.log2up (Z.of_int (Size.bit ik)) in
-      let mask_usefull_bits = !:(one_mask<<:max_bit) in
-      let concrete_values = concretize ((z2 &: mask_usefull_bits), (o2 &: mask_usefull_bits)) in
-      if (((o2 &: mask_usefull_bits) == Ints_t.of_int 0) && (z2 != one_mask)) || (List.length concrete_values) == 0 
-        then 
-          (one_mask, zero_mask)
-      else 
-        let (v1, v2) = (ref zero_mask, ref zero_mask) in
-        List.iter (fun x -> let (a, b) = (shift_right_action ik (z1, o1) x) in
-          v1 := !v1 |: a;
-          v2 := !v2 |: b
-        ) concrete_values;
-        (!v1, !v2)
+      let shift_counts = concretize (z2, o2) in
+      List.fold_left (fun acc c ->
+        let next = shift_right ik (z1, o1) c in join acc next
+      ) (zero_mask, zero_mask) shift_counts
 
-  let shift_left_action _ (z,o) c =
-    let z_msk = make_lsb_bitmask c in
-    ((z <<: c) |: z_msk, o <<: c)
+  let shift_left _ (z,o) c =
+    let zero_mask = bitmask_up_to c in
+    ((z <<: c) |: zero_mask, o <<: c)
 
   let shift_left ik (z1, o1) (z2, o2) = 
-    (* (one_mask, Ints_t.of_int (Size.bit ik)) *)
     if is_const (z2, o2) 
       then 
-        shift_left_action ik (z1, o1) (Ints_t.to_int o2)
+        shift_left ik (z1, o1) (Ints_t.to_int o2)
     else
-      let max_bit = Z.log2up (Z.of_int (Size.bit ik)) in
-      let mask_usefull_bits = !:(one_mask <<: max_bit) in
-      let concrete_values = concretize ((z2 &: mask_usefull_bits), (o2 &: mask_usefull_bits)) in
-      if (((o2 &: mask_usefull_bits) == Ints_t.of_int 0) && (z2 != one_mask)) || (List.length concrete_values) == 0 
-      then 
-        (one_mask, zero_mask)
-      else 
-        let (v1, v2) = (ref zero_mask, ref zero_mask) in
-        List.iter (fun x -> let (a, b) = (shift_left_action ik (z1, o1) x) in
-          v1 := !v1 |: a;
-          v2 := !v2 |: b
-        ) concrete_values;
-        (!v1, !v2)
-
+      let shift_counts = concretize (z2, o2) in
+      List.fold_left (fun acc c ->
+        let next = shift_left ik (z1, o1) c in join acc next
+      ) (zero_mask, zero_mask) shift_counts
 end
 
 module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Ints_t.t and type t = (Ints_t.t * Ints_t.t) = struct
@@ -163,7 +157,11 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int
 
   let top () = (BArith.one_mask, BArith.one_mask)
   let bot () = (BArith.zero_mask, BArith.zero_mask)
-  let top_of ik = top ()
+
+  let top_of ik = 
+    if 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) = 
@@ -204,37 +202,48 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int
   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 range ik bf = (BArith.min ik bf, BArith.max ik bf)
+  
+  let maximal (z,o) =     
+    if (z < Ints_t.zero) <> (o < Ints_t.zero) then Some o
+    else None
 
-  let maximal (z,o) = let isPositive = z < Ints_t.zero in
-    if o < Ints_t.zero && isPositive then (match Ints_t.upper_bound with Some maxVal -> Some (maxVal &: o) | None -> None )
-    else Some o 
+  let minimal (z,o) =     
+    if (z < Ints_t.zero) <> (o < Ints_t.zero) then Some (!:z)
+    else None
 
-  let minimal (z,o) = let isNegative = o < Ints_t.zero in
-    if z < Ints_t.zero && isNegative then (match Ints_t.lower_bound with Some minVal -> Some (minVal |: (!:z)) | None -> None )
-    else Some (!:z)
+  let wrap ik (z,o) = 
+    let (min_ik, max_ik) = Size.range ik in
+    if isSigned ik then
+      let newz = (z &: (Ints_t.of_bigint max_ik)) |: ((Ints_t.of_bigint min_ik) *: (BArith.get_bit z (Size.bit ik - 1))) in
+      let newo = (o &: (Ints_t.of_bigint max_ik)) |: ((Ints_t.of_bigint min_ik) *: (BArith.get_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) ik (z,o) = 
-    if BArith.is_invalid ik (z,o) then 
+    if BArith.is_invalid (z,o) then 
       (bot (), {underflow=false; overflow=false})
     else      
       let (min_ik, max_ik) = Size.range ik in
-      let wrap ik (z,o) = 
-        if isSigned ik then
-          let newz = (z &: (Ints_t.of_bigint max_ik)) |: ((Ints_t.of_bigint min_ik) *: (BArith.get_bit z (Size.bit ik - 1))) in
-          let newo = (o &: (Ints_t.of_bigint max_ik)) |: ((Ints_t.of_bigint min_ik) *: (BArith.get_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)
-      in
-      let (min,max) = range ik (z,o) in
-      let underflow = Z.compare min min_ik < 0 in
-      let overflow = Z.compare max max_ik > 0 in
+      let isPos = z < Ints_t.zero in 
+      let isNeg = o < Ints_t.zero in
+      let underflow = if 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      
       let new_bitfield = wrap ik (z,o)
       in
-      if suppress_ovwarn then (new_bitfield, {underflow=false; overflow=false})
-      else (new_bitfield, {underflow=underflow; overflow=overflow})
+      let overflow_info = if suppress_ovwarn then {underflow=false; overflow=false} else  {underflow=underflow; overflow=overflow} in      
+      if not (underflow || overflow) then
+        ((z,o), overflow_info)
+      else if should_wrap ik then
+        (new_bitfield, overflow_info)
+      else if should_ignore_overflow ik then 
+        (M.warn ~category:M.Category.Integer.overflow "Bitfield: Value was outside of range, indicating overflow, but 'sem.int.signed_overflow' is 'assume_none' -> Returned Top";
+        (* (bot (), overflow_info)) *)
+        (top_of ik, overflow_info))
+      else 
+        (top_of ik, overflow_info)
 
   let cast_to ?(suppress_ovwarn=false) ?torg ?no_ov t = norm ~suppress_ovwarn t
 
@@ -296,9 +305,8 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int
         analyze_bits (pos - 1) new_acc
     in      
     let result = analyze_bits (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
-    norm ~suppress_ovwarn ik casted
-
+    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
 
@@ -351,15 +359,42 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int
 
   let lognot ik i1 = BArith.lognot i1 |> norm ik |> fst
 
+  let precision ik = snd @@ Size.bits ik
+  let cap_bitshifts_to_precision ik (z,o) =
+    let mask = BArith.bitmask_up_to (Int.succ @@ Z.log2up @@ Z.of_int @@ precision ik) in
+    (z |: !:mask, o &: mask)
+
+  let is_invalid_shift_operation ik a b = BArith.is_invalid b
+    || BArith.is_invalid a
+
+  let is_undefined_shift_operation ik a b =
+    let some_negatives = BArith.min ik b < Z.zero in
+    let b_is_geq_precision = Z.to_int @@ BArith.min ik b >= precision ik in
+    (isSigned ik) && (some_negatives || b_is_geq_precision) && not (a = BArith.zero)
+
   let shift_right ik a b = 
-    M.trace "bitfield" "shift_right";
-    if BArith.is_invalid ik b || BArith.is_invalid ik a || (isSigned ik && BArith.min ik b < Z.zero) then (bot (), {underflow=false; overflow=false})
-    else norm ik (BArith.shift_right ik a b)
+    if M.tracing then M.trace "bitfield" "%a >> %a" pretty a pretty b; 
+    if is_invalid_shift_operation ik a b
+      then
+        (bot (), {underflow=false; overflow=false})
+    else if is_undefined_shift_operation ik a b
+      then
+        (top_of ik, {underflow=false; overflow=false})
+    else
+      let defined_shifts = cap_bitshifts_to_precision ik b in
+      norm ik @@ BArith.shift_right ik a defined_shifts
 
   let shift_left ik a b =
-    M.trace "bitfield" "shift_left";
-    if BArith.is_invalid ik b || BArith.is_invalid ik a || (isSigned ik && BArith.min ik b < Z.zero) then (bot (), {underflow=false; overflow=false})
-    else norm ik (BArith.shift_left ik a b)
+    if M.tracing then M.trace "bitfield" "%a << %a" pretty a pretty b;
+    if is_invalid_shift_operation ik a b
+      then
+        (bot (), {underflow=false; overflow=false})
+    else if is_undefined_shift_operation ik a b
+      then
+        (top_of ik, {underflow=false; overflow=false})
+    else
+      let defined_shifts = cap_bitshifts_to_precision ik b in
+      norm ik @@ BArith.shift_left ik a defined_shifts
 
   (* Arith *)
 
@@ -388,10 +423,6 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int
     let (rv, rm) = add_paper pv pm qv qm in 
     let o3 = rv |: rm in 
     let z3 = !:rv |: rm in
-    (* let _ = print_endline (show (z3, o3)) in 
-    let _ = (match maximal (z3,o3) with Some k -> print_endline (Ints_t.to_string k) | None -> print_endline "None") in
-    let _ = (match minimal (z3,o3) with Some k -> print_endline (Ints_t.to_string k) | None -> print_endline "None") in
-    let _ = (match Size.range ik with (a,b) -> print_endline ("(" ^ Z.to_string a ^ "; " ^ Z.to_string b ^ ")")) in  *)
     norm ik (z3,o3)
 
   let sub ?no_ov ik (z1, o1) (z2, o2) =
@@ -407,11 +438,11 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int
     let rv = dv &: !:mu in
     let rm = mu in 
     let o3 = rv |: rm in 
-    let z3 = !:rv |: rm in
+    let z3 = !:rv |: rm in    
     norm ik (z3, o3)
 
   let neg ?no_ov ik x =
-    M.trace "bitfield" "neg";
+    if M.tracing then M.trace "bitfield" "neg";
     sub ?no_ov ik BArith.zero x
 
   let mul ?no_ov ik (z1, o1) (z2, o2) =
@@ -448,7 +479,9 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Int
     norm ik (!z3, !o3)
 
   let div ?no_ov ik (z1, o1) (z2, o2) =
-    let res = if BArith.is_const (z1, o1) && BArith.is_const (z2, o2) then (let tmp = z1 /: z2 in (!:tmp, tmp)) else top_of ik in
+    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) && is_power_of_two o2 then (z1 >>: (Ints_t.to_int o2), o1 >>: (Ints_t.to_int o2))
+      else top_of ik in
     norm ik res
 
   let rem ik x y = 
diff --git a/src/cdomain/value/cdomains/int/congruenceDomain.ml b/src/cdomain/value/cdomains/int/congruenceDomain.ml
index 964485acee..549f1b5059 100644
--- a/src/cdomain/value/cdomains/int/congruenceDomain.ml
+++ b/src/cdomain/value/cdomains/int/congruenceDomain.ml
@@ -500,7 +500,9 @@ struct
     refn
 
   let refine_with_congruence ik a b = meet ik a b
-  let refine_with_bitfield ik a b = a
+  let refine_with_bitfield ik a (z,o) = 
+    if Z.lognot z = o then meet ik a (Some (o, Z.zero))
+    else a
   let refine_with_excl_list ik a b = a
   let refine_with_incl_list ik a b = a
 
diff --git a/src/cdomain/value/cdomains/int/defExcDomain.ml b/src/cdomain/value/cdomains/int/defExcDomain.ml
index 1df48ba141..38921e16c8 100644
--- a/src/cdomain/value/cdomains/int/defExcDomain.ml
+++ b/src/cdomain/value/cdomains/int/defExcDomain.ml
@@ -300,8 +300,10 @@ struct
       norm ik @@ (`Excluded (ex, r))
 
     let to_bitfield ik x = 
-      let one_mask = Z.lognot Z.zero 
-      in (one_mask, one_mask)
+      match x with 
+      `Definite c -> (Z.lognot c, c) |
+      _ -> let one_mask = Z.lognot Z.zero 
+           in (one_mask, one_mask)
 
   let starting ?(suppress_ovwarn=false) ikind x =
     let _,u_ik = Size.range ikind in
@@ -534,7 +536,9 @@ struct
     ] (* S TODO: decide frequencies *)
 
   let refine_with_congruence ik a b = a
-  let refine_with_bitfield ik x y = x
+  let refine_with_bitfield ik x (z,o) = 
+    if Z.lognot z = o then meet ik x (`Definite o)
+    else 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 b169f299d2..29497e3f31 100644
--- a/src/cdomain/value/cdomains/int/enumsDomain.ml
+++ b/src/cdomain/value/cdomains/int/enumsDomain.ml
@@ -251,7 +251,13 @@ module Enums : S with type int_t = Z.t = struct
   let to_incl_list = function Inc s when not (BISet.is_empty s) -> Some (BISet.elements s) | _ -> None
 
   let to_bitfield ik x = 
-    let one_mask = Z.lognot Z.zero 
+    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 (Z.lognot o, o) |
+    Inc i -> BISet.fold (fun o (az, ao) -> (Z.logor (Z.lognot o) az, Z.logor o ao)) i (Z.zero, Z.zero) |
+    _ -> let one_mask = Z.lognot Z.zero     
     in (one_mask, one_mask)
 
   let starting ?(suppress_ovwarn=false) ikind x =
@@ -360,7 +366,9 @@ 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 y = x
+  let refine_with_bitfield ik x (z,o) =
+    if Z.lognot z = o then meet ik x (Inc (BISet.singleton o))
+    else x
 
   let refine_with_interval ik a b = a (* TODO: refine inclusion (exclusion?) set *)
 
diff --git a/src/cdomain/value/cdomains/int/intDomTuple.ml b/src/cdomain/value/cdomains/int/intDomTuple.ml
index 74072b80a6..de4486b10e 100644
--- a/src/cdomain/value/cdomains/int/intDomTuple.ml
+++ b/src/cdomain/value/cdomains/int/intDomTuple.ml
@@ -63,13 +63,14 @@ 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
@@ -79,7 +80,8 @@ module IntDomTupleImpl = struct
     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);
+    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 *)
@@ -308,7 +310,8 @@ module IntDomTupleImpl = struct
     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
@@ -316,13 +319,14 @@ module IntDomTupleImpl = struct
       , 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 
-      , map (fun ?no_ov x -> r.f1_ovc ?no_ov (module I6) x |> fst) f)
+      , BatOption.map fst bf)
 
   (* map2 with overflow check *)
   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
@@ -330,7 +334,7 @@ module IntDomTupleImpl = struct
       , 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 
-      , opt_map2 (fun ?no_ov x y -> r.f2_ovc ?no_ov (module I6) x y |> fst) xf yf)
+      , BatOption.map fst bf)
 
   let map ik r (a, b, c, d, e, f) =
     refine ik
diff --git a/src/cdomain/value/cdomains/int/intervalDomain.ml b/src/cdomain/value/cdomains/int/intervalDomain.ml
index bef586dbb7..c7c281fe9e 100644
--- a/src/cdomain/value/cdomains/int/intervalDomain.ml
+++ b/src/cdomain/value/cdomains/int/intervalDomain.ml
@@ -106,7 +106,18 @@ struct
     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
-    
+
+    let wrap ik (z,o) = 
+      let (min_ik, max_ik) = Size.range ik in
+      if isSigned ik then
+        let newz = Ints_t.logor (Ints_t.logand z (Ints_t.of_bigint max_ik)) (Ints_t.mul (Ints_t.of_bigint min_ik) (Ints_t.logand Ints_t.one (Ints_t.shift_right z (Size.bit ik - 1)))) in
+        let newo = Ints_t.logor (Ints_t.logand o (Ints_t.of_bigint max_ik)) (Ints_t.mul (Ints_t.of_bigint min_ik) (Ints_t.logand Ints_t.one (Ints_t.shift_right o (Size.bit ik - 1)))) in
+        (newz,newo)
+      else
+        let newz = Ints_t.logor z (Ints_t.lognot (Ints_t.of_bigint max_ik)) in
+        let newo = Ints_t.logand o (Ints_t.of_bigint max_ik) in
+        (newz,newo)
+      in    
     let rec analyze_bits pos (acc_z, acc_o) =
       if pos < 0 then (acc_z, acc_o)
       else
@@ -138,7 +149,7 @@ struct
     in      
     let result = analyze_bits (Size.bit ik - 1) (Ints_t.zero, Ints_t.zero) 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 casted
+    in wrap ik casted
 
   let of_bool _ik = function true -> one | false -> zero
   let to_bool (a: t) = match a with
diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index 991fb114cf..eeb2789004 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -6,4 +6,4 @@ include DefExcDomain
 include EnumsDomain
 include CongruenceDomain
 include BitfieldDomain
-include IntDomTuple
+include IntDomTuple
\ No newline at end of file
diff --git a/tests/regression/82-bitfield/02-complex-arith.c b/tests/regression/82-bitfield/02-complex-arith.c
index ff0db443ee..a1f718b86b 100644
--- a/tests/regression/82-bitfield/02-complex-arith.c
+++ b/tests/regression/82-bitfield/02-complex-arith.c
@@ -1,5 +1,6 @@
 // PARAM: --disable ana.int.interval --disable ana.int.def_exc --enable ana.int.bitfield
 #include <stdlib.h>
+#include <goblint.h>
 
 int main() {
   int a;
@@ -22,10 +23,10 @@ int main() {
   int c_add = a + b;
 
   if (c_add == 40) {
-    goblint_check(1);  // reachable
+    __goblint_check(1);  // reachable
   }
   if (c_add == 42) {
-    goblint_check(1);  // reachable
+    __goblint_check(1);  // reachable
   }
   if (c_add > 42 || c_add < 40) {
     __goblint_check(0);  // NOWARN (unreachable)
@@ -36,10 +37,10 @@ int main() {
   int c_minus = b - a;
 
   if (c_minus == 6) {
-    goblint_check(1);  // reachable
+    __goblint_check(1);  // reachable
   }
   if (c_minus == 4) {
-    goblint_check(1);  // reachable
+    __goblint_check(1);  // reachable
   }
   if (c_minus > 6 || c_minus < 4) {
     __goblint_check(0);  // NOWARN (unreachable)
@@ -50,10 +51,10 @@ int main() {
   int c_mult = a * b;
 
   if (c_mult == 391) {
-    goblint_check(1);  // reachable
+    __goblint_check(1);  // reachable
   }
   if (c_mult == 437) {
-    goblint_check(1);  // reachable
+    __goblint_check(1);  // reachable
   }
 
   // DIV
diff --git a/tests/regression/82-bitfield/10-refine-intervalB.c b/tests/regression/82-bitfield/10-refine-intervalB.c
index d9441f05e9..bf1be8bfea 100644
--- a/tests/regression/82-bitfield/10-refine-intervalB.c
+++ b/tests/regression/82-bitfield/10-refine-intervalB.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.int.interval --enable ana.int.bitfield --set ana.int.refinement fixpoint --trace inv --trace branch --trace invariant
+// PARAM: --enable ana.int.interval --enable ana.int.bitfield --set ana.int.refinement fixpoint
 #include <goblint.h>
 
 int main() {
diff --git a/tests/regression/82-bitfield/11-refine-intervalC.c b/tests/regression/82-bitfield/11-refine-intervalC.c
index 4abaac9b89..6dc63b2494 100644
--- a/tests/regression/82-bitfield/11-refine-intervalC.c
+++ b/tests/regression/82-bitfield/11-refine-intervalC.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.int.interval --enable ana.int.bitfield --set ana.int.refinement fixpoint --trace inv --trace branch --trace invariant
+// PARAM: --enable ana.int.interval --enable ana.int.bitfield --set ana.int.refinement fixpoint
 #include <goblint.h>
 
 int main() {
diff --git a/tests/unit/cdomains/intDomainTest.ml b/tests/unit/cdomains/intDomainTest.ml
index 93356757ff..1b6b963f4f 100644
--- a/tests/unit/cdomains/intDomainTest.ml
+++ b/tests/unit/cdomains/intDomainTest.ml
@@ -255,7 +255,13 @@ struct
   module I = IntDomain.SOverflowUnlifter (I)
 
   let ik = Cil.IInt
+  let ik_uint = Cil.IUInt
   let ik_char = Cil.IChar
+  let ik_uchar = Cil.IUChar
+  let ik_short = Cil.IShort
+  let ik_ushort = Cil.IUShort
+
+  let ik_lst = [ik_char; ik_uchar; ik_short; ik_ushort; ik; ik_uint;]
 
   let assert_equal x y =
     OUnit.assert_equal ~printer:I.show x y
@@ -332,25 +338,25 @@ struct
 
   let test_wrap_1 _ =
     let z = of_int 31376 in
-    let b_uint8 = I.of_int IChar z in
-    let b_sint8 = I.of_int ISChar z 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 IShort z in
+    let b_sint16 = I.of_int IUShort z in
 
     (* See https://www.simonv.fr/TypesConvert/?integers *)
-    assert_equal (I.of_int IChar (of_int 144)) b_uint8;
-    assert_equal (I.of_int ISChar (of_int (-112))) b_sint8;
+    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 IShort (of_int 31376)) b_sint16
+    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 IChar (I.of_int IChar z1) (I.of_int IChar z2) in
+    let join_cast_unsigned = I.join IUChar (I.of_int IUChar z1) (I.of_int IUChar z2) in
 
-    let expected_unsigned = I.join IChar (I.of_int IChar (of_int 147)) (I.of_int IChar (of_int 150)) 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 IChar (I.of_int IChar (of_int (-106))) (I.of_int IChar (of_int (-109))) 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
@@ -396,6 +402,7 @@ struct
     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
@@ -415,8 +422,8 @@ struct
   let test_cast_to _ =
     let b1 = I.of_int ik (of_int 1234) in
 
-    assert_equal (I.of_int IChar (of_int (210))) (I.cast_to IChar b1);
-    assert_equal (I.of_int ISChar (of_int (-46))) (I.cast_to ISChar b1);
+    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)
 
@@ -468,42 +475,175 @@ struct
     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 string_of_ik ik = match ik with
+    | Cil.IInt -> "int"
+    | Cil.IUInt -> "unsigned_int"
+    | Cil.IChar -> "char"
+    | Cil.IUChar -> "unsigned_char"
+    | Cil.IShort -> "short"
+    | Cil.IUShort -> "unsigned_short"
+    | _ -> "undefined C primitive type"
+
+  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) shift ik a b expected = 
+    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 = (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"
+      (string_of_ik 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
 
-  let assert_shift shift symb ik a b expected_values = 
-    let bf1 = of_list ik (List.map of_int a) in
-    let bf2 = of_list ik (List.map of_int b) in
-    let bf_shift_resolution = (shift ik bf1 bf2) in
-    let x = of_list ik (List.map of_int expected_values) in
-    let output_string = I.show bf1 ^ symb ^ I.show bf2 ^ " was: " ^ I.show bf_shift_resolution ^ " but should be: " ^  I.show x in
-    let output  = "Test shift ("^ I.show bf1 ^ symb ^ I.show bf2  ^ ") failed: " ^ output_string in
-    assert_bool (output) (I.equal bf_shift_resolution x)
+  let assert_shift_left ?(rev_cond=false) = assert_shift ~rev_cond:rev_cond `L
+  let assert_shift_right ?(rev_cond=false) = assert_shift ~rev_cond:rev_cond `R
 
-  let assert_shift_left ik a b res = assert_shift I.shift_left " << " ik a b res
-  let assert_shift_right ik a b res = assert_shift I.shift_right " >> " ik a b res
+  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_left _ =
-    assert_shift_left ik_char [-3] [7] [-128];
-    assert_shift_left ik [-3] [7] [-384];
-    assert_shift_left ik [2] [1; 2] [2; 4; 8; 16];
-    assert_shift_left ik [1; 2] [1] [2; 4];
-    assert_shift_left ik [-1; 1] [1] [-2; 2];
-    assert_shift_left ik [-1] [4] [-16];
-    assert_shift_left ik [-1] [1] [-2];
-    assert_shift_left ik [-1] [2] [-4];
-    assert_shift_left ik [-1] [3] [-8];
-    assert_shift_left ik [-2] [1; 2] [-2; -4; -8; -16];
-    assert_shift_left ik [-1] [1; 2] [-1; -2; -4; -8];
-    assert_shift_left ik [1073741824] [128; 384] [0];
-    assert_shift_left ik [1073741824] [0; 128; 384] [1073741824]
-
-  let test_shift_right _ =
-    assert_shift_right ik [4] [1] [2];
-    assert_shift_right ik [-4] [1] [-2];
-    assert_shift_right ik [1] [1] [0];
-    assert_shift_right ik [1] [1; 2] [0; 1];
-    assert_shift_right ik [1; 2] [1; 2] [0; 1; 2; 3];
-    assert_shift_right ik [32] [64; 2] [8; 32];
-    assert_shift_right ik [32] [128; 384] [0]
+  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 ~count:1000 (*~collect: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" (string_of_ik 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" (string_of_ik 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 highest_bit_set ?(is_neg=false) ik =
+    let open IntDomain.Size in
+    let pos = Int.pred @@ snd @@ bits ik in
+    (if isSigned ik then if is_neg
+      then cast ik @@ Z.of_int @@ Int.neg @@ Int.shift_left 1 pos
+      else cast ik @@ Z.of_int @@ Int.pred @@ Int.shift_left 1 pos
+    else
+      cast ik @@ Z.of_int @@ Int.shift_left 1 pos) |> Z.to_int
+
+  let test_shift_left =
+  [
+    "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]);
+
+    List.iter (fun ik ->
+      assert_shift_left ik bot (`I [1]) bot;
+      assert_shift_left ik (`I [1]) bot bot;
+      assert_shift_left ik bot bot bot;
+
+      assert_shift_left ik (`I [0]) top (`I [0]);
+
+      if isSigned ik
+      then (
+        (*assert_shift_left ~rev_cond:true ik (`I [1]) top top;*) (* TODO fails *)
+
+        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 ~rev_cond:true ik (`I [1]) (`I [under_precision ik]) top;
+        assert_shift_left ik (`I [1]) (`I [precision ik]) top;
+        assert_shift_left ik (`I [1]) (`I [over_precision ik]) top;
+
+        assert_shift_left ik (`I [-1]) (`I [under_precision ik]) (`I [highest_bit_set ~is_neg:true ik]);
+        assert_shift_left ik (`I [-1]) (`I [precision ik]) top; 
+        assert_shift_left ik (`I [-1]) (`I [over_precision ik]) top; 
+      ) else (
+        (* See C11 N2310 at 6.5.7 *)
+        assert_shift_left ik (`I [1]) (`I [under_precision ik]) (`I [highest_bit_set ik]);
+        assert_shift_left ik (`I [1]) (`I [precision ik]) (`I [0]);
+        assert_shift_left 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 (`I [1]) bot;
+      assert_shift_right ik (`I [1]) bot bot;
+      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;*) (* TODO fails *)
+
+        assert_shift_right ik (`I [2]) (`I [-1]) top; (* Negative shifts are undefined behavior *)
+        assert_shift_right ik (`I [min_of ik]) top top;
+
+        assert_shift_right ik (`I [max_of ik]) (`I [under_precision ik]) (`I [1]);
+        assert_shift_right ik (`I [max_of ik]) (`I [precision ik]) top;
+        assert_shift_right ik (`I [max_of ik]) (`I [over_precision ik]) top;
+
+        assert_shift_right ik (`I [min_of ik]) (`I [under_precision ik]) (`I [-2]);
+        assert_shift_right ik (`I [min_of ik]) (`I [precision ik]) top;
+        assert_shift_right ik (`I [min_of ik]) (`I [over_precision ik]) top;
+      ) else (
+        (* See C11 N2310 at 6.5.7 *)
+        assert_shift_right ik (`I [max_of ik]) (`I [under_precision ik]) (`I [1]);
+        assert_shift_right ik (`I [max_of ik]) (`I [precision ik]) (`I [0]);
+        assert_shift_right ik (`I [max_of ik]) (`I [over_precision ik]) (`I [0]);
+      )
+
+    ) ik_lst
+    
+  ]
 
 
   (* Arith *)
@@ -761,8 +901,8 @@ struct
     "test_logor" >:: test_logor;
     "test_lognot" >:: test_lognot;
     
-    "test_shift_left" >:: test_shift_left;
-    "test_shift_right" >:: test_shift_right;
+    "test_shift_left" >::: test_shift_left;
+    "test_shift_right" >::: test_shift_right;
 
     "test_add" >:: test_add;
     "test_sub" >:: test_sub;
@@ -868,22 +1008,29 @@ struct
   let of_list ik is = List.fold_left (fun acc x -> B.join ik acc (B.of_int ik x)) (B.bot ()) is
 
   let v1 = Z.of_int 0
-  let v2 = Z.of_int 2
-  let vr = Z.mul v1 v2
+  let v2 = Z.of_int 0
+  let vr = Z.add v1 v2
 
-  let is = [-3;3]
-  let res = [0;13;26;39;52;65;78;91]
+  let is = [0;1]
+  let res = [0;-1]
 
-  let b1 = of_list ik (List.map Z.of_int is)
-  let b2 = B.of_int ik v2
+  let b1 = B.of_int ik v1
+  let b2 = of_list ik (List.map Z.of_int is)
   let br = of_list ik (List.map Z.of_int res)
 
-  let test_add _ = assert_equal ~cmp:B.leq ~printer:B.show br (B.mul ik b2 b1)
+  let bool_res = B.join ik (B.of_int ik Z.zero) (B.of_int ik Z.one)
+
+  (* let _ = print_endline (B.show b1)
+  let _ = print_endline (B.show b2)
+  let _ = print_endline (B.show (B.sub ik b1 b2))
+  let _ = print_endline (B.show br) *)
+
+  let test_add _ = assert_equal ~cmp:B.leq ~printer:B.show br (B.sub ik b1 b2)
 
-  let test_lt _ = assert_equal ~cmp:B.leq ~printer:B.show (B.join ik (B.of_int ik Z.zero) (B.of_int ik Z.one)) (B.lt ik b1 b2)
+  let test_lt _ = assert_equal ~cmp:B.leq ~printer:B.show bool_res (B.lt ik b1 b2)
 
   let test () =  [
-    "test_lt" >:: test_lt;
+    "test_add" >:: test_add;
   ]
 end