diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml
index 61d28fc505..c0316ed877 100644
--- a/src/analyses/apron/relationAnalysis.apron.ml
+++ b/src/analyses/apron/relationAnalysis.apron.ml
@@ -173,25 +173,8 @@ struct
     | _ ->
       st
 
-
-  (** An extended overflow handling inside relationAnalysis for expression assignments when overflows are assumed to occur.
-      Since affine equalities can only keep track of integer bounds of expressions evaluating to definite constants, we now query the integer bounds information for expressions from other analysis.
-      If an analysis returns bounds that are unequal to min and max of ikind , we can exclude the possibility that an overflow occurs and the abstract effect of the expression assignment can be used, i.e. we do not have to set the variable's value to top. *)
-
-  let no_overflow (ask: Queries.ask) exp =
-    match Cilfacade.get_ikind_exp exp with
-    | exception Invalid_argument _ -> false (* is thrown by get_ikind_exp when the type of the expression is not an integer type *)
-    | exception Cilfacade.TypeOfError _ -> false
-    | ik ->
-      if IntDomain.should_wrap ik then
-        false
-      else if IntDomain.should_ignore_overflow ik then
-        true
-      else
-        not (ask.f (MaySignedOverflow exp))
-
   let no_overflow man exp = lazy (
-    let res = no_overflow man exp in
+    let res = SharedFunctions.no_overflow man exp in
     if M.tracing then M.tracel "no_ov" "no_ov %b exp: %a" res d_exp exp;
     res
   )
@@ -611,7 +594,7 @@ struct
         (* filter one-vars and exact *)
         (* RD.invariant simplifies two octagon SUPEQ constraints to one EQ, so exact works *)
         if (one_var || GobApron.Lincons1.num_vars lincons1 >= 2) && (exact || Apron.Lincons1.get_typ lincons1 <> EQ) then
-          RD.cil_exp_of_lincons1 lincons1
+          RD.cil_exp_of_lincons1 ask e_inv lincons1
           |> Option.map e_inv
           |> Option.filter (fun exp -> not (InvariantCil.exp_contains_tmp exp) && InvariantCil.exp_is_in_scope scope exp)
         else
diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml
index 992b7fb587..062e807f7d 100644
--- a/src/analyses/apron/relationPriv.apron.ml
+++ b/src/analyses/apron/relationPriv.apron.ml
@@ -732,7 +732,7 @@ struct
               (* filter one-vars and exact *)
               (* RD.invariant simplifies two octagon SUPEQ constraints to one EQ, so exact works *)
               if (one_var || GobApron.Lincons1.num_vars lincons1 >= 2) && (exact || Apron.Lincons1.get_typ lincons1 <> EQ) then
-                RD.cil_exp_of_lincons1 lincons1
+                RD.cil_exp_of_lincons1 ask Fun.id lincons1
                 |> Option.filter (fun exp -> not (InvariantCil.exp_contains_tmp exp))
               else
                 None
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index ab0d61a874..f88a2b905f 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -1321,7 +1321,7 @@ struct
       For now we return true if the expression contains a shift left.
   *)
   (* TODO: deduplicate https://github.com/goblint/analyzer/pull/1297#discussion_r1477804502 *)
-  let rec exp_may_signed_overflow man exp =
+  let rec exp_may_overflow man exp ~unsigned =
     let res = match Cilfacade.get_ikind_exp exp with
       | exception (Cilfacade.TypeOfError _) (* Cilfacade.typeOf *)
       | exception (Invalid_argument _) -> (* get_ikind *)
@@ -1383,20 +1383,20 @@ struct
         | Imag e
         | SizeOfE e
         | AlignOfE e
-        | CastE (_, e) -> exp_may_signed_overflow man e
+        | CastE (_, e) -> exp_may_overflow man e ~unsigned:unsigned
         | UnOp (unop, e, _) ->
           (* check if the current operation causes a signed overflow *)
           begin match unop with
             | Neg -> (* an overflow happens when the lower bound of the interval is less than MIN_INT *)
-              Cil.isSigned ik && checkPredicate e (Z.gt)
+              (unsigned || Cil.isSigned ik) && checkPredicate e (Z.gt)
             (* operations that do not result in overflow in C: *)
             | BNot|LNot -> false
           end
           (* look for overflow in subexpression *)
-          || exp_may_signed_overflow man e
+          || exp_may_overflow man e ~unsigned:unsigned
         | BinOp (binop, e1, e2, _) ->
           (* check if the current operation causes a signed overflow *)
-          (Cil.isSigned ik && begin match binop with
+          ((unsigned || Cil.isSigned ik) && begin match binop with
               | PlusA|PlusPI|IndexPI -> checkBinop e1 e2 (GobOption.map2 Z.(+))
               | MinusA|MinusPI|MinusPP -> checkBinop e1 e2 (GobOption.map2 Z.(-))
               | Mult -> checkBinop e1 e2 (GobOption.map2 Z.mul)
@@ -1408,27 +1408,27 @@ struct
               (* Shiftlt can cause overflow and also undefined behaviour in case the second operand is non-positive*)
               | Shiftlt -> true end)
           (* look for overflow in subexpression *)
-          || exp_may_signed_overflow man e1 || exp_may_signed_overflow man e2
+          || exp_may_overflow man e1 ~unsigned:unsigned || exp_may_overflow man e2 ~unsigned:unsigned
         | Question (e1, e2, e3, _) ->
           (* does not result in overflow in C *)
-          exp_may_signed_overflow man e1 || exp_may_signed_overflow man e2 || exp_may_signed_overflow man e3
+          exp_may_overflow man e1 ~unsigned:unsigned || exp_may_overflow man e2 ~unsigned:unsigned || exp_may_overflow man e3 ~unsigned:unsigned
         | Lval lval
         | AddrOf lval
-        | StartOf lval -> lval_may_signed_overflow man lval
+        | StartOf lval -> lval_may_overflow man lval ~unsigned:unsigned
     in
-    if M.tracing then M.trace "signed_overflow" "base exp_may_signed_overflow %a. Result = %b" d_plainexp exp res; res
-  and lval_may_signed_overflow man (lval : lval) =
+    if M.tracing then M.trace "signed_overflow" "base exp_may_overflow %a. Result = %b" d_plainexp exp res; res
+  and lval_may_overflow man (lval : lval) ~unsigned =
     let (host, offset) = lval in
-    let host_may_signed_overflow = function
+    let host_may_overflow = function
       | Var v -> false
-      | Mem e -> exp_may_signed_overflow man e
+      | Mem e -> exp_may_overflow man e ~unsigned:unsigned
     in
-    let rec offset_may_signed_overflow = function
+    let rec offset_may_overflow = function
       | NoOffset -> false
-      | Index (e, o) -> exp_may_signed_overflow man e || offset_may_signed_overflow o
-      | Field (f, o) -> offset_may_signed_overflow o
+      | Index (e, o) -> exp_may_overflow man e ~unsigned:unsigned || offset_may_overflow o
+      | Field (f, o) -> offset_may_overflow o
     in
-    host_may_signed_overflow host || offset_may_signed_overflow offset
+    host_may_overflow host || offset_may_overflow offset
 
   let query man (type a) (q: a Q.t): a Q.result =
     match q with
@@ -1601,9 +1601,12 @@ struct
     | Q.InvariantGlobal g ->
       let g: V.t = Obj.obj g in
       query_invariant_global man g
-    | Q.MaySignedOverflow e -> (let res = exp_may_signed_overflow man e in
-                                if M.tracing then M.trace "signed_overflow" "base exp_may_signed_overflow %a. Result = %b" d_plainexp e res; res
-                               )
+    | Q.MaySignedOverflow e ->
+      let res = exp_may_overflow man e ~unsigned:false in
+      if M.tracing then M.trace "signed_overflow" "base exp_may_overflow %a. Result = %b" d_plainexp e res; res
+    | Q.MayOverflow e ->
+      let res = exp_may_overflow man e ~unsigned:true in
+      if M.tracing then M.trace "overflow" "base exp_may_overflow %a. Result = %b" d_plainexp e res; res
     | _ -> Q.Result.top q
 
   let update_variable variable typ value cpa =
diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml
index 2dd3b1e224..ba255ce9df 100644
--- a/src/cdomains/apron/apronDomain.apron.ml
+++ b/src/cdomains/apron/apronDomain.apron.ml
@@ -216,7 +216,7 @@ sig
   val to_lincons_array : t -> Lincons1.earray
   val of_lincons_array : Lincons1.earray -> t
 
-  val cil_exp_of_lincons1: Lincons1.t -> exp option
+  val cil_exp_of_lincons1: Queries.ask -> (exp -> exp) -> Lincons1.t -> exp option
   val invariant: t -> Lincons1.t list
 end
 
diff --git a/src/cdomains/apron/relationDomain.apron.ml b/src/cdomains/apron/relationDomain.apron.ml
index 5d266cf474..a61af02ff7 100644
--- a/src/cdomains/apron/relationDomain.apron.ml
+++ b/src/cdomains/apron/relationDomain.apron.ml
@@ -135,7 +135,7 @@ end
 module type S3 =
 sig
   include S2
-  val cil_exp_of_lincons1: Lincons1.t -> exp option
+  val cil_exp_of_lincons1: Queries.ask -> (exp -> exp) -> Lincons1.t -> exp option
   val invariant: t -> Lincons1.t list
 end
 
diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml
index 446b9d792d..4a0c1a90dd 100644
--- a/src/cdomains/apron/sharedFunctions.apron.ml
+++ b/src/cdomains/apron/sharedFunctions.apron.ml
@@ -41,6 +41,20 @@ let int_of_scalar ?(scalewith=Z.one) ?round (scalar: Scalar.t) =
     | _ ->
       failwith ("int_of_scalar: unsupported: " ^ Scalar.show scalar)
 
+(** An extended overflow handling inside relationAnalysis for expression assignments when overflows are assumed to occur.
+    Since affine equalities can only keep track of integer bounds of expressions evaluating to definite constants, we now query the integer bounds information for expressions from other analysis.
+    If an analysis returns bounds that are unequal to min and max of ikind , we can exclude the possibility that an overflow occurs and the abstract effect of the expression assignment can be used, i.e. we do not have to set the variable's value to top. *)
+let no_overflow (ask: Queries.ask) exp =
+  match Cilfacade.get_ikind_exp exp with
+  | exception Invalid_argument _ -> false (* is thrown by get_ikind_exp when the type of the expression is not an integer type *)
+  | exception Cilfacade.TypeOfError _ -> false
+  | ik ->
+    if IntDomain.should_wrap ik then
+      false
+    else if IntDomain.should_ignore_overflow ik then
+      true
+    else
+      not (ask.f (MaySignedOverflow exp))
 
 module type ConvertArg =
 sig
@@ -210,12 +224,12 @@ struct
       texpr1_expr_of_cil_exp exp
     in
     let exp = Cil.constFold false exp in
-    if M.tracing then 
+    if M.tracing then
       match conv exp with
-      | exception Unsupported_CilExp ex -> 
+      | exception Unsupported_CilExp ex ->
         M.tracel "rel-texpr-cil-conv" "unsuccessfull: %s" (show_unsupported_cilExp ex);
         raise (Unsupported_CilExp ex)
-      | res -> 
+      | res ->
         M.trace "relation" "texpr1_expr_of_cil_exp: %a -> %a (%b)" d_plainexp exp Texpr1.Expr.pretty res (Lazy.force no_ov);
         M.tracel "rel-texpr-cil-conv" "successfull: Good";
         res
@@ -269,50 +283,99 @@ struct
 
   let longlong = TInt(ILongLong,[])
 
+  let check_for_overflows_no_further_cast (ask: Queries.ask) (e_inv: exp -> exp) cast_exp exp_plain =
+    if not (ask.f (MayOverflow (e_inv cast_exp))) then
+      cast_exp, exp_plain
+    else (
+      M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil var in overflow preserving manner: %a" CilType.Exp.pretty cast_exp;
+      raise Unsupported_Linexpr1
+    )
+
+  let is_cast_injective_vtype vinfo = IntDomain.Size.is_cast_injective ~from_type:vinfo.vtype ~to_type:longlong
+
+  let rec check_for_overflows (ask: Queries.ask) (e_inv: exp -> exp) exp exp_plain =
+    if not (ask.f (MayOverflow (e_inv exp))) then
+      exp, exp_plain
+    else
+      match exp, exp_plain with
+      | Lval (Var vinfo, NoOffset) as var, _ when is_cast_injective_vtype vinfo ->
+        let cast_var = Cilfacade.mkCast ~e:var ~newt:longlong in
+        check_for_overflows_no_further_cast ask e_inv cast_var cast_var
+      | BinOp (op, (Const i as c), ((Lval (Var vinfo, NoOffset)) as var), _), _ when is_cast_injective_vtype vinfo ->
+        let cast_var = Cilfacade.mkCast ~e:var ~newt:longlong in
+        let cast_exp_plain = BinOp (op, c, cast_var, longlong) in
+        let cast_exp = Cilfacade.makeBinOp op c cast_var in
+        check_for_overflows_no_further_cast ask e_inv cast_exp cast_exp_plain
+      | BinOp (op, ((Lval (Var vinfo1, NoOffset)) as var1), ((Lval (Var vinfo2, NoOffset)) as var2), _), BinOp (_, _, var2_plain, _) when is_cast_injective_vtype vinfo1 && is_cast_injective_vtype vinfo2 ->
+        let cast_var = Cilfacade.mkCast ~e:var1 ~newt:longlong in
+        let cast_exp_plain = BinOp (op, cast_var, var2_plain, longlong) in
+        let cast_exp = Cilfacade.makeBinOp op cast_var var2 in
+        check_for_overflows_no_further_cast ask e_inv cast_exp cast_exp_plain
+      | BinOp (op, exp1, exp2, _), BinOp (_, _, exp2_plain, _) ->
+        let cast_exp1 = Cilfacade.mkCast ~e:exp1 ~newt:longlong in
+        let cast_exp_plain = BinOp (op, cast_exp1, exp2_plain, longlong) in
+        let cast_exp = Cilfacade.makeBinOp op cast_exp1 exp2 in
+        check_for_overflows_no_further_cast ask e_inv cast_exp cast_exp_plain
+      | _ ->
+        M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil expression in overflow preserving manner: %a" CilType.Exp.pretty exp;
+        raise Unsupported_Linexpr1
+
+  (* Determines the integer kind (ikind) for a given constant.
+     - Defaults to IInt for values that fit int range to minimize the number of LL suffixes in invariants.
+     - Uses ILongLong to handle larger constants and prevent integer overflows.
+     - If the constant cannot fit into ILongLong, it is discarded with a warning. *)
+  let const_ikind i =
+    match () with
+    | _ when Cil.fitsInInt IInt i -> IInt
+    | _ when Cil.fitsInInt ILongLong i -> ILongLong
+    | _ ->
+      M.warn ~category:Analyzer "Invariant Apron: coefficient does not fit long long type: %s" (Z.to_string i);
+      raise Unsupported_Linexpr1
 
   (** Returned boolean indicates whether returned expression should be negated. *)
   let coeff_to_const ~scalewith (c:Coeff.union_5) =
     match c with
     | Scalar c ->
       (match int_of_scalar ?scalewith c with
-       | Some i ->
-         let ci,truncation = truncateCilint ILongLong i in
-         if truncation = NoTruncation then
-           if Z.compare i Z.zero >= 0 then
-             false, Const (CInt(i,ILongLong,None))
-           else
-             (* attempt to negate if that does not cause an overflow *)
-             let cneg, truncation = truncateCilint ILongLong (Z.neg i) in
-             if truncation = NoTruncation then
-               true, Const (CInt((Z.neg i),ILongLong,None))
-             else
-               false, Const (CInt(i,ILongLong,None))
-         else
-           (M.warn ~category:Analyzer "Invariant Apron: coefficient is not int: %a" Scalar.pretty c; raise Unsupported_Linexpr1)
-       | None -> raise Unsupported_Linexpr1)
+      | Some i ->
+        let ikind = const_ikind i in
+        let ci,truncation = truncateCilint ikind i in
+        if truncation = NoTruncation then
+          if Z.compare i Z.zero >= 0 then
+            false, Const (CInt(i,ikind,None))
+          else
+            (* attempt to negate if that does not cause an overflow *)
+            let cneg, truncation = truncateCilint ikind (Z.neg i) in
+            if truncation = NoTruncation then
+              true, Const (CInt((Z.neg i),ikind,None))
+            else
+              false, Const (CInt(i,ikind,None))
+        else
+          (M.warn ~category:Analyzer "Invariant Apron: coefficient is not int: %a" Scalar.pretty c; raise Unsupported_Linexpr1)
+      | None -> raise Unsupported_Linexpr1)
     | _ -> raise Unsupported_Linexpr1
 
   (** Returned boolean indicates whether returned expression should be negated. *)
-  let cil_exp_of_linexpr1_term ~scalewith (c: Coeff.t) v =
+  let cil_exp_of_linexpr1_term ~scalewith (ask: Queries.ask) (e_inv: exp -> exp) (c: Coeff.t) v =
     match V.to_cil_varinfo v with
-    | Some vinfo when IntDomain.Size.is_cast_injective ~from_type:vinfo.vtype ~to_type:(TInt(ILongLong,[]))   ->
-      let var = Cilfacade.mkCast ~e:(Lval(Var vinfo,NoOffset)) ~newt:longlong in
+    | Some vinfo ->
+      let var = Lval (Var vinfo, NoOffset) in
       let flip, coeff = coeff_to_const ~scalewith c in
-      let prod = BinOp(Mult, coeff, var, longlong) in
-      flip, prod
+      let exp = Cilfacade.makeBinOp Mult coeff var in
+      let exp_plain = BinOp (Mult, coeff, var, Cilfacade.typeOf exp) in
+      let prod, prod_plain = check_for_overflows ask e_inv exp exp_plain in
+      flip, (prod, prod_plain)
     | None ->
       M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil var: %a" Var.pretty v;
       raise Unsupported_Linexpr1
-    | _ ->
-      M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil var in overflow preserving manner: %a" Var.pretty v;
-      raise Unsupported_Linexpr1
 
   (** Returned booleans indicates whether returned expressions should be negated. *)
-  let cil_exp_of_linexpr1 ?scalewith (linexpr1:Linexpr1.t) =
-    let terms = ref [coeff_to_const ~scalewith (Linexpr1.get_cst linexpr1)] in
+  let cil_exp_of_linexpr1 ?scalewith (ask: Queries.ask) (e_inv: exp -> exp) (linexpr1:Linexpr1.t) =
+    let flip, coeff = coeff_to_const ~scalewith (Linexpr1.get_cst linexpr1) in
+    let terms = ref [flip, (coeff, coeff)] in
     let append_summand (c:Coeff.union_5) v =
       if not (Coeff.is_zero c) then
-        terms := cil_exp_of_linexpr1_term ~scalewith c v :: !terms
+        terms := cil_exp_of_linexpr1_term ~scalewith (ask: Queries.ask) e_inv c v :: !terms
     in
     Linexpr1.iter append_summand linexpr1;
     !terms
@@ -344,19 +407,23 @@ struct
       Linexpr1.iter lcm_coeff linexpr1; !lcm_denom
     with UnsupportedScalar -> Z.one
 
-  let cil_exp_of_lincons1 (lincons1:Lincons1.t) =
-    let zero = Cil.kinteger ILongLong 0 in
+  let cil_exp_of_lincons1 (ask: Queries.ask) (e_inv: exp -> exp) (lincons1:Lincons1.t)  =
+    let zero = Cil.kinteger IInt 0 in
     try
       let linexpr1 = Lincons1.get_linexpr1 lincons1 in
       let common_denominator = lcm_den linexpr1 in
-      let terms = cil_exp_of_linexpr1 ~scalewith:common_denominator linexpr1 in
+      let terms = cil_exp_of_linexpr1 ~scalewith:common_denominator (ask: Queries.ask) e_inv linexpr1 in
       let (nterms, pterms) = BatTuple.Tuple2.mapn (List.map snd) (List.partition fst terms) in (* partition terms into negative (nterms) and positive (pterms) *)
       let fold_terms terms =
-        List.fold_left (fun acc term ->
+        List.fold_left (fun acc (term, term_plain) ->
             match acc with
-            | None -> Some term
-            | Some exp -> Some (BinOp (PlusA, exp, term, longlong))
+            | None -> Some (check_for_overflows ask e_inv term term_plain)
+            | Some (exp, exp_plain) ->
+              let exp' = Cilfacade.makeBinOp PlusA exp term in
+              let exp_plain' = BinOp (PlusA, exp_plain, term_plain, Cilfacade.typeOf exp') in
+              Some (check_for_overflows ask e_inv exp' exp_plain')
           ) None terms
+        |> Option.map snd
         |> BatOption.default zero
       in
       let lhs = fold_terms pterms in
@@ -461,7 +528,7 @@ struct
   let add_vars t vars = Vector.timing_wrap "add_vars" (add_vars t) vars
 
   let remove_vars t vars =
-    let t = copy t in 
+    let t = copy t in
     let env' = Environment.remove_vars t.env vars in
     dimchange2_remove t env'
 
diff --git a/src/domains/queries.ml b/src/domains/queries.ml
index 31e93dd0b2..55d6fff1ca 100644
--- a/src/domains/queries.ml
+++ b/src/domains/queries.ml
@@ -142,6 +142,7 @@ type _ t =
   | IsEverMultiThreaded: MayBool.t t
   | TmpSpecial: Mval.Exp.t -> ML.t t
   | MaySignedOverflow: exp -> MayBool.t t
+  | MayOverflow: exp -> MayBool.t t
   | GasExhausted: CilType.Fundec.t ->  MustBool.t t
   | YamlEntryGlobal: Obj.t * YamlWitnessType.Task.t -> YS.t t (** YAML witness entries for a global unknown ([Obj.t] represents [Spec.V.t]) and YAML witness task. *)
   | GhostVarAvailable: WitnessGhostVar.t -> MayBool.t t
@@ -217,6 +218,7 @@ struct
     | IsEverMultiThreaded -> (module MayBool)
     | TmpSpecial _ -> (module ML)
     | MaySignedOverflow  _ -> (module MayBool)
+    | MayOverflow  _ -> (module MayBool)
     | GasExhausted _ -> (module MustBool)
     | YamlEntryGlobal _ -> (module YS)
     | GhostVarAvailable _ -> (module MayBool)
@@ -291,6 +293,7 @@ struct
     | IsEverMultiThreaded -> MayBool.top ()
     | TmpSpecial _ -> ML.top ()
     | MaySignedOverflow _ -> MayBool.top ()
+    | MayOverflow _ -> MayBool.top ()
     | GasExhausted _ -> MustBool.top ()
     | YamlEntryGlobal _ -> YS.top ()
     | GhostVarAvailable _ -> MayBool.top ()
@@ -361,11 +364,12 @@ struct
     | Any (TmpSpecial _) -> 56
     | Any (IsAllocVar _) -> 57
     | Any (MaySignedOverflow _) -> 58
-    | Any (GasExhausted _) -> 59
-    | Any (YamlEntryGlobal _) -> 60
-    | Any (MustProtectingLocks _) -> 61
-    | Any (GhostVarAvailable _) -> 62
-    | Any InvariantGlobalNodes -> 63
+    | Any (MayOverflow _) -> 59
+    | Any (GasExhausted _) -> 60
+    | Any (YamlEntryGlobal _) -> 61
+    | Any (MustProtectingLocks _) -> 62
+    | Any (GhostVarAvailable _) -> 63
+    | Any InvariantGlobalNodes -> 64
 
   let rec compare a b =
     let r = Stdlib.compare (order a) (order b) in
@@ -423,6 +427,7 @@ struct
       | Any (MustBeSingleThreaded {since_start=s1;}),  Any (MustBeSingleThreaded {since_start=s2;}) -> Stdlib.compare s1 s2
       | Any (TmpSpecial lv1), Any (TmpSpecial lv2) -> Mval.Exp.compare lv1 lv2
       | Any (MaySignedOverflow e1), Any (MaySignedOverflow e2) -> CilType.Exp.compare e1 e2
+      | Any (MayOverflow e1), Any (MayOverflow e2) -> CilType.Exp.compare e1 e2
       | Any (GasExhausted f1), Any (GasExhausted f2) -> CilType.Fundec.compare f1 f2
       | Any (GhostVarAvailable v1), Any (GhostVarAvailable v2) -> WitnessGhostVar.compare v1 v2
       (* only argumentless queries should remain *)
@@ -470,6 +475,7 @@ struct
     | Any (MustBeSingleThreaded {since_start}) -> Hashtbl.hash since_start
     | Any (TmpSpecial lv) -> Mval.Exp.hash lv
     | Any (MaySignedOverflow e) -> CilType.Exp.hash e
+    | Any (MayOverflow e) -> CilType.Exp.hash e
     | Any (GasExhausted f) -> CilType.Fundec.hash f
     | Any (GhostVarAvailable v) -> WitnessGhostVar.hash v
     (* IterSysVars:                                                                    *)
@@ -537,6 +543,7 @@ struct
     | Any IsEverMultiThreaded -> Pretty.dprintf "IsEverMultiThreaded"
     | Any (TmpSpecial lv) -> Pretty.dprintf "TmpSpecial %a" Mval.Exp.pretty lv
     | Any (MaySignedOverflow e) -> Pretty.dprintf "MaySignedOverflow %a" CilType.Exp.pretty e
+    | Any (MayOverflow e) -> Pretty.dprintf "MayOverflow %a" CilType.Exp.pretty e
     | Any (GasExhausted f) -> Pretty.dprintf "GasExhausted %a" CilType.Fundec.pretty f
     | Any (GhostVarAvailable v) -> Pretty.dprintf "GhostVarAvailable %a" WitnessGhostVar.pretty v
     | Any InvariantGlobalNodes -> Pretty.dprintf "InvariantGlobalNodes"
diff --git a/tests/regression/36-apron/12-traces-min-rpb1.t b/tests/regression/36-apron/12-traces-min-rpb1.t
index 2c2d3266bc..fed6e0f0dc 100644
--- a/tests/regression/36-apron/12-traces-min-rpb1.t
+++ b/tests/regression/36-apron/12-traces-min-rpb1.t
@@ -33,7 +33,7 @@
           line: 14
           column: 3
           function: t_fun
-        value: (long long )h == (long long )g
+        value: h == g
         format: c_expression
     - invariant:
         type: location_invariant
@@ -42,7 +42,7 @@
           line: 19
           column: 3
           function: t_fun
-        value: (long long )h == (long long )g
+        value: h == g
         format: c_expression
     - invariant:
         type: location_invariant
@@ -51,7 +51,7 @@
           line: 29
           column: 3
           function: main
-        value: (long long )h == (long long )g
+        value: h == g
         format: c_expression
 
 
@@ -164,5 +164,5 @@
     content:
     - invariant:
         type: flow_insensitive_invariant
-        value: '! multithreaded || (A_locked || (long long )g == (long long )h)'
+        value: '! multithreaded || (A_locked || g == h)'
         format: c_expression
diff --git a/tests/regression/36-apron/52-queuesize.t b/tests/regression/36-apron/52-queuesize.t
index 2cc80fba5e..0856143f4a 100644
--- a/tests/regression/36-apron/52-queuesize.t
+++ b/tests/regression/36-apron/52-queuesize.t
@@ -57,7 +57,7 @@ Without diff-box:
           line: 15
           column: 3
           function: pop
-        value: (long long )capacity >= (long long )free
+        value: (long long )used + free == capacity
         format: c_expression
     - invariant:
         type: location_invariant
@@ -66,7 +66,7 @@ Without diff-box:
           line: 15
           column: 3
           function: pop
-        value: (long long )free >= 0LL
+        value: 2147483647 >= capacity
         format: c_expression
     - invariant:
         type: location_invariant
@@ -75,7 +75,7 @@ Without diff-box:
           line: 15
           column: 3
           function: pop
-        value: (long long )used + (long long )free == (long long )capacity
+        value: capacity >= free
         format: c_expression
     - invariant:
         type: location_invariant
@@ -84,7 +84,7 @@ Without diff-box:
           line: 15
           column: 3
           function: pop
-        value: 2147483647LL >= (long long )capacity
+        value: free >= 0
         format: c_expression
     - invariant:
         type: location_invariant
@@ -93,7 +93,7 @@ Without diff-box:
           line: 36
           column: 3
           function: push
-        value: (long long )capacity >= (long long )free
+        value: (long long )used + free == capacity
         format: c_expression
     - invariant:
         type: location_invariant
@@ -102,7 +102,7 @@ Without diff-box:
           line: 36
           column: 3
           function: push
-        value: (long long )free >= 0LL
+        value: 2147483647 >= capacity
         format: c_expression
     - invariant:
         type: location_invariant
@@ -111,7 +111,7 @@ Without diff-box:
           line: 36
           column: 3
           function: push
-        value: (long long )used + (long long )free == (long long )capacity
+        value: capacity >= free
         format: c_expression
     - invariant:
         type: location_invariant
@@ -120,7 +120,7 @@ Without diff-box:
           line: 36
           column: 3
           function: push
-        value: 2147483647LL >= (long long )capacity
+        value: free >= 0
         format: c_expression
 
 With diff-box:
@@ -180,7 +180,7 @@ With diff-box:
           line: 15
           column: 3
           function: pop
-        value: (long long )capacity >= (long long )free
+        value: (long long )used + free == capacity
         format: c_expression
     - invariant:
         type: location_invariant
@@ -189,7 +189,7 @@ With diff-box:
           line: 15
           column: 3
           function: pop
-        value: (long long )free >= 0LL
+        value: capacity >= free
         format: c_expression
     - invariant:
         type: location_invariant
@@ -198,7 +198,7 @@ With diff-box:
           line: 15
           column: 3
           function: pop
-        value: (long long )used + (long long )free == (long long )capacity
+        value: free >= 0
         format: c_expression
     - invariant:
         type: location_invariant
@@ -207,7 +207,7 @@ With diff-box:
           line: 36
           column: 3
           function: push
-        value: (long long )capacity >= (long long )free
+        value: (long long )used + free == capacity
         format: c_expression
     - invariant:
         type: location_invariant
@@ -216,7 +216,7 @@ With diff-box:
           line: 36
           column: 3
           function: push
-        value: (long long )free >= 0LL
+        value: capacity >= free
         format: c_expression
     - invariant:
         type: location_invariant
@@ -225,7 +225,7 @@ With diff-box:
           line: 36
           column: 3
           function: push
-        value: (long long )used + (long long )free == (long long )capacity
+        value: free >= 0
         format: c_expression
 
 Compare witnesses:
@@ -239,7 +239,7 @@ Compare witnesses:
         line: 36
         column: 3
         function: push
-      value: 2147483647LL >= (long long )capacity
+      value: 2147483647 >= capacity
       format: c_expression
   - invariant:
       type: location_invariant
@@ -248,6 +248,6 @@ Compare witnesses:
         line: 15
         column: 3
         function: pop
-      value: 2147483647LL >= (long long )capacity
+      value: 2147483647 >= capacity
       format: c_expression
   ---
diff --git a/tests/regression/46-apron2/98-issue-1511b.t b/tests/regression/46-apron2/98-issue-1511b.t
index 5b6b802506..7eeeb57bec 100644
--- a/tests/regression/46-apron2/98-issue-1511b.t
+++ b/tests/regression/46-apron2/98-issue-1511b.t
@@ -15,32 +15,32 @@
     unsupported: 0
     disabled: 0
     total validation entries: 26
-  [Success][Witness] invariant confirmed: ((long long )j + (long long )d) + 2147483648LL >= 0LL (98-issue-1511b.c:22:5)
-  [Success][Witness] invariant confirmed: ((long long )k + (long long )d) + 2147483647LL >= 0LL (98-issue-1511b.c:22:5)
-  [Success][Witness] invariant confirmed: ((long long )k + (long long )j) + 2147483646LL >= 0LL (98-issue-1511b.c:22:5)
-  [Success][Witness] invariant confirmed: (long long )d + 2147483648LL >= (long long )j (98-issue-1511b.c:22:5)
-  [Success][Witness] invariant confirmed: (long long )d + 2147483649LL >= (long long )k (98-issue-1511b.c:22:5)
-  [Success][Witness] invariant confirmed: (long long )j + 1LL >= (long long )k (98-issue-1511b.c:22:5)
-  [Success][Witness] invariant confirmed: (long long )j + 2147483647LL >= (long long )d (98-issue-1511b.c:22:5)
-  [Success][Witness] invariant confirmed: (long long )k + 2147483646LL >= (long long )d (98-issue-1511b.c:22:5)
-  [Success][Witness] invariant confirmed: (long long )k + 2147483646LL >= (long long )j (98-issue-1511b.c:22:5)
-  [Success][Witness] invariant confirmed: 1LL >= (long long )k + (long long )j (98-issue-1511b.c:22:5)
-  [Success][Witness] invariant confirmed: 2147483647LL >= (long long )j + (long long )d (98-issue-1511b.c:22:5)
-  [Success][Witness] invariant confirmed: 2147483648LL >= (long long )k + (long long )d (98-issue-1511b.c:22:5)
+  [Success][Witness] invariant confirmed: ((long long )k + d) + 2147483647 >= 0 (98-issue-1511b.c:22:5)
+  [Success][Witness] invariant confirmed: (j + d) + 2147483648LL >= 0 (98-issue-1511b.c:22:5)
+  [Success][Witness] invariant confirmed: (k + j) + 2147483646 >= 0 (98-issue-1511b.c:22:5)
+  [Success][Witness] invariant confirmed: 1 >= k + j (98-issue-1511b.c:22:5)
+  [Success][Witness] invariant confirmed: 2147483647 >= j + d (98-issue-1511b.c:22:5)
+  [Success][Witness] invariant confirmed: 2147483648LL >= (long long )k + d (98-issue-1511b.c:22:5)
+  [Success][Witness] invariant confirmed: d + 2147483648LL >= j (98-issue-1511b.c:22:5)
+  [Success][Witness] invariant confirmed: d + 2147483649LL >= k (98-issue-1511b.c:22:5)
+  [Success][Witness] invariant confirmed: j + 1 >= k (98-issue-1511b.c:22:5)
+  [Success][Witness] invariant confirmed: j + 2147483647 >= d (98-issue-1511b.c:22:5)
   [Success][Witness] invariant confirmed: j == 0 (98-issue-1511b.c:22:5)
-  [Success][Witness] invariant confirmed: ((long long )j + (long long )d) + 2147483648LL >= 0LL (98-issue-1511b.c:27:5)
-  [Success][Witness] invariant confirmed: ((long long )k + (long long )d) + 2147483647LL >= 0LL (98-issue-1511b.c:27:5)
-  [Success][Witness] invariant confirmed: ((long long )k + (long long )j) + 2147483646LL >= 0LL (98-issue-1511b.c:27:5)
-  [Success][Witness] invariant confirmed: (long long )d + 2147483648LL >= (long long )j (98-issue-1511b.c:27:5)
-  [Success][Witness] invariant confirmed: (long long )d + 2147483649LL >= (long long )k (98-issue-1511b.c:27:5)
-  [Success][Witness] invariant confirmed: (long long )j + 1LL >= (long long )k (98-issue-1511b.c:27:5)
-  [Success][Witness] invariant confirmed: (long long )j + 2147483647LL >= (long long )d (98-issue-1511b.c:27:5)
-  [Success][Witness] invariant confirmed: (long long )k + 2147483646LL >= (long long )d (98-issue-1511b.c:27:5)
-  [Success][Witness] invariant confirmed: (long long )k + 2147483646LL >= (long long )j (98-issue-1511b.c:27:5)
-  [Success][Witness] invariant confirmed: 1LL >= (long long )k + (long long )j (98-issue-1511b.c:27:5)
-  [Success][Witness] invariant confirmed: 2147483647LL >= (long long )j + (long long )d (98-issue-1511b.c:27:5)
-  [Success][Witness] invariant confirmed: 2147483648LL >= (long long )k + (long long )d (98-issue-1511b.c:27:5)
+  [Success][Witness] invariant confirmed: k + 2147483646 >= d (98-issue-1511b.c:22:5)
+  [Success][Witness] invariant confirmed: k + 2147483646 >= j (98-issue-1511b.c:22:5)
+  [Success][Witness] invariant confirmed: ((long long )k + d) + 2147483647 >= 0 (98-issue-1511b.c:27:5)
+  [Success][Witness] invariant confirmed: (j + d) + 2147483648LL >= 0 (98-issue-1511b.c:27:5)
+  [Success][Witness] invariant confirmed: (k + j) + 2147483646 >= 0 (98-issue-1511b.c:27:5)
+  [Success][Witness] invariant confirmed: 1 >= k + j (98-issue-1511b.c:27:5)
+  [Success][Witness] invariant confirmed: 2147483647 >= j + d (98-issue-1511b.c:27:5)
+  [Success][Witness] invariant confirmed: 2147483648LL >= (long long )k + d (98-issue-1511b.c:27:5)
+  [Success][Witness] invariant confirmed: d + 2147483648LL >= j (98-issue-1511b.c:27:5)
+  [Success][Witness] invariant confirmed: d + 2147483649LL >= k (98-issue-1511b.c:27:5)
+  [Success][Witness] invariant confirmed: j + 1 >= k (98-issue-1511b.c:27:5)
+  [Success][Witness] invariant confirmed: j + 2147483647 >= d (98-issue-1511b.c:27:5)
   [Success][Witness] invariant confirmed: j == 0 (98-issue-1511b.c:27:5)
+  [Success][Witness] invariant confirmed: k + 2147483646 >= d (98-issue-1511b.c:27:5)
+  [Success][Witness] invariant confirmed: k + 2147483646 >= j (98-issue-1511b.c:27:5)
 
 
 # Issue #1712
diff --git a/tests/regression/56-witness/74-safe-program-example-loop-invariants-1.c b/tests/regression/56-witness/74-safe-program-example-loop-invariants-1.c
new file mode 100644
index 0000000000..11424bc69b
--- /dev/null
+++ b/tests/regression/56-witness/74-safe-program-example-loop-invariants-1.c
@@ -0,0 +1,31 @@
+// This file is part of sv-witnesses repository: https://github.com/sosy-lab/sv-witnesses
+//
+// SPDX-FileCopyrightText: 2023 Dirk Beyer <https://www.sosy-lab.org>
+//
+// SPDX-License-Identifier: Apache-2.0
+// CRAM
+void reach_error(){}
+extern unsigned char __VERIFIER_nondet_uchar(void);
+int main() {
+  unsigned char n = __VERIFIER_nondet_uchar();
+  if (n == 0) {
+    return 0;
+  }
+  unsigned char v = 0;
+  unsigned int  s = 0;
+  unsigned int  i = 0;
+  while (i < n) {
+    v = __VERIFIER_nondet_uchar();
+    s += v;
+    ++i;
+  }
+  if (s < v) {
+    reach_error();
+    return 1;
+  }
+  if (s > 65025) {
+    reach_error();
+    return 1;
+  }
+  return 0;
+}
diff --git a/tests/regression/56-witness/74-safe-program-example-loop-invariants-1.t b/tests/regression/56-witness/74-safe-program-example-loop-invariants-1.t
new file mode 100644
index 0000000000..5b81bddbbf
--- /dev/null
+++ b/tests/regression/56-witness/74-safe-program-example-loop-invariants-1.t
@@ -0,0 +1,230 @@
+  $ goblint --set ana.activated[+] apron --enable witness.yaml.enabled --set witness.yaml.entry-types '["invariant_set"]' --set witness.yaml.invariant-types '["loop_invariant"]' --enable ana.sv-comp.functions 74-safe-program-example-loop-invariants-1.c
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 20
+    dead: 0
+    total lines: 20
+  [Info][Witness] witness generation summary:
+    location invariants: 0
+    loop invariants: 24
+    flow-insensitive invariants: 0
+    total generation entries: 1
+
+  $ yamlWitnessStrip < witness.yml
+  - entry_type: invariant_set
+    content:
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 74-safe-program-example-loop-invariants-1.c
+          line: 17
+          column: 3
+          function: main
+        value: (long long )s + 255 >= i
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 74-safe-program-example-loop-invariants-1.c
+          line: 17
+          column: 3
+          function: main
+        value: (long long )s + 255 >= n
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 74-safe-program-example-loop-invariants-1.c
+          line: 17
+          column: 3
+          function: main
+        value: (long long )s + 255 >= v
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 74-safe-program-example-loop-invariants-1.c
+          line: 17
+          column: 3
+          function: main
+        value: (long long )s + i >= 0
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 74-safe-program-example-loop-invariants-1.c
+          line: 17
+          column: 3
+          function: main
+        value: (long long )s + n >= 1
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 74-safe-program-example-loop-invariants-1.c
+          line: 17
+          column: 3
+          function: main
+        value: 4294967550LL >= (long long )((unsigned int )((int )v)) + s
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 74-safe-program-example-loop-invariants-1.c
+          line: 17
+          column: 3
+          function: main
+        value: 4294967550LL >= (long long )s + i
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 74-safe-program-example-loop-invariants-1.c
+          line: 17
+          column: 3
+          function: main
+        value: 4294967550LL >= (long long )s + n
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 74-safe-program-example-loop-invariants-1.c
+          line: 17
+          column: 3
+          function: main
+        value: 510 >= n + i
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 74-safe-program-example-loop-invariants-1.c
+          line: 17
+          column: 3
+          function: main
+        value: 510 >= v + i
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 74-safe-program-example-loop-invariants-1.c
+          line: 17
+          column: 3
+          function: main
+        value: 510 >= v + n
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 74-safe-program-example-loop-invariants-1.c
+          line: 17
+          column: 3
+          function: main
+        value: i + 254 >= v
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 74-safe-program-example-loop-invariants-1.c
+          line: 17
+          column: 3
+          function: main
+        value: i + 255 >= n
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 74-safe-program-example-loop-invariants-1.c
+          line: 17
+          column: 3
+          function: main
+        value: i + 4294967294LL >= s
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 74-safe-program-example-loop-invariants-1.c
+          line: 17
+          column: 3
+          function: main
+        value: n != (unsigned char)0
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 74-safe-program-example-loop-invariants-1.c
+          line: 17
+          column: 3
+          function: main
+        value: n + 254 >= v
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 74-safe-program-example-loop-invariants-1.c
+          line: 17
+          column: 3
+          function: main
+        value: n + 4294967294LL >= s
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 74-safe-program-example-loop-invariants-1.c
+          line: 17
+          column: 3
+          function: main
+        value: n + i >= 1
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 74-safe-program-example-loop-invariants-1.c
+          line: 17
+          column: 3
+          function: main
+        value: n >= i
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 74-safe-program-example-loop-invariants-1.c
+          line: 17
+          column: 3
+          function: main
+        value: v + 255 >= i
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 74-safe-program-example-loop-invariants-1.c
+          line: 17
+          column: 3
+          function: main
+        value: v + 255 >= n
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 74-safe-program-example-loop-invariants-1.c
+          line: 17
+          column: 3
+          function: main
+        value: v + 4294967295LL >= s
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 74-safe-program-example-loop-invariants-1.c
+          line: 17
+          column: 3
+          function: main
+        value: v + i >= 0
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 74-safe-program-example-loop-invariants-1.c
+          line: 17
+          column: 3
+          function: main
+        value: v + n >= 1
+        format: c_expression
diff --git a/tests/regression/56-witness/75-safe-program-example-loop-invariants-2.c b/tests/regression/56-witness/75-safe-program-example-loop-invariants-2.c
new file mode 100644
index 0000000000..82114b616b
--- /dev/null
+++ b/tests/regression/56-witness/75-safe-program-example-loop-invariants-2.c
@@ -0,0 +1,27 @@
+void reach_error(){}
+extern unsigned int __VERIFIER_nondet_uint();
+extern unsigned char __VERIFIER_nondet_uchar(void);
+// CRAM
+int main() {
+  unsigned int n = __VERIFIER_nondet_uint();
+  if (n == 0) {
+    return 0;
+  }
+  unsigned int v = 0;
+  unsigned int s = 0;
+  unsigned int i = 0;
+  while (i < n) {
+    v = __VERIFIER_nondet_uchar();
+    s += v;
+    ++i;
+  }
+  if (s < v) {
+    reach_error();
+    return 1;
+  }
+  if (s > 65025) {
+    reach_error();
+    return 1;
+  }
+  return 0;
+}
\ No newline at end of file
diff --git a/tests/regression/56-witness/75-safe-program-example-loop-invariants-2.t b/tests/regression/56-witness/75-safe-program-example-loop-invariants-2.t
new file mode 100644
index 0000000000..f69ead1538
--- /dev/null
+++ b/tests/regression/56-witness/75-safe-program-example-loop-invariants-2.t
@@ -0,0 +1,239 @@
+  $ goblint --set ana.activated[+] apron --enable witness.yaml.enabled --set witness.yaml.entry-types '["invariant_set"]' --set witness.yaml.invariant-types '["loop_invariant"]' --enable ana.sv-comp.functions 75-safe-program-example-loop-invariants-2.c
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 21
+    dead: 0
+    total lines: 21
+  [Info][Witness] witness generation summary:
+    location invariants: 0
+    loop invariants: 25
+    flow-insensitive invariants: 0
+    total generation entries: 1
+
+  $ yamlWitnessStrip < witness.yml
+  - entry_type: invariant_set
+    content:
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 75-safe-program-example-loop-invariants-2.c
+          line: 13
+          column: 3
+          function: main
+        value: (long long )i + 255 >= v
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 75-safe-program-example-loop-invariants-2.c
+          line: 13
+          column: 3
+          function: main
+        value: (long long )n + 254 >= v
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 75-safe-program-example-loop-invariants-2.c
+          line: 13
+          column: 3
+          function: main
+        value: (long long )n + i >= 1
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 75-safe-program-example-loop-invariants-2.c
+          line: 13
+          column: 3
+          function: main
+        value: (long long )s + 255 >= v
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 75-safe-program-example-loop-invariants-2.c
+          line: 13
+          column: 3
+          function: main
+        value: (long long )s + i >= 0
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 75-safe-program-example-loop-invariants-2.c
+          line: 13
+          column: 3
+          function: main
+        value: (long long )s + n >= 1
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 75-safe-program-example-loop-invariants-2.c
+          line: 13
+          column: 3
+          function: main
+        value: (long long )v + i >= 0
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 75-safe-program-example-loop-invariants-2.c
+          line: 13
+          column: 3
+          function: main
+        value: (long long )v + n >= 1
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 75-safe-program-example-loop-invariants-2.c
+          line: 13
+          column: 3
+          function: main
+        value: 4294967550LL >= (long long )v + i
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 75-safe-program-example-loop-invariants-2.c
+          line: 13
+          column: 3
+          function: main
+        value: 4294967550LL >= (long long )v + n
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 75-safe-program-example-loop-invariants-2.c
+          line: 13
+          column: 3
+          function: main
+        value: 4294967550LL >= (long long )v + s
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 75-safe-program-example-loop-invariants-2.c
+          line: 13
+          column: 3
+          function: main
+        value: 8589934590LL >= (long long )n + i
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 75-safe-program-example-loop-invariants-2.c
+          line: 13
+          column: 3
+          function: main
+        value: 8589934590LL >= (long long )s + i
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 75-safe-program-example-loop-invariants-2.c
+          line: 13
+          column: 3
+          function: main
+        value: 8589934590LL >= (long long )s + n
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 75-safe-program-example-loop-invariants-2.c
+          line: 13
+          column: 3
+          function: main
+        value: i + 4294967294LL >= s
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 75-safe-program-example-loop-invariants-2.c
+          line: 13
+          column: 3
+          function: main
+        value: i + 4294967295LL >= n
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 75-safe-program-example-loop-invariants-2.c
+          line: 13
+          column: 3
+          function: main
+        value: n != 0U
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 75-safe-program-example-loop-invariants-2.c
+          line: 13
+          column: 3
+          function: main
+        value: n + 4294967294LL >= s
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 75-safe-program-example-loop-invariants-2.c
+          line: 13
+          column: 3
+          function: main
+        value: n >= i
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 75-safe-program-example-loop-invariants-2.c
+          line: 13
+          column: 3
+          function: main
+        value: s + 4294967295LL >= i
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 75-safe-program-example-loop-invariants-2.c
+          line: 13
+          column: 3
+          function: main
+        value: s + 4294967295LL >= n
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 75-safe-program-example-loop-invariants-2.c
+          line: 13
+          column: 3
+          function: main
+        value: v + 4294967295LL >= i
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 75-safe-program-example-loop-invariants-2.c
+          line: 13
+          column: 3
+          function: main
+        value: v + 4294967295LL >= n
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 75-safe-program-example-loop-invariants-2.c
+          line: 13
+          column: 3
+          function: main
+        value: v + 4294967295LL >= s
+        format: c_expression
+    - invariant:
+        type: loop_invariant
+        location:
+          file_name: 75-safe-program-example-loop-invariants-2.c
+          line: 13
+          column: 3
+          function: main
+        value: v <= 255U
+        format: c_expression