diff --git a/goblint.opam b/goblint.opam
index a48112395b..e7428cf930 100644
--- a/goblint.opam
+++ b/goblint.opam
@@ -58,7 +58,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
 # also remember to generate/adjust goblint.opam.locked!
 pin-depends: [
-  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#83835348d20b3f51f1e8e505480b773c9fa5f96b" ]
+  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#64f3010e56563cf78ab3f4535b8614ef8f4e3abf" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
   # quoter workaround reverted for release, so no pin needed
diff --git a/goblint.opam.locked b/goblint.opam.locked
index 65bc433404..45f3c14c0b 100644
--- a/goblint.opam.locked
+++ b/goblint.opam.locked
@@ -94,7 +94,7 @@ version: "dev"
 pin-depends: [
   [
     "goblint-cil.1.8.2"
-    "git+https://github.com/goblint/cil.git#83835348d20b3f51f1e8e505480b773c9fa5f96b"
+    "git+https://github.com/goblint/cil.git#64f3010e56563cf78ab3f4535b8614ef8f4e3abf"
   ]
   [
     "apron.v0.9.13"
diff --git a/goblint.opam.template b/goblint.opam.template
index 78646816ed..6b4f796f0c 100644
--- a/goblint.opam.template
+++ b/goblint.opam.template
@@ -1,7 +1,7 @@
 # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
 # also remember to generate/adjust goblint.opam.locked!
 pin-depends: [
-  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#83835348d20b3f51f1e8e505480b773c9fa5f96b" ]
+  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#64f3010e56563cf78ab3f4535b8614ef8f4e3abf" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
   # quoter workaround reverted for release, so no pin needed
diff --git a/src/analyses/arinc.ml b/src/analyses/arinc.ml
index e714ca86a3..bce44ccc50 100644
--- a/src/analyses/arinc.ml
+++ b/src/analyses/arinc.ml
@@ -136,7 +136,7 @@ struct
   let is_return_code_type exp = Cilfacade.typeOf exp |> unrollTypeDeep |> function
     | TEnum(ei, _) when ei.ename = "T13" -> true
     | _ -> false
-  let return_code_is_success = function 0L | 1L -> true | _ -> false
+  let return_code_is_success z = Cilint.is_zero_cilint z || Cilint.compare_cilint z Cilint.one_cilint = 0
   let str_return_code i = if return_code_is_success i then "SUCCESS" else "ERROR"
   let str_return_dlval (v,o as dlval) =
     sprint d_lval (Lval.CilLval.to_lval dlval) ^ "_" ^ string_of_int v.vdecl.line |>
@@ -195,7 +195,7 @@ struct
               let add_one str_rhs = add_edges env @@ ArincUtil.Assign (str_return_dlval dlval, str_rhs) in
               let add_top () = add_edges ~r:(str_return_dlval dlval) env @@ ArincUtil.Nop in
               match stripCasts rval with
-              | Const CInt64(i,_,_) -> add_one @@ str_return_code i
+              | Const CInt(i,_,_) -> add_one @@ str_return_code i
               (*       | Lval rlval ->
                         iterMayPointTo ctx (AddrOf rlval) (fun rdlval -> add_return_dlval env `Read rdlval; add_one @@ str_return_dlval rdlval) *)
               | _ -> add_top ()
@@ -212,8 +212,8 @@ struct
         let check a b tv =
           (* we are interested in a comparison between some lval lval (which has the type of the return code enum) and a value of that enum (which gets converted to an Int by CIL) *)
           match a, b with
-          | Lval lval, Const CInt64(i,_,_)
-          | Const CInt64(i,_,_), Lval lval when is_return_code_type (Lval lval) ->
+          | Lval lval, Const CInt(i,_,_)
+          | Const CInt(i,_,_), Lval lval when is_return_code_type (Lval lval) ->
             (* let success = return_code_is_success i = tv in (* both must be true or false *) *)
             (* ignore(printf "if %s: %a = %B (line %i)\n" (if success then "success" else "error") d_plainexp exp tv (!Tracing.current_loc).line); *)
             (match env.node with
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 5b3db1b43d..b8edd2990b 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -486,12 +486,10 @@ struct
 
   let convertToQueryLval x =
     let rec offsNormal o =
+      let ik = Cilfacade.ptrdiff_ikind () in
       let toInt i =
-        match IdxDom.to_int i with
-        | Some x ->
-          (* TODO: Handle values outside of int64 *)
-          let x = BI.to_int64 x in
-          Const (CInt64 (x,IInt, None))
+        match IdxDom.to_int @@ ID.cast_to ik i with
+        | Some x -> Const (CInt (x,ik, None))
         | _ -> mkCast (Const (CStr "unknown")) intType
 
       in
@@ -667,10 +665,10 @@ struct
       (* query functions were no help ... now try with values*)
       match (if get_bool "exp.lower-constants" then constFold true exp else exp) with
       (* Integer literals *)
-      (* seems like constFold already converts CChr to CInt64 *)
+      (* seems like constFold already converts CChr to CInt *)
       | Const (CChr x) -> eval_rv a gs st (Const (charConstToInt x)) (* char becomes int, see Cil doc/ISO C 6.4.4.4.10 *)
-      | Const (CInt64 (num,ikind,str)) ->
-        (match str with Some x -> M.tracel "casto" "CInt64 (%s, %a, %s)\n" (Int64.to_string num) d_ikind ikind x | None -> ());
+      | Const (CInt (num,ikind,str)) ->
+        (match str with Some x -> M.tracel "casto" "CInt (%s, %a, %s)\n" (Cilint.string_of_cilint num) d_ikind ikind x | None -> ());
         `Int (ID.cast_to ikind (IntDomain.of_const (num,ikind,str)))
       (* String literals *)
       | Const (CStr x) -> `Address (AD.from_string x) (* normal 8-bit strings, type: char* *)
@@ -700,8 +698,8 @@ struct
           let cast_ok = function
             | Addr a ->
               begin
-                match Cil.isInteger (sizeOf t), Cil.isInteger (sizeOf (get_type_addr a)) with
-                | Some i1, Some i2 -> Int64.compare i1 i2 <= 0
+                match Cil.getInteger (sizeOf t), Cil.getInteger (sizeOf (get_type_addr a)) with
+                | Some i1, Some i2 -> Cilint.compare_cilint i1 i2 <= 0
                 | _ ->
                   if contains_vla t || contains_vla (get_type_addr a) then
                     begin
@@ -1665,7 +1663,7 @@ struct
     let lval_t = Cilfacade.typeOf rval in
     let char_array_hack () =
       let rec split_offset = function
-        | Index(Const(CInt64(i, _, _)), NoOffset) -> (* ...[i] *)
+        | Index(Const(CInt(i, _, _)), NoOffset) -> (* ...[i] *)
           Index(zero, NoOffset), Some i (* all i point to StartOf(string) *)
         | NoOffset -> NoOffset, None
         | Index(exp, offs) ->
@@ -1682,7 +1680,7 @@ struct
       in
       match last_index lval, stripCasts rval with
       | Some (lv, i), Const(CChr c) when c<>'\000' -> (* "abc" <> "abc\000" in OCaml! *)
-        let i = i64_to_int i in
+        let i = Cilint.int_of_cilint i in
         (* ignore @@ printf "%a[%i] = %c\n" d_lval lv i c; *)
         let s = try Hashtbl.find char_array lv with Not_found -> Bytes.empty in (* current string for lv or empty string *)
         if i >= Bytes.length s then ((* optimized b/c Out_of_memory *)
diff --git a/src/analyses/deadlock.ml b/src/analyses/deadlock.ml
index c7d3710b29..bf25172587 100644
--- a/src/analyses/deadlock.ml
+++ b/src/analyses/deadlock.ml
@@ -79,7 +79,7 @@ struct
   let rec conv_offset x =
     match x with
     | `NoOffset    -> `NoOffset
-    | `Index (Const (CInt64 (i,ikind,s)),o) -> `Index (IntDomain.of_const (i,ikind,s), conv_offset o)
+    | `Index (Const (CInt (i,ikind,s)),o) -> `Index (IntDomain.of_const (i,ikind,s), conv_offset o)
     | `Index (_,o) -> `Index (ValueDomain.IndexDomain.top (), conv_offset o)
     | `Field (f,o) -> `Field (f, conv_offset o)
 
diff --git a/src/analyses/expRelation.ml b/src/analyses/expRelation.ml
index 87dd0c85d4..04995d3143 100644
--- a/src/analyses/expRelation.ml
+++ b/src/analyses/expRelation.ml
@@ -4,6 +4,7 @@
 
 open Prelude.Ana
 open Analyses
+open Cilint
 
 module Spec : Analyses.MCPSpec =
 struct
@@ -58,14 +59,15 @@ struct
       Basetype.CilExp.equal (canonize e1) (canonize e2)
     | Queries.MayBeLess (e1, e2) when not (isFloat e1) ->
       begin
+        (* Compare the cilint first in the hope that it is cheaper than the LVal comparison *)
         match e1, e2 with
-        | BinOp(PlusA, Lval l1, Const(CInt64(i,_,_)), _), Lval l2 when (lvalsEq l1 l2 && Int64.compare i Int64.zero > 0) ->
+        | BinOp(PlusA, Lval l1, Const(CInt(i,_,_)), _), Lval l2 when (compare_cilint i zero_cilint > 0 && lvalsEq l1 l2) ->
             false  (* c > 0 => (! x+c < x) *)
-        | Lval l1, BinOp(PlusA, Lval l2, Const(CInt64(i,_,_)), _) when (lvalsEq l1 l2 && Int64.compare i Int64.zero < 0) ->
+        | Lval l1, BinOp(PlusA, Lval l2, Const(CInt(i,_,_)), _) when (compare_cilint i zero_cilint < 0 && lvalsEq l1 l2) ->
             false  (* c < 0 => (! x < x+c )*)
-        | BinOp(MinusA, Lval l1, Const(CInt64(i,_,_)), _), Lval l2 when (lvalsEq l1 l2 && Int64.compare i Int64.zero < 0) ->
+        | BinOp(MinusA, Lval l1, Const(CInt(i,_,_)), _), Lval l2 when (compare_cilint i zero_cilint < 0 && lvalsEq l1 l2) ->
             false  (* c < 0 => (! x-c < x) *)
-        | Lval l1, BinOp(MinusA, Lval l2, Const(CInt64(i,_,_)), _) when (lvalsEq l1 l2 && Int64.compare i Int64.zero > 0) ->
+        | Lval l1, BinOp(MinusA, Lval l2, Const(CInt(i,_,_)), _) when (compare_cilint i zero_cilint > 0 && lvalsEq l1 l2) ->
             false  (* c < 0 => (! x < x-c) *)
         | _ ->
             true
@@ -73,10 +75,10 @@ struct
     | Queries.MayBeEqual (e1,e2) when not (isFloat e1) ->
       begin
         match e1,e2 with
-        | BinOp(PlusA, Lval l1, Const(CInt64(i,_,_)), _), Lval l2
-        | Lval l2, BinOp(PlusA, Lval l1, Const(CInt64(i,_,_)), _)
-        | BinOp(MinusA, Lval l1, Const(CInt64(i,_,_)), _), Lval l2
-        | Lval l2, BinOp(MinusA, Lval l1, Const(CInt64(i,_,_)), _) when (lvalsEq l1 l2) && Int64.compare i Int64.zero <> 0  ->
+        | BinOp(PlusA, Lval l1, Const(CInt(i,_,_)), _), Lval l2
+        | Lval l2, BinOp(PlusA, Lval l1, Const(CInt(i,_,_)), _)
+        | BinOp(MinusA, Lval l1, Const(CInt(i,_,_)), _), Lval l2
+        | Lval l2, BinOp(MinusA, Lval l1, Const(CInt(i,_,_)), _) when compare_cilint i zero_cilint <> 0 && (lvalsEq l1 l2) ->
             false
         | _ -> true
       end
diff --git a/src/analyses/fileUse.ml b/src/analyses/fileUse.ml
index 4ccd478e2a..c49e4211d0 100644
--- a/src/analyses/fileUse.ml
+++ b/src/analyses/fileUse.ml
@@ -89,11 +89,11 @@ struct
     let check a b tv =
       (* ignore(printf "check: %a = %a, %B\n" d_plainexp a d_plainexp b tv); *)
       match a, b with
-      | Const (CInt64(i, kind, str)), Lval lval
-      | Lval lval, Const (CInt64(i, kind, str)) ->
+      | Const (CInt(i, kind, str)), Lval lval
+      | Lval lval, Const (CInt(i, kind, str)) ->
         (* ignore(printf "branch(%s==%i, %B)\n" v.vname (Int64.to_int i) tv); *)
         let k = D.key_from_lval lval in
-        if i = Int64.zero && tv then (
+        if Cilint.compare_cilint i Cilint.zero_cilint = 0 && tv then (
           (* ignore(printf "error-branch\n"); *)
           D.error k m
         )else
diff --git a/src/analyses/flag.ml b/src/analyses/flag.ml
index a57f77ee70..5900499c62 100644
--- a/src/analyses/flag.ml
+++ b/src/analyses/flag.ml
@@ -55,14 +55,14 @@ struct
           let x = var.vname in if List.mem x !noflags then () else
             (* let _ = print_endline ( List.fold_left (fun acc a -> a ^ ", " ^ acc) "" !flags   ) in  *)
             (match rval with
-             | Const (CInt64 (i,_,_)) -> if List.mem x !flags then
+             | Const (CInt(i,_,_)) -> if List.mem x !flags then
                  let v = Hashtbl.find vars x in
                  (* let _ = print_endline ( "assign" ^ (Int64.to_string i)) in   *)
                  (* let _ = print_endline ( x ^ " has values " ^ VSet.fold (fun e str -> (Val.short 50 e) ^", " ^str  ) v " ") in       *)
-                 if (VSet.mem (Val.of_int i) v) then () else
+                 if (VSet.mem (Val.of_int (Cilint.int64_of_cilint i)) v) then () else (* dubious, but was already like this *)
                  if (VSet.cardinal v < flagmax) then
                    (* let _ = print_endline ( "add") in   *)
-                   Hashtbl.replace vars x (VSet.add (Val.of_int i) v)
+                   Hashtbl.replace vars x (VSet.add (Val.of_int (Cilint.int64_of_cilint i)) v) (* dubious, but was already like this *)
                  else begin
                    (* let _ = print_endline ( "remove") in   *)
                    flags := listrem x !flags;
@@ -72,7 +72,7 @@ struct
                  end
                else begin
                  flags := x ::!flags;
-                 Hashtbl.add vars x (VSet.add (Val.of_int i) (VSet.empty ()) )
+                 Hashtbl.add vars x (VSet.add (Val.of_int (Cilint.int64_of_cilint i)) (VSet.empty ())) (* dubious, but was already like this *)
                end
              | _ ->
                noflags := x::!noflags; if List.mem x !flags then begin
diff --git a/src/analyses/malloc_null.ml b/src/analyses/malloc_null.ml
index 245cf5bad8..19534f8c9a 100644
--- a/src/analyses/malloc_null.ml
+++ b/src/analyses/malloc_null.ml
@@ -24,7 +24,7 @@ struct
   let rec conv_offset x =
     match x with
     | `NoOffset    -> `NoOffset
-    | `Index (Const (CInt64 (i,ik,s)),o) -> `Index (IntDomain.of_const (i,ik,s), conv_offset o)
+    | `Index (Const (CInt (i,ik,s)),o) -> `Index (IntDomain.of_const (i,ik,s), conv_offset o)
     | `Index (_,o) -> `Index (IdxDom.top (), conv_offset o)
     | `Field (f,o) -> `Field (f, conv_offset o)
 
diff --git a/src/analyses/mayLocks.ml b/src/analyses/mayLocks.ml
index cf33e696be..a175dfb92b 100644
--- a/src/analyses/mayLocks.ml
+++ b/src/analyses/mayLocks.ml
@@ -24,7 +24,7 @@ struct
   let rec conv_offset x =
     match x with
     | `NoOffset    -> `NoOffset
-    | `Index (Const (CInt64 (i,ikind,s)),o) -> `Index (IntDomain.of_const (i,ikind,s), conv_offset o)
+    | `Index (Const (CInt (i,ikind,s)),o) -> `Index (IntDomain.of_const (i,ikind,s), conv_offset o)
     | `Index (_,o) -> `Index (ValueDomain.IndexDomain.top (), conv_offset o)
     | `Field (f,o) -> `Field (f, conv_offset o)
 
diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml
index b081e0dfa0..baee950388 100644
--- a/src/analyses/mutexAnalysis.ml
+++ b/src/analyses/mutexAnalysis.ml
@@ -50,7 +50,7 @@ struct
   let rec conv_offset x =
     match x with
     | `NoOffset    -> `NoOffset
-    | `Index (Const (CInt64 (i,_,s)),o) -> `Index (IntDomain.of_const (i,Cilfacade.ptrdiff_ikind (),s), conv_offset o)
+    | `Index (Const (CInt (i,_,s)),o) -> `Index (IntDomain.of_const (i,Cilfacade.ptrdiff_ikind (),s), conv_offset o)
     | `Index (_,o) -> `Index (ValueDomain.IndexDomain.top (), conv_offset o)
     | `Field (f,o) -> `Field (f, conv_offset o)
 
@@ -63,7 +63,7 @@ struct
   let rec conv_const_offset x =
     match x with
     | NoOffset    -> `NoOffset
-    | Index (Const (CInt64 (i,_,s)),o) -> `Index (IntDomain.of_const (i,Cilfacade.ptrdiff_ikind (),s), conv_const_offset o)
+    | Index (Const (CInt (i,_,s)),o) -> `Index (IntDomain.of_const (i,Cilfacade.ptrdiff_ikind (),s), conv_const_offset o)
     | Index (_,o) -> `Index (ValueDomain.IndexDomain.top (), conv_const_offset o)
     | Field (f,o) -> `Field (f, conv_const_offset o)
 
diff --git a/src/analyses/octagon.ml b/src/analyses/octagon.ml
index f47af24c8f..226b9f4d21 100644
--- a/src/analyses/octagon.ml
+++ b/src/analyses/octagon.ml
@@ -36,11 +36,11 @@ struct
 
   let evaluate_sums oct exp =
     let match_exp = function
-      | BinOp(Mult, Lval(Var(var), _), Const(CInt64 (c, _, _)), _)
-      | BinOp(Mult, Const(CInt64 (c, _, _)), Lval(Var(var), NoOffset), _) ->
+      | BinOp(Mult, Lval(Var(var), _), Const(CInt (c, _, _)), _)
+      | BinOp(Mult, Const(CInt (c, _, _)), Lval(Var(var), NoOffset), _) ->
         Some (c, var)
       | Lval(Var(var), NoOffset) ->
-        Some (Int64.one, var)
+        Some (Cilint.one_cilint, var)
       | _ -> None
     in
 
@@ -48,8 +48,7 @@ struct
     | BinOp(op, expl, expr, _) when op = PlusA || op = MinusA ->
       begin match match_exp expl, match_exp expr with
         | Some(cl, varl), Some(cr, varr) when (BV.compare varl varr <> 0) -> (* this is needed as projection with varl=varr throws an exception (?) *)
-          let cr = if op = PlusA then cr else Int64.neg cr in
-          let cl, cr = Tuple2.mapn BI.of_int64 (cl, cr) in
+          let cr = if op = PlusA then cr else Cilint.neg_cilint cr in
           let cl, cr = INV.of_int oct_ik cl, INV.of_int oct_ik cr in
           let varSum = D.projection varl (Some (true, varr)) oct in
           let varDif1 = D.projection varl (Some (false, varr)) oct in
@@ -74,7 +73,7 @@ struct
     | None ->
       begin
         match exp with
-        | Const (CInt64 (i, _, _)) -> INV.of_int oct_ik (BI.of_int64 i)
+        | Const (CInt (i, _, _)) -> INV.of_int oct_ik i
         | Lval (Var var, NoOffset) -> D.projection var None oct
         | UnOp (Neg, exp, _) ->
           INV.neg (evaluate_exp oct exp)
@@ -116,19 +115,19 @@ struct
               D.set_constraint (var1, Some(ConstraintType.minus, v), CT.UpperAndLower, i) oct, true (* TODO: Is this ok, we need to be careful when to do closures *)
          in
          (match rval with
-          | BinOp(op, Lval(Var(var), NoOffset), Const(CInt64 (integer, _, _)), _)
+          | BinOp(op, Lval(Var(var), NoOffset), Const(CInt (integer, _, _)), _)
             when (op = PlusA || op = MinusA) && is_local_and_not_pointed_to var ->
             begin
-              let integer = BI.of_int64 @@
+              let integer =
                 if op = MinusA then
-                  Int64.neg integer
+                  Cilint.neg_cilint integer
                 else
                   integer
               in
               assignVarPlusInt var integer
             end
-          | BinOp(PlusA, Const(CInt64 (integer, _, _)), Lval(Var(var), NoOffset), _) when is_local_and_not_pointed_to var ->
-            assignVarPlusInt var (BI.of_int64 integer)
+          | BinOp(PlusA, Const(CInt (integer, _, _)), Lval(Var(var), NoOffset), _) when is_local_and_not_pointed_to var ->
+            assignVarPlusInt var integer
           | Lval(Var var, NoOffset) when is_local_and_not_pointed_to var ->
             assignVarPlusInt var BI.zero
           | exp ->
@@ -304,18 +303,18 @@ struct
 
   let query ctx (type a) (q: a Queries.t): a Queries.result =
     let rec getSumAndDiffForVars exp1 exp2 =
-      let addConstant x c = BatOption.map (OctagonDomain.INV.add (OctagonDomain.INV.of_int oct_ik (BI.of_int64 c))) x in
+      let addConstant x c = BatOption.map (OctagonDomain.INV.add (OctagonDomain.INV.of_int oct_ik c)) x in
       match exp1, exp2 with
-      | BinOp(PlusA, Lval l1, Const(CInt64(c,_,_)), _), Lval l2 ->
+      | BinOp(PlusA, Lval l1, Const(CInt(c,_,_)), _), Lval l2 ->
         let sum, diff = getSumAndDiffForVars (Lval l1) (Lval l2) in   (* reason why this is correct a <= x-y <= b -->  *)
         addConstant sum c, addConstant diff c                         (* a+c <= (x+c)-y <= b+c (add c to all sides)    *)
-      | Lval l1, BinOp(PlusA, Lval l2, Const(CInt64(c,_,_)), _) ->
+      | Lval l1, BinOp(PlusA, Lval l2, Const(CInt(c,_,_)), _) ->
         let sum, diff = getSumAndDiffForVars (Lval l1) (Lval l2) in   (* reason why this is correct a <= x-y <= b -->  *)
-        addConstant sum (Int64.neg c), addConstant diff (Int64.neg c) (* x-(y+c)= x-y-c --> a-c <= x-(y+c) <= b-c      *)
-      | BinOp(MinusA, Lval l1, Const(CInt64(c,_,_)), _), Lval l2 ->
+        addConstant sum (Cilint.neg_cilint c), addConstant diff (Cilint.neg_cilint c) (* x-(y+c)= x-y-c --> a-c <= x-(y+c) <= b-c      *)
+      | BinOp(MinusA, Lval l1, Const(CInt(c,_,_)), _), Lval l2 ->
         let sum, diff = getSumAndDiffForVars (Lval l1) (Lval l2) in   (* reason why this is correct a <= x-y <= b -->  *)
-        addConstant sum (Int64.neg c), addConstant diff (Int64.neg c) (* (x-c)-y = x-y-c --> a-c <= (x-c)-y <= b-c     *)
-      | Lval l1, BinOp(MinusA, Lval l2, Const(CInt64(c,_,_)), _) ->
+        addConstant sum (Cilint.neg_cilint c), addConstant diff (Cilint.neg_cilint c) (* (x-c)-y = x-y-c --> a-c <= (x-c)-y <= b-c     *)
+      | Lval l1, BinOp(MinusA, Lval l2, Const(CInt(c,_,_)), _) ->
         let sum, diff = getSumAndDiffForVars (Lval l1) (Lval l2) in   (* reason why this is correct a <= x-y <= b -->  *)
         addConstant sum c, addConstant diff c                         (* x-(y-c) = x-y+c --> a+c <= x-(y-c) <= b+c     *)
       | Lval(Var v1, NoOffset), Lval(Var v2, NoOffset) ->
@@ -323,7 +322,7 @@ struct
         if not flag then
           sum, diff
         else
-          sum, BatOption.map (OctagonDomain.INV.mul (INV.of_int oct_ik (BI.of_int64 Int64.minus_one))) diff
+          sum, BatOption.map (OctagonDomain.INV.mul (INV.of_int oct_ik Cilint.mone_cilint)) diff
       | _ -> None, None
     in
     match q with
diff --git a/src/analyses/osek.ml b/src/analyses/osek.ml
index ac2b08539a..ed4271ebb0 100644
--- a/src/analyses/osek.ml
+++ b/src/analyses/osek.ml
@@ -608,14 +608,14 @@ struct
   let rec conv_offset x =
     match x with
     | `NoOffset    -> `NoOffset
-    | `Index (Const (CInt64 (i,ik,s)),o) -> `Index (IntDomain.of_const (i,ik,s), conv_offset o)
+    | `Index (Const (CInt (i,ik,s)),o) -> `Index (IntDomain.of_const (i,ik,s), conv_offset o)
     | `Index (_,o) -> `Index (ValueDomain.IndexDomain.top (), conv_offset o)
     | `Field (f,o) -> `Field (f, conv_offset o)
 
   let rec conv_const_offset x =
     match x with
     | NoOffset    -> `NoOffset
-    | Index (Const (CInt64 (i,ik,s)),o) -> `Index (IntDomain.of_const (i,ik,s), conv_const_offset o)
+    | Index (Const (CInt (i,ik,s)),o) -> `Index (IntDomain.of_const (i,ik,s), conv_const_offset o)
     | Index (_,o) -> `Index (ValueDomain.IndexDomain.top (), conv_const_offset o)
     | Field (f,o) -> `Field (f, conv_const_offset o)
 
@@ -850,8 +850,8 @@ struct
         if not (D.is_empty regular) then (
           let res = List.fold_left (fun rs r -> (names r) ^ ", " ^ rs) "" (D.ReverseAddrSet.elements regular) in
           let ev = match arglist with
-            | [CastE (_, Const (CInt64 (c,_,_))) | Const (CInt64 (c,_,_))] ->
-              fst @@ Hashtbl.find events (Int64.to_string c)
+            | [CastE (_, Const (CInt (c,_,_))) | Const (CInt (c,_,_))] ->
+              fst @@ Hashtbl.find events (Cilint.string_of_cilint c)
             | _ -> print_endline "No event found for argument of WaitEvent"; "_not_found_"
           in
           print_endline (task ^ " waited for event "^ ev ^ " while holding resource(s) " ^ res)
diff --git a/src/analyses/spec.ml b/src/analyses/spec.ml
index 96465e53f1..5910e8fedc 100644
--- a/src/analyses/spec.ml
+++ b/src/analyses/spec.ml
@@ -293,14 +293,14 @@ struct
     let check a b tv =
       (* ignore(printf "check: %a = %a\n" d_plainexp a d_plainexp b); *)
       match a, b with
-      | Const (CInt64(i, kind, str)), Lval lval
-      | Lval lval, Const (CInt64(i, kind, str)) ->
+      | Const (CInt(i, kind, str)), Lval lval
+      | Lval lval, Const (CInt(i, kind, str)) ->
         (* let binop = BinOp (Eq, a, b, Cil.intType) in *)
         (* standardize the format of the expression to 'lval==i'. -> spec needs to follow that format, the code is mapped to it. *)
-        let binop = BinOp (Eq, Lval lval, Const (CInt64(i, kind, str)), Cil.intType) in
+        let binop = BinOp (Eq, Lval lval, Const (CInt(i, kind, str)), Cil.intType) in
         let key = D.key_from_lval lval in
         let value = D.find key m in
-        if i = Int64.zero && tv then (
+        if Cilint.is_zero_cilint i && tv then (
           M.debug "error-branch";
           (* D.remove key m *)
         )else(
diff --git a/src/analyses/symbLocks.ml b/src/analyses/symbLocks.ml
index dde4ab19ac..2f472d3c2a 100644
--- a/src/analyses/symbLocks.ml
+++ b/src/analyses/symbLocks.ml
@@ -113,7 +113,7 @@ struct
     match x with
     | NoOffset    -> `NoOffset
 
-    | Index (Const  (CInt64 (i,ikind,s)),o) -> `Index (IntDomain.of_const (i,ikind,s), conv_const_offset o)
+    | Index (Const  (CInt (i,ikind,s)),o) -> `Index (IntDomain.of_const (i,ikind,s), conv_const_offset o)
     | Index (_,o) -> `Index (ValueDomain.IndexDomain.top (), conv_const_offset o)
     | Field (f,o) -> `Field (f, conv_const_offset o)
 
@@ -133,7 +133,7 @@ struct
     let rec conv_const_offset x =
       match x with
       | NoOffset    -> `NoOffset
-      | Index (Const  (CInt64 (i,ikind,s)),o) -> `Index (IntDomain.of_const (i,ikind,s), conv_const_offset o)
+      | Index (Const  (CInt (i,ikind,s)),o) -> `Index (IntDomain.of_const (i,ikind,s), conv_const_offset o)
       | Index (_,o) -> `Index (ValueDomain.IndexDomain.top (), conv_const_offset o)
       | Field (f,o) -> `Field (f, conv_const_offset o)
     in
diff --git a/src/analyses/tutorials/constants.ml b/src/analyses/tutorials/constants.ml
index ee5a0e1f7f..cda41c4315 100644
--- a/src/analyses/tutorials/constants.ml
+++ b/src/analyses/tutorials/constants.ml
@@ -34,8 +34,11 @@ struct
   let rec eval (state : D.t) (e: exp) =
     match e with
     | Const c -> (match c with
-      | CInt64 (i,_,_) -> I.of_int i
-      | _ -> I.top ()
+        | CInt (i,_,_) ->
+          (try I.of_int (Z.to_int64 i) with Z.Overflow -> I.top ())
+        (* Our underlying int domain here can not deal with values that do not fit into int64 *)
+        (* Use Z.to_int64 instead of Cilint.int64_of_cilint to get exception instead of silent wrap-around *)
+        | _ -> I.top ()
       )
     | Lval lv -> (match get_local lv with
       | Some v -> D.find v state
diff --git a/src/analyses/tutorials/signs.ml b/src/analyses/tutorials/signs.ml
index d68b2973b2..9f3e633561 100644
--- a/src/analyses/tutorials/signs.ml
+++ b/src/analyses/tutorials/signs.ml
@@ -2,6 +2,7 @@
 
 open Prelude.Ana
 open Analyses
+open Cilint
 
 module Signs =
 struct
@@ -22,8 +23,8 @@ struct
 
   (* TODO: An attempt to abstract integers, but it's just a little wrong... *)
   let of_int i =
-    if i < Int64.zero then Zero
-    else if i > Int64.zero then Zero
+    if compare_cilint i zero_cilint < 0 then Zero
+    else if compare_cilint i zero_cilint > 0 then Zero
     else Zero
 
   let gt x y = match x, y with
@@ -60,7 +61,7 @@ struct
 
   (* This should now evaluate expressions. *)
   let eval (d: D.t) (exp: exp): SL.t = match exp with
-    | Const (CInt64 (i, _, _)) -> SL.top () (* TODO: Fix me! *)
+    | Const (CInt (i, _, _)) -> SL.top () (* TODO: Fix me! *)
     | Lval (Var x, NoOffset) -> D.find x d
     | _ -> SL.top ()
 
diff --git a/src/analyses/uninit.ml b/src/analyses/uninit.ml
index e400386c92..353c26e725 100644
--- a/src/analyses/uninit.ml
+++ b/src/analyses/uninit.ml
@@ -36,7 +36,7 @@ struct
   let rec conv_offset x =
     match x with
     | `NoOffset    -> `NoOffset
-    | `Index (Const (CInt64 (i,ik,s)),o) -> `Index (IntDomain.of_const (i,ik,s), conv_offset o)
+    | `Index (Const (CInt (i,ik,s)),o) -> `Index (IntDomain.of_const (i,ik,s), conv_offset o)
     | `Index (_,o) -> `Index (IdxDom.top (), conv_offset o)
     | `Field (f,o) -> `Field (f, conv_offset o)
 
diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml
index 0e0aa24785..7bb2d73008 100644
--- a/src/analyses/varEq.ml
+++ b/src/analyses/varEq.ml
@@ -53,7 +53,7 @@ struct
     |	CStr s1  , CStr s2	 -> s1 = s2
     |	CWStr is1, CWStr is2 -> is1 = is2
     |	CChr c1  , CChr c2   -> c1 = c2
-    |	CInt64 (v1,k1,_), CInt64 (v2,k2,_) -> v1 = v2 && k1 = k2
+    |	CInt (v1,k1,_), CInt (v2,k2,_) -> Cilint.compare_cilint v1 v2 = 0 && k1 = k2
     |	CReal (f1,k1,_) , CReal (f2,k2,_)  -> f1 = f2 && k1 = k2
     |	CEnum (_,n1,e1), CEnum (_,n2,e2) -> n1 = n2 && e1.ename = e2.ename
     | _ -> false
diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml
index 56215351d7..c887f8799e 100644
--- a/src/cdomains/apron/apronDomain.apron.ml
+++ b/src/cdomains/apron/apronDomain.apron.ml
@@ -162,11 +162,8 @@ struct
             raise Unsupported_CilExp
         else
           failwith "texpr1_expr_of_cil_exp: globals must be replaced with temporary locals"
-      | Const (CInt64 (i, _, s)) ->
-        let str = match s with
-          | Some s -> s
-          | None -> Int64.to_string i
-        in
+      | Const (CInt (i, _, _)) ->
+        let str = Cilint.string_of_cilint i in
         Cst (Coeff.s_of_mpqf (Mpqf.of_string str))
       | exp ->
         let expr =
diff --git a/src/cdomains/exp.ml b/src/cdomains/exp.ml
index 2c493750c3..afb0a6ef11 100644
--- a/src/cdomains/exp.ml
+++ b/src/cdomains/exp.ml
@@ -109,7 +109,7 @@ struct
 
   let eq_const c1 c2 =
     match c1, c2 with
-    | CInt64 (i1,_,_), CInt64 (i2,_,_) -> i1=i2
+    | CInt (i1,_,_), CInt (i2,_,_)     -> Cilint.compare_cilint i1 i2 = 0
     |	CStr s1        , CStr s2         -> s1=s2
     |	CWStr s1       , CWStr s2        -> s1=s2
     |	CChr c1        , CChr c2         -> c1=c2
@@ -278,7 +278,7 @@ struct
     *)	| EAddr :: EDeref :: x -> ees_to_offs x
     | EDeref :: EAddr :: x -> ees_to_offs x
     | EField f :: x -> `Field (f,ees_to_offs x)
-    | EIndex (Const (CInt64 (i, ik, str))) :: x -> `Index (IntDomain.of_const (i, ik, str),ees_to_offs x)
+    | EIndex (Const (CInt (i, ik, str))) :: x -> `Index (IntDomain.of_const (i, ik, str),ees_to_offs x)
     | EIndex i :: x -> `NoOffset              (* Ideally this would be ValueDomain.IntDomain but that leads to issues *)
     | x  -> raise NotSimpleEnough             (* with a cyclic build *)
 
diff --git a/src/cdomains/intDomain.ml b/src/cdomains/intDomain.ml
index d8a30e8a60..7349de5726 100644
--- a/src/cdomains/intDomain.ml
+++ b/src/cdomains/intDomain.ml
@@ -407,7 +407,7 @@ module Size = struct (* size in bits as int, range as int64 *)
     | `Signed -> ILongLong
     | `Unsigned -> IULongLong
   let top_typ = TInt (ILongLong, [])
-  let min_for x = intKindForValue (fst (truncateCilint (max (sign_big_int x)) (Big x))) (sign_big_int x = `Unsigned)
+  let min_for x = intKindForValue (fst (truncateCilint (max (sign_big_int x)) x)) (sign_big_int x = `Unsigned)
   let bit = function (* bits needed for representation *)
     | IBool -> 1
     | ik -> bytesSizeOfInt ik * 8
@@ -832,10 +832,10 @@ struct
     match x with
     | Some (x1, x2) when Ints_t.compare x1 x2 = 0 ->
       let x1 = Ints_t.to_bigint x1 in
-      Invariant.of_exp Cil.(BinOp (Eq, c, kintegerCilint ik (Big x1), intType))
+      Invariant.of_exp Cil.(BinOp (Eq, c, kintegerCilint ik x1, intType))
     | Some (x1, x2) ->
       let open Invariant in
-      let (x1', x2') = BatTuple.Tuple2.mapn (fun a -> Cilint.Big (Ints_t.to_bigint a)) (x1, x2) in
+      let (x1', x2') = BatTuple.Tuple2.mapn (Ints_t.to_bigint) (x1, x2) in
       (try
         (* Cilfacade.typeOf will fail if c is heap allocated *)
         let i1 = if Ints_t.compare (min_int ik) x1 <> 0 then of_exp Cil.(BinOp (Le, kintegerCilint ik x1', c, intType)) else none in
@@ -1624,10 +1624,10 @@ struct
   let invariant_ikind c ik (x:t) =
     let c = Cil.(Lval (BatOption.get c.Invariant.lval)) in
     match x with
-    | `Definite x -> Invariant.of_exp Cil.(BinOp (Eq, c, kintegerCilint ik (Big x), intType))
+    | `Definite x -> Invariant.of_exp Cil.(BinOp (Eq, c, kintegerCilint ik x, intType))
     | `Excluded (s, _) ->
       S.fold (fun x a ->
-          let i = Invariant.of_exp Cil.(BinOp (Ne, c, kintegerCilint ik (Big x), intType)) in
+          let i = Invariant.of_exp Cil.(BinOp (Ne, c, kintegerCilint ik x, intType)) in
           Invariant.(a && i)
         ) s Invariant.none
     | `Bot -> Invariant.none
@@ -2055,12 +2055,12 @@ module Enums : S with type int_t = BigInt.t = struct
     match x with
     | Inc ps ->
       List.fold_left (fun a x ->
-          let i = Invariant.of_exp Cil.(BinOp (Eq, c, kintegerCilint ik (Big x), intType)) in
+          let i = Invariant.of_exp Cil.(BinOp (Eq, c, kintegerCilint ik x, intType)) in
           Invariant.(a || i)
         ) Invariant.none (BISet.elements ps)
     | Exc (ns, _) ->
       List.fold_left (fun a x ->
-          let i = Invariant.of_exp Cil.(BinOp (Ne, c, kintegerCilint ik (Big x), intType)) in
+          let i = Invariant.of_exp Cil.(BinOp (Ne, c, kintegerCilint ik x, intType)) in
           Invariant.(a && i)
         ) Invariant.none (BISet.elements ns)
 
@@ -2506,11 +2506,11 @@ struct
     let l = Cil.(Lval (BatOption.get ctxt.Invariant.lval)) in
     match x with
     | Some (c, m) when m =: Ints_t.zero ->
-       let c = Cilint.Big (Ints_t.to_bigint c) in
-       Invariant.of_exp Cil.(BinOp (Eq, l, Cil.kintegerCilint ik c, intType))
+      let c = Ints_t.to_bigint c in
+      Invariant.of_exp Cil.(BinOp (Eq, l, Cil.kintegerCilint ik c, intType))
     | Some (c, m) ->
        let open Cil in
-       let (c, m) = BatTuple.Tuple2.mapn (fun a -> kintegerCilint ik @@ Cilint.Big (Ints_t.to_bigint a)) (c, m) in
+       let (c, m) = BatTuple.Tuple2.mapn (fun a -> kintegerCilint ik @@ Ints_t.to_bigint a) (c, m) in
        (try
           Invariant.of_exp (BinOp (Eq, (BinOp (Mod, l, m, TInt(ik,[]))), c, intType))
         with e -> None)
@@ -2945,7 +2945,7 @@ module IntDomTupleImpl = struct
     | Some v ->
       (* If definite, output single equality instead of every subdomain repeating same equality *)
       let c_exp = Cil.(Lval (Option.get c.Invariant.lval)) in
-      Invariant.of_exp Cil.(BinOp (Eq, c_exp, kintegerCilint ik (Big v), intType))
+      Invariant.of_exp Cil.(BinOp (Eq, c_exp, kintegerCilint ik v, intType))
     | None ->
       let is = to_list (mapp { fp = fun (type a) (module I:S with type t = a) -> I.invariant_ikind c ik } x)
       in List.fold_left (fun a i ->
@@ -2965,7 +2965,4 @@ struct
 
 end
 
-let of_const (i, ik, str) =
-  match str with
-  | Some t -> IntDomTuple.of_int ik @@ BI.of_string t
-  | None -> IntDomTuple.of_int ik @@ BI.of_int64 i
+let of_const (i, ik, str) = IntDomTuple.of_int ik i
diff --git a/src/cdomains/intDomain.mli b/src/cdomains/intDomain.mli
index e41f095699..4173e2d209 100644
--- a/src/cdomains/intDomain.mli
+++ b/src/cdomains/intDomain.mli
@@ -323,7 +323,7 @@ module IntDomTuple : sig
   val no_interval: t -> t
 end
 
-val of_const: int64 * Cil.ikind * string option -> IntDomTuple.t
+val of_const: Cilint.cilint * Cil.ikind * string option -> IntDomTuple.t
 
 
 module Size : sig
diff --git a/src/incremental/compareAST.ml b/src/incremental/compareAST.ml
index 7d720fe526..fca341c083 100644
--- a/src/incremental/compareAST.ml
+++ b/src/incremental/compareAST.ml
@@ -39,7 +39,7 @@ let compare_name a b =
   if a = b then true else BatString.(starts_with a anon_struct && starts_with b anon_struct || starts_with a anon_union && starts_with b anon_union)
 
 let rec eq_constant (a: constant) (b: constant) = match a, b with
-    CInt64 (val1, kind1, str1), CInt64 (val2, kind2, str2) -> val1 = val2 && kind1 = kind2 (* Ignore string representation, i.e. 0x2 == 2 *)
+  | CInt (val1, kind1, str1), CInt (val2, kind2, str2) -> Cilint.compare_cilint val1 val2 = 0 && kind1 = kind2 (* Ignore string representation, i.e. 0x2 == 2 *)
   | CEnum (exp1, str1, enuminfo1), CEnum (exp2, str2, enuminfo2) -> eq_exp exp1 exp2 (* Ignore name and enuminfo  *)
   | a, b -> a = b
 
diff --git a/src/util/cilfacade.ml b/src/util/cilfacade.ml
index 4c608bfc70..801d04240e 100644
--- a/src/util/cilfacade.ml
+++ b/src/util/cilfacade.ml
@@ -290,7 +290,7 @@ let typeOfRealAndImagComponents t =
 
 let rec typeOf (e: exp) : typ =
   match e with
-  | Const(CInt64 (_, ik, _)) -> TInt(ik, [])
+  | Const(CInt (_, ik, _)) -> TInt(ik, [])
 
   (* Character constants have type int.  ISO/IEC 9899:1999 (E),
    * section 6.4.4.4 [Character constants], paragraph 10, if you
diff --git a/src/util/wideningThresholds.ml b/src/util/wideningThresholds.ml
index 9bbf6e30f0..03f40678d8 100644
--- a/src/util/wideningThresholds.ml
+++ b/src/util/wideningThresholds.ml
@@ -7,15 +7,11 @@ class extractConstantsVisitor(widening_thresholds) = object
 
   method! vexpr e =
     match e with
-    | Const (CInt64(i,ik,str)) ->
-      let bi = match str with
-        | Some t -> Z.of_string t
-        | None -> Z.of_int64 i
-      in
-      widening_thresholds := Thresholds.add bi !widening_thresholds;
+    | Const (CInt(i,ik,_)) ->
+      widening_thresholds := Thresholds.add i !widening_thresholds;
       (* Adding double value of all constants so that we can establish for single variables that they are <= const*)
       (* This is only needed for Apron, one might want to remove it later *)
-      widening_thresholds := Thresholds.add (Z.mul (Z.of_int 2) bi) !widening_thresholds;
+      widening_thresholds := Thresholds.add (Z.mul (Z.of_int 2) i) !widening_thresholds;
       DoChildren
     | _ -> DoChildren
 end
diff --git a/tests/regression/27-inv_invariants/01-ints.c b/tests/regression/27-inv_invariants/01-ints.c
index b00eb916c6..f3eec60e62 100644
--- a/tests/regression/27-inv_invariants/01-ints.c
+++ b/tests/regression/27-inv_invariants/01-ints.c
@@ -55,8 +55,7 @@ int main() {
     // xl could also be -3
     assert(xl == -2 && yl >= 1); //UNKNOWN!
   if (xl > 1 && xl < 5 && xl % 2 == 1) {
-    // UNKNOWN due to Interval32 not being able to represent long
-    // assert(xl != 2); // [2,4] -> [3,4] TO-DO x % 2 == 1
+    assert(xl != 2); // [2,4] -> [3,4] TO-DO x % 2 == 1
   }
 
 
@@ -156,8 +155,7 @@ int main2() {
     // xl could also be -three
     assert(xl == -two && yl >= one); //UNKNOWN!
   if (xl > one && xl < five && xl % two == one) {
-    // UNKNOWN due to Intervalthreetwo not being able to represent long
-    // assert(xl != two); // [two,four] -> [three,four] TO-DO x % two == one
+    assert(xl != two); // [two,four] -> [three,four] TO-DO x % two == one
   }