diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml
index 841fe15d6c..f81c89018a 100644
--- a/src/analyses/apron/relationAnalysis.apron.ml
+++ b/src/analyses/apron/relationAnalysis.apron.ml
@@ -256,8 +256,9 @@ struct
             if M.tracing then M.traceli "relation" "assign inner %a = %a (%a)" CilType.Varinfo.pretty v d_exp e' d_plainexp e';
             if M.tracing then M.trace "relation" "st: %a" RD.pretty apr';
             let r = RD.assign_exp ask apr' (RV.local v) e' (no_overflow ask simplified_e) in
-            if M.tracing then M.traceu "relation" "-> %a" RD.pretty r;
-            r
+            let r' = assert_type_bounds ask r v in
+            if M.tracing then M.traceu "relation" "-> %a" RD.pretty r';
+            r'
           )
       )
     in
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index e4288d05b8..3688ac8666 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -928,7 +928,7 @@ struct
     (* | Lval (Mem e, ofs) -> get ~man st (eval_lv ~man (Mem e, ofs)) *)
     | (Mem e, ofs) ->
       (*if M.tracing then M.tracel "cast" "Deref: lval: %a" d_plainlval lv;*)
-      let rec contains_vla (t:typ) = match t with
+      let rec contains_vla (t:typ) = match Cil.unrollType t with
         | TPtr (t, _) -> contains_vla t
         | TArray(t, None, args) -> true
         | TArray(t, Some exp, args) when isConstant exp -> contains_vla t
@@ -1452,7 +1452,8 @@ struct
         match eval_rv_address ~man man.local e with
         | Address a ->
           let slen = Seq.map String.length (List.to_seq (AD.to_string a)) in
-          let lenOf = function
+          let lenOf t =
+            match Cil.unrollType t with
             | TArray (_, l, _) -> (try Some (lenOfArray l) with LenOfArray -> None)
             | _ -> None
           in
@@ -1563,7 +1564,7 @@ struct
               let lval = Addr.Mval.to_cil mval in
               (try `Lifted (Bytes.to_string (Hashtbl.find char_array lval))
                with Not_found -> Queries.Result.top q)
-            | _ -> (* what about ISChar and IUChar? *)
+            | _ -> (* TODO: what about ISChar and IUChar? what about TEnum? *)
               (* ignore @@ printf "Type %a\n" d_plaintype t; *)
               Queries.Result.top q
           end
@@ -2030,10 +2031,8 @@ struct
       match exp with
       | None -> nst
       | Some exp ->
-        let t_override = match Cilfacade.fundec_return_type fundec with
-          | TVoid _ -> M.warn ~category:M.Category.Program "Returning a value from a void function"; assert false
-          | ret -> ret
-        in
+        let t_override = Cilfacade.fundec_return_type fundec in
+        assert (not (Cil.isVoidType t_override)); (* Returning a value from a void function, CIL removes the Return expression for us anyway. *)
         let rv = eval_rv ~man man.local exp in
         let st' = set ~man ~t_override nst (return_var ()) t_override rv in
         match ThreadId.get_current ask with
@@ -2284,7 +2283,7 @@ struct
         ) a
     | _ -> false
 
-  let get_size_of_ptr_target man ptr =
+  let get_size_of_ptr_target man ptr = (* TODO: deduplicate with memOutOfBounds *)
     let intdom_of_int x =
       ID.of_int (Cilfacade.ptrdiff_ikind ()) (Z.of_int x)
     in
@@ -2301,7 +2300,7 @@ struct
         let pts_elems_to_sizes (addr: Queries.AD.elt) =
           begin match addr with
             | Addr (v, _) ->
-              begin match v.vtype with
+              begin match Cil.unrollType v.vtype with
                 | TArray (item_typ, _, _) ->
                   let item_typ_size_in_bytes = size_of_type_in_bytes item_typ in
                   begin match man.ask (Queries.EvalLength ptr) with
diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml
index fd52d099bf..a32d804794 100644
--- a/src/analyses/baseInvariant.ml
+++ b/src/analyses/baseInvariant.ml
@@ -112,14 +112,18 @@ struct
         r
       )
     | Mem (Lval lv), off ->
-      let lvals = eval_lv ~man st (Mem (Lval lv), off) in
-      let res = AD.fold (fun a acc ->
+      (* Underlying lvals (may have offsets themselves), e.g., for struct members NOT including any offset appended to outer Mem *)
+      let lvals = eval_lv ~man st (Mem (Lval lv), NoOffset) in
+      (* Additional offset of value being refined in Addr Offset type *)
+      let original_offset = convert_offset ~man st off in
+      let res = AD.fold (fun base_a acc ->
           Option.bind acc (fun acc ->
-              match a with
-              | Addr (base, _) as orig ->
-                let (a:VD.t) = Address (AD.singleton (AD.Addr.of_var base)) in
-                if M.tracing then M.tracel "inv" "Consider case of lval %a = %a" d_lval lv VD.pretty a;
-                let st = set' lv a st in
+              match base_a with
+              | Addr _ ->
+                let (lval_a:VD.t) = Address (AD.singleton base_a) in
+                if M.tracing then M.tracel "inv" "Consider case of lval %a = %a" d_lval lv VD.pretty lval_a;
+                let st = set' lv lval_a st in
+                let orig = AD.Addr.add_offset base_a original_offset in
                 let old_val = get ~man st (AD.singleton orig) None in
                 let old_val = VD.cast (Cilfacade.typeOfLval x) old_val in (* needed as the type of this pointer may be different *)
                 (* this what I would originally have liked to do, but eval_rv_lval_refine uses queries and thus stale values *)
@@ -237,7 +241,7 @@ struct
       | BinOp(op, rval, Lval x, typ) -> derived_invariant (BinOp(switchedOp op, Lval x, rval, typ)) tv
       | BinOp(op, CastE (t1, c1), CastE (t2, c2), t) when (op = Eq || op = Ne) && typeSig t1 = typeSig t2 && VD.is_statically_safe_cast t1 (Cilfacade.typeOf c1) && VD.is_statically_safe_cast t2 (Cilfacade.typeOf c2)
         -> derived_invariant (BinOp (op, c1, c2, t)) tv
-      | BinOp(op, CastE (TInt (ik, _) as t1, Lval x), rval, typ) ->
+      | BinOp(op, CastE (t1, Lval x), rval, typ) when Cil.isIntegralType t1 ->
         begin match eval_rv ~man st (Lval x) with
           | Int v ->
             if VD.is_dynamically_safe_cast t1 (Cilfacade.typeOfLval x) (Int v) then
@@ -246,7 +250,7 @@ struct
               `NotUnderstood
           | _ -> `NotUnderstood
         end
-      | BinOp(op, rval, CastE (TInt (_, _) as ti, Lval x), typ) ->
+      | BinOp(op, rval, CastE (ti, Lval x), typ) when Cil.isIntegralType ti ->
         derived_invariant (BinOp (switchedOp op, CastE(ti, Lval x), rval, typ)) tv
       | BinOp(op, (Const _ | AddrOf _), rval, typ) ->
         (* This is last such that we never reach here with rval being Lval (it is swapped around). *)
@@ -611,8 +615,8 @@ struct
       else
         match exp, c_typed with
         | UnOp (LNot, e, _), Int c ->
-          (match Cilfacade.typeOf e with
-           | TInt  _ | TPtr _ ->
+          (match Cil.unrollType (Cilfacade.typeOf e) with
+           | TInt  _ | TEnum _ | TPtr _ ->
              let ikind = Cilfacade.get_ikind_exp e in
              let c' =
                match ID.to_bool (unop_ID LNot c) with
diff --git a/src/analyses/extractPthread.ml b/src/analyses/extractPthread.ml
index d31243ae70..1c02d0cbfa 100644
--- a/src/analyses/extractPthread.ml
+++ b/src/analyses/extractPthread.ml
@@ -359,7 +359,7 @@ end
 module Variable = struct
   type t = varinfo
 
-  let is_integral v = match v.vtype with TInt _ -> true | _ -> false
+  let is_integral v = isIntegralType v.vtype
 
   let is_global v = v.vglob
 
diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml
index 93ca1c810f..ff3946d047 100644
--- a/src/analyses/memOutOfBounds.ml
+++ b/src/analyses/memOutOfBounds.ml
@@ -77,7 +77,7 @@ struct
         ) a
     | _ -> false
 
-  let get_size_of_ptr_target man ptr =
+  let get_size_of_ptr_target man ptr = (* TODO: deduplicate with base *)
     if points_to_alloc_only man ptr then
       (* Ask for BlobSize from the base address (the second component being set to true) in order to avoid BlobSize giving us bot *)
       man.ask (Queries.BlobSize {exp = ptr; base_address = true})
@@ -92,7 +92,7 @@ struct
                 set_mem_safety_flag InvalidDeref;
                 M.warn "Var %a is potentially accessed out-of-scope. Invalid memory access may occur" CilType.Varinfo.pretty v
               );
-              begin match v.vtype with
+              begin match Cil.unrollType v.vtype with
                 | TArray (item_typ, _, _) ->
                   let item_typ_size_in_bytes = size_of_type_in_bytes item_typ in
                   begin match man.ask (Queries.EvalLength ptr) with
diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml
index c712ca9644..e378e1be33 100644
--- a/src/analyses/mutexAnalysis.ml
+++ b/src/analyses/mutexAnalysis.ml
@@ -337,11 +337,7 @@ struct
             | ts when Queries.TS.is_top ts ->
               ()
             | ts ->
-              let f = function
-                | TComp (_, _) -> true
-                | _ -> false
-              in
-              if Queries.TS.exists f ts then
+              if Queries.TS.exists Cilfacade.isStructOrUnionType ts then
                 old_access None
           end;
           on_ad ad
diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml
index 263506b4fb..95479d587c 100644
--- a/src/analyses/raceAnalysis.ml
+++ b/src/analyses/raceAnalysis.ml
@@ -351,7 +351,8 @@ struct
             | ts ->
               if not (Queries.TS.is_empty ts) then
                 includes_uk := true;
-              let f = function
+              let f t =
+                match Cil.unrollType t with
                 | TComp (ci, _) ->
                   add_access_struct (conf - 50) ci
                 | _ -> ()
diff --git a/src/analyses/tutorials/constants.ml b/src/analyses/tutorials/constants.ml
index 5a5a8f7051..cd40d6ffe5 100644
--- a/src/analyses/tutorials/constants.ml
+++ b/src/analyses/tutorials/constants.ml
@@ -18,13 +18,8 @@ struct
   (* No contexts *)
   include Analyses.IdentityUnitContextsSpec
 
-  let is_integer_var (v: varinfo) =
-    match v.vtype with
-      | TInt _ -> true
-      | _ -> false
-
   let get_local = function
-    | Var v, NoOffset when is_integer_var v && not (v.vglob || v.vaddrof) -> Some v (* local integer variable whose address is never taken *)
+    | Var v, NoOffset when isIntegralType v.vtype && not (v.vglob || v.vaddrof) -> Some v (* local integer variable whose address is never taken *)
     | _, _ -> None
 
   (** Evaluates expressions *)
diff --git a/src/autoTune.ml b/src/autoTune.ml
index ed5b8a59a0..3bd81edda8 100644
--- a/src/autoTune.ml
+++ b/src/autoTune.ml
@@ -311,6 +311,7 @@ class addTypeAttributeVisitor = object
 
   (*Set arrays with important types for thread analysis to unroll*)
   method! vtype typ =
+    (* TODO: reuse predicates in Access module (also handles TNamed correctly) *)
     let is_important_type (t: typ): bool = match t with
       | TNamed (info, attr) -> List.mem info.tname ["pthread_mutex_t"; "spinlock_t"; "pthread_t"]
       | TInt (IInt, attr) -> hasAttribute "mutex" attr
@@ -375,7 +376,7 @@ class octagonVariableVisitor(varMap, globals) = object
 
   method! vexpr = function
     (*an expression of type +/- a +/- b where a,b are either variables or constants*)
-    | BinOp (op, e1,e2, (TInt _)) when isComparison op -> (
+    | BinOp (op, e1,e2, _) when isComparison op -> (
         List.iter (fun var -> addOrCreateVarMapping varMap var 5 globals) (extractOctagonVars e1);
         List.iter (fun var -> addOrCreateVarMapping varMap var 5 globals) (extractOctagonVars e2);
         DoChildren
diff --git a/src/autoTune0.ml b/src/autoTune0.ml
index 8f87256854..00b6725109 100644
--- a/src/autoTune0.ml
+++ b/src/autoTune0.ml
@@ -91,6 +91,11 @@ let collectFactors visitAction visitedObject =
   ignore (visitAction visitor visitedObject);
   factors
 
-let is_large_array = function
-  | TArray (_,Some (Const (CInt (i,_,_))),_) -> i > Z.of_int @@ 10 * get_int "ana.base.arrays.unrolling-factor"
+let is_large_array t =
+  match Cil.unrollType t with
+  | TArray (_, e, _) ->
+    begin match Cil.lenOfArray e with (* TODO: Cil.lenOfArray but with Z.t? *)
+      | i -> i > 10 * get_int "ana.base.arrays.unrolling-factor"
+      | exception Cil.LenOfArray -> false
+    end
   | _ -> false
diff --git a/src/cdomain/value/cdomains/int/bitfieldDomain.ml b/src/cdomain/value/cdomains/int/bitfieldDomain.ml
index d8fc66c8ba..c6de18b9d5 100644
--- a/src/cdomain/value/cdomains/int/bitfieldDomain.ml
+++ b/src/cdomain/value/cdomains/int/bitfieldDomain.ml
@@ -22,7 +22,7 @@ module InfixIntOps (Ints_t : IntOps.IntOps) = struct
 end
 
 (*
-  Operations in the abstract domain mostly based on 
+  Operations in the abstract domain mostly based on
 
   "Abstract Domains for Bit-Level Machine Integer and Floating-point Operations"
   of Antoine Miné
@@ -45,7 +45,7 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct
   (* one_mask corresponds to (-1). It has an infinite amount of 1 bits *)
   let one_mask = !:zero_mask
 
-  let of_int x = (!:x, x) 
+  let of_int x = (!:x, x)
 
   let join (z1,o1) (z2,o2) = (z1 |: z2, o1 |: o2)
   let meet (z1,o1) (z2,o2) = (z1 &: z2, o1 &: o2)
@@ -64,11 +64,11 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct
 
   let nabla x y= if x =: (x |: y) then x else one_mask
 
-  let widen (z1,o1) (z2,o2) = (nabla z1 z2, nabla o1 o2)            
+  let widen (z1,o1) (z2,o2) = (nabla z1 z2, nabla o1 o2)
 
   let lognot (z,o) = (o,z)
 
-  let logxor (z1,o1)  (z2,o2) = ((z1 &: z2) |: (o1 &: o2), 
+  let logxor (z1,o1)  (z2,o2) = ((z1 &: z2) |: (o1 &: o2),
                                  (z1 &: o2) |: (o1 &: z2))
 
   let logand (z1,o1) (z2,o2) = (z1 |: z2, o1 &: o2)
@@ -79,37 +79,37 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct
 
   let nth_bit p n = Ints_t.one &: (p >>: n) =: Ints_t.one
 
-  let min ik (z,o) = 
+  let min ik (z,o) =
     (* checking whether the MSB is set *)
-    let signBit = Ints_t.one <<: ((Size.bit ik) - 1) in 
+    let signBit = Ints_t.one <<: ((Size.bit ik) - 1) in
     let isNegative = signBit &: o <>: Ints_t.zero in
     (* mask to set all bits outside of ik to 1 *)
-    let signMask = !: (Ints_t.of_bigint (snd (Size.range ik))) in    
-    if GoblintCil.isSigned ik && isNegative then 
+    let signMask = !: (Ints_t.of_bigint (snd (Size.range ik))) in
+    if GoblintCil.isSigned ik && isNegative then
       (* maximal number of 0 with correct sign extension *)
       Ints_t.to_bigint(signMask |: (!: z))
-    else 
+    else
       (* maximal number of 0 with correct sign extension *)
       Ints_t.to_bigint(!: z)
 
   let max ik (z,o) =
     (* checking whether the MSB is set *)
-    let signBit = Ints_t.one <<: ((Size.bit ik) - 1) in 
+    let signBit = Ints_t.one <<: ((Size.bit ik) - 1) in
     let isPositive = signBit &: z <>: Ints_t.zero in
     (* mask to set all bits outside of ik to 1 *)
-    let signMask = Ints_t.of_bigint (snd (Size.range ik)) in        
-    if GoblintCil.isSigned ik && isPositive then 
+    let signMask = Ints_t.of_bigint (snd (Size.range ik)) in
+    if GoblintCil.isSigned ik && isPositive then
       (* maximal number of 1 with correct sign extension*)
       Ints_t.to_bigint(signMask &: o)
-    else 
+    else
       (* maximal number of 1 *)
-      Ints_t.to_bigint o 
+      Ints_t.to_bigint o
 
   (** [concretize bf] computes the set of all possible integer values represented by the bitfield [bf].
 
       @param (z,o) The bitfield to concretize.
 
-      @info By default, the function generates all possible values that the bitfield can represent, 
+      @info By default, the function generates all possible values that the bitfield can represent,
             which results in an exponential complexity of O(2^n) where [n] is the width of [ik].
             It is recommended to constrain the number of bits that are concretized to avoid non-termination.
   *)
@@ -161,7 +161,7 @@ module BitfieldArith (Ints_t : IntOps.IntOps) = struct
 
   let nth_bit p n = if nth_bit p n then Ints_t.one else Ints_t.zero
 
-  let is_power_of_two x = (x &: (x -: Ints_t.one) = Ints_t.zero) 
+  let is_power_of_two x = (x &: (x -: Ints_t.one) = Ints_t.zero)
 
   let has_neg_values ik b = Z.compare (min ik b) Z.zero < 0
 
@@ -193,13 +193,13 @@ 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 = 
-    if GoblintCil.isSigned ik then top () 
+  let top_of ik =
+    if GoblintCil.isSigned ik then top ()
     else (BArith.one_mask, Ints_t.of_bigint (snd (Size.range ik)))
 
   let bot_of ik = bot ()
 
-  let to_pretty_bits (z,o) = 
+  let to_pretty_bits (z,o) =
     let known_bitmask = BArith.bits_known (z,o) in
     let invalid_bitmask = BArith.bits_invalid (z,o) in
 
@@ -213,7 +213,7 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): Bitfield_SOverflow with type in
       let bit =
         if current_bit_invalid then "⊥"
         else if not current_bit_known then "?"
-        else Ints_t.to_string bit_value 
+        else Ints_t.to_string bit_value
       in
       if (o_mask = Ints_t.of_int (-1) || o_mask = Ints_t.zero) && (z_mask = Ints_t.of_int (-1) || z_mask = Ints_t.zero) then
         let prefix = bit ^ "..." ^ bit in
@@ -223,7 +223,7 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): Bitfield_SOverflow with type in
     in
     "0b" ^ create_pretty_bf_string o z known_bitmask invalid_bitmask ""
 
-  let show t = 
+  let show t =
     if t = bot () then "⊥" else
       let (z,o) = t in
       if GobConfig.get_bool "dbg.full-output" then
@@ -233,16 +233,16 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): Bitfield_SOverflow with type in
 
   include Std (struct type nonrec t = t let name = name let top_of = top_of let bot_of = bot_of let show = show let equal = equal end)
 
-  let maximal (z,o) =     
+  let maximal (z,o) =
     if (z <: Ints_t.zero) <> (o <: Ints_t.zero) then Some o
     else None
 
-  let minimal (z,o) =     
+  let minimal (z,o) =
     if (z <: Ints_t.zero) <> (o <: Ints_t.zero) then Some (!:z)
     else None
 
   (* setting all bits outside of the ik range to the correct sign bit *)
-  let wrap ik (z,o) = 
+  let wrap ik (z,o) =
     let (min_ik, max_ik) = Size.range ik in
     if GoblintCil.isSigned ik then
       let newz = (z &: (Ints_t.of_bigint max_ik)) |: ((Ints_t.of_bigint min_ik) *: (BArith.nth_bit z (Size.bit ik - 1))) in
@@ -253,32 +253,32 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): Bitfield_SOverflow with type in
       let newo = o &: (Ints_t.of_bigint max_ik) in
       (newz,newo)
 
-  let norm ?(suppress_ovwarn=false) ?(ov=false) ik (z,o) = 
-    if BArith.is_invalid (z,o) then 
+  let norm ?(suppress_ovwarn=false) ?(ov=false) ik (z,o) =
+    if BArith.is_invalid (z,o) then
       bot ()
-    else         
-      let new_bitfield = wrap ik (z,o) in     
+    else
+      let new_bitfield = wrap ik (z,o) in
       if not ov || should_wrap ik then
         new_bitfield
-      else 
+      else
         top_of ik
 
-  let cast_to ?(suppress_ovwarn=false) ?torg ?(no_ov=false) ik (z,o) = 
-    let (min_ik, max_ik) = Size.range ik in 
-    let (underflow, overflow) = match torg with   
+  let cast_to ?(suppress_ovwarn=false) ?torg ?(no_ov=false) ik (z,o) =
+    let (min_ik, max_ik) = Size.range ik in
+    let (underflow, overflow) = match torg with
       | None -> (false, false) (* ik does not change *)
-      | Some (GoblintCil.Cil.TInt (old_ik, _)) ->         
-        let underflow = Z.compare (BArith.min old_ik (z,o)) min_ik < 0 in 
-        let overflow = Z.compare max_ik (BArith.max old_ik (z,o)) < 0 in 
+      | Some (GoblintCil.Cil.TInt (old_ik, _) | TEnum ({ekind = old_ik; _}, _)) ->
+        let underflow = Z.compare (BArith.min old_ik (z,o)) min_ik < 0 in
+        let overflow = Z.compare max_ik (BArith.max old_ik (z,o)) < 0 in
         (underflow, overflow)
-      | _ -> 
-        let isPos = z <: Ints_t.zero in 
+      | _ ->
+        let isPos = z <: Ints_t.zero in
         let isNeg = o <: Ints_t.zero in
         let underflow = if GoblintCil.isSigned ik then (((Ints_t.of_bigint min_ik) &: z) <>: Ints_t.zero) && isNeg else isNeg in
         let overflow = (((!:(Ints_t.of_bigint max_ik)) &: o) <>: Ints_t.zero) && isPos in
         (underflow, overflow)
     in
-    let overflow_info = if suppress_ovwarn then {underflow=false; overflow=false} else {underflow=underflow; overflow=overflow} in      
+    let overflow_info = if suppress_ovwarn then {underflow=false; overflow=false} else {underflow=underflow; overflow=overflow} in
     (norm ~suppress_ovwarn:(suppress_ovwarn) ~ov:(underflow || overflow) ik (z,o), overflow_info)
 
   let join ik b1 b2 = norm ik @@ (BArith.join b1 b2)
@@ -295,19 +295,19 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): Bitfield_SOverflow with type in
 
   let narrow ik x y = meet ik x y
 
-  let of_int ik (x: int_t) = 
-    let (min_ik, max_ik) = Size.range ik in 
-    let y = Ints_t.to_bigint x in 
-    let underflow = Z.compare y min_ik < 0 in 
-    let overflow = Z.compare max_ik y < 0 in 
-    let overflow_info = {underflow=underflow; overflow=overflow} in    
-    (norm ~ov:(underflow || overflow) ik (BArith.of_int x), overflow_info) 
+  let of_int ik (x: int_t) =
+    let (min_ik, max_ik) = Size.range ik in
+    let y = Ints_t.to_bigint x in
+    let underflow = Z.compare y min_ik < 0 in
+    let overflow = Z.compare max_ik y < 0 in
+    let overflow_info = {underflow=underflow; overflow=overflow} in
+    (norm ~ov:(underflow || overflow) ik (BArith.of_int x), overflow_info)
 
   let to_int (z,o) = if is_bot (z,o) then None else
     if BArith.is_const (z,o) then Some o
     else None
 
-  let equal_to i bf = 
+  let equal_to i bf =
     if BArith.of_int i = bf then `Eq
     else if leq (BArith.of_int i) bf then `Top
     else `Neq
@@ -336,7 +336,7 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): Bitfield_SOverflow with type in
         let bit_status =
           if Ints_t.compare smallest_number_with_flipped_bit endv <= 0 then
             Top
-          else 
+          else
             (* bit can't change inside the interval -> it's the same as in startv *)
           if Ints_t.equal (Ints_t.logand (Ints_t.shift_right startv pos) Ints_t.one) Ints_t.one then
             One
@@ -345,16 +345,16 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): Bitfield_SOverflow with type in
         in
 
         (* set bit in masks depending on bit_status *)
-        let new_acc = 
+        let new_acc =
           match bit_status with
           | Top-> (Ints_t.logor position_mask acc_z, Ints_t.logor position_mask acc_o)
           | One-> (Ints_t.logand (Ints_t.lognot position_mask) acc_z, Ints_t.logor position_mask acc_o)
           | Zero-> (Ints_t.logor position_mask acc_z, Ints_t.logand (Ints_t.lognot position_mask) acc_o)
-        in 
+        in
         construct_bitfield (pos - 1) new_acc
-    in      
+    in
     let result = construct_bitfield (Size.bit ik - 1) (bot()) in
-    let casted = (Ints_t.of_bigint (Size.cast ik ((Ints_t.to_bigint (fst result)))), Ints_t.of_bigint (Size.cast ik ((Ints_t.to_bigint (snd result))))) 
+    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
@@ -368,13 +368,13 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): Bitfield_SOverflow with type in
 
   let to_bitfield ik x = norm ik x
 
-  let of_congruence ik (c,m) = 
-    if m = Ints_t.zero then 
+  let of_congruence ik (c,m) =
+    if m = Ints_t.zero then
       of_int ik c |> fst
-    else if BArith.is_power_of_two m && Ints_t.one <>: m then 
-      let mod_mask = !:(m -: Ints_t.one) in 
-      let z = mod_mask |: (!: c) in 
-      let o = mod_mask |: c in 
+    else if BArith.is_power_of_two m && Ints_t.one <>: m then
+      let mod_mask = !:(m -: Ints_t.one) in
+      let z = mod_mask |: (!: c) in
+      let o = mod_mask |: c in
       norm ik (z,o)
     else top_of ik
 
@@ -432,31 +432,31 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): Bitfield_SOverflow with type in
     | true,_ | _,true -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s << %s" (show a) (show b)))
     | _ ->
       top_on_undefined_shift ~is_shift_left:true ik a b @@ fun () ->
-      let max_shift = if Z.fits_int (BArith.max ik b) then Z.to_int (BArith.max ik b) else Int.max_int in 
-      let (min_ik, max_ik) = Size.range ik in 
-      let min_res = if max_shift < 0 then Z.pred min_ik else Z.shift_left (BArith.min ik a) max_shift in 
-      let max_res = if max_shift < 0 then Z.succ max_ik else Z.shift_left (BArith.max ik a) max_shift in 
-      let underflow = Z.compare min_res min_ik < 0 in 
-      let overflow = Z.compare max_ik max_res < 0 in 
+      let max_shift = if Z.fits_int (BArith.max ik b) then Z.to_int (BArith.max ik b) else Int.max_int in
+      let (min_ik, max_ik) = Size.range ik in
+      let min_res = if max_shift < 0 then Z.pred min_ik else Z.shift_left (BArith.min ik a) max_shift in
+      let max_res = if max_shift < 0 then Z.succ max_ik else Z.shift_left (BArith.max ik a) max_shift in
+      let underflow = Z.compare min_res min_ik < 0 in
+      let overflow = Z.compare max_ik max_res < 0 in
       (norm ~ov:(underflow || overflow) ik (BArith.shift_left ik a b), {underflow=underflow; overflow=overflow})
 
   (* Arith *)
 
   (*
-  add, sub and mul based on the paper 
+  add, sub and mul based on the paper
   "Sound, Precise, and Fast Abstract Interpretation with Tristate Numbers"
   of Vishwanathan et al.
-  https://doi.org/10.1109/CGO53902.2022.9741267 
+  https://doi.org/10.1109/CGO53902.2022.9741267
   *)
 
-  let add_paper pv pm qv qm = 
+  let add_paper pv pm qv qm =
     let sv = pv +: qv in
     let sm = pm +: qm in
     let sigma = sv +: sm in
     let chi = sigma ^: sv in
     let mu = pm |: qm |: chi in
     let rv = sv &: !:mu in
-    let rm = mu in 
+    let rm = mu in
     (rv, rm)
 
   let add ?no_ov ik (z1, o1) (z2, o2) =
@@ -464,14 +464,14 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): Bitfield_SOverflow with type in
     let pm = o1 &: z1 in
     let qv = o2 &: !:z2 in
     let qm = o2 &: z2 in
-    let (rv, rm) = add_paper pv pm qv qm in 
-    let o3 = rv |: rm in 
+    let (rv, rm) = add_paper pv pm qv qm in
+    let o3 = rv |: rm in
     let z3 = !:rv |: rm in
-    let (max1, max2) = (BArith.max ik (z1, o1), BArith.max ik (z2, o2)) in 
-    let (min1, min2) = (BArith.min ik (z1, o1), BArith.min ik (z2, o2)) in 
-    let (min_ik, max_ik) = Size.range ik in 
-    let underflow = Z.compare (Z.add min1 min2) min_ik < 0 in 
-    let overflow = Z.compare max_ik (Z.add max1 max2) < 0 in 
+    let (max1, max2) = (BArith.max ik (z1, o1), BArith.max ik (z2, o2)) in
+    let (min1, min2) = (BArith.min ik (z1, o1), BArith.min ik (z2, o2)) in
+    let (min_ik, max_ik) = Size.range ik in
+    let underflow = Z.compare (Z.add min1 min2) min_ik < 0 in
+    let overflow = Z.compare max_ik (Z.add max1 max2) < 0 in
     (norm ~ov:(overflow || underflow) ik (z3,o3), {underflow=underflow; overflow=overflow})
 
   let sub ?no_ov ik (z1, o1) (z2, o2) =
@@ -485,14 +485,14 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): Bitfield_SOverflow with type in
     let chi = alpha ^: beta in
     let mu = pm |: qm |: chi in
     let rv = dv &: !:mu in
-    let rm = mu in 
-    let o3 = rv |: rm in 
-    let z3 = !:rv |: rm in   
-    let (max1, max2) = (BArith.max ik (z1, o1), BArith.max ik (z2, o2)) in 
-    let (min1, min2) = (BArith.min ik (z1, o1), BArith.min ik (z2, o2)) in 
-    let (min_ik, max_ik) = Size.range ik in 
-    let underflow = Z.compare (Z.sub min1 max2) min_ik < 0 in 
-    let overflow = Z.compare max_ik (Z.sub max1 min2) < 0 in 
+    let rm = mu in
+    let o3 = rv |: rm in
+    let z3 = !:rv |: rm in
+    let (max1, max2) = (BArith.max ik (z1, o1), BArith.max ik (z2, o2)) in
+    let (min1, min2) = (BArith.min ik (z1, o1), BArith.min ik (z2, o2)) in
+    let (min_ik, max_ik) = Size.range ik in
+    let underflow = Z.compare (Z.sub min1 max2) min_ik < 0 in
+    let overflow = Z.compare max_ik (Z.sub max1 min2) < 0 in
     (norm ~ov:(overflow || underflow) ik (z3, o3), {underflow=underflow; overflow=overflow})
 
   let neg ?no_ov ik x =
@@ -501,11 +501,11 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): Bitfield_SOverflow with type in
 
   let mul ?no_ov ik (z1, o1) (z2, o2) =
     let pm = ref (z1 &: o1) in
-    let pv = ref (o1 &: !:z1) in 
+    let pv = ref (o1 &: !:z1) in
     let qm = ref (z2 &: o2) in
-    let qv = ref (o2 &: !:z2) in 
-    let accv = ref BArith.zero_mask in 
-    let accm = ref BArith.zero_mask in 
+    let qv = ref (o2 &: !:z2) in
+    let accv = ref BArith.zero_mask in
+    let accm = ref BArith.zero_mask in
     let size = if GoblintCil.isSigned ik then Size.bit ik - 1 else Size.bit ik in
     let bitmask = Ints_t.of_bigint (fst (Size.range ik)) in
     let signBitUndef1 = z1 &: o1 &: bitmask in
@@ -513,8 +513,8 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): Bitfield_SOverflow with type in
     let signBitUndef = signBitUndef1 |: signBitUndef2 in
     let signBitDefO = (o1 ^: o2) &: bitmask in
     let signBitDefZ = !:(o1 ^: o2) &: bitmask in
-    for _ = size downto 0 do 
-      (if !pm &: Ints_t.one == Ints_t.one then 
+    for _ = size downto 0 do
+      (if !pm &: Ints_t.one == Ints_t.one then
          accm := snd(add_paper Ints_t.zero !accm Ints_t.zero (!qv |: !qm))
        else if !pv &: Ints_t.one == Ints_t.one then
          accv := fst(add_paper !accv Ints_t.zero !qv Ints_t.zero);
@@ -524,58 +524,58 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): Bitfield_SOverflow with type in
       pm := !pm >>: 1;
       qv := !qv <<: 1;
       qm := !qm <<: 1;
-    done; 
-    let (rv, rm) = add_paper !accv Ints_t.zero Ints_t.zero !accm in 
-    let o3 = rv |: rm in 
+    done;
+    let (rv, rm) = add_paper !accv Ints_t.zero Ints_t.zero !accm in
+    let o3 = rv |: rm in
     let z3 = !:rv |: rm in
-    let (max1, max2) = (BArith.max ik (z1, o1), BArith.max ik (z2, o2)) in 
-    let (min1, min2) = (BArith.min ik (z1, o1), BArith.min ik (z2, o2)) in 
-    let (min_ik, max_ik) = Size.range ik in 
-    let min_res = Z.min (Z.mul min1 max2) (Z.mul max1 min2) in 
-    let max_res = Z.max (Z.mul min1 min2) (Z.mul max1 max2) in 
-    let underflow = Z.compare min_res min_ik < 0 in 
-    let overflow = Z.compare max_ik max_res < 0 in  
-    let z3 = if GoblintCil.isSigned ik then signBitUndef |: signBitDefZ |: z3 else z3 in 
-    let o3 = if GoblintCil.isSigned ik then signBitUndef |: signBitDefO |: o3 else o3 in 
+    let (max1, max2) = (BArith.max ik (z1, o1), BArith.max ik (z2, o2)) in
+    let (min1, min2) = (BArith.min ik (z1, o1), BArith.min ik (z2, o2)) in
+    let (min_ik, max_ik) = Size.range ik in
+    let min_res = Z.min (Z.mul min1 max2) (Z.mul max1 min2) in
+    let max_res = Z.max (Z.mul min1 min2) (Z.mul max1 max2) in
+    let underflow = Z.compare min_res min_ik < 0 in
+    let overflow = Z.compare max_ik max_res < 0 in
+    let z3 = if GoblintCil.isSigned ik then signBitUndef |: signBitDefZ |: z3 else z3 in
+    let o3 = if GoblintCil.isSigned ik then signBitUndef |: signBitDefO |: o3 else o3 in
     (norm ~ov:(overflow || underflow) ik (z3, o3), {underflow=underflow; overflow=overflow})
 
 
   let div ?no_ov ik (z1, o1) (z2, o2) =
-    if o2 = Ints_t.zero then 
-      (top_of ik, {underflow=false; overflow=false}) 
+    if o2 = Ints_t.zero then
+      (top_of ik, {underflow=false; overflow=false})
     else
-      let res = 
-        if BArith.is_const (z1, o1) && BArith.is_const (z2, o2) then 
-          (let tmp = o1 /: o2 in (!:tmp, tmp)) 
-        else if BArith.is_const (z2, o2) && BArith.is_power_of_two o2 then           
-          let exp = Z.trailing_zeros (Ints_t.to_bigint o2) in 
+      let res =
+        if BArith.is_const (z1, o1) && BArith.is_const (z2, o2) then
+          (let tmp = o1 /: o2 in (!:tmp, tmp))
+        else if BArith.is_const (z2, o2) && BArith.is_power_of_two o2 then
+          let exp = Z.trailing_zeros (Ints_t.to_bigint o2) in
           (z1 >>: exp, o1 >>: exp)
-        else 
-          top_of ik 
+        else
+          top_of ik
       in
-      let min_ik = Size.range ik |> fst |> Ints_t.of_bigint in    
-      (* div can only overflow for divisions like -(INT_MIN) / (-1) *)   
+      let min_ik = Size.range ik |> fst |> Ints_t.of_bigint in
+      (* div can only overflow for divisions like -(INT_MIN) / (-1) *)
       let overflow = GoblintCil.isSigned ik && leq (!: min_ik, min_ik) (z1, o1) && leq (Ints_t.zero, BArith.one_mask) (z2, o2) in
       (norm ~ov:overflow ik res, {underflow=false; overflow=overflow})
 
-  let rem ik (z1, o1) (z2, o2) = 
+  let rem ik (z1, o1) (z2, o2) =
     if o2 = Ints_t.zero then top_of ik else
     if BArith.is_const (z1, o1) && BArith.is_const (z2, o2) then
-      let tmp = o1 %: o2 in (!:tmp, tmp)       
-    else if BArith.is_const (z2, o2) && BArith.is_power_of_two o2 then 
+      let tmp = o1 %: o2 in (!:tmp, tmp)
+    else if BArith.is_const (z2, o2) && BArith.is_power_of_two o2 then
       let mask = Ints_t.sub o2 Ints_t.one in
       let newz = Ints_t.logor z1 (Ints_t.lognot mask) in
       let newo = Ints_t.logand o1 mask in
       norm ik (newz, newo)
-    else 
+    else
       top_of ik
 
   let eq ik x y =
-    if Z.compare (BArith.max ik x) (BArith.min ik y) <= 0 && Z.compare (BArith.min ik x) (BArith.max ik y) >= 0 then 
-      of_bool ik true 
-    else if Z.compare (BArith.min ik x) (BArith.max ik y) > 0 || Z.compare (BArith.max ik x) (BArith.min ik y) < 0 then 
-      of_bool ik false 
-    else 
+    if Z.compare (BArith.max ik x) (BArith.min ik y) <= 0 && Z.compare (BArith.min ik x) (BArith.max ik y) >= 0 then
+      of_bool ik true
+    else if Z.compare (BArith.min ik x) (BArith.max ik y) > 0 || Z.compare (BArith.max ik x) (BArith.min ik y) < 0 then
+      of_bool ik false
+    else
       BArith.top_bool
 
   let ne ik x y = match eq ik x y with
@@ -583,45 +583,45 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): Bitfield_SOverflow with type in
     | t when t = of_bool ik false -> of_bool ik true
     | _ -> BArith.top_bool
 
-  let le ik x y = 
-    if Z.compare (BArith.max ik x) (BArith.min ik y) <= 0 then 
-      of_bool ik true 
-    else if Z.compare (BArith.min ik x) (BArith.max ik y) > 0 then 
-      of_bool ik false 
-    else 
+  let le ik x y =
+    if Z.compare (BArith.max ik x) (BArith.min ik y) <= 0 then
+      of_bool ik true
+    else if Z.compare (BArith.min ik x) (BArith.max ik y) > 0 then
+      of_bool ik false
+    else
       BArith.top_bool
 
   let ge ik x y = le ik y x
 
-  let lt ik x y = 
-    if Z.compare (BArith.max ik x) (BArith.min ik y) < 0 then 
-      of_bool ik true 
-    else if Z.compare (BArith.min ik x) (BArith.max ik y) >= 0 then 
-      of_bool ik false 
-    else 
+  let lt ik x y =
+    if Z.compare (BArith.max ik x) (BArith.min ik y) < 0 then
+      of_bool ik true
+    else if Z.compare (BArith.min ik x) (BArith.max ik y) >= 0 then
+      of_bool ik false
+    else
       BArith.top_bool
 
   let gt ik x y = lt ik y x
 
   (* Invariant *)
 
-  let invariant_ikind e ik (z,o) = 
-    if z =: BArith.one_mask && o =: BArith.one_mask then 
+  let invariant_ikind e ik (z,o) =
+    if z =: BArith.one_mask && o =: BArith.one_mask then
       Invariant.top ()
-    else if  BArith.is_invalid (z,o) then 
+    else if  BArith.is_invalid (z,o) then
       Invariant.none
-    else      
+    else
       let open GoblintCil.Cil in
-      let def0 = z &: (!: o) in       
-      let def1 = o &: (!: z) in 
+      let def0 = z &: (!: o) in
+      let def1 = o &: (!: z) in
       let (def0, def1) = BatTuple.Tuple2.mapn (kintegerCilint ik) (Ints_t.to_bigint def0, Ints_t.to_bigint def1) in
-      let exp0 = Invariant.of_exp (BinOp (Eq, (BinOp (BAnd, (UnOp (BNot, e, TInt(ik,[]))), def0, TInt(ik,[]))), def0, intType)) in 
-      let exp1 = Invariant.of_exp (BinOp (Eq, (BinOp (BAnd, e, def1, TInt(ik,[]))), def1, intType)) in 
+      let exp0 = Invariant.of_exp (BinOp (Eq, (BinOp (BAnd, (UnOp (BNot, e, TInt(ik,[]))), def0, TInt(ik,[]))), def0, intType)) in
+      let exp1 = Invariant.of_exp (BinOp (Eq, (BinOp (BAnd, e, def1, TInt(ik,[]))), def1, intType)) in
       Invariant.meet exp0 exp1
 
-  let starting ?(suppress_ovwarn=false) ik n = 
+  let starting ?(suppress_ovwarn=false) ik n =
     let (min_ik, max_ik) = Size.range ik in
-    of_interval ~suppress_ovwarn ik (n, Ints_t.of_bigint max_ik) 
+    of_interval ~suppress_ovwarn ik (n, Ints_t.of_bigint max_ik)
 
   let ending ?(suppress_ovwarn=false) ik n =
     let (min_ik, max_ik) = Size.range ik in
@@ -634,10 +634,10 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): Bitfield_SOverflow with type in
     | Some (c, m) -> meet ik bf (of_congruence ik (c,m))
     | _ -> norm ik bf
 
-  let refine_with_interval ik t itv = 
+  let refine_with_interval ik t itv =
     match itv with
     | None -> norm ik t
-    | Some (l, u) -> meet ik t (of_interval ik (l, u) |> fst)  
+    | Some (l, u) -> meet ik t (of_interval ik (l, u) |> fst)
 
   let refine_with_bitfield ik x y = meet ik x y
 
@@ -646,53 +646,53 @@ module BitfieldFunctor (Ints_t : IntOps.IntOps): Bitfield_SOverflow with type in
   let refine_with_incl_list ik t (incl : (int_t list) option) : t =
     let joined =match incl with
       | None -> top_of ik
-      | Some ls -> 
+      | Some ls ->
         List.fold_left (fun acc i -> BArith.join acc (BArith.of_int i)) (bot_of ik) ls
     in
     meet ik t joined
 
 
-  let refine_bor (az, ao) (bz, bo) (cz, co) =     
-    let cDef0 = cz &: (!: co) in 
-    let cDef1 = co &: (!: cz) in         
-    let aDef0 = az &: (!: ao) in   
+  let refine_bor (az, ao) (bz, bo) (cz, co) =
+    let cDef0 = cz &: (!: co) in
+    let cDef1 = co &: (!: cz) in
+    let aDef0 = az &: (!: ao) in
     let bDef0 = bz &: (!: bo) in
     (* if a bit is definitely 0 in b and definitely 1 in c, the same bit must be definitely 1 in a *)
     (* example (with t for top): (tttt) | (t010) = (1011) *)
     (* we can refine (tttt) to (ttt1) because the lowest 1 of c must come from a *)
-    let az = az &: (!: (bDef0 &: cDef1)) in 
+    let az = az &: (!: (bDef0 &: cDef1)) in
     let bz = bz &: (!: (aDef0 &: cDef1)) in
     (* if a bit is definitely 0 in c, the same bit must be definitely 0 in a too *)
     (* example (with t for top): (ttt1) | (t010) = (1011) *)
     (* we can refine (ttt1) to (t0t1) because the second bit of a cannot be a 1 *)
-    let ao = ao &: (!: cDef0) in     
-    let bo = bo &: (!: cDef0) in 
+    let ao = ao &: (!: cDef0) in
+    let bo = bo &: (!: cDef0) in
     ((az, ao), (bz, bo))
 
-  let refine_band (az, ao) (bz, bo) (cz, co) = 
-    let cDef0 = cz &: (!: co) in 
-    let cDef1 = co &: (!: cz) in 
+  let refine_band (az, ao) (bz, bo) (cz, co) =
+    let cDef0 = cz &: (!: co) in
+    let cDef1 = co &: (!: cz) in
     let aDef1 = ao &: (!: az) in
     let bDef1 = bo &: (!: bz) in
     (* if a bit is definitely 1 in c, the same bit must be definitely 1 in a too *)
     (* example (with t for top): (tttt) & (t010) = (1011) *)
     (* we can refine (tttt) to (1t11) *)
-    let az = az &: (!: cDef1) in 
-    let bz = bz &: (!: cDef1) in 
+    let az = az &: (!: cDef1) in
+    let bz = bz &: (!: cDef1) in
     (* if a bit is definitely 1 in b and definitely 0 in c, the same bit must be definitely 0 in a *)
     (* example (with t for top): (tttt) & (t110) = (1011) *)
     (* we can refine (tttt) to (t0tt) *)
-    let ao = ao &: (!: (bDef1 &: cDef0)) in     
+    let ao = ao &: (!: (bDef1 &: cDef0)) in
     let bo = bo &: (!: (aDef1 &: cDef0)) in
     ((az, ao), (bz, bo))
 
-  let arbitrary ik = 
+  let arbitrary ik =
     let open QCheck.Iter in
     let int_arb = QCheck.map ~rev:Ints_t.to_int64 Ints_t.of_int64 GobQCheck.Arbitrary.int64 in
     let pair_arb = QCheck.pair int_arb int_arb in
     let shrink bf =
-      (GobQCheck.shrink pair_arb bf 
-       >|= (fun (zs, os) -> 
+      (GobQCheck.shrink pair_arb bf
+       >|= (fun (zs, os) ->
            (* Shrinking works by setting some unsure bits to 0. This reduces the number of possible values, and makes the decimal representation of the masks smaller *)
            let random_mask = Ints_t.of_int64 (Random.int64 (Int64.of_int (Size.bits ik |> snd))) in
            let unsure_bitmask= zs &: os in
diff --git a/src/cdomain/value/cdomains/int/congruenceDomain.ml b/src/cdomain/value/cdomains/int/congruenceDomain.ml
index 63a3271e33..843949c254 100644
--- a/src/cdomain/value/cdomains/int/congruenceDomain.ml
+++ b/src/cdomain/value/cdomains/int/congruenceDomain.ml
@@ -143,7 +143,7 @@ struct
     match BitfieldDomain.Bitfield.to_int (z,o) with
     | Some x -> normalize ik (Some (x, Z.zero))
     | _ ->
-      (* get posiiton of first top bit *)
+      (* get position of first top bit *)
       let tl_zeros = Z.trailing_zeros (Z.logand z o) in
       let ik_bits = Size.bit ik in
       let m = if tl_zeros > ik_bits then Z.one else Z.pow Z.one tl_zeros in
@@ -182,8 +182,8 @@ struct
         let (min_ikorg, max_ikorg) = range ikorg in
         ikorg = t || (max_t >=: max_ikorg && min_t <=: min_ikorg)
       in
-      match torg with
-      | Some (Cil.TInt (ikorg, _)) when p ikorg ->
+      match Option.map Cil.unrollType torg with
+      | Some (Cil.TInt (ikorg, _) | TEnum ({ekind = ikorg; _}, _)) when p ikorg ->
         if M.tracing then M.trace "cong-cast" "some case";
         x
       | _ -> top ()
diff --git a/src/cdomain/value/cdomains/int/defExcDomain.ml b/src/cdomain/value/cdomains/int/defExcDomain.ml
index ef5c23c5ef..0133b0ab0a 100644
--- a/src/cdomain/value/cdomains/int/defExcDomain.ml
+++ b/src/cdomain/value/cdomains/int/defExcDomain.ml
@@ -320,9 +320,7 @@ struct
 
   let of_excl_list t l =
     let r = size t in (* elements in l are excluded from the full range of t! *)
-    `Excluded (List.fold_right S.add l (S.empty ()), r)
-  (* TODO: Change after #1686 has landed *)
-  (* `Excluded (S.of_list l, r) *)
+    `Excluded (S.of_list l, r)
 
   let is_excl_list l = match l with `Excluded _ -> true | _ -> false
   let to_excl_list (x:t) = match x with
diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index eeb2789004..991fb114cf 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
\ No newline at end of file
+include IntDomTuple
diff --git a/src/cdomain/value/cdomains/structDomain.ml b/src/cdomain/value/cdomains/structDomain.ml
index d24c287ad0..0b70034442 100644
--- a/src/cdomain/value/cdomains/structDomain.ml
+++ b/src/cdomain/value/cdomains/structDomain.ml
@@ -269,18 +269,16 @@ struct
         match rem_fields with
         | [] -> second_choice
         | h::t -> begin
-            match (h.ftype, get_bool "ana.base.structs.key.prefer-ptrs", get_bool "ana.base.structs.key.avoid-ints") with
+            match Cil.unrollType h.ftype, get_bool "ana.base.structs.key.prefer-ptrs", get_bool "ana.base.structs.key.avoid-ints" with
             | (TPtr (_, _), _, _) -> h
-            | (TInt (_, _), true, _)
-            | (TInt (_, _), _, true) -> first_appropriate_key t second_choice
-            | (TInt (_, _), _, _) -> h
+            | ((TInt _ | TEnum _), true, _)
+            | ((TInt _ | TEnum _), _, true) -> first_appropriate_key t second_choice
+            | ((TInt _ | TEnum _), _, _) -> h
             | (_, false, _) -> h
             | (_, _, false) -> first_appropriate_key t second_choice
             | (_, _, _) ->
-              let second = match second_choice.ftype with
-                | TInt (_,_) -> h
-                | _ -> second_choice
-              in first_appropriate_key t second
+              let second = if Cil.isIntegralType second_choice.ftype then h else second_choice in
+              first_appropriate_key t second
           end
       in Some (first_appropriate_key fields (List.hd fields))
 
@@ -503,8 +501,8 @@ struct
   let chosen_domain () = get_string "ana.base.structs.domain"
 
   let pick_combined setting (comp: compinfo) =
-    let all_bool () = List.for_all (fun f -> match f.ftype with TInt(IBool, _) -> true | _ -> false) comp.cfields in
-    let has_ptr () = List.exists (fun f -> match f.ftype with TPtr(_, _) -> true | _ -> false) comp.cfields in
+    let all_bool () = List.for_all (fun f -> Cilfacade.isBoolType f.ftype) comp.cfields in
+    let has_ptr () = List.exists (fun f -> Cil.isPointerType f.ftype) comp.cfields in
     match setting with
     | "combined-sk" -> if has_ptr () then "keyed" else "simple"
     | "combined-all" ->
diff --git a/src/cdomain/value/cdomains/valueDomain.ml b/src/cdomain/value/cdomains/valueDomain.ml
index 73c8175de1..acf95ccf54 100644
--- a/src/cdomain/value/cdomains/valueDomain.ml
+++ b/src/cdomain/value/cdomains/valueDomain.ml
@@ -156,6 +156,7 @@ struct
     | _ when is_mutex_type t -> Mutex
     | t when is_jmp_buf_type t -> JmpBuf (JmpBufs.bot ())
     | TInt _ -> Bot (*Int (ID.bot ()) -- should be lower than any int or address*)
+    (* TODO: TEnum? *)
     | TFloat _ -> Bot
     | TPtr _ -> Address (AD.bot ())
     | TComp ({cstruct=true; _} as ci,_) -> Struct (Structs.create (fun fd -> bot_value ~varAttr:fd.fattr fd.ftype) ci)
@@ -192,6 +193,7 @@ struct
     | 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)
+    (* 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)
@@ -211,6 +213,7 @@ struct
     | t when is_jmp_buf_type t -> JmpBuf (JmpBufs.top ())
     | t when is_mutexattr_type t -> MutexAttr (MutexAttrDomain.top ())
     | TInt (ik,_) -> Int (ID.(cast_to ik (top_of ik)))
+    (* 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 -> top_value ~varAttr:fd.fattr fd.ftype) ci)
@@ -244,6 +247,7 @@ struct
     | t when is_jmp_buf_type t -> JmpBuf (JmpBufs.top ())
     | t when is_mutexattr_type t -> MutexAttr (MutexAttrDomain.top ())
     | TInt (ikind, _) -> Int (ID.of_int ikind Z.zero)
+    (* TODO: TEnum? *)
     | TFloat (fkind, _) when not (Cilfacade.isComplexFKind fkind) -> Float (FD.of_const fkind 0.0)
     | TPtr _ -> Address AD.null_ptr
     | TComp ({cstruct=true; _} as ci,_) -> Struct (Structs.create (fun fd -> zero_init_value ~varAttr:fd.fattr fd.ftype) ci)
@@ -360,8 +364,8 @@ struct
     | TFloat (FFloat128, _), TFloat (FDouble,_) -> true
     | TFloat (FFloat128, _), TFloat (FLongDouble,_) -> true
     | _, TFloat _ -> false (* casting float to an integral type always looses the decimals *)
-    | TFloat (fk, _), TInt((IBool | IChar | IUChar | ISChar | IShort | IUShort), _) when not (Cilfacade.isComplexFKind fk)  -> true (* reasonably small integers can be stored in all fkinds *)
-    | TFloat ((FDouble | FLongDouble | FFloat128), _), TInt((IInt | IUInt | ILong | IULong), _) -> true (* values stored in between 16 and 32 bits can only be stored in at least doubles *)
+    | TFloat (fk, _), (TInt((IBool | IChar | IUChar | ISChar | IShort | IUShort), _) | TEnum ({ekind = IBool | IChar | IUChar | ISChar | IShort | IUShort; _}, _)) when not (Cilfacade.isComplexFKind fk)  -> true (* reasonably small integers can be stored in all fkinds *)
+    | TFloat ((FDouble | FLongDouble | FFloat128), _), (TInt((IInt | IUInt | ILong | IULong), _) | TEnum ({ekind = IInt | IUInt | ILong | IULong; _}, _)) -> true (* values stored in between 16 and 32 bits can only be stored in at least doubles *)
     | TFloat _, _ -> false (* all wider integers can not be completely put into a float, partially because our internal representation of long double is the same as for doubles *)
     | (TInt _ | TEnum _ | TPtr _) , (TInt _ | TEnum _ | TPtr _) ->
       IntDomain.Size.is_cast_injective ~from_type:t1 ~to_type:t2 && bitsSizeOf t2 >= bitsSizeOf t1
@@ -372,7 +376,7 @@ struct
     if is_statically_safe_cast t2 t1 then
       true
     else
-      match t2, t1, v with
+      match Cil.unrollType t2, Cil.unrollType t1, v with
       | (TInt (ik2,_) | TEnum ({ekind=ik2; _},_)) , (TInt (ik1,_) | TEnum ({ekind=ik1; _},_)), Int v ->
         let cl, cu = IntDomain.Size.range ik2 in
         let l, u = ID.minimal v, ID.maximal v in
@@ -392,7 +396,8 @@ struct
     | a, b -> a = b
 
   let cast_addr t a =
-    let rec stripVarLenArr = function
+    let rec stripVarLenArr t =
+      match Cil.unrollType t with
       | TPtr(t, args) -> TPtr(stripVarLenArr t, args)
       | TArray(t, None, args) -> TArray(stripVarLenArr t, None, args)
       | TArray(t, Some exp, args) when isConstant exp -> TArray(stripVarLenArr t, Some exp, args)
@@ -418,7 +423,7 @@ struct
       | _ -> (* cast to smaller/inner type *)
         if M.tracing then M.tracel "casta" "cast to smaller size";
         if d = Some true then err "Ptr-cast to type of incompatible size!" else
-          begin match ta, t with
+          begin match Cil.unrollType ta, Cil.unrollType t with
             (* struct to its first field *)
             | TComp ({cfields = fi::_; _}, _), _ ->
               if M.tracing then M.tracel "casta" "cast struct to its first field";
@@ -432,26 +437,31 @@ struct
             | _ -> err @@ Format.sprintf "Cast to neither array index nor struct field. is_zero_offset: %b" (Addr.Offs.cmp_zero_offset o = `MustZero)
           end
     in
-    let one_addr = let open Addr in function
-        (* only allow conversion of float pointers if source and target type are the same *)
-        | Addr ({ vtype = TFloat(fkind, _); _}, _) as x when (match t with TFloat (fkind', _) when fkind = fkind' -> true | _ -> false) -> x
-        (* do not allow conversion from/to float pointers*)
-        | Addr ({ vtype = TFloat(_); _}, _) -> UnknownPtr
-        | _ when (match t with TFloat _ -> true | _ -> false) -> UnknownPtr
-        | Addr ({ vtype = TVoid _; _} as v, offs) when not (Cilfacade.isCharType t) -> (* we had no information about the type (e.g. malloc), so we add it; ignore for casts to char* since they're special conversions (N1570 6.3.2.3.7) *)
-          Addr ({ v with vtype = t }, offs) (* HACK: equal varinfo with different type, causes inconsistencies down the line, when we again assume vtype being "right", but joining etc gives no consideration to which type version to keep *)
-        | Addr (v, o) as a ->
-          begin try Addr (v, (adjust_offs v o None)) (* cast of one address by adjusting the abstract offset *)
-            with
-            | CastError s -> (* don't know how to handle this cast :( *)
-              if M.tracing then M.tracel "caste" "%s" s;
-              a (* probably garbage, but this is deref's problem *)
-            (*raise (CastError s)*)
-            | SizeOfError (s,t) ->
-              M.warn "size of error: %s" s;
-              a
-          end
-        | x -> x (* TODO we should also keep track of the type here *)
+    let one_addr =
+      let open Addr in
+      function
+      | Addr.Addr ({ vtype; _} as v, o) as a ->
+        begin match Cil.unrollType vtype, Cil.unrollType t with
+          (* only allow conversion of float pointers if source and target type are the same *)
+          | TFloat (fkind, _), TFloat (fkind', _) when fkind = fkind' -> a
+          (* do not allow conversion from/to float pointers*)
+          | TFloat _, _
+          | _, TFloat _ -> UnknownPtr
+          | TVoid _, _ when not (Cilfacade.isCharType t) -> (* we had no information about the type (e.g. malloc), so we add it; ignore for casts to char* since they're special conversions (N1570 6.3.2.3.7) *)
+            Addr ({ v with vtype = t }, o) (* HACK: equal varinfo with different type, causes inconsistencies down the line, when we again assume vtype being "right", but joining etc gives no consideration to which type version to keep *)
+          | _, _ ->
+            begin try Addr (v, (adjust_offs v o None)) (* cast of one address by adjusting the abstract offset *)
+              with
+              | CastError s -> (* don't know how to handle this cast :( *)
+                if M.tracing then M.tracel "caste" "%s" s;
+                a (* probably garbage, but this is deref's problem *)
+              (*raise (CastError s)*)
+              | SizeOfError (s,t) ->
+                M.warn "size of error: %s" s;
+                a
+            end
+        end
+      | x -> x (* TODO we should also keep track of the type here *)
     in
     let a' = AD.map one_addr a in
     if M.tracing then M.tracel "cast" "cast_addr %a to %a is %a!" AD.pretty a d_type t AD.pretty a';
@@ -507,8 +517,8 @@ struct
           Address (match v with
               | Int x when ID.to_int x = Some Z.zero -> AD.null_ptr
               | Int x -> AD.top_ptr
-              (* we ignore casts to void*! TODO report UB! *)
-              | Address x -> (match t with TVoid _ -> x | _ -> cast_addr t x)
+              (* we ignore casts to void* (above)! TODO report UB! *)
+              | Address x -> cast_addr t x
               (*| Address x -> x*)
               | _ -> log_top __POS__; AD.top_ptr
             )
@@ -931,7 +941,7 @@ struct
           | `Field (fld, offs) -> begin
               match x with
               | Union (`Lifted l_fld, value) ->
-                (match value, fld.ftype with
+                (match value, Cil.unrollType fld.ftype with
                  (* only return an actual value if we have a type and return actually the exact same type *)
                  | Float f_value, TFloat(fkind, _) when FD.get_fkind f_value = fkind -> Float f_value
                  | Float _, t -> top_value t
@@ -1100,10 +1110,9 @@ struct
                       | `NoOffset -> top (), offs
                       | `Index (idx, _) when Cil.isArrayType fld.ftype ->
                         begin
-                          match fld.ftype with
+                          match Cil.unrollType fld.ftype with
                           | TArray(_, l, _) ->
-                            let len = try Cil.lenOfArray l
-                              with Cil.LenOfArray -> 42 (* will not happen, VLA not allowed in union and struct *) in
+                            let len = Cil.lenOfArray l in (* LenOfArray exception will not happen, VLA not allowed in union and struct *)
                             Array(CArrays.make (IndexDomain.of_int (Cilfacade.ptrdiff_ikind ()) (Z.of_int len)) Top), offs
                           | _ -> top (), offs (* will not happen*)
                         end
@@ -1123,7 +1132,7 @@ struct
                 let l', o' = shift_one_over l o in
                 match x with
                 | Array x' ->
-                  let t = (match t with
+                  let t = (match Cil.unrollType t with
                       | TArray(t1 ,_,_) -> t1
                       | _ -> t) in (* This is necessary because t is not a TArray in case of calloc *)
                   let e = determine_offset ask l o exp (Some v) in
@@ -1131,7 +1140,7 @@ struct
                   let new_array_value = CArrays.set ask x' (e, idx) new_value_at_index in
                   Array new_array_value
                 | Bot ->
-                  let t,len = (match t with
+                  let t,len = (match Cil.unrollType t with
                       | TArray(t1 ,len,_) -> t1, len
                       | _ -> t, None) in (* This is necessary because t is not a TArray in case of calloc *)
                   let x' = CArrays.bot () in
@@ -1193,7 +1202,7 @@ struct
 
   (* Won't compile without the final :t annotation *)
   let rec update_array_lengths (eval_exp: exp -> t) (v:t) (typ:Cil.typ):t =
-    match v, typ with
+    match v, Cil.unrollType typ with
     | Array(n), TArray(ti, e, _) ->
       begin
         let update_fun x = update_array_lengths eval_exp x ti in
diff --git a/src/cdomain/value/domains/invariantCil.ml b/src/cdomain/value/domains/invariantCil.ml
index f41d48ab61..9e50df2741 100644
--- a/src/cdomain/value/domains/invariantCil.ml
+++ b/src/cdomain/value/domains/invariantCil.ml
@@ -91,6 +91,7 @@ class exp_contains_anon_type_visitor = object
     | TComp ({cname; _}, _) when String.starts_with ~prefix:"__anon" cname ->
       raise Stdlib.Exit
     | _ ->
+      (* CIL visitor does not go into TNamed, but we don't need to anyway: direct occurrences of __anon struct names in invariants are the problem. *)
       DoChildren
 end
 let exp_contains_anon_type =
diff --git a/src/cdomain/value/util/wideningThresholds.ml b/src/cdomain/value/util/wideningThresholds.ml
index df89728a40..b26a3b446e 100644
--- a/src/cdomain/value/util/wideningThresholds.ml
+++ b/src/cdomain/value/util/wideningThresholds.ml
@@ -13,10 +13,10 @@ class extractThresholdsFromConditionsVisitor(upper_thresholds,lower_thresholds,
 
   method! vexpr = function
     (* Comparisons of type: 10 <= expr, expr >= 10, expr < 10, 10 > expr *)
-    | BinOp (Le, (Const (CInt(i,_,_))), _, (TInt _))
-    | BinOp (Ge, _, (Const (CInt(i,_,_))), (TInt _))
-    | BinOp (Lt, _, (Const (CInt(i,_,_))), (TInt _))
-    | BinOp (Gt, (Const (CInt(i,_,_))), _, (TInt _)) ->
+    | BinOp (Le, (Const (CInt(i,_,_))), _, _)
+    | BinOp (Ge, _, (Const (CInt(i,_,_))), _)
+    | BinOp (Lt, _, (Const (CInt(i,_,_))), _)
+    | BinOp (Gt, (Const (CInt(i,_,_))), _, _) ->
       addThreshold upper_thresholds @@ i;
       addThreshold lower_thresholds @@ Z.pred i;
 
@@ -28,10 +28,10 @@ class extractThresholdsFromConditionsVisitor(upper_thresholds,lower_thresholds,
       DoChildren
 
     (* Comparisons of type: 10 < expr, expr > 10, expr <= 10, 10 >= expr *)
-    | BinOp (Lt, (Const (CInt(i,_,_))), _, (TInt _))
-    | BinOp (Gt, _, (Const (CInt(i,_,_))), (TInt _))
-    | BinOp (Le, _, (Const (CInt(i,_,_))), (TInt _))
-    | BinOp (Ge, (Const (CInt(i,_,_))), _, (TInt _)) ->
+    | BinOp (Lt, (Const (CInt(i,_,_))), _, _)
+    | BinOp (Gt, _, (Const (CInt(i,_,_))), _)
+    | BinOp (Le, _, (Const (CInt(i,_,_))), _)
+    | BinOp (Ge, (Const (CInt(i,_,_))), _, _) ->
       let i = Z.succ i in (* The same as above with i+1 because for integers expr <= 10 <=> expr < 11 *)
       addThreshold upper_thresholds @@ i;
       addThreshold lower_thresholds @@ Z.pred i;
@@ -44,10 +44,10 @@ class extractThresholdsFromConditionsVisitor(upper_thresholds,lower_thresholds,
       DoChildren
 
     (* Comparisons of type: 10 == expr, expr == 10, expr != 10, 10 != expr *)
-    | BinOp (Eq, (Const (CInt(i,_,_))), _, (TInt _))
-    | BinOp (Eq, _, (Const (CInt(i,_,_))), (TInt _))
-    | BinOp (Ne, _, (Const (CInt(i,_,_))), (TInt _))
-    | BinOp (Ne, (Const (CInt(i,_,_))), _, (TInt _)) ->
+    | BinOp (Eq, (Const (CInt(i,_,_))), _, _)
+    | BinOp (Eq, _, (Const (CInt(i,_,_))), _)
+    | BinOp (Ne, _, (Const (CInt(i,_,_))), _)
+    | BinOp (Ne, (Const (CInt(i,_,_))), _, _) ->
       addThreshold upper_thresholds @@ i;
       addThreshold lower_thresholds @@ i;
 
diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml
index 013dca3405..4a571a3a2e 100644
--- a/src/cdomains/apron/sharedFunctions.apron.ml
+++ b/src/cdomains/apron/sharedFunctions.apron.ml
@@ -171,11 +171,12 @@ struct
               | BinOp (Mod, e1, e2, _) -> bop_near Mod e1 e2
               | BinOp (Div, e1, e2, _) ->
                 Binop (Div, texpr1 e1, texpr1 e2, Int, Zero)
-              | CastE (TInt (t_ik, _) as t, e) ->
+              | CastE (t, e) when Cil.isIntegralType t ->
                 begin match  IntDomain.Size.is_cast_injective ~from_type:(Cilfacade.typeOf e) ~to_type:t with (* TODO: unnecessary cast check due to overflow check below? or maybe useful in general to also assume type bounds based on argument types? *)
                   | exception Invalid_argument a -> raise (Unsupported_CilExp (Ikind_non_integer a))
                   | true -> texpr1 e
                   | false -> (* Cast is not injective - we now try to establish suitable ranges manually  *)
+                    let t_ik = Cilfacade.get_ikind t in
                     (* retrieving a valuerange for a non-injective cast works by a query to the value-domain with subsequent value extraction from domtuple - which should be speculative, since it is not program code *)
                     let const,res = GobRef.wrap AnalysisState.executing_speculative_computations true @@ fun () ->
                       (* try to evaluate e by EvalInt Query *)
diff --git a/src/common/framework/cfgTools.ml b/src/common/framework/cfgTools.ml
index 60a9a4dc84..3e137bdc0e 100644
--- a/src/common/framework/cfgTools.ml
+++ b/src/common/framework/cfgTools.ml
@@ -701,7 +701,7 @@ let getGlobalInits (file: file) : edges  =
       else if not (Hashtbl.mem inits (assign (any_index lval))) then
         Hashtbl.add inits (assign (any_index lval)) ()
     | CompoundInit (typ, lst) ->
-      let ntyp = match typ, lst with
+      let ntyp = match Cil.unrollType typ, lst with
         | TArray(t, None, attr), [] -> TArray(t, Some zero, attr) (* set initializer type to t[0] for flexible array members of structs that are intialized with {} *)
         | _, _ -> typ
       in
diff --git a/src/common/util/cilfacade.ml b/src/common/util/cilfacade.ml
index 68c1410f2a..6d0738db8a 100644
--- a/src/common/util/cilfacade.ml
+++ b/src/common/util/cilfacade.ml
@@ -27,18 +27,28 @@ let isCharType t =
   | TInt ((IChar | ISChar | IUChar), _) -> true
   | _ -> false
 
+let isBoolType t =
+  match Cil.unrollType t with
+  | TInt (IBool, _) -> true
+  | _ -> false
+
 let isFloatType t =
   match Cil.unrollType t with
   | TFloat _ -> true
   | _ -> false
 
-let rec isVLAType t =
+let rec isVLAType t = (* TODO: use in base? *)
   match Cil.unrollType t with
   | TArray (et, len, _) ->
     let variable_len = GobOption.exists (Fun.negate Cil.isConstant) len in
     variable_len || isVLAType et
   | _ -> false
 
+let isStructOrUnionType t =
+  match Cil.unrollType t with
+  | TComp _ -> true
+  | _ -> false
+
 let is_first_field x = match x.fcomp.cfields with
   | [] -> false
   | f :: _ -> CilType.Fieldinfo.equal f x
@@ -576,7 +586,7 @@ let countLoc fn =
 
 
 let fundec_return_type f =
-  match f.svar.vtype with
+  match Cil.unrollType f.svar.vtype with
   | TFun (return_type, _, _, _) -> return_type
   | _ -> failwith "fundec_return_type: not TFun"
 
diff --git a/src/domain/lattice.ml b/src/domain/lattice.ml
index 9559ac9922..2bd32a8ca0 100644
--- a/src/domain/lattice.ml
+++ b/src/domain/lattice.ml
@@ -145,7 +145,7 @@ struct
 end
 
 (* HAS SIDE-EFFECTS ---- PLEASE INSTANCIATE ONLY ONCE!!! *)
-module HConsed (Base:S) (Arg: sig val assume_idempotent: bool end) =
+module HConsed (Arg: sig val assume_idempotent: bool end) (Base:S) =
 struct
   include Printable.HConsed (Base)
 
diff --git a/src/domain/mapDomain.ml b/src/domain/mapDomain.ml
index 033302d8df..cf563dab44 100644
--- a/src/domain/mapDomain.ml
+++ b/src/domain/mapDomain.ml
@@ -263,7 +263,7 @@ module HConsed (M: S) : S with
   type key = M.key and
   type value = M.value =
 struct
-  include Lattice.HConsed (M) (struct let assume_idempotent = false end)
+  include Lattice.HConsed (struct let assume_idempotent = false end) (M)
 
   type key = M.key
   type value = M.value
diff --git a/src/domains/access.ml b/src/domains/access.ml
index f7ce68a18b..39c8a753ec 100644
--- a/src/domains/access.ml
+++ b/src/domains/access.ml
@@ -257,7 +257,11 @@ let get_type fb e =
   let r = get_type fb e in
   (* printf "result = %a\n" d_acct r; *)
   match r with
-  | `Type (TPtr (t,a)) -> `Type t (* Why this special case? Almost always taken if not `Struct. *)
+  | `Type t as x ->
+    begin match Cil.unrollType t with
+      | TPtr (t, a) ->  `Type t (* Why this special case? Almost always taken if not `Struct. *)
+      | _ -> x
+    end
   | x -> x (* Mostly for `Struct, but also rare cases with non-pointer `Type. Should they happen at all? *)
 
 let get_val_type e: acc_typ =
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index c7cfce95d2..4c32b286c8 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -259,7 +259,7 @@ struct
         Queries.AD.to_var_may ad (* TODO: don't convert, handle UnknownPtr below *)
     in
     let one_function f =
-      match f.vtype with
+      match Cil.unrollType f.vtype with
       | TFun (_, params, var_arg, _)  ->
         let arg_length = List.length args in
         let p_length = Option.map_default List.length 0 params in
diff --git a/src/lifters/specLifters.ml b/src/lifters/specLifters.ml
index 33284fcba2..93d82aae5f 100644
--- a/src/lifters/specLifters.ml
+++ b/src/lifters/specLifters.ml
@@ -5,20 +5,26 @@ open GoblintCil
 open Analyses
 open GobConfig
 
+module type NameLifter =
+sig
+  val lift_name: string -> string
+end
 
-(** Lifts a [Spec] so that the domain is [Hashcons]d *)
-module HashconsLifter (S:Spec)
+module type LatticeLifter =
+  functor (L: Lattice.S) ->
+  sig
+    include Lattice.S
+
+    val lift: L.t -> t
+    val unlift: t -> L.t
+  end
+
+module DomainLifter (N: NameLifter) (F: LatticeLifter) (S:Spec)
   : Spec with module G = S.G
           and module C = S.C
 =
 struct
-  module HConsedArg =
-  struct
-    (* We do refine int values on narrow and meet {!IntDomain.IntDomTupleImpl}, which can lead to fixpoint issues if we assume x op x = x *)
-    (* see https://github.com/goblint/analyzer/issues/1005 *)
-    let assume_idempotent = GobConfig.get_string "ana.int.refinement" = "never"
-  end
-  module D = Lattice.HConsed (S.D) (HConsedArg)
+  module D = F (S.D)
   module G = S.G
   module C = S.C
   module V = S.V
@@ -28,9 +34,9 @@ struct
     let of_elt x = of_elt (D.unlift x)
   end
 
-  let name () = S.name () ^" hashconsed"
+  let name () = N.lift_name (S.name ())
 
-  type marshal = S.marshal (* TODO: should hashcons table be in here to avoid relift altogether? *)
+  type marshal = S.marshal
   let init = S.init
   let finalize = S.finalize
 
@@ -98,104 +104,50 @@ struct
     D.lift @@ S.event (conv man) e (conv oman)
 end
 
-(** Lifts a [Spec] so that the context is [Hashcons]d. *)
-module HashconsContextLifter (S:Spec)
-  : Spec with module D = S.D
-          and module G = S.G
-          and module C = Printable.HConsed (S.C)
-=
+(** Lifts a [Spec] so that the domain is [Hashcons]d *)
+module HashconsLifter (S: Spec) = (* keep functor eta-expanded to look up option when lifter is actually used *)
 struct
-  module D = S.D
-  module G = S.G
-  module C = Printable.HConsed (S.C)
-  module V = S.V
-  module P = S.P
-
-  let name () = S.name () ^" context hashconsed"
-
-  type marshal = S.marshal (* TODO: should hashcons table be in here to avoid relift altogether? *)
-  let init = S.init
-  let finalize = S.finalize
-
-  let startstate = S.startstate
-  let exitstate  = S.exitstate
-  let morphstate = S.morphstate
-
-  let conv man =
-    { man with context = (fun () -> C.unlift (man.context ())) }
-
-  let context man fd = C.lift % S.context (conv man) fd
-  let startcontext () = C.lift @@ S.startcontext ()
-
-  let sync man reason =
-    S.sync (conv man) reason
-
-  let query man (type a) (q: a Queries.t): a Queries.result =
-    match q with
-    | Queries.IterPrevVars f ->
-      let g i (n, c, j) e = f i (n, Obj.repr (C.lift (Obj.obj c)), j) e in
-      S.query (conv man) (Queries.IterPrevVars g)
-    | _ -> S.query (conv man) q
-
-  let assign man lv e =
-    S.assign (conv man) lv e
-
-  let vdecl man v =
-    S.vdecl (conv man) v
-
-  let branch man e tv =
-    S.branch (conv man) e tv
-
-  let body man f =
-    S.body (conv man) f
-
-  let return man r f =
-    S.return (conv man) r f
-
-  let asm man =
-    S.asm (conv man)
-
-  let skip man =
-    S.skip (conv man)
-
-  let enter man r f args =
-    S.enter (conv man) r f args
-
-  let special man r f args =
-    S.special (conv man) r f args
+  module NameLifter =
+  struct
+    let lift_name x = x ^ " hashconsed"
+  end
 
-  let combine_env man r fe f args fc es f_ask =
-    S.combine_env (conv man) r fe f args (Option.map C.unlift fc) es f_ask
+  module HConsedArg =
+  struct
+    (* We do refine int values on narrow and meet {!IntDomain.IntDomTupleImpl}, which can lead to fixpoint issues if we assume x op x = x *)
+    (* see https://github.com/goblint/analyzer/issues/1005 *)
+    let assume_idempotent = GobConfig.get_string "ana.int.refinement" = "never"
+  end
 
-  let combine_assign man r fe f args fc es f_ask =
-    S.combine_assign (conv man) r fe f args (Option.map C.unlift fc) es f_ask
+  include DomainLifter (NameLifter) (Lattice.HConsed (HConsedArg)) (S)
 
-  let threadenter man ~multiple lval f args =
-    S.threadenter (conv man) ~multiple lval f args
+  (* TODO: should marshal hashcons table to avoid relift altogether? *)
+end
 
-  let threadspawn man ~multiple lval f args fman =
-    S.threadspawn (conv man) ~multiple lval f args (conv fman)
+module type PrintableLifter =
+  functor (P: Printable.S) ->
+  sig
+    include Printable.S
 
-  let paths_as_set man = S.paths_as_set (conv man)
-  let event man e oman = S.event (conv man) e (conv oman)
-end
+    val lift: P.t -> t
+    val unlift: t -> P.t
+  end
 
-(** Lifts a [Spec] so that the context is [HashCached]. *)
-module HashCachedContextLifter (S:Spec)
+module ContextLifter (N: NameLifter) (F: PrintableLifter) (S:Spec)
   : Spec with module D = S.D
           and module G = S.G
-          and module C = Printable.HashCached (S.C)
+          and module C = F (S.C)
 =
 struct
   module D = S.D
   module G = S.G
-  module C = Printable.HashCached (S.C)
+  module C = F (S.C)
   module V = S.V
   module P = S.P
 
-  let name () = S.name () ^" context hashcached"
+  let name () = N.lift_name (S.name ())
 
-  type marshal = S.marshal 
+  type marshal = S.marshal
   let init = S.init
   let finalize = S.finalize
 
@@ -262,6 +214,13 @@ struct
   let event man e oman = S.event (conv man) e (conv oman)
 end
 
+(** Lifts a [Spec] so that the context is [Hashcons]d. *)
+module HashconsContextLifter = ContextLifter (struct let lift_name s = s ^ " context hashconsed" end) (Printable.HConsed)
+(* TODO: should marshal hashcons table to avoid relift altogether? *)
+
+(** Lifts a [Spec] so that the context is [HashCached]. *)
+module HashCachedContextLifter = ContextLifter (struct let lift_name s = s ^ " context hashcached" end) (Printable.HashCached)
+
 (* see option ana.opt.equal *)
 module OptEqual (S: Spec) = struct
   module D = struct include S.D let equal x y = x == y || equal x y end
diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml
index 506337ac1b..4dee3a62c8 100644
--- a/src/util/loopUnrolling.ml
+++ b/src/util/loopUnrolling.ml
@@ -261,7 +261,7 @@ let findLoopVarAndGoal loopStatement func (op, exp1, exp2) =
   | _ -> None
 
 let getLoopVar loopStatement func = function
-  | BinOp (op, exp1, exp2, TInt _) when isCompare op -> findLoopVarAndGoal loopStatement func (op, exp1, exp2)
+  | BinOp (op, exp1, exp2, _) when isCompare op -> findLoopVarAndGoal loopStatement func (op, exp1, exp2)
   | _ -> None
 
 let getsPointedAt var func =
diff --git a/tests/regression/03-practical/36-struct-ptr.c b/tests/regression/03-practical/36-struct-ptr.c
new file mode 100644
index 0000000000..e96a7f7966
--- /dev/null
+++ b/tests/regression/03-practical/36-struct-ptr.c
@@ -0,0 +1,20 @@
+#include <goblint.h>
+struct aws_al {
+	unsigned long current_size;
+};
+
+struct aws_pq {
+	int pred;
+	struct aws_al container;
+};
+
+int main() {
+	struct aws_pq queue = { 0, { 0}};
+	struct aws_al *const list = &queue.container;
+
+	if (list->current_size == 0UL) {
+		if (list->current_size == 0UL) {
+			__goblint_check(1); //REACHABLE
+		}
+	}
+}
diff --git a/tests/regression/24-octagon/18-dead.c b/tests/regression/24-octagon/18-dead.c
new file mode 100644
index 0000000000..5b5ccd908c
--- /dev/null
+++ b/tests/regression/24-octagon/18-dead.c
@@ -0,0 +1,23 @@
+//SKIP PARAM: --enable ana.int.interval --set ana.activated[+] apron
+// NOCRASH (was arithmetic on bottom)
+int main(void)
+{
+    int a;
+    unsigned short b;
+    int tmp;
+
+    b = (unsigned short )a;
+
+    if ((int )b + (int )b < (int )b) {
+
+        tmp = (int )b;
+        b += 1;
+
+        if (! tmp) {
+           tmp = 1;
+        }
+
+    }
+
+    return 0;
+}
diff --git a/tests/regression/78-termination/01-simple-loop-terminating.c b/tests/regression/78-termination/01-simple-loop-terminating.c
index 8ca4610057..f44e2f4bd0 100644
--- a/tests/regression/78-termination/01-simple-loop-terminating.c
+++ b/tests/regression/78-termination/01-simple-loop-terminating.c
@@ -3,7 +3,7 @@
 
 int main()
 {
-  int i = 1;
+  unsigned int i = 1;
 
   while (i <= 10)
   {
diff --git a/tests/regression/78-termination/03-nested-loop-terminating.c b/tests/regression/78-termination/03-nested-loop-terminating.c
index 6b31204567..442db425f0 100644
--- a/tests/regression/78-termination/03-nested-loop-terminating.c
+++ b/tests/regression/78-termination/03-nested-loop-terminating.c
@@ -3,9 +3,9 @@
 
 int main()
 {
-  int rows = 3;
-  int columns = 4;
-  int i = 1;
+  unsigned int rows = 3;
+  unsigned int columns = 4;
+  unsigned int i = 1;
 
   // Outer while loop for rows
   while (i <= rows)
diff --git a/tests/regression/78-termination/04-nested-loop-nonterminating.c b/tests/regression/78-termination/04-nested-loop-nonterminating.c
index 21b6014509..dba98215c4 100644
--- a/tests/regression/78-termination/04-nested-loop-nonterminating.c
+++ b/tests/regression/78-termination/04-nested-loop-nonterminating.c
@@ -7,7 +7,7 @@ int main()
 
   while (outerCount <= 3)
   {
-    int innerCount = 1;
+    unsigned int innerCount = 1;
 
     while (1) // NONTERMLOOP termination analysis shall mark beginning of while as non-terminating loop
     {
diff --git a/tests/regression/78-termination/05-for-loop-terminating.c b/tests/regression/78-termination/05-for-loop-terminating.c
index 7a2b789496..1c503abcd9 100644
--- a/tests/regression/78-termination/05-for-loop-terminating.c
+++ b/tests/regression/78-termination/05-for-loop-terminating.c
@@ -3,7 +3,7 @@
 
 int main()
 {
-  int i;
+  unsigned int i;
 
   for (i = 1; i <= 10; i++)
   {
diff --git a/tests/regression/78-termination/07-nested-for-loop-terminating.c b/tests/regression/78-termination/07-nested-for-loop-terminating.c
index 3293a1fa2c..9e24fb4b54 100644
--- a/tests/regression/78-termination/07-nested-for-loop-terminating.c
+++ b/tests/regression/78-termination/07-nested-for-loop-terminating.c
@@ -3,8 +3,8 @@
 
 int main()
 {
-  int rows = 3;
-  int columns = 4;
+  unsigned int rows = 3;
+  unsigned int columns = 4;
 
   // Nested loop to iterate over rows and columns
   for (int i = 1; i <= rows; i++)
diff --git a/tests/regression/78-termination/08-nested-for-loop-nonterminating.c b/tests/regression/78-termination/08-nested-for-loop-nonterminating.c
index cb65a0d267..a56b7e1abf 100644
--- a/tests/regression/78-termination/08-nested-for-loop-nonterminating.c
+++ b/tests/regression/78-termination/08-nested-for-loop-nonterminating.c
@@ -3,7 +3,7 @@
 
 int main()
 {
-  int outerCount, innerCount;
+  unsigned int outerCount, innerCount;
 
   for (outerCount = 1; outerCount <= 3; outerCount++)
   {
diff --git a/tests/regression/78-termination/09-complex-for-loop-terminating.c b/tests/regression/78-termination/09-complex-for-loop-terminating.c
index 74ee41eae8..1432c56531 100644
--- a/tests/regression/78-termination/09-complex-for-loop-terminating.c
+++ b/tests/regression/78-termination/09-complex-for-loop-terminating.c
@@ -3,7 +3,7 @@
 #include <stdio.h>
 
 int loops0(){
-  int i, j, k;
+  unsigned int i, j, k;
 
   // Outer loop
   for (i = 1; i <= 5; i++)
@@ -36,7 +36,7 @@ int loops0(){
 }
 
 int loops1(){
-  int i, j, k;
+  unsigned int i, j, k;
 
   // Loop with conditions
   for (i = 1; i <= 10; i++)
@@ -81,7 +81,7 @@ int loops1(){
   printf("\n");
 
   // Loop with multiple variables
-  int a, b, c;
+  unsigned int a, b, c;
   for (a = 1, b = 2, c = 3; a <= 10; a++, b += 2, c += 3)
   {
     printf("%d %d %d\n", a, b, c);
diff --git a/tests/regression/78-termination/10-complex-loop-terminating.c b/tests/regression/78-termination/10-complex-loop-terminating.c
index 96253c445f..94c31e402d 100644
--- a/tests/regression/78-termination/10-complex-loop-terminating.c
+++ b/tests/regression/78-termination/10-complex-loop-terminating.c
@@ -3,9 +3,9 @@
 #include <stdio.h>
 
 int loops0(){
-  int i = 1;
-  int j = 1;
-  int k = 5;
+  unsigned int i = 1;
+  unsigned int j = 1;
+  unsigned int k = 5;
 
   // Outer while loop
   while (i <= 5)
@@ -84,9 +84,9 @@ int loops0(){
 
 int loops1()
 {
-  int i = 1;
-  int j = 1;
-  int k = 5;
+  unsigned int i = 1;
+  unsigned int j = 1;
+  unsigned int k = 5;
 
   // Outer while loop
   while (i <= 5)
@@ -145,9 +145,9 @@ int loops1()
 }
 
 int loops2(){
-  int i = 1;
-  int j = 1;
-  int k = 5;
+  unsigned int i = 1;
+  unsigned int j = 1;
+  unsigned int k = 5;
 
   // Loop with nested conditions
   i = 1;
@@ -197,9 +197,9 @@ int loops2(){
   printf("\n");
 
   // Loop with multiple variables
-  int a = 1;
-  int b = 2;
-  int c = 3;
+  unsigned int a = 1;
+  unsigned int b = 2;
+  unsigned int c = 3;
   while (a <= 10)
   {
     printf("%d %d %d\n", a, b, c);
@@ -215,4 +215,4 @@ int main(){
   loops1();
   loops2();
   return 0;
-}
\ No newline at end of file
+}
diff --git a/tests/regression/78-termination/12-do-while-instant-terminating.c b/tests/regression/78-termination/12-do-while-instant-terminating.c
index 5bc18902b3..4b34c0733d 100644
--- a/tests/regression/78-termination/12-do-while-instant-terminating.c
+++ b/tests/regression/78-termination/12-do-while-instant-terminating.c
@@ -3,7 +3,7 @@
 
 int main()
 {
-  int i = 0;
+  unsigned int i = 0;
 
   do
   {
diff --git a/tests/regression/78-termination/13-do-while-terminating.c b/tests/regression/78-termination/13-do-while-terminating.c
index 6ac6946495..b9137a7508 100644
--- a/tests/regression/78-termination/13-do-while-terminating.c
+++ b/tests/regression/78-termination/13-do-while-terminating.c
@@ -3,7 +3,7 @@
 
 int main()
 {
-  int i = 1;
+  unsigned int i = 1;
 
   do
   {
diff --git a/tests/regression/78-termination/14-do-while-nonterminating.c b/tests/regression/78-termination/14-do-while-nonterminating.c
index 0a9df3421f..c75cab2877 100644
--- a/tests/regression/78-termination/14-do-while-nonterminating.c
+++ b/tests/regression/78-termination/14-do-while-nonterminating.c
@@ -3,12 +3,14 @@
 
 int main()
 {
-  int i = 1;
+  unsigned int i = 1;
 
   do
   {
     printf("Inside the do-while loop\n");
     i++;
+
+    if(i ==0) {i = 2;}
   } while (i >= 2); // NONTERMLOOP termination analysis shall mark while as non-terminating loop
 
   printf("Exited the loop\n");
diff --git a/tests/regression/78-termination/15-complex-loop-combination-terminating.c b/tests/regression/78-termination/15-complex-loop-combination-terminating.c
index 4912bbb1f2..74471c3e47 100644
--- a/tests/regression/78-termination/15-complex-loop-combination-terminating.c
+++ b/tests/regression/78-termination/15-complex-loop-combination-terminating.c
@@ -4,7 +4,7 @@
 
 int non_nested_loops(){
   // Non-nested loops
-  int i;
+  unsigned int i;
 
   // for loop
   for (i = 1; i <= 10; i++)
@@ -13,7 +13,7 @@ int non_nested_loops(){
   }
 
   // while loop
-  int j = 1;
+  unsigned int j = 1;
   while (j <= 10)
   {
     printf("While loop iteration: %d\n", j);
@@ -21,7 +21,7 @@ int non_nested_loops(){
   }
 
   // do-while loop
-  int k = 1;
+  unsigned int k = 1;
   do
   {
     printf("Do-While loop iteration: %d\n", k);
@@ -30,9 +30,9 @@ int non_nested_loops(){
   return 0;
 }
 
-int nested_loops(){
+int nested_loops1(){
    // Nested loops
-  int a, b;
+  unsigned int a, b;
 
   // Nested for and while loop
   for (a = 1; a <= 5; a++)
@@ -44,12 +44,14 @@ int nested_loops(){
       c++;
     }
   }
+}
 
+int nested_loops2(){
   // Nested while and do-while loop
-  int x = 1;
+  unsigned int x = 1;
   while (x <= 5)
   {
-    int y = 1;
+    unsigned int y = 1;
     do
     {
       printf("Nested While-Do-While loop: %d\n", y);
@@ -57,9 +59,11 @@ int nested_loops(){
     } while (y <= x);
     x++;
   }
+}
 
+int nested_loops3(){
   // Nested do-while and for loop
-  int p = 1;
+  unsigned int p = 1;
   do
   {
     for (int q = 1; q <= p; q++)
@@ -72,10 +76,10 @@ int nested_loops(){
 }
 
 int nested_while_loop_with_break(){
-  int m;
+  unsigned int m;
 
   // Nested while loop with a break statement
-  int n = 1;
+  unsigned int n = 1;
   while (n <= 5)
   {
     printf("Outer While loop iteration: %d\n", n);
@@ -96,7 +100,7 @@ int nested_while_loop_with_break(){
 
 int nested_loop_with_conditions(){
   // Loop with nested conditions
-  for (int v = 1; v <= 10; v++)
+  for (unsigned int v = 1; v <= 10; v++)
   {
     printf("Loop with Nested Conditions: %d - ", v);
     if (v < 5)
@@ -117,7 +121,9 @@ int nested_loop_with_conditions(){
 int main()
 {
   non_nested_loops();
-  nested_loops();
+  nested_loops1();
+  nested_loops2();
+  nested_loops3();
   // Additional nested loops
   nested_while_loop_with_break();
   nested_loop_with_conditions();
diff --git a/tests/regression/78-termination/16-nested-loop-nontrivial-nonterminating.c b/tests/regression/78-termination/16-nested-loop-nontrivial-nonterminating.c
index 267a2d2fd8..547524747b 100644
--- a/tests/regression/78-termination/16-nested-loop-nontrivial-nonterminating.c
+++ b/tests/regression/78-termination/16-nested-loop-nontrivial-nonterminating.c
@@ -3,11 +3,11 @@
 
 int main()
 {
-  int outerCount = 1;
+  unsigned int outerCount = 1;
 
   while (outerCount <= 3)
   {
-    int innerCount = 1;
+    unsigned int innerCount = 1;
 
     while (outerCount < 3 || innerCount > 0) // NONTERMLOOP termination analysis shall mark beginning of while as non-terminating loop
     {
diff --git a/tests/regression/78-termination/17-goto-terminating.c b/tests/regression/78-termination/17-goto-terminating.c
index 2f678d294b..4453b3ca49 100644
--- a/tests/regression/78-termination/17-goto-terminating.c
+++ b/tests/regression/78-termination/17-goto-terminating.c
@@ -4,7 +4,7 @@
 
 int main()
 {
-  int num = 1;
+  unsigned int num = 1;
 
 loop:
   printf("Current number: %d\n", num);
diff --git a/tests/regression/78-termination/18-goto-nonterminating.c b/tests/regression/78-termination/18-goto-nonterminating.c
index 6de80effd7..c8ad519a27 100644
--- a/tests/regression/78-termination/18-goto-nonterminating.c
+++ b/tests/regression/78-termination/18-goto-nonterminating.c
@@ -3,7 +3,7 @@
 
 int main()
 {
-  int num = 1;
+  unsigned int num = 1;
 
 loop:
   printf("Current number: %d\n", num);
diff --git a/tests/regression/78-termination/19-rand-terminating.c b/tests/regression/78-termination/19-rand-terminating.c
index a5b6c22941..33b33f2d29 100644
--- a/tests/regression/78-termination/19-rand-terminating.c
+++ b/tests/regression/78-termination/19-rand-terminating.c
@@ -11,7 +11,7 @@ int main()
   if (rand())
   {
     // Loop inside the if part
-    for (int i = 1; i <= 5; i++)
+    for (unsigned int i = 1; i <= 5; i++)
     {
       printf("Loop inside if part: %d\n", i);
     }
@@ -19,7 +19,7 @@ int main()
   else
   {
     // Loop inside the else part
-    int j = 1;
+    unsigned int j = 1;
     while (j <= 5)
     {
       printf("Loop inside else part: %d\n", j);
diff --git a/tests/regression/78-termination/20-rand-nonterminating.c b/tests/regression/78-termination/20-rand-nonterminating.c
index 21b25ed9dd..f695c2f552 100644
--- a/tests/regression/78-termination/20-rand-nonterminating.c
+++ b/tests/regression/78-termination/20-rand-nonterminating.c
@@ -11,7 +11,7 @@ int main()
   if (rand())
   {
     // Loop inside the if part
-    for (int i = 1; i >= 0; i++) // NONTERMLOOP termination analysis shall mark beginning of while as non-terminating loop
+    for (unsigned int i = 1; i >= 0; i++) // NONTERMLOOP termination analysis shall mark beginning of while as non-terminating loop
     {
       printf("Loop inside if part: %d\n", i);
     }
diff --git a/tests/regression/78-termination/21-no-exit-on-rand-unproofable.c b/tests/regression/78-termination/21-no-exit-on-rand-unproofable.c
index 5f82d91079..2fd64baed8 100644
--- a/tests/regression/78-termination/21-no-exit-on-rand-unproofable.c
+++ b/tests/regression/78-termination/21-no-exit-on-rand-unproofable.c
@@ -3,7 +3,7 @@
 
 int main()
 {
-  int forever, i = 0;
+  unsigned int forever, i = 0;
 
   // This loop is not provable, therefore it should throw a warning
   while (i < 4 || forever == 1) // NONTERMLOOP termination analysis shall mark beginning of while as non-terminating loop
@@ -17,4 +17,4 @@ int main()
       }
     }
   }
-}
\ No newline at end of file
+}
diff --git a/tests/regression/78-termination/22-exit-on-rand-unproofable.c b/tests/regression/78-termination/22-exit-on-rand-unproofable.c
index 33838ca83d..71cb208f6d 100644
--- a/tests/regression/78-termination/22-exit-on-rand-unproofable.c
+++ b/tests/regression/78-termination/22-exit-on-rand-unproofable.c
@@ -3,7 +3,7 @@
 
 int main()
 {
-  int forever = 1;
+  unsigned int forever = 1;
 
   // This loop is not provable, therefore it should throw a warning
   while (forever == 1) // NONTERMLOOP termination analysis shall mark beginning of while as non-terminating loop
@@ -13,4 +13,4 @@ int main()
       forever = 0;
     }
   }
-}
\ No newline at end of file
+}
diff --git a/tests/regression/78-termination/23-exit-on-rand-terminating.c b/tests/regression/78-termination/23-exit-on-rand-terminating.c
index e65c064c40..55efc59445 100644
--- a/tests/regression/78-termination/23-exit-on-rand-terminating.c
+++ b/tests/regression/78-termination/23-exit-on-rand-terminating.c
@@ -4,7 +4,7 @@
 
 int main()
 {
-  int short_run, i = 0;
+  unsigned int short_run, i = 0;
   // Currently not able to detect this as terminating due to multiple conditions
   while (i < 90 && short_run != 1)
   {
@@ -14,4 +14,4 @@ int main()
       short_run = 1;
     }
   }
-}
\ No newline at end of file
+}
diff --git a/tests/regression/78-termination/25-leave-loop-goto-terminating.c b/tests/regression/78-termination/25-leave-loop-goto-terminating.c
index 61c8b8f58d..baeaf275c5 100644
--- a/tests/regression/78-termination/25-leave-loop-goto-terminating.c
+++ b/tests/regression/78-termination/25-leave-loop-goto-terminating.c
@@ -1,9 +1,9 @@
-// SKIP TERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra
+// SKIP TODO TERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra
 #include <stdio.h>
 
 int main()
 {
-  int counter = 0;
+  unsigned int counter = 0;
 
   while (1)
   {
diff --git a/tests/regression/78-termination/26-enter-loop-goto-terminating.c b/tests/regression/78-termination/26-enter-loop-goto-terminating.c
index aa85f22b3e..7b3cbd59c1 100644
--- a/tests/regression/78-termination/26-enter-loop-goto-terminating.c
+++ b/tests/regression/78-termination/26-enter-loop-goto-terminating.c
@@ -3,7 +3,7 @@
 
 int main()
 {
-  int counter = 0;
+  unsigned int counter = 0;
 
   goto jump_point;
 
@@ -13,7 +13,7 @@ int main()
 
     // Dummy code
     printf("Iteration %d\n", counter);
-    int result = counter * 2;
+    unsigned int result = counter * 2;
   jump_point:
     printf("Result: %d\n", result);
 
diff --git a/tests/regression/78-termination/28-do-while-continue-terminating.c b/tests/regression/78-termination/28-do-while-continue-terminating.c
index d3b424f9b0..ca2dca5e8b 100644
--- a/tests/regression/78-termination/28-do-while-continue-terminating.c
+++ b/tests/regression/78-termination/28-do-while-continue-terminating.c
@@ -3,7 +3,7 @@
 
 int main()
 {
-  int i = 1;
+  unsigned int i = 1;
 
   do
   {
diff --git a/tests/regression/78-termination/29-do-while-continue-nonterminating.c b/tests/regression/78-termination/29-do-while-continue-nonterminating.c
index dd931c012f..151ff6112a 100644
--- a/tests/regression/78-termination/29-do-while-continue-nonterminating.c
+++ b/tests/regression/78-termination/29-do-while-continue-nonterminating.c
@@ -3,13 +3,15 @@
 
 int main()
 {
-  int i = 1;
+  unsigned int i = 1;
 
   do
   {
     printf("Inside the do-while loop\n");
     i++;
 
+    if(i ==0) {i = 2;}
+
     if (i % 2)
     {
       printf("Continue as %i is odd\n", i);
diff --git a/tests/regression/78-termination/30-goto-out-of-inner-loop-terminating.c b/tests/regression/78-termination/30-goto-out-of-inner-loop-terminating.c
index c07b558d07..16dfd4400e 100644
--- a/tests/regression/78-termination/30-goto-out-of-inner-loop-terminating.c
+++ b/tests/regression/78-termination/30-goto-out-of-inner-loop-terminating.c
@@ -3,14 +3,14 @@
 
 int main()
 {
-  int rows = 5;
-  int columns = 5;
+  unsigned int rows = 5;
+  unsigned int columns = 5;
 
   // Outer loop for rows
-  for (int i = 1; i <= rows; i++)
+  for (unsigned int i = 1; i <= rows; i++)
   {
     // Inner loop for columns
-    for (int j = 1; j <= columns; j++)
+    for (unsigned int j = 1; j <= columns; j++)
     {
       if (j == 3)
       {
diff --git a/tests/regression/78-termination/31-goto-out-of-inner-loop-nonterminating.c b/tests/regression/78-termination/31-goto-out-of-inner-loop-nonterminating.c
index f9b9275620..d518773cd5 100644
--- a/tests/regression/78-termination/31-goto-out-of-inner-loop-nonterminating.c
+++ b/tests/regression/78-termination/31-goto-out-of-inner-loop-nonterminating.c
@@ -7,7 +7,7 @@ int main()
   int columns = 5;
 
   // Outer loop for rows
-  for (int i = 1; 1; i++) // NONTERMLOOP termination analysis shall mark beginning of for as non-terminating loop
+  for (unsigned int i = 1; 1; i++) // NONTERMLOOP termination analysis shall mark beginning of for as non-terminating loop
   {
     // Inner loop for columns
     for (int j = 1; j <= columns; j++)
diff --git a/tests/regression/78-termination/34-nested-for-loop-nonterminating.c b/tests/regression/78-termination/34-nested-for-loop-nonterminating.c
index 2f21f9e996..b4048d82a2 100644
--- a/tests/regression/78-termination/34-nested-for-loop-nonterminating.c
+++ b/tests/regression/78-termination/34-nested-for-loop-nonterminating.c
@@ -3,11 +3,11 @@
 
 int main()
 {
-  int outerCount, innerCount;
+  unsigned int outerCount, innerCount;
 
   for (outerCount = 1; outerCount <= 3; outerCount++)
   {
-    for (innerCount = 1; innerCount > 0; innerCount++) // NONTERMLOOP termination analysis shall mark beginning of for as non-terminating loop
+    for (innerCount = 1; innerCount > 0; innerCount += 4) // NONTERMLOOP termination analysis shall mark beginning of for as non-terminating loop
     {
       printf("(%d, %d) ", outerCount, innerCount);
     }
diff --git a/tests/regression/78-termination/35-goto-out-of-inner-loop-with-print-terminating.c b/tests/regression/78-termination/35-goto-out-of-inner-loop-with-print-terminating.c
index 4c738e1173..4337ccc8fa 100644
--- a/tests/regression/78-termination/35-goto-out-of-inner-loop-with-print-terminating.c
+++ b/tests/regression/78-termination/35-goto-out-of-inner-loop-with-print-terminating.c
@@ -3,14 +3,14 @@
 
 int main()
 {
-  int rows = 5;
-  int columns = 5;
+  unsigned int rows = 5;
+  unsigned int columns = 5;
 
   // Outer loop for rows
-  for (int i = 1; i <= rows; i++)
+  for (unsigned int i = 1; i <= rows; i++)
   {
     // Inner loop for columns
-    for (int j = 1; j <= columns; j++)
+    for (unsigned int j = 1; j <= columns; j++)
     {
       if (j == 3)
       {
diff --git a/tests/regression/78-termination/40-multi-expression-conditions-terminating.c b/tests/regression/78-termination/40-multi-expression-conditions-terminating.c
index 80f8c5a1e8..d991683d2b 100644
--- a/tests/regression/78-termination/40-multi-expression-conditions-terminating.c
+++ b/tests/regression/78-termination/40-multi-expression-conditions-terminating.c
@@ -3,7 +3,7 @@
 
 int main()
 {
-  int i;
+  unsigned int i;
 
   // Loop with complex conditions
   for (i = 1; i <= 10; i++)
@@ -28,7 +28,7 @@ int main()
   printf("\n");
 
   // Loop with multiple conditions
-  int s = 1;
+  unsigned int s = 1;
   while (s <= 10 && s % 2 == 0) // CIL defines new jump labels to default location (-1)
   {
     printf("Loop with Multiple Conditions: %d\n", s);
@@ -36,9 +36,9 @@ int main()
   }
 
   // Loop with multiple variables
-  int t, u;
+  unsigned int t, u;
   for (t = 1, u = 10; t <= 5 && u >= 5; t++, u--) // CIL defines new jump labels to default location (-1)
   {
     printf("Loop with Multiple Variables: %d %d\n", t, u);
   }
-}
\ No newline at end of file
+}
diff --git a/tests/regression/78-termination/41-for-continue-terminating.c b/tests/regression/78-termination/41-for-continue-terminating.c
index d87a705868..0557dd13af 100644
--- a/tests/regression/78-termination/41-for-continue-terminating.c
+++ b/tests/regression/78-termination/41-for-continue-terminating.c
@@ -4,7 +4,7 @@
 int main()
 {
   // Loop with a continue statement
-  for (int i = 1; i <= 10; i++)
+  for (unsigned int i = 1; i <= 10; i++)
   {
     if (i % 2 == 0)
     {
@@ -16,7 +16,7 @@ int main()
 
 
   // Loop with a continue statement
-  for (int r = 1; r <= 10; r++)
+  for (unsigned int r = 1; r <= 10; r++)
   {
     if (r % 3 == 0)
     {
@@ -24,4 +24,4 @@ int main()
     }
     printf("Loop with Continue: %d\n", r);
   }
-}
\ No newline at end of file
+}
diff --git a/tests/regression/78-termination/43-return-from-endless-loop-terminating.c b/tests/regression/78-termination/43-return-from-endless-loop-terminating.c
index fb48e1cdbe..5104f6ef37 100644
--- a/tests/regression/78-termination/43-return-from-endless-loop-terminating.c
+++ b/tests/regression/78-termination/43-return-from-endless-loop-terminating.c
@@ -2,7 +2,7 @@
 #include <stdio.h>
 
 int main() {
-  int i = 1;
+  unsigned int i = 1;
 
   while (i != 0) {
     printf("%d\n", i);
diff --git a/tests/regression/78-termination/50-decreasing-signed-int.c b/tests/regression/78-termination/50-decreasing-signed-int.c
index 01daa5ee21..3d594dbd61 100644
--- a/tests/regression/78-termination/50-decreasing-signed-int.c
+++ b/tests/regression/78-termination/50-decreasing-signed-int.c
@@ -1,9 +1,9 @@
 // SKIP TERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain octagon
 int main()
 {
-	int x;
+	unsigned int x;
 
-	if(x <= 0){
+	if(x == 0){
 		return 0;
 	}
 	while (x > 0) {
diff --git a/tests/unit/cdomains/intDomainTest.ml b/tests/unit/cdomains/intDomainTest.ml
index 5d022d7ce2..7cedef3188 100644
--- a/tests/unit/cdomains/intDomainTest.ml
+++ b/tests/unit/cdomains/intDomainTest.ml
@@ -17,81 +17,85 @@ struct
   let itrue      = I.of_bool true
   let ifalse     = I.of_bool false
 
+  let assert_poly_equal = assert_equal
+  let assert_equal x y =
+    assert_equal ~cmp:I.equal ~printer:I.show x y
+
 
   let test_int_comp _ =
-    assert_equal ~printer:I.show izero (I.of_int zero);
-    assert_equal ~printer:I.show ione  (I.of_int one);
-    assert_equal ~printer:I.show itrue (I.of_bool true);
-    assert_equal ~printer:I.show ifalse(I.of_bool false);
-    assert_equal (Some one ) (I.to_int ione);
-    assert_equal (Some zero) (I.to_int izero);
-    assert_equal (Some zero) (I.to_int ifalse)
+    assert_equal izero (I.of_int zero);
+    assert_equal ione  (I.of_int one);
+    assert_equal itrue (I.of_bool true);
+    assert_equal ifalse(I.of_bool false);
+    assert_poly_equal (Some one ) (I.to_int ione);
+    assert_poly_equal (Some zero) (I.to_int izero);
+    assert_poly_equal (Some zero) (I.to_int ifalse)
 
 
   let test_bool _ =
-    assert_equal (Some true ) (I.to_bool ione);
-    assert_equal (Some false) (I.to_bool izero);
-    assert_equal (Some true ) (I.to_bool itrue);
-    assert_equal (Some false) (I.to_bool ifalse);
-    assert_equal ~printer:I.show itrue  (I.lt ione  itwo);
-    assert_equal ~printer:I.show ifalse (I.gt ione  itwo);
-    assert_equal ~printer:I.show itrue  (I.le ione  ione);
-    assert_equal ~printer:I.show ifalse (I.ge izero itwo);
-    assert_equal ~printer:I.show itrue  (I.eq izero izero);
-    assert_equal ~printer:I.show ifalse (I.ne ione  ione)
+    assert_poly_equal (Some true ) (I.to_bool ione);
+    assert_poly_equal (Some false) (I.to_bool izero);
+    assert_poly_equal (Some true ) (I.to_bool itrue);
+    assert_poly_equal (Some false) (I.to_bool ifalse);
+    assert_equal itrue  (I.lt ione  itwo);
+    assert_equal ifalse (I.gt ione  itwo);
+    assert_equal itrue  (I.le ione  ione);
+    assert_equal ifalse (I.ge izero itwo);
+    assert_equal itrue  (I.eq izero izero);
+    assert_equal ifalse (I.ne ione  ione)
 
 
   let test_neg _ =
-    assert_equal ~printer:I.show in5 (I.neg i5);
-    assert_equal ~printer:I.show i5 (I.neg (I.neg i5));
-    assert_equal ~printer:I.show izero (I.neg izero)
+    assert_equal in5 (I.neg i5);
+    assert_equal i5 (I.neg (I.neg i5));
+    assert_equal izero (I.neg izero)
 
 
   let test_add _ =
-    assert_equal ~printer:I.show ione (I.add izero ione);
-    assert_equal ~printer:I.show ione (I.add ione  izero);
-    assert_equal ~printer:I.show izero(I.add izero izero)
+    assert_equal ione (I.add izero ione);
+    assert_equal ione (I.add ione  izero);
+    assert_equal izero(I.add izero izero)
 
 
   let test_sub _ =
-    assert_equal ~printer:I.show ione (I.sub izero iminus_one);
-    assert_equal ~printer:I.show ione (I.sub ione  izero);
-    assert_equal ~printer:I.show izero(I.sub izero izero)
+    assert_equal ione (I.sub izero iminus_one);
+    assert_equal ione (I.sub ione  izero);
+    assert_equal izero(I.sub izero izero)
 
 
   let test_mul _ =
-    assert_equal ~printer:I.show izero(I.mul izero iminus_one);
-    assert_equal ~printer:I.show izero(I.mul izero izero);
-    assert_equal ~printer:I.show ione (I.mul ione  ione);
-    assert_equal ~printer:I.show i42  (I.mul ione  i42)
+    assert_equal izero(I.mul izero iminus_one);
+    assert_equal izero(I.mul izero izero);
+    assert_equal ione (I.mul ione  ione);
+    assert_equal i42  (I.mul ione  i42)
 
 
   let test_div _ =
-    assert_equal ~printer:I.show ione (I.div ione ione);
-    assert_equal ~printer:I.show ione (I.div i5 i5);
-    assert_equal ~printer:I.show i5   (I.div i5 ione);
-    assert_equal ~printer:I.show in5  (I.div i5 iminus_one);
+    assert_equal ione (I.div ione ione);
+    assert_equal ione (I.div i5 i5);
+    assert_equal i5   (I.div i5 ione);
+    assert_equal in5  (I.div i5 iminus_one);
     assert_bool "div_by_0" (try I.is_top (I.div i5 izero) with Division_by_zero -> true)
 
 
   let test_rem _ =
-    assert_equal ~printer:I.show ione (I.rem ione  i5);
-    assert_equal ~printer:I.show izero(I.rem izero i5);
-    assert_equal ~printer:I.show itwo (I.rem i42   i5);
-    assert_equal ~printer:I.show itwo (I.rem i42   in5)
+    assert_equal ione (I.rem ione  i5);
+    assert_equal izero(I.rem izero i5);
+    assert_equal itwo (I.rem i42   i5);
+    assert_equal itwo (I.rem i42   in5)
 
 
   let test_bit _ =
-    assert_equal ~printer:I.show iminus_one (I.lognot izero);
-    assert_equal ~printer:I.show iminus_two (I.lognot ione);
-    assert_equal ~printer:I.show i5   (I.logand i5 i5);
-    assert_equal ~printer:I.show i4   (I.logand i5 i4);
-    assert_equal ~printer:I.show i5   (I.logor  i4 ione);
-    assert_equal ~printer:I.show ione (I.logxor i4 i5);
-    assert_equal ~printer:I.show itwo (I.shift_left  ione ione );
-    assert_equal ~printer:I.show ione (I.shift_left  ione izero);
-    assert_equal ~printer:I.show ione (I.shift_right itwo ione);
-    assert_equal ~printer:I.show izero(I.shift_right ione ione)
+    assert_equal iminus_one (I.lognot izero);
+    assert_equal iminus_two (I.lognot ione);
+    assert_equal i5   (I.logand i5 i5);
+    assert_equal i4   (I.logand i5 i4);
+    assert_equal i5   (I.logor  i4 ione);
+    assert_equal ione (I.logxor i4 i5);
+    assert_equal itwo (I.shift_left  ione ione );
+    assert_equal ione (I.shift_left  ione izero);
+    assert_equal ione (I.shift_right itwo ione);
+    assert_equal izero(I.shift_right ione ione)
 
 
   let test () =
@@ -112,91 +116,97 @@ module Ikind = struct let ikind () = Cil.ILong end
 module A = IntTest (IntDomain.Integers (IntOps.BigIntOps))
 module B = IntTest (IntDomain.Flat (IntDomain.Integers (IntOps.BigIntOps)))
 module C = IntTest (IntDomainProperties.WithIkind (IntDomain.DefExc) (Ikind))
-module T = struct
-  include IntDomainProperties.WithIkind (IntDomain.DefExc) (Ikind)
-  let of_excl_list xs = of_excl_list Cil.ILong xs
-end
 
-let tzero      = T.of_int zero
-let tone       = T.of_int one
-let tminus_one = T.of_int minus_one
-let ttwo       = T.of_int (of_int 2)
-let tminus_two = T.of_int (of_int (-2))
-let t4         = T.of_int (of_int 4)
-let t5         = T.of_int (of_int 5)
-let tn5        = T.of_int (of_int (-5))
-let t42        = T.of_int (of_int 42)
-let ttrue      = T.of_bool true
-let tfalse     = T.of_bool false
-let ttop       = T.top ()
-let tbot       = T.bot ()
-let tex0       = T.of_excl_list [zero]
-let tex1       = T.of_excl_list [one ]
-let tex10      = T.of_excl_list [zero; one]
-let tex01      = T.of_excl_list [one; zero]
-
-let test_bot _ =
-  assert_bool "bot != bot" (T.is_bot tbot);
-  assert_bool "top != top" (T.is_top ttop);
-  assert_bool "top == bot" (not (T.is_bot ttop));
-  assert_bool "bot == top" (not (T.is_top tbot));
-  assert_bool "0 == top" (not (T.is_top tzero));
-  assert_bool "1 == top" (not (T.is_top tone))
-
-let test_join _ =
-  assert_equal ~printer:T.show tone (T.join tbot  tone);
-  assert_equal ~printer:T.show tzero(T.join tbot  tzero);
-  assert_equal ~printer:T.show tone (T.join tone  tbot);
-  assert_equal ~printer:T.show tzero(T.join tzero tbot);
-  assert_equal ~printer:T.show ttop (T.join ttop  tone);
-  assert_equal ~printer:T.show ttop (T.join ttop  tzero);
-  assert_equal ~printer:T.show ttop (T.join tone  ttop);
-  assert_equal ~printer:T.show ttop (T.join tzero ttop);
-  assert_equal ~printer:T.show tbot (T.join tbot  tbot);
-  assert_equal ~printer:T.show tone (T.join tone  tone);
-  (* assert_equal ~printer:T.show tex0 (T.join tone  ttwo); *) (* TODO: now more precise range *)
-  (* assert_equal ~printer:T.show ttop (T.join tone  tzero); *) (* TODO: now more precise range *)
-  assert_equal ~printer:T.show tex0 (T.join tex0  tex0);
-  assert_equal ~printer:T.show tex1 (T.join tex1  tex1);
-  assert_equal ~printer:T.show ttop (T.join tex1  tex0);
-  assert_equal ~printer:T.show ttop (T.join tex0  tex1);
-  (* assert_equal ~printer:T.show tex0 (T.join tone  ttwo); *) (* TODO: now more precise range *)
-  assert_equal ~printer:T.show tex1 (T.join tex1  tzero);
-  assert_equal ~printer:T.show tex0 (T.join tex0  tone );
-  assert_equal ~printer:T.show tex1 (T.join tex1  tzero);
-  assert_equal ~printer:T.show tex0 (T.join tex0  tone )
-
-let test_meet _ =
-  assert_equal ~printer:T.show tbot (T.meet tbot  tone);
-  assert_equal ~printer:T.show tbot (T.meet tbot  tzero);
-  assert_equal ~printer:T.show tbot (T.meet tone  tbot);
-  assert_equal ~printer:T.show tbot (T.meet tzero tbot);
-  assert_equal ~printer:T.show tone (T.meet ttop  tone);
-  assert_equal ~printer:T.show tzero(T.meet ttop  tzero);
-  assert_equal ~printer:T.show tone (T.meet tone  ttop);
-  assert_equal ~printer:T.show tzero(T.meet tzero ttop);
-  assert_equal ~printer:T.show tbot (T.meet tbot  tbot);
-  assert_equal ~printer:T.show tone (T.meet tone  tone);
-  assert_equal ~printer:T.show tbot (T.meet tone  ttwo);
-  assert_equal ~printer:T.show tbot (T.meet tone  tzero);
-  assert_equal ~printer:T.show tex0 (T.meet tex0  tex0);
-  assert_equal ~printer:T.show tex1 (T.meet tex1  tex1);
-  assert_equal ~printer:T.show tex10(T.meet tex1  tex0);
-  assert_equal ~printer:T.show tex01(T.meet tex0  tex1);
-  assert_equal ~printer:T.show tzero(T.meet tex1  tzero);
-  assert_equal ~printer:T.show tone (T.meet tex0  tone );
-  assert_equal ~printer:T.show tzero(T.meet tex1  tzero);
-  assert_equal ~printer:T.show tone (T.meet tex0  tone )
-
-let test_ex_set _ =
-  assert_equal (Some [zero; one]) (T.to_excl_list tex10 |> Option.map fst);
-  assert_equal (Some [zero; one]) (T.to_excl_list tex01 |> Option.map fst);
-  assert_bool  "Not [1;0] is not excl set" (T.is_excl_list tex10);
-  assert_bool  "bot is excl set" (not (T.is_excl_list tbot));
-  assert_bool  "42  is excl set" (not (T.is_excl_list t42));
-  assert_equal (Some true) (T.to_bool tex0);
-  assert_equal (Some true) (T.to_bool tex10);
-  assert_equal None (T.to_bool tex1)
+module D = struct
+  module T = struct
+    include IntDomainProperties.WithIkind (IntDomain.DefExc) (Ikind)
+    let of_excl_list xs = of_excl_list Cil.ILong xs
+  end
+
+  let tzero      = T.of_int zero
+  let tone       = T.of_int one
+  let tminus_one = T.of_int minus_one
+  let ttwo       = T.of_int (of_int 2)
+  let tminus_two = T.of_int (of_int (-2))
+  let t4         = T.of_int (of_int 4)
+  let t5         = T.of_int (of_int 5)
+  let tn5        = T.of_int (of_int (-5))
+  let t42        = T.of_int (of_int 42)
+  let ttrue      = T.of_bool true
+  let tfalse     = T.of_bool false
+  let ttop       = T.top ()
+  let tbot       = T.bot ()
+  let tex0       = T.of_excl_list [zero]
+  let tex1       = T.of_excl_list [one ]
+  let tex10      = T.of_excl_list [zero; one]
+  let tex01      = T.of_excl_list [one; zero]
+
+  let test_bot _ =
+    assert_bool "bot != bot" (T.is_bot tbot);
+    assert_bool "top != top" (T.is_top ttop);
+    assert_bool "top == bot" (not (T.is_bot ttop));
+    assert_bool "bot == top" (not (T.is_top tbot));
+    assert_bool "0 == top" (not (T.is_top tzero));
+    assert_bool "1 == top" (not (T.is_top tone))
+
+  let assert_poly_equal = assert_equal
+  let assert_equal x y = assert_equal ~cmp: T.equal ~printer:T.show x y
+
+  let test_join _ =
+    assert_equal tone (T.join tbot  tone);
+    assert_equal tzero(T.join tbot  tzero);
+    assert_equal tone (T.join tone  tbot);
+    assert_equal tzero(T.join tzero tbot);
+    assert_equal ttop (T.join ttop  tone);
+    assert_equal ttop (T.join ttop  tzero);
+    assert_equal ttop (T.join tone  ttop);
+    assert_equal ttop (T.join tzero ttop);
+    assert_equal tbot (T.join tbot  tbot);
+    assert_equal tone (T.join tone  tone);
+    (* assert_equal tex0 (T.join tone  ttwo); *) (* TODO: now more precise range *)
+    (* assert_equal ttop (T.join tone  tzero); *) (* TODO: now more precise range *)
+    assert_equal tex0 (T.join tex0  tex0);
+    assert_equal tex1 (T.join tex1  tex1);
+    assert_equal ttop (T.join tex1  tex0);
+    assert_equal ttop (T.join tex0  tex1);
+    (* assert_equal ~printer:T.show tex0 (T.join tone  ttwo); *) (* TODO: now more precise range *)
+    assert_equal tex1 (T.join tex1  tzero);
+    assert_equal tex0 (T.join tex0  tone );
+    assert_equal tex1 (T.join tex1  tzero);
+    assert_equal tex0 (T.join tex0  tone )
+
+  let test_meet _ =
+    assert_equal tbot (T.meet tbot  tone);
+    assert_equal tbot (T.meet tbot  tzero);
+    assert_equal tbot (T.meet tone  tbot);
+    assert_equal tbot (T.meet tzero tbot);
+    assert_equal tone (T.meet ttop  tone);
+    assert_equal tzero(T.meet ttop  tzero);
+    assert_equal tone (T.meet tone  ttop);
+    assert_equal tzero(T.meet tzero ttop);
+    assert_equal tbot (T.meet tbot  tbot);
+    assert_equal tone (T.meet tone  tone);
+    assert_equal tbot (T.meet tone  ttwo);
+    assert_equal tbot (T.meet tone  tzero);
+    assert_equal tex0 (T.meet tex0  tex0);
+    assert_equal tex1 (T.meet tex1  tex1);
+    assert_equal tex10(T.meet tex1  tex0);
+    assert_equal tex01(T.meet tex0  tex1);
+    assert_equal tzero(T.meet tex1  tzero);
+    assert_equal tone (T.meet tex0  tone );
+    assert_equal tzero(T.meet tex1  tzero);
+    assert_equal tone (T.meet tex0  tone )
+
+  let test_ex_set _ =
+    assert_poly_equal (Some [zero; one]) (T.to_excl_list tex10 |> Option.map fst);
+    assert_poly_equal (Some [zero; one]) (T.to_excl_list tex01 |> Option.map fst);
+    assert_bool  "Not [1;0] is not excl set" (T.is_excl_list tex10);
+    assert_bool  "bot is excl set" (not (T.is_excl_list tbot));
+    assert_bool  "42  is excl set" (not (T.is_excl_list t42));
+    assert_poly_equal (Some true) (T.to_bool tex0);
+    assert_poly_equal (Some true) (T.to_bool tex10);
+    assert_poly_equal None (T.to_bool tex1)
+end
 
 module IntervalTest (I : IntDomain.SOverflow with type int_t = Z.t) =
 struct
@@ -996,10 +1006,10 @@ let test () =
     "int_Integers"  >::: A.test ();
     "int_Flattened" >::: B.test ();
     "int_DefExc"     >::: C.test ();
-    "test_bot"      >::  test_bot;
-    "test_join"     >::  test_join;
-    "test_meet"     >::  test_meet;
-    "test_excl_list">::  test_ex_set;
+    "test_bot"      >::  D.test_bot;
+    "test_join"     >::  D.test_join;
+    "test_meet"     >::  D.test_meet;
+    "test_excl_list">::  D.test_ex_set;
     "interval" >::: Interval.test ();
     "bitfield" >::: Bitfield.test ();
     "intervalSet" >::: IntervalSet.test ();