diff --git a/CHANGELOG.md b/CHANGELOG.md
index 420cc7145e..1fb07a7dc2 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,14 @@
+## v2.5.0
+Functionally equivalent to Goblint in SV-COMP 2025.
+
+* Add 32bit vs 64bit architecture support (#54, #1574).
+* Add per-function context gas analysis (#1569, #1570, #1598).
+* Adapt automatic static loop unrolling (#1516, #1582, #1583, #1584, #1590, #1595, #1599).
+* Adapt automatic configuration tuning (#1450, #1612, #1181, #1604).
+* Simplify non-relational integer invariants in witnesses (#1517).
+* Fix excessive hash collisions (#1594, #1602).
+* Clean up various code (#1095, #1523, #1554, #1575, #1588, #1597, #1614).
+
 ## v2.4.0
 * Remove unmaintained analyses: spec, file (#1281).
 * Add linear two-variable equalities analysis (#1297, #1412, #1466).
@@ -10,7 +21,7 @@
 * Fix mutex type analysis unsoundness and enable it by default (#1414, #1416, #1510).
 * Add points-to set refinement on mutex path splitting (#1287, #1343, #1374, #1396, #1407).
 * Improve narrowing operators (#1502, #1540, #1543).
-* Extract automatic configuration tuning for soundness (#1369).
+* Extract automatic configuration tuning for soundness (#1469).
 * Fix many locations in witnesses (#1355, #1372, #1400, #1403).
 * Improve output readability (#1294, #1312, #1405, #1497).
 * Refactor logging (#1117).
diff --git a/conf/svcomp-ghost.json b/conf/svcomp-ghost.json
index cb4d8f1384..d1b4171b2b 100644
--- a/conf/svcomp-ghost.json
+++ b/conf/svcomp-ghost.json
@@ -10,7 +10,8 @@
       "interval": true
     },
     "float": {
-      "interval": true
+      "interval": true,
+      "evaluate_math_functions": true
     },
     "activated": [
       "base",
@@ -47,27 +48,6 @@
     "context": {
       "widen": false
     },
-    "malloc": {
-      "wrappers": [
-        "kmalloc",
-        "__kmalloc",
-        "usb_alloc_urb",
-        "__builtin_alloca",
-        "kzalloc",
-
-        "ldv_malloc",
-
-        "kzalloc_node",
-        "ldv_zalloc",
-        "kmalloc_array",
-        "kcalloc",
-
-        "ldv_xmalloc",
-        "ldv_xzalloc",
-        "ldv_calloc",
-        "ldv_kzalloc"
-      ]
-    },
     "base": {
       "arrays": {
         "domain": "partitioned"
@@ -110,6 +90,7 @@
         "wideningThresholds",
         "loopUnrollHeuristic",
         "memsafetySpecification",
+        "noOverflows",
         "termination",
         "tmpSpecialAnalysis"
       ]
@@ -149,17 +130,7 @@
       "accessed": false,
       "exact": true,
       "all-locals": false,
-      "flow_insensitive-as": "invariant_set-location_invariant",
-      "exclude-vars": [
-        "tmp\\(___[0-9]+\\)?",
-        "cond",
-        "RETURN",
-        "__\\(cil_\\)?tmp_?[0-9]*\\(_[0-9]+\\)?",
-        ".*____CPAchecker_TMP_[0-9]+",
-        "__VERIFIER_assert__cond",
-        "__ksymtab_.*",
-        "\\(ldv_state_variable\\|ldv_timer_state\\|ldv_timer_list\\|ldv_irq_\\(line_\\|data_\\)?[0-9]+\\|ldv_retval\\)_[0-9]+"
-      ]
+      "flow_insensitive-as": "invariant_set-location_invariant"
     }
   },
   "pre": {
diff --git a/conf/svcomp-validate.json b/conf/svcomp-validate.json
index 64564f480f..bec171f1e8 100644
--- a/conf/svcomp-validate.json
+++ b/conf/svcomp-validate.json
@@ -10,7 +10,8 @@
       "interval": true
     },
     "float": {
-      "interval": true
+      "interval": true,
+      "evaluate_math_functions": true
     },
     "activated": [
       "base",
diff --git a/conf/svcomp.json b/conf/svcomp.json
index c1ccaa4ab3..dedc393ba1 100644
--- a/conf/svcomp.json
+++ b/conf/svcomp.json
@@ -10,7 +10,8 @@
       "interval": true
     },
     "float": {
-      "interval": true
+      "interval": true,
+      "evaluate_math_functions": true
     },
     "activated": [
       "base",
diff --git a/conf/svcomp24-validate.json b/conf/svcomp24-validate.json
index 7832ffa6af..d83b1767a4 100644
--- a/conf/svcomp24-validate.json
+++ b/conf/svcomp24-validate.json
@@ -10,7 +10,8 @@
       "interval": true
     },
     "float": {
-      "interval": true
+      "interval": true,
+      "evaluate_math_functions": true
     },
     "activated": [
       "base",
diff --git a/conf/svcomp24.json b/conf/svcomp24.json
index 7e30554ceb..1c60f84920 100644
--- a/conf/svcomp24.json
+++ b/conf/svcomp24.json
@@ -10,7 +10,8 @@
       "interval": true
     },
     "float": {
-      "interval": true
+      "interval": true,
+      "evaluate_math_functions": true
     },
     "activated": [
       "base",
diff --git a/conf/svcomp25-validate.json b/conf/svcomp25-validate.json
new file mode 100644
index 0000000000..bec171f1e8
--- /dev/null
+++ b/conf/svcomp25-validate.json
@@ -0,0 +1,123 @@
+{
+  "ana": {
+    "sv-comp": {
+      "enabled": true,
+      "functions": true
+    },
+    "int": {
+      "def_exc": true,
+      "enums": false,
+      "interval": true
+    },
+    "float": {
+      "interval": true,
+      "evaluate_math_functions": true
+    },
+    "activated": [
+      "base",
+      "threadid",
+      "threadflag",
+      "threadreturn",
+      "mallocWrapper",
+      "mutexEvents",
+      "mutex",
+      "access",
+      "race",
+      "escape",
+      "expRelation",
+      "mhp",
+      "assert",
+      "var_eq",
+      "symb_locks",
+      "region",
+      "thread",
+      "threadJoins",
+      "abortUnless",
+      "unassume"
+    ],
+    "path_sens": [
+      "mutex",
+      "malloc_null",
+      "uninit",
+      "expsplit",
+      "activeSetjmp",
+      "memLeak",
+      "threadflag"
+    ],
+    "context": {
+      "widen": false
+    },
+    "base": {
+      "arrays": {
+        "domain": "partitioned"
+      }
+    },
+    "race": {
+      "free": false,
+      "call": false
+    },
+    "autotune": {
+      "enabled": true,
+      "activated": [
+        "singleThreaded",
+        "mallocWrappers",
+        "noRecursiveIntervals",
+        "enums",
+        "congruence",
+        "octagon",
+        "wideningThresholds",
+        "loopUnrollHeuristic",
+        "memsafetySpecification",
+        "noOverflows",
+        "termination",
+        "tmpSpecialAnalysis"
+      ]
+    },
+    "widen": {
+      "tokens": true
+    }
+  },
+  "exp": {
+    "region-offsets": true
+  },
+  "solver": "td3",
+  "sem": {
+    "unknown_function": {
+      "spawn": false
+    },
+    "int": {
+      "signed_overflow": "assume_none"
+    },
+    "null-pointer": {
+      "dereference": "assume_none"
+    }
+  },
+  "witness": {
+    "graphml": {
+      "enabled": false
+    },
+    "yaml": {
+      "enabled": false,
+      "strict": true,
+      "format-version": "2.0",
+      "entry-types": [
+        "location_invariant",
+        "loop_invariant",
+        "invariant_set",
+        "violation_sequence"
+      ],
+      "invariant-types": [
+        "location_invariant",
+        "loop_invariant"
+      ]
+    },
+    "invariant": {
+      "loop-head": true,
+      "after-lock": true,
+      "other": true
+    }
+  },
+  "pre": {
+    "enabled": false
+  }
+}
diff --git a/conf/svcomp25.json b/conf/svcomp25.json
new file mode 100644
index 0000000000..dedc393ba1
--- /dev/null
+++ b/conf/svcomp25.json
@@ -0,0 +1,118 @@
+{
+  "ana": {
+    "sv-comp": {
+      "enabled": true,
+      "functions": true
+    },
+    "int": {
+      "def_exc": true,
+      "enums": false,
+      "interval": true
+    },
+    "float": {
+      "interval": true,
+      "evaluate_math_functions": true
+    },
+    "activated": [
+      "base",
+      "threadid",
+      "threadflag",
+      "threadreturn",
+      "mallocWrapper",
+      "mutexEvents",
+      "mutex",
+      "access",
+      "race",
+      "escape",
+      "expRelation",
+      "mhp",
+      "assert",
+      "var_eq",
+      "symb_locks",
+      "region",
+      "thread",
+      "threadJoins",
+      "abortUnless"
+    ],
+    "path_sens": [
+      "mutex",
+      "malloc_null",
+      "uninit",
+      "expsplit",
+      "activeSetjmp",
+      "memLeak",
+      "threadflag"
+    ],
+    "context": {
+      "widen": false
+    },
+    "base": {
+      "arrays": {
+        "domain": "partitioned"
+      }
+    },
+    "race": {
+      "free": false,
+      "call": false
+    },
+    "autotune": {
+      "enabled": true,
+      "activated": [
+        "singleThreaded",
+        "mallocWrappers",
+        "noRecursiveIntervals",
+        "enums",
+        "congruence",
+        "octagon",
+        "wideningThresholds",
+        "loopUnrollHeuristic",
+        "memsafetySpecification",
+        "noOverflows",
+        "termination",
+        "tmpSpecialAnalysis"
+      ]
+    }
+  },
+  "exp": {
+    "region-offsets": true
+  },
+  "solver": "td3",
+  "sem": {
+    "unknown_function": {
+      "spawn": false
+    },
+    "int": {
+      "signed_overflow": "assume_none"
+    },
+    "null-pointer": {
+      "dereference": "assume_none"
+    }
+  },
+  "witness": {
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    },
+    "yaml": {
+      "enabled": true,
+      "format-version": "2.0",
+      "entry-types": [
+        "invariant_set"
+      ],
+      "invariant-types": [
+        "loop_invariant"
+      ]
+    },
+    "invariant": {
+      "loop-head": true,
+      "after-lock": false,
+      "other": false,
+      "accessed": false,
+      "exact": true
+    }
+  },
+  "pre": {
+    "enabled": false
+  }
+}
diff --git a/docs/developer-guide/releasing.md b/docs/developer-guide/releasing.md
index 7530d9ad20..aca0749eb9 100644
--- a/docs/developer-guide/releasing.md
+++ b/docs/developer-guide/releasing.md
@@ -77,6 +77,8 @@
 
     This includes: git tag name, git tag message and zipped conf file.
 
+5. Open MR with conf file name to the [bench-defs](https://gitlab.com/sosy-lab/sv-comp/bench-defs) repository.
+
 ### For each prerun
 
 1. Update opam pins:
diff --git a/dune-project b/dune-project
index 54915cf964..9a1d958484 100644
--- a/dune-project
+++ b/dune-project
@@ -16,7 +16,7 @@
 (homepage "https://goblint.in.tum.de")
 (documentation "https://goblint.readthedocs.io/en/latest/")
 (authors "Simmo Saan" "Michael Schwarz" "Julian Erhard" "Sarah Tilscher" "Karoliine Holter" "Ralf Vogler" "Kalmer Apinis" "Vesal Vojdani" ) ; same authors as in .zenodo.json and CITATION.cff
-(maintainers "Simmo Saan <simmo.saan@gmail.com>" "Michael Schwarz <michael.schwarz93@gmail.com>" "Karoliine Holter")
+(maintainers "Simmo Saan <simmo.saan@gmail.com>" "Michael Schwarz <michael.schwarz93@gmail.com>" "Karoliine Holter <karoliine.holter@ut.ee>")
 (license MIT)
 
 (package
@@ -37,7 +37,7 @@ Goblint includes analyses for assertions, overflows, deadlocks, etc and can be e
     "concurrency"))
   (depends
     (ocaml (>= 4.14))
-    (goblint-cil (>= 2.0.4)) ; TODO no way to define as pin-depends? Used goblint.opam.template to add it for now. https://github.com/ocaml/dune/issues/3231. Alternatively, removing this line and adding cil as a git submodule and `(vendored_dirs cil)` as ./dune also works. This way, no more need to reinstall the pinned cil opam package on changes. However, then cil is cleaned and has to be rebuild together with goblint.
+    (goblint-cil (>= 2.0.5)) ; TODO no way to define as pin-depends? Used goblint.opam.template to add it for now. https://github.com/ocaml/dune/issues/3231. Alternatively, removing this line and adding cil as a git submodule and `(vendored_dirs cil)` as ./dune also works. This way, no more need to reinstall the pinned cil opam package on changes. However, then cil is cleaned and has to be rebuild together with goblint.
     (batteries (>= 3.5.1))
     (zarith (>= 1.10))
     (yojson (>= 2.0.0))
diff --git a/goblint.opam b/goblint.opam
index 44e5ccd2c2..219c67d011 100644
--- a/goblint.opam
+++ b/goblint.opam
@@ -9,7 +9,7 @@ Goblint includes analyses for assertions, overflows, deadlocks, etc and can be e
 maintainer: [
   "Simmo Saan <simmo.saan@gmail.com>"
   "Michael Schwarz <michael.schwarz93@gmail.com>"
-  "Karoliine Holter"
+  "Karoliine Holter <karoliine.holter@ut.ee>"
 ]
 authors: [
   "Simmo Saan"
@@ -37,7 +37,7 @@ bug-reports: "https://github.com/goblint/analyzer/issues"
 depends: [
   "dune" {>= "3.7"}
   "ocaml" {>= "4.14"}
-  "goblint-cil" {>= "2.0.4"}
+  "goblint-cil" {>= "2.0.5"}
   "batteries" {>= "3.5.1"}
   "zarith" {>= "1.10"}
   "yojson" {>= "2.0.0"}
@@ -97,7 +97,8 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 # also remember to generate/adjust goblint.opam.locked!
 available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
 pin-depends: [
-  [ "goblint-cil.2.0.4" "git+https://github.com/goblint/cil.git#9f4fac450c02bc61a13717784515056b185794cd" ]
+  # published goblint-cil 2.0.5 is currently up-to-date, but pinned for reproducibility
+  [ "goblint-cil.2.0.5" "git+https://github.com/goblint/cil.git#c79208b21ea61d7b72eae29a18c1ddeda4795dfd" ]
   # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new camlidl release
   [ "camlidl.1.12" "git+https://github.com/xavierleroy/camlidl.git#1c1e87e3f56c2c6b3226dd0af3510ef414b462d0" ]
   # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release
diff --git a/goblint.opam.locked b/goblint.opam.locked
index 9fbee1e02b..e5176b9007 100644
--- a/goblint.opam.locked
+++ b/goblint.opam.locked
@@ -5,7 +5,7 @@ synopsis: "Static analysis framework for C"
 maintainer: [
   "Simmo Saan <simmo.saan@gmail.com>"
   "Michael Schwarz <michael.schwarz93@gmail.com>"
-  "Karoliine Holter"
+  "Karoliine Holter <karoliine.holter@ut.ee>"
 ]
 authors: [
   "Simmo Saan"
@@ -64,7 +64,7 @@ depends: [
   "fileutils" {= "0.6.4"}
   "fmt" {= "0.9.0"}
   "fpath" {= "0.7.3"}
-  "goblint-cil" {= "2.0.4"}
+  "goblint-cil" {= "2.0.5"}
   "hex" {= "1.5.0"}
   "integers" {= "0.7.0"}
   "json-data-encoding" {= "1.0.1"}
@@ -139,8 +139,8 @@ post-messages: [
 ]
 pin-depends: [
   [
-    "goblint-cil.2.0.4"
-    "git+https://github.com/goblint/cil.git#9f4fac450c02bc61a13717784515056b185794cd"
+    "goblint-cil.2.0.5"
+    "git+https://github.com/goblint/cil.git#c79208b21ea61d7b72eae29a18c1ddeda4795dfd"
   ]
   [
     "camlidl.1.12"
diff --git a/goblint.opam.template b/goblint.opam.template
index 0a517fbfa0..84dcc24d8d 100644
--- a/goblint.opam.template
+++ b/goblint.opam.template
@@ -2,7 +2,8 @@
 # also remember to generate/adjust goblint.opam.locked!
 available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
 pin-depends: [
-  [ "goblint-cil.2.0.4" "git+https://github.com/goblint/cil.git#9f4fac450c02bc61a13717784515056b185794cd" ]
+  # published goblint-cil 2.0.5 is currently up-to-date, but pinned for reproducibility
+  [ "goblint-cil.2.0.5" "git+https://github.com/goblint/cil.git#c79208b21ea61d7b72eae29a18c1ddeda4795dfd" ]
   # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new camlidl release
   [ "camlidl.1.12" "git+https://github.com/xavierleroy/camlidl.git#1c1e87e3f56c2c6b3226dd0af3510ef414b462d0" ]
   # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release
diff --git a/gobview b/gobview
index 76e42c34d3..8e1b755ebc 160000
--- a/gobview
+++ b/gobview
@@ -1 +1 @@
-Subproject commit 76e42c34d36bd2ab6900efd661a972ba4824f065
+Subproject commit 8e1b755ebc5fb479095fb4dcc30305fe02501e47
diff --git a/lib/sv-comp/stub/src/sv-comp.c b/lib/sv-comp/stub/src/sv-comp.c
index 12c04125d6..469a641e73 100644
--- a/lib/sv-comp/stub/src/sv-comp.c
+++ b/lib/sv-comp/stub/src/sv-comp.c
@@ -35,10 +35,10 @@ __VERIFIER_nondet2(unsigned int, u32)
 __VERIFIER_nondet2(unsigned short int, u16) // not in rules
 __VERIFIER_nondet2(unsigned char, u8) // not in rules
 __VERIFIER_nondet2(unsigned char, unsigned_char) // not in rules
-__VERIFIER_nondet2(long long, longlong) // not in rules yet (https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/issues/1341)
-__VERIFIER_nondet2(unsigned long long, ulonglong) // not in rules yet (https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/issues/1341)
-__VERIFIER_nondet2(__uint128_t, uint128) // not in rules yet (https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/issues/1341)
-__VERIFIER_nondet2(__int128_t, int128) // not in rules yet (https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/issues/1341)
+__VERIFIER_nondet2(long long, longlong)
+__VERIFIER_nondet2(unsigned long long, ulonglong)
+__VERIFIER_nondet2(__uint128_t, uint128)
+__VERIFIER_nondet2(__int128_t, int128)
 __VERIFIER_nondet2(unsigned char, uchar)
 __VERIFIER_nondet2(unsigned int, uint)
 __VERIFIER_nondet2(unsigned long, ulong)
diff --git a/scripts/sv-comp/archive.sh b/scripts/sv-comp/archive.sh
index 37fa2758d9..aefac8f769 100755
--- a/scripts/sv-comp/archive.sh
+++ b/scripts/sv-comp/archive.sh
@@ -4,7 +4,7 @@
 
 make clean
 
-git tag -m "SV-COMP 2024" svcomp24
+git tag -m "SV-COMP 2025" svcomp25
 
 dune build --profile=release src/goblint.exe
 rm -f goblint
@@ -32,8 +32,8 @@ zip goblint/scripts/sv-comp/goblint.zip \
     goblint/lib/libboxD.so \
     goblint/lib/libpolkaMPQ.so \
     goblint/lib/LICENSE.APRON \
-    goblint/conf/svcomp24.json \
-    goblint/conf/svcomp24-validate.json \
+    goblint/conf/svcomp25.json \
+    goblint/conf/svcomp25-validate.json \
     goblint/lib/libc/stub/include/assert.h \
     goblint/lib/goblint/runtime/include/goblint.h \
     goblint/lib/libc/stub/src/stdlib.c \
diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml
index 1c5d0abc7d..df3cf545c5 100644
--- a/src/analyses/apron/relationAnalysis.apron.ml
+++ b/src/analyses/apron/relationAnalysis.apron.ml
@@ -702,7 +702,7 @@ struct
           Priv.lock ask ctx.global st m
         ) st addr
     | Events.Unlock addr when ThreadFlag.has_ever_been_multi ask -> (* TODO: is this condition sound? *)
-      WideningTokens.with_local_side_tokens (fun () ->
+      WideningTokenLifter.with_local_side_tokens (fun () ->
           CommonPriv.lift_unlock ask (fun st m ->
               Priv.unlock ask ctx.global ctx.sideg st m
             ) st addr
@@ -713,7 +713,7 @@ struct
       Priv.escape ctx.node (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg st escaped
     | Assert exp ->
       assert_fn ctx exp true
-    | Events.Unassume {exp = e; uuids} ->
+    | Events.Unassume {exp = e; tokens} ->
       let e_orig = e in
       let ask = Analyses.ask_of_ctx ctx in
       let e = replace_deref_exps ctx.ask e in
@@ -749,7 +749,7 @@ struct
 
       (* TODO: parallel write_global? *)
       let st =
-        WideningTokens.with_side_tokens (WideningTokens.TS.of_list uuids) (fun () ->
+        WideningTokenLifter.with_side_tokens (WideningTokenLifter.TS.of_list tokens) (fun () ->
             VH.fold (fun v v_in st ->
                 (* TODO: is this sideg fine? *)
                 write_global ask ctx.global ctx.sideg st v v_in
@@ -783,7 +783,7 @@ struct
       let new_value = RD.join old_value st in
       PCU.RH.replace results ctx.node new_value;
     end;
-    WideningTokens.with_local_side_tokens (fun () ->
+    WideningTokenLifter.with_local_side_tokens (fun () ->
         Priv.sync (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg ctx.local (reason :> [`Normal | `Join | `JoinCall of CilType.Fundec.t | `Return | `Init | `Thread])
       )
 
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index c7a4dfba49..f6e41361a3 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -445,7 +445,7 @@ struct
     in
     if M.tracing then M.tracel "sync" "sync multi=%B earlyglobs=%B" multi !earlyglobs;
     if !earlyglobs || multi then
-      WideningTokens.with_local_side_tokens (fun () ->
+      WideningTokenLifter.with_local_side_tokens (fun () ->
           Priv.sync (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) (priv_sideg ctx.sideg) ctx.local reason
         )
     else
@@ -3092,7 +3092,7 @@ struct
     (* Perform actual [set]-s with final unassumed values.
        This invokes [Priv.write_global], which was suppressed above. *)
     let e_d' =
-      WideningTokens.with_side_tokens (WideningTokens.TS.of_list uuids) (fun () ->
+      WideningTokenLifter.with_side_tokens (WideningTokenLifter.TS.of_list uuids) (fun () ->
           CPA.fold (fun x v acc ->
               let addr: AD.t = AD.of_mval (x, `NoOffset) in
               set ~ctx ~invariant:false acc addr x.vtype v
@@ -3111,7 +3111,7 @@ struct
           Priv.lock ask (priv_getg ctx.global) st m
         ) st addr
     | Events.Unlock addr when ThreadFlag.has_ever_been_multi ask -> (* TODO: is this condition sound? *)
-      WideningTokens.with_local_side_tokens (fun () ->
+      WideningTokenLifter.with_local_side_tokens (fun () ->
           CommonPriv.lift_unlock ask (fun st m ->
               Priv.unlock ask (priv_getg ctx.global) (priv_sideg ctx.sideg) st m
             ) st addr
@@ -3125,8 +3125,8 @@ struct
       set ~ctx ctx.local (eval_lv ~ctx ctx.local lval) (Cilfacade.typeOfLval lval) (Thread (ValueDomain.Threads.singleton tid))
     | Events.Assert exp ->
       assert_fn ctx exp true
-    | Events.Unassume {exp; uuids} ->
-      Timing.wrap "base unassume" (unassume ctx exp) uuids
+    | Events.Unassume {exp; tokens} ->
+      Timing.wrap "base unassume" (unassume ctx exp) tokens
     | Events.Longjmped {lval} ->
       begin match lval with
         | Some lval ->
diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml
index 51a27e19f8..52f0888d3f 100644
--- a/src/analyses/baseInvariant.ml
+++ b/src/analyses/baseInvariant.ml
@@ -777,33 +777,37 @@ struct
             | _ -> assert false
           end
         | Const _ , _ -> st (* nothing to do *)
-        | CastE ((TFloat (_, _)), e), Float c ->
-          (match unrollType (Cilfacade.typeOf e), FD.get_fkind c with
-           | TFloat (FLongDouble as fk, _), FFloat
-           | TFloat (FDouble as fk, _), FFloat
-           | TFloat (FLongDouble as fk, _), FDouble
-           | TFloat (fk, _), FLongDouble
-           | TFloat (FDouble as fk, _), FDouble
-           | TFloat (FFloat as fk, _), FFloat -> inv_exp (Float (FD.cast_to fk c)) e st
-           | _ -> fallback (fun () -> Pretty.text "CastE: incompatible types") st)
-        | CastE ((TInt (ik, _)) as t, e), Int c
-        | CastE ((TEnum ({ekind = ik; _ }, _)) as t, e), Int c -> (* Can only meet the t part of an Lval in e with c (unless we meet with all overflow possibilities)! Since there is no good way to do this, we only continue if e has no values outside of t. *)
-          (match eval e st with
-           | Int i ->
-             (match unrollType (Cilfacade.typeOf e) with
-              | (TInt(ik_e, _) as t')
-              | (TEnum ({ekind = ik_e; _ }, _) as t') ->
-                if VD.is_dynamically_safe_cast t t' (Int i) then
-                  (* let c' = ID.cast_to ik_e c in *)
-                  (* Suppressing overflow warnings as this is not a computation that comes from the program *)
-                  let res_range = (ID.cast_to ~suppress_ovwarn:true ik (ID.top_of ik_e)) in
-                  let c' = ID.cast_to ik_e (ID.meet c res_range) in (* TODO: cast without overflow, is this right for normal invariant? *)
-                  if M.tracing then M.tracel "inv" "cast: %a from %a to %a: i = %a; cast c = %a to %a = %a" d_exp e d_ikind ik_e d_ikind ik ID.pretty i ID.pretty c d_ikind ik_e ID.pretty c';
-                  inv_exp (Int c') e st
-                else
-                  fallback (fun () -> Pretty.dprintf "CastE: %a evaluates to %a which is bigger than the type it is cast to which is %a" d_plainexp e ID.pretty i CilType.Typ.pretty t) st
-              | x -> fallback (fun () -> Pretty.dprintf "CastE: e did evaluate to Int, but the type did not match %a" CilType.Typ.pretty t) st)
-           | v -> fallback (fun () -> Pretty.dprintf "CastE: e did not evaluate to Int, but %a" VD.pretty v) st)
+        | CastE (t, e), c_typed ->
+          begin match Cil.unrollType t, c_typed with
+            | TFloat (_, _), Float c ->
+              (match unrollType (Cilfacade.typeOf e), FD.get_fkind c with
+               | TFloat (FLongDouble as fk, _), FFloat
+               | TFloat (FDouble as fk, _), FFloat
+               | TFloat (FLongDouble as fk, _), FDouble
+               | TFloat (fk, _), FLongDouble
+               | TFloat (FDouble as fk, _), FDouble
+               | TFloat (FFloat as fk, _), FFloat -> inv_exp (Float (FD.cast_to fk c)) e st
+               | _ -> fallback (fun () -> Pretty.text "CastE: incompatible types") st)
+            | (TInt (ik, _) as t), Int c
+            | (TEnum ({ekind = ik; _ }, _) as t), Int c -> (* Can only meet the t part of an Lval in e with c (unless we meet with all overflow possibilities)! Since there is no good way to do this, we only continue if e has no values outside of t. *)
+              (match eval e st with
+               | Int i ->
+                 (match unrollType (Cilfacade.typeOf e) with
+                  | (TInt(ik_e, _) as t')
+                  | (TEnum ({ekind = ik_e; _ }, _) as t') ->
+                    if VD.is_dynamically_safe_cast t t' (Int i) then
+                      (* let c' = ID.cast_to ik_e c in *)
+                      (* Suppressing overflow warnings as this is not a computation that comes from the program *)
+                      let res_range = (ID.cast_to ~suppress_ovwarn:true ik (ID.top_of ik_e)) in
+                      let c' = ID.cast_to ik_e (ID.meet c res_range) in (* TODO: cast without overflow, is this right for normal invariant? *)
+                      if M.tracing then M.tracel "inv" "cast: %a from %a to %a: i = %a; cast c = %a to %a = %a" d_exp e d_ikind ik_e d_ikind ik ID.pretty i ID.pretty c d_ikind ik_e ID.pretty c';
+                      inv_exp (Int c') e st
+                    else
+                      fallback (fun () -> Pretty.dprintf "CastE: %a evaluates to %a which is bigger than the type it is cast to which is %a" d_plainexp e ID.pretty i CilType.Typ.pretty t) st
+                  | x -> fallback (fun () -> Pretty.dprintf "CastE: e did evaluate to Int, but the type did not match %a" CilType.Typ.pretty t) st)
+               | v -> fallback (fun () -> Pretty.dprintf "CastE: e did not evaluate to Int, but %a" VD.pretty v) st)
+            | _, _ -> fallback (fun () -> Pretty.dprintf "CastE: %a not implemented" d_plainexp (CastE (t, e))) st
+          end
         | e, _ -> fallback (fun () -> Pretty.dprintf "%a not implemented" d_plainexp e) st
     in
     if eval_bool exp st = Some (not tv) then contra st (* we already know that the branch is dead *)
diff --git a/src/analyses/mCP.ml b/src/analyses/mCP.ml
index 9923bfe956..f2f36b1360 100644
--- a/src/analyses/mCP.ml
+++ b/src/analyses/mCP.ml
@@ -156,20 +156,20 @@ struct
     else
       iter (uncurry spawn_one) @@ group_assoc_eq Basetype.Variables.equal xs
 
-  let do_sideg ctx (xs:(V.t * (WideningTokens.TS.t * G.t)) list) =
+  let do_sideg ctx (xs:(V.t * (WideningTokenLifter.TS.t * G.t)) list) =
     let side_one v dts =
       let side_one_ts ts d =
         (* Do side effects with the tokens that were active at the time.
            Transfer functions have exited the with_side_token wrappers by now. *)
-        let old_side_tokens = !WideningTokens.side_tokens in
-        WideningTokens.side_tokens := ts;
+        let old_side_tokens = !WideningTokenLifter.side_tokens in
+        WideningTokenLifter.side_tokens := ts;
         Fun.protect (fun () ->
             ctx.sideg v @@ fold_left G.join (G.bot ()) d
           ) ~finally:(fun () ->
-            WideningTokens.side_tokens := old_side_tokens
+            WideningTokenLifter.side_tokens := old_side_tokens
           )
       in
-      iter (uncurry side_one_ts) @@ group_assoc_eq WideningTokens.TS.equal dts
+      iter (uncurry side_one_ts) @@ group_assoc_eq WideningTokenLifter.TS.equal dts
     in
     iter (uncurry side_one) @@ group_assoc_eq V.equal xs
 
@@ -359,7 +359,7 @@ struct
       | None -> (fun ?(multiple=false) v d    -> failwith ("Cannot \"spawn\" in " ^ tfname ^ " context."))
     in
     let sideg = match sides with
-      | Some sides -> (fun v g    -> sides  := (v, (!WideningTokens.side_tokens, g)) :: !sides)
+      | Some sides -> (fun v g    -> sides  := (v, (!WideningTokenLifter.side_tokens, g)) :: !sides)
       | None -> (fun v g       -> failwith ("Cannot \"sideg\" in " ^ tfname ^ " context."))
     in
     let emit = match emits with
diff --git a/src/analyses/unassumeAnalysis.ml b/src/analyses/unassumeAnalysis.ml
index d95c3f9989..1b430e651a 100644
--- a/src/analyses/unassumeAnalysis.ml
+++ b/src/analyses/unassumeAnalysis.ml
@@ -29,7 +29,7 @@ struct
 
   type inv = {
     exp: Cil.exp;
-    uuid: string;
+    token: WideningToken.t;
   }
 
   let invs: inv NH.t = NH.create 100
@@ -71,7 +71,7 @@ struct
         | _ -> ()
       );
 
-    let yaml = match Yaml_unix.of_file (Fpath.v (GobConfig.get_string "witness.yaml.unassume")) with
+    let yaml = match GobResult.Syntax.(Fpath.of_string (GobConfig.get_string "witness.yaml.unassume") >>= Yaml_unix.of_file) with
       | Ok yaml -> yaml
       | Error (`Msg m) ->
         Logs.error "Yaml_unix.of_file: %s" m;
@@ -90,7 +90,7 @@ struct
       let uuid = entry.metadata.uuid in
       let target_type = YamlWitnessType.EntryType.entry_type entry.entry_type in
 
-      let unassume_nodes_invariant ~loc ~nodes inv =
+      let unassume_nodes_invariant ~loc ~nodes ?i inv =
         let msgLoc: M.Location.t = CilLocation loc in
         match InvariantParser.parse_cabs inv with
         | Ok inv_cabs ->
@@ -101,7 +101,7 @@ struct
               match InvariantParser.parse_cil inv_parser ~check:false ~fundec ~loc inv_cabs with
               | Ok inv_exp ->
                 M.debug ~category:Witness ~loc:msgLoc "located invariant to %a: %a" Node.pretty n Cil.d_exp inv_exp;
-                NH.add invs n {exp = inv_exp; uuid}
+                NH.add invs n {exp = inv_exp; token = (uuid, i)}
               | Error e ->
                 M.error ~category:Witness ~loc:msgLoc "CIL couldn't parse invariant: %s" inv;
                 M.info ~category:Witness ~loc:msgLoc "invariant has undefined variables or side effects: %s" inv
@@ -154,7 +154,7 @@ struct
                     M.debug ~category:Witness ~loc:msgLoc "located invariant to %a: %a" Node.pretty n Cil.d_exp inv_exp;
                     if not (NH.mem pre_invs n) then
                       NH.replace pre_invs n (EH.create 10);
-                    EH.add (NH.find pre_invs n) pre_exp {exp = inv_exp; uuid}
+                    EH.add (NH.find pre_invs n) pre_exp {exp = inv_exp; token = (uuid, None)}
                   | Error e ->
                     M.error ~category:Witness ~loc:msgLoc "CIL couldn't parse invariant: %s" inv;
                     M.info ~category:Witness ~loc:msgLoc "invariant has undefined variables or side effects: %s" inv
@@ -189,42 +189,42 @@ struct
 
       let unassume_invariant_set (invariant_set: YamlWitnessType.InvariantSet.t) =
 
-        let unassume_location_invariant (location_invariant: YamlWitnessType.InvariantSet.LocationInvariant.t) =
+        let unassume_location_invariant ~i (location_invariant: YamlWitnessType.InvariantSet.LocationInvariant.t) =
           let loc = YamlWitness.loc_of_location location_invariant.location in
           let inv = location_invariant.value in
           let msgLoc: M.Location.t = CilLocation loc in
 
           match Locator.find_opt location_locator loc with
           | Some nodes ->
-            unassume_nodes_invariant ~loc ~nodes inv
+            unassume_nodes_invariant ~loc ~nodes ~i inv
           | None ->
             M.warn ~category:Witness ~loc:msgLoc "couldn't locate invariant: %s" inv
         in
 
-        let unassume_loop_invariant (loop_invariant: YamlWitnessType.InvariantSet.LoopInvariant.t) =
+        let unassume_loop_invariant ~i (loop_invariant: YamlWitnessType.InvariantSet.LoopInvariant.t) =
           let loc = YamlWitness.loc_of_location loop_invariant.location in
           let inv = loop_invariant.value in
           let msgLoc: M.Location.t = CilLocation loc in
 
           match Locator.find_opt loop_locator loc with
           | Some nodes ->
-            unassume_nodes_invariant ~loc ~nodes inv
+            unassume_nodes_invariant ~loc ~nodes ~i inv
           | None ->
             M.warn ~category:Witness ~loc:msgLoc "couldn't locate invariant: %s" inv
         in
 
-        let validate_invariant (invariant: YamlWitnessType.InvariantSet.Invariant.t) =
+        let validate_invariant i (invariant: YamlWitnessType.InvariantSet.Invariant.t) =
           let target_type = YamlWitnessType.InvariantSet.InvariantType.invariant_type invariant.invariant_type in
           match YamlWitness.invariant_type_enabled target_type, invariant.invariant_type with
           | true, LocationInvariant x ->
-            unassume_location_invariant x
+            unassume_location_invariant ~i x
           | true, LoopInvariant x ->
-            unassume_loop_invariant x
+            unassume_loop_invariant ~i x
           | false, (LocationInvariant _ | LoopInvariant _) ->
             M.info_noloc ~category:Witness "disabled invariant of type %s" target_type
         in
 
-        List.iter validate_invariant invariant_set.content
+        List.iteri validate_invariant invariant_set.content
       in
 
       match YamlWitness.entry_type_enabled target_type, entry.entry_type with
@@ -262,9 +262,9 @@ struct
       M.info ~category:Witness "unassume invariant: %a" CilType.Exp.pretty e;
       if not !AnalysisState.postsolving then (
         if not (GobConfig.get_bool "ana.unassume.precheck" && Queries.ID.to_bool (ctx.ask (EvalInt e)) = Some false) then (
-          let uuids = x.uuid :: List.map (fun {uuid; _} -> uuid) xs in
-          ctx.emit (Unassume {exp = e; uuids});
-          List.iter WideningTokens.add uuids
+          let tokens = x.token :: List.map (fun {token; _} -> token) xs in
+          ctx.emit (Unassume {exp = e; tokens});
+          List.iter WideningTokenLifter.add tokens
         )
       );
       ctx.local
diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml
index 03ac3ed3f0..043b728799 100644
--- a/src/cdomains/apron/apronDomain.apron.ml
+++ b/src/cdomains/apron/apronDomain.apron.ml
@@ -19,7 +19,7 @@ module M = Messages
 
 let widening_thresholds_apron = ResettableLazy.from_fun (fun () ->
     let t = if GobConfig.get_string "ana.apron.threshold_widening_constants" = "comparisons" then WideningThresholds.octagon_thresholds () else WideningThresholds.thresholds_incl_mul2 () in
-    let r = List.map (fun x -> Apron.Scalar.of_mpqf @@ Mpqf.of_mpz @@ Z_mlgmpidl.mpz_of_z x) t in
+    let r = List.map Scalar.of_z t in
     Array.of_list r
   )
 
diff --git a/src/cdomains/apron/gobApron.apron.ml b/src/cdomains/apron/gobApron.apron.ml
index fbb1fe9ec5..327e43e321 100644
--- a/src/cdomains/apron/gobApron.apron.ml
+++ b/src/cdomains/apron/gobApron.apron.ml
@@ -12,6 +12,8 @@ struct
       let pp = pp
     end
     )
+
+  let of_z z = of_mpqf (Mpqf.of_mpz (Z_mlgmpidl.mpz_of_z z))
 end
 
 module Coeff =
diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml
index c1ca3661a5..6af7030a51 100644
--- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml
+++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml
@@ -790,7 +790,7 @@ struct
     let of_coeff xi coeffs o =
       let typ = (Option.get @@ V.to_cil_varinfo xi).vtype in
       let ikind = Cilfacade.get_ikind typ in
-      let cst = Coeff.s_of_mpqf @@ Mpqf.of_mpz (Z_mlgmpidl.mpz_of_z @@ IntDomain.Size.cast ikind o) in
+      let cst = Coeff.s_of_z (IntDomain.Size.cast ikind o) in
       let lincons = Lincons1.make (Linexpr1.make t.env) Lincons1.EQ in
       Lincons1.set_list lincons coeffs (Some cst);
       lincons
diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml
index 86b5f2770f..b9d93bfd99 100644
--- a/src/cdomains/apron/sharedFunctions.apron.ml
+++ b/src/cdomains/apron/sharedFunctions.apron.ml
@@ -133,7 +133,7 @@ struct
           else
             failwith "texpr1_expr_of_cil_exp: globals must be replaced with temporary locals"
         | Const (CInt (i, _, _)) ->
-          Cst (Coeff.s_of_mpqf (Mpqf.of_mpz (Z_mlgmpidl.mpz_of_z i)))
+          Cst (Coeff.s_of_z i)
         | exp ->
           match Cilfacade.get_ikind_exp exp with
           | ik ->
@@ -175,7 +175,7 @@ struct
                     (* convert response to a constant *)
                     let const = IntDomain.IntDomTuple.to_int @@ IntDomain.IntDomTuple.cast_to t_ik res in
                     match const with
-                    | Some c -> Cst (Coeff.s_of_mpqf (Mpqf.of_mpz (Z_mlgmpidl.mpz_of_z c))) (* Got a constant value -> use it straight away *)
+                    | Some c -> Cst (Coeff.s_of_z c) (* Got a constant value -> use it straight away *)
                     (* I gotten top, we can not guarantee injectivity *)
                     | None -> if IntDomain.IntDomTuple.is_top_of t_ik res then raise (Unsupported_CilExp (Cast_not_injective t))
                       else ( (* Got a ranged value different from top, so let's check bounds manually *)
diff --git a/src/config/options.schema.json b/src/config/options.schema.json
index 362e028ee3..43e2ad1d59 100644
--- a/src/config/options.schema.json
+++ b/src/config/options.schema.json
@@ -2715,7 +2715,7 @@
             },
             "strict": {
               "title": "witness.yaml.strict",
-              "description": "",
+              "description": "Fail YAML witness validation if there's an error/unsupported/disabled entry.",
               "type": "boolean",
               "default": false
             },
diff --git a/src/domains/events.ml b/src/domains/events.ml
index b194847bac..cf12900c98 100644
--- a/src/domains/events.ml
+++ b/src/domains/events.ml
@@ -14,7 +14,7 @@ type t =
   | Assign of {lval: CilType.Lval.t; exp: CilType.Exp.t} (** Used to simulate old [ctx.assign]. *) (* TODO: unused *)
   | UpdateExpSplit of exp (** Used by expsplit analysis to evaluate [exp] on post-state. *)
   | Assert of exp
-  | Unassume of {exp: CilType.Exp.t; uuids: string list}
+  | Unassume of {exp: CilType.Exp.t; tokens: WideningToken.t list}
   | Longjmped of {lval: CilType.Lval.t option}
 
 (** Should event be emitted after transfer function raises [Deadcode]? *)
@@ -45,5 +45,5 @@ let pretty () = function
   | Assign {lval; exp} -> dprintf "Assign {lval=%a, exp=%a}" CilType.Lval.pretty lval CilType.Exp.pretty exp
   | UpdateExpSplit exp -> dprintf "UpdateExpSplit %a" d_exp exp
   | Assert exp -> dprintf "Assert %a" d_exp exp
-  | Unassume {exp; uuids} -> dprintf "Unassume {exp=%a; uuids=%a}" d_exp exp (docList Pretty.text) uuids
+  | Unassume {exp; tokens} -> dprintf "Unassume {exp=%a; tokens=%a}" d_exp exp (d_list ", " WideningToken.pretty) tokens
   | Longjmped {lval} -> dprintf "Longjmped {lval=%a}" (docOpt (CilType.Lval.pretty ())) lval
diff --git a/src/framework/control.ml b/src/framework/control.ml
index 1d0ebb869b..2566939817 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -39,7 +39,7 @@ let spec_module: (module Spec) Lazy.t = lazy (
       |> lift (get_bool "ana.opt.hashcons") (module HashconsLifter)
       (* Widening tokens must be outside of hashcons, because widening token domain ignores token sets for identity, so hashcons doesn't allow adding tokens.
          Also must be outside of deadcode, because deadcode splits (like mutex lock event) don't pass on tokens. *)
-      |> lift (get_bool "ana.widen.tokens") (module WideningTokens.Lifter)
+      |> lift (get_bool "ana.widen.tokens") (module WideningTokenLifter.Lifter)
       |> lift true (module LongjmpLifter.Lifter)
       |> lift termination_enabled (module RecursionTermLifter.Lifter) (* Always activate the recursion termination analysis, when the loop termination analysis is activated*)
     )
diff --git a/src/goblint_lib.ml b/src/goblint_lib.ml
index 16d8a29d16..415fb21605 100644
--- a/src/goblint_lib.ml
+++ b/src/goblint_lib.ml
@@ -181,7 +181,8 @@ module SpecLifters = SpecLifters
 module LongjmpLifter = LongjmpLifter
 module RecursionTermLifter = RecursionTermLifter
 module ContextGasLifter = ContextGasLifter
-module WideningTokens = WideningTokens
+module WideningToken = WideningToken
+module WideningTokenLifter = WideningTokenLifter
 
 module WitnessConstraints = WitnessConstraints
 
diff --git a/src/lifters/wideningToken.ml b/src/lifters/wideningToken.ml
new file mode 100644
index 0000000000..0639521038
--- /dev/null
+++ b/src/lifters/wideningToken.ml
@@ -0,0 +1,16 @@
+(** Widening token for {!WideningTokenLifter}. *)
+
+module Uuid =
+struct
+  include Basetype.RawStrings
+  let name () = "uuid"
+end
+
+module Index =
+struct
+  include Printable.Option (IntDomain.Integers (IntOps.NIntOps)) (struct let name = "None" end)
+  let name () = "index"
+end
+
+(* Change to variant type if need other tokens than witness UUIDs. *)
+include Printable.Prod (Uuid) (Index)
diff --git a/src/lifters/wideningTokens.ml b/src/lifters/wideningTokenLifter.ml
similarity index 98%
rename from src/lifters/wideningTokens.ml
rename to src/lifters/wideningTokenLifter.ml
index 41bb5d8477..634468a9ca 100644
--- a/src/lifters/wideningTokens.ml
+++ b/src/lifters/wideningTokenLifter.ml
@@ -6,8 +6,7 @@
 
     @see <http://www2.in.tum.de/bib/files/mihaila13widening.pdf> Mihaila, B., Sepp, A. & Simon, A. Widening as Abstract Domain. *)
 
-(** Widening token. *)
-module Token = Basetype.RawStrings (* Change to variant type if need other tokens than witness UUIDs. *)
+module Token = WideningToken
 
 (** Widening token set. *)
 module TS = SetDomain.ToppedSet (Token) (struct let topname = "Top" end)
diff --git a/src/util/library/libraryFunctions.ml b/src/util/library/libraryFunctions.ml
index af5c2ae927..6643b58eef 100644
--- a/src/util/library/libraryFunctions.ml
+++ b/src/util/library/libraryFunctions.ml
@@ -6,6 +6,16 @@ open GobConfig
 
 module M = Messages
 
+let intmax_t = lazy (
+  let res = ref None in
+  GoblintCil.iterGlobals !Cilfacade.current_file (function
+      | GType ({tname = "intmax_t"; ttype; _}, _) ->
+        res := Some ttype;
+      | _ -> ()
+    );
+  !res
+)
+
 (** C standard library functions.
     These are specified by the C standard. *)
 let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
@@ -139,7 +149,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("abs", special [__ "j" []] @@ fun j -> Math { fun_args = (Abs (IInt, j)) });
     ("labs", special [__ "j" []] @@ fun j -> Math { fun_args = (Abs (ILong, j)) });
     ("llabs", special [__ "j" []] @@ fun j -> Math { fun_args = (Abs (ILongLong, j)) });
-    ("imaxabs", unknown [drop "j" []]);
+    ("imaxabs", special [__ "j" []] @@ fun j -> Math { fun_args = (Abs (Cilfacade.get_ikind (Option.get (Lazy.force intmax_t)), j)) });
     ("localtime_r", unknown [drop "timep" [r]; drop "result" [w]]);
     ("strpbrk", unknown [drop "s" [r]; drop "accept" [r]]);
     ("_setjmp", special [__ "env" [w]] @@ fun env -> Setjmp { env }); (* only has one underscore *)
diff --git a/src/util/std/gobYaml.ml b/src/util/std/gobYaml.ml
index 624cdbf1fa..4c8576ade2 100644
--- a/src/util/std/gobYaml.ml
+++ b/src/util/std/gobYaml.ml
@@ -44,3 +44,5 @@ let list = function
 let entries = function
   | `O assoc -> Ok assoc
   | _ -> Error (`Msg "Failed to get entries from non-object value")
+
+let int i = float (float_of_int i)
diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index ec9a542919..e3978f9929 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -278,6 +278,11 @@ struct
 
     let entries = [] in
 
+    let cnt_loop_invariant = ref 0 in
+    let cnt_location_invariant = ref 0 in
+    let cnt_flow_insensitive_invariant = ref 0 in
+    (* TODO: precondition invariants? *)
+
     (* Generate location invariants (without precondition) *)
     let entries =
       if entry_type_enabled YamlWitnessType.LocationInvariant.entry_type then (
@@ -297,6 +302,7 @@ struct
               List.fold_left (fun acc inv ->
                   let invariant = Entry.invariant (CilType.Exp.show inv) in
                   let entry = Entry.location_invariant ~task ~location ~invariant in
+                  incr cnt_location_invariant;
                   entry :: acc
                 ) acc invs
             | `Bot | `Top -> (* TODO: 0 for bot (dead code)? *)
@@ -326,6 +332,7 @@ struct
                 List.fold_left (fun acc inv ->
                     let invariant = Entry.invariant (CilType.Exp.show inv) in
                     let entry = Entry.loop_invariant ~task ~location ~invariant in
+                    incr cnt_loop_invariant;
                     entry :: acc
                   ) acc invs
               | `Bot | `Top -> (* TODO: 0 for bot (dead code)? *)
@@ -371,6 +378,7 @@ struct
                   List.fold_left (fun acc inv ->
                       let invariant = Entry.invariant (CilType.Exp.show inv) in
                       let entry = Entry.flow_insensitive_invariant ~task ~invariant in
+                      incr cnt_flow_insensitive_invariant;
                       entry :: acc
                     ) acc invs
                 | `Lifted inv, "location_invariant" ->
@@ -542,6 +550,7 @@ struct
                   List.fold_left (fun acc inv ->
                       let invariant = CilType.Exp.show inv in
                       let invariant = Entry.location_invariant' ~location ~invariant in
+                      incr cnt_location_invariant;
                       invariant :: acc
                     ) acc invs
                 | `Bot | `Top -> (* TODO: 0 for bot (dead code)? *)
@@ -571,6 +580,7 @@ struct
                     List.fold_left (fun acc inv ->
                         let invariant = CilType.Exp.show inv in
                         let invariant = Entry.loop_invariant' ~location ~invariant in
+                        incr cnt_loop_invariant;
                         invariant :: acc
                       ) acc invs
                   | `Bot | `Top -> (* TODO: 0 for bot (dead code)? *)
@@ -619,6 +629,9 @@ struct
     let yaml_entries = List.rev_map YamlWitnessType.Entry.to_yaml entries in (* reverse to make entries in file in the same order as generation messages *)
 
     M.msg_group Info ~category:Witness "witness generation summary" [
+      (Pretty.dprintf "location invariants: %d" !cnt_location_invariant, None);
+      (Pretty.dprintf "loop invariants: %d" !cnt_loop_invariant, None);
+      (Pretty.dprintf "flow-insensitive invariants: %d" !cnt_flow_insensitive_invariant, None);
       (Pretty.dprintf "total generation entries: %d" (List.length yaml_entries), None);
     ];
 
@@ -702,7 +715,7 @@ struct
 
     let inv_parser = InvariantParser.create FileCfg.file in
 
-    let yaml = match Yaml_unix.of_file (Fpath.v (GobConfig.get_string "witness.yaml.validate")) with
+    let yaml = match GobResult.Syntax.(Fpath.of_string (GobConfig.get_string "witness.yaml.validate") >>= Yaml_unix.of_file) with
       | Ok yaml -> yaml
       | Error (`Msg m) ->
         Logs.error "Yaml_unix.of_file: %s" m;
@@ -986,7 +999,9 @@ struct
     | true when !cnt_disabled > 0 ->
       Error "witness disabled"
     | _ when !cnt_refuted > 0 ->
-      Ok (Svcomp.Result.False None)
+      (* Refuted only when assuming the invariant is reachable. *)
+      (* Ok (Svcomp.Result.False None) *) (* Wasn't a problem because valid*->correctness->false gave 0 points under old validator track scoring schema: https://doi.org/10.1007/978-3-031-22308-2_8. *)
+      Ok Svcomp.Result.Unknown (* Now valid*->correctness->false gives 1p (negative) points under new validator track scoring schema: https://doi.org/10.1007/978-3-031-57256-2_15. *)
     | _ when !cnt_unconfirmed > 0 ->
       Ok Unknown
     | _ ->
diff --git a/src/witness/yamlWitnessType.ml b/src/witness/yamlWitnessType.ml
index bcd8e9435f..7a57197a6f 100644
--- a/src/witness/yamlWitnessType.ml
+++ b/src/witness/yamlWitnessType.ml
@@ -450,15 +450,35 @@ struct
 
   module Constraint =
   struct
+
+    module Value =
+    struct
+      type t =
+        | String of string
+        | Int of int (* Why doesn't format consider ints (for switch branches) as strings here, like everywhere else? *)
+      [@@deriving eq, ord, hash]
+
+      let to_yaml = function
+        | String s -> GobYaml.string s
+        | Int i -> GobYaml.int i
+
+      let of_yaml y =
+        let open GobYaml in
+        match y with
+        | `String s -> Ok (String s)
+        | `Float f -> Ok (Int (int_of_float f))
+        | _ -> Error (`Msg "Expected a string or integer value")
+    end
+
     type t = {
-      value: string;
+      value: Value.t;
       format: string option;
     }
     [@@deriving eq, ord, hash]
 
     let to_yaml {value; format} =
       `O ([
-          ("value", `String value);
+          ("value", Value.to_yaml value);
         ] @ (match format with
           | Some format -> [
               ("format", `String format);
@@ -469,7 +489,7 @@ struct
 
     let of_yaml y =
       let open GobYaml in
-      let+ value = y |> find "value" >>= to_string
+      let+ value = y |> find "value" >>= Value.of_yaml
       and+ format = y |> Yaml.Util.find "format" >>= option_map to_string in
       {value; format}
   end
diff --git a/tests/regression/03-practical/35-base-mutex-macos.t b/tests/regression/03-practical/35-base-mutex-macos.t
index 9e5f36d337..1d8a184d4c 100644
--- a/tests/regression/03-practical/35-base-mutex-macos.t
+++ b/tests/regression/03-practical/35-base-mutex-macos.t
@@ -4,6 +4,9 @@
     dead: 0
     total lines: 2
   [Info][Witness] witness generation summary:
+    location invariants: 0
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 1
 
 There should be no invariants about __sig.
diff --git a/tests/regression/13-privatized/01-priv_nr.t b/tests/regression/13-privatized/01-priv_nr.t
index bbc285098a..0186709027 100644
--- a/tests/regression/13-privatized/01-priv_nr.t
+++ b/tests/regression/13-privatized/01-priv_nr.t
@@ -10,6 +10,9 @@
     dead: 0
     total lines: 19
   [Info][Witness] witness generation summary:
+    location invariants: 3
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 3
   [Info][Race] Memory locations race summary:
     safe: 1
@@ -64,6 +67,9 @@
     dead: 0
     total lines: 19
   [Info][Witness] witness generation summary:
+    location invariants: 3
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 3
   [Info][Race] Memory locations race summary:
     safe: 1
@@ -118,6 +124,9 @@
     dead: 0
     total lines: 19
   [Info][Witness] witness generation summary:
+    location invariants: 3
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 3
   [Info][Race] Memory locations race summary:
     safe: 1
diff --git a/tests/regression/29-svcomp/dune b/tests/regression/29-svcomp/dune
index 95ac66a5ec..9b2396b313 100644
--- a/tests/regression/29-svcomp/dune
+++ b/tests/regression/29-svcomp/dune
@@ -17,4 +17,4 @@
 
 (cram
  (applies_to 36-svcomp-arch)
- (enabled_if (<> %{system} macosx))) ; https://dune.readthedocs.io/en/stable/reference/boolean-language.html
+ (enabled_if %{read:../../util/multilibAvailable})) ; https://dune.readthedocs.io/en/stable/reference/boolean-language.html
diff --git a/tests/regression/36-apron/12-traces-min-rpb1.t b/tests/regression/36-apron/12-traces-min-rpb1.t
index c0ae5c118e..3e2786debe 100644
--- a/tests/regression/36-apron/12-traces-min-rpb1.t
+++ b/tests/regression/36-apron/12-traces-min-rpb1.t
@@ -13,6 +13,9 @@
     write with [lock:{A}, thread:[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]] (conf. 110)  (exp: & g) (12-traces-min-rpb1.c:14:3-14:8)
     read with [mhp:{created={[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]}}, thread:[main]] (conf. 110)  (exp: & g) (12-traces-min-rpb1.c:27:3-27:26)
   [Info][Witness] witness generation summary:
+    location invariants: 3
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 3
   [Info][Race] Memory locations race summary:
     safe: 0
diff --git a/tests/regression/36-apron/52-queuesize.t b/tests/regression/36-apron/52-queuesize.t
index 62851f2ec9..f0a977891a 100644
--- a/tests/regression/36-apron/52-queuesize.t
+++ b/tests/regression/36-apron/52-queuesize.t
@@ -37,6 +37,9 @@ Without diff-box:
   [Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (52-queuesize.c:56:10-56:11)
   [Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (52-queuesize.c:78:12-78:13)
   [Info][Witness] witness generation summary:
+    location invariants: 8
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 8
   [Info][Race] Memory locations race summary:
     safe: 3
@@ -173,6 +176,9 @@ With diff-box:
   [Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (52-queuesize.c:56:10-56:11)
   [Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (52-queuesize.c:78:12-78:13)
   [Info][Witness] witness generation summary:
+    location invariants: 6
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 6
   [Info][Race] Memory locations race summary:
     safe: 3
diff --git a/tests/regression/39-signed-overflows/11-imaxabs.c b/tests/regression/39-signed-overflows/11-imaxabs.c
new file mode 100644
index 0000000000..47bd26569f
--- /dev/null
+++ b/tests/regression/39-signed-overflows/11-imaxabs.c
@@ -0,0 +1,24 @@
+//PARAM: --enable ana.int.interval --set ana.activated[+] tmpSpecial
+#include<stdlib.h>
+#include <stdint.h>
+#include <inttypes.h>
+int main() {
+    int64_t data;
+    if (data > (-0x7fffffffffffffff - 1))
+    {
+        if (imaxabs(data) < 100)
+        {
+            __goblint_check(data < 100);
+            __goblint_check(-100 < data);
+            int64_t result = data * data; // NOWARN
+        }
+
+        if(imaxabs(data) <= 100)
+        {
+            __goblint_check(data <= 100);
+            __goblint_check(-100 <= data);
+            int64_t result = data * data; // NOWARN
+        }
+    }
+    return 8;
+}
diff --git a/tests/regression/39-signed-overflows/12-imaxabs-sqrt.c b/tests/regression/39-signed-overflows/12-imaxabs-sqrt.c
new file mode 100644
index 0000000000..b121645b27
--- /dev/null
+++ b/tests/regression/39-signed-overflows/12-imaxabs-sqrt.c
@@ -0,0 +1,12 @@
+//PARAM: --enable ana.int.interval --enable ana.float.interval --enable ana.float.evaluate_math_functions --set ana.activated[+] tmpSpecial
+#include<math.h>
+#include <stdint.h>
+#include <inttypes.h>
+int main() {
+    int64_t data;
+    if (data > (-0x7fffffffffffffff - 1) && imaxabs((intmax_t)data) <= sqrtl(0x7fffffffffffffffLL))
+    {
+        int64_t result = data * data; // TODO NOWARN
+    }
+    return 8;
+}
diff --git a/tests/regression/39-signed-overflows/13-imaxabs-macos.c b/tests/regression/39-signed-overflows/13-imaxabs-macos.c
new file mode 100644
index 0000000000..745d5b74c4
--- /dev/null
+++ b/tests/regression/39-signed-overflows/13-imaxabs-macos.c
@@ -0,0 +1,25 @@
+//PARAM: --enable ana.int.interval --set ana.activated[+] tmpSpecial
+// 39-signed-overflows/11-imaxabs, but with long long as int64_t instead (https://github.com/goblint/analyzer/pull/1519#issuecomment-2417032186).
+#include<stdlib.h>
+#include <stdint.h>
+#include <inttypes.h>
+int main() {
+    long long data;
+    if (data > (-0x7fffffffffffffff - 1))
+    {
+        if (imaxabs(data) < 100)
+        {
+            __goblint_check(data < 100);
+            __goblint_check(-100 < data);
+            long long result = data * data; // NOWARN
+        }
+
+        if(imaxabs(data) <= 100)
+        {
+            __goblint_check(data <= 100);
+            __goblint_check(-100 <= data);
+            long long result = data * data; // NOWARN
+        }
+    }
+    return 8;
+}
diff --git a/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.t b/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.t
index 3a3b7c43cf..860ffae3bd 100644
--- a/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.t
+++ b/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.t
@@ -211,6 +211,9 @@
   [Warning][Deadcode][CWE-571] condition 'k < 100' (possibly inserted by CIL) is always true (11-unrolled-loop-invariant.c:9:12-9:19)
   [Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (11-unrolled-loop-invariant.c:8:10-8:16)
   [Info][Witness] witness generation summary:
+    location invariants: 11
+    loop invariants: 5
+    flow-insensitive invariants: 0
     total generation entries: 16
 
   $ yamlWitnessStrip < witness.yml
diff --git a/tests/regression/56-witness/05-prec-problem.t b/tests/regression/56-witness/05-prec-problem.t
index 733f16269e..51f92ca203 100644
--- a/tests/regression/56-witness/05-prec-problem.t
+++ b/tests/regression/56-witness/05-prec-problem.t
@@ -6,6 +6,9 @@
     total lines: 13
   [Warning][Deadcode][CWE-570] condition '0' (possibly inserted by CIL) is always false (05-prec-problem.c:13:12-13:13)
   [Info][Witness] witness generation summary:
+    location invariants: 0
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 6
 
 TODO: Don't generate duplicate entries from each context: should have generated just 3.
diff --git a/tests/regression/56-witness/08-witness-all-locals.t b/tests/regression/56-witness/08-witness-all-locals.t
index fc4462201d..fe6aefefbd 100644
--- a/tests/regression/56-witness/08-witness-all-locals.t
+++ b/tests/regression/56-witness/08-witness-all-locals.t
@@ -4,6 +4,9 @@
     dead: 0
     total lines: 4
   [Info][Witness] witness generation summary:
+    location invariants: 3
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 3
 
   $ yamlWitnessStrip < witness.yml
@@ -50,6 +53,9 @@ Fewer entries are emitted if locals from nested block scopes are excluded:
     dead: 0
     total lines: 4
   [Info][Witness] witness generation summary:
+    location invariants: 2
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 2
 
   $ yamlWitnessStrip < witness.yml
diff --git a/tests/regression/56-witness/46-top-bool-invariant.t b/tests/regression/56-witness/46-top-bool-invariant.t
index 741b00966f..be41ef58f2 100644
--- a/tests/regression/56-witness/46-top-bool-invariant.t
+++ b/tests/regression/56-witness/46-top-bool-invariant.t
@@ -6,6 +6,9 @@ def_exc only:
     dead: 0
     total lines: 2
   [Info][Witness] witness generation summary:
+    location invariants: 2
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 2
 
   $ yamlWitnessStrip < witness.yml
@@ -40,6 +43,9 @@ interval only:
     dead: 0
     total lines: 2
   [Info][Witness] witness generation summary:
+    location invariants: 2
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 2
 
   $ yamlWitnessStrip < witness.yml
@@ -74,6 +80,9 @@ enums only:
     dead: 0
     total lines: 2
   [Info][Witness] witness generation summary:
+    location invariants: 1
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 1
 
   $ yamlWitnessStrip < witness.yml
@@ -97,6 +106,9 @@ congruence only:
     dead: 0
     total lines: 2
   [Info][Witness] witness generation summary:
+    location invariants: 0
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 0
 
   $ yamlWitnessStrip < witness.yml
@@ -110,6 +122,9 @@ interval_set only:
     dead: 0
     total lines: 2
   [Info][Witness] witness generation summary:
+    location invariants: 2
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 2
 
   $ yamlWitnessStrip < witness.yml
@@ -144,6 +159,9 @@ all:
     dead: 0
     total lines: 2
   [Info][Witness] witness generation summary:
+    location invariants: 1
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 1
 
   $ yamlWitnessStrip < witness.yml
@@ -167,6 +185,9 @@ all without inexact-type-bounds:
     dead: 0
     total lines: 2
   [Info][Witness] witness generation summary:
+    location invariants: 0
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 0
 
   $ yamlWitnessStrip < witness.yml
diff --git a/tests/regression/56-witness/47-top-int-invariant.t b/tests/regression/56-witness/47-top-int-invariant.t
index cdfe65673f..35d5978c00 100644
--- a/tests/regression/56-witness/47-top-int-invariant.t
+++ b/tests/regression/56-witness/47-top-int-invariant.t
@@ -6,6 +6,9 @@ def_exc only:
     dead: 0
     total lines: 2
   [Info][Witness] witness generation summary:
+    location invariants: 2
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 2
 
   $ yamlWitnessStrip < witness.yml
@@ -40,6 +43,9 @@ interval only:
     dead: 0
     total lines: 2
   [Info][Witness] witness generation summary:
+    location invariants: 2
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 2
 
   $ yamlWitnessStrip < witness.yml
@@ -74,6 +80,9 @@ enums only:
     dead: 0
     total lines: 2
   [Info][Witness] witness generation summary:
+    location invariants: 2
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 2
 
   $ yamlWitnessStrip < witness.yml
@@ -108,6 +117,9 @@ congruence only:
     dead: 0
     total lines: 2
   [Info][Witness] witness generation summary:
+    location invariants: 0
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 0
 
   $ yamlWitnessStrip < witness.yml
@@ -121,6 +133,9 @@ interval_set only:
     dead: 0
     total lines: 2
   [Info][Witness] witness generation summary:
+    location invariants: 2
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 2
 
   $ yamlWitnessStrip < witness.yml
@@ -155,6 +170,9 @@ all:
     dead: 0
     total lines: 2
   [Info][Witness] witness generation summary:
+    location invariants: 2
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 2
 
   $ yamlWitnessStrip < witness.yml
@@ -189,6 +207,9 @@ all without inexact-type-bounds:
     dead: 0
     total lines: 2
   [Info][Witness] witness generation summary:
+    location invariants: 0
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 0
 
   $ yamlWitnessStrip < witness.yml
diff --git a/tests/regression/56-witness/70-apron-unassume-set-tokens.c b/tests/regression/56-witness/70-apron-unassume-set-tokens.c
new file mode 100644
index 0000000000..6ff07f6064
--- /dev/null
+++ b/tests/regression/56-witness/70-apron-unassume-set-tokens.c
@@ -0,0 +1,18 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.activated[+] unassume --set witness.yaml.unassume 70-apron-unassume-set-tokens.yml --set ana.apron.domain polyhedra --enable ana.widen.tokens
+#include <assert.h>
+// Uses polyhedra instead of octagon such that widening tokens are actually needed by test instead of narrowing.
+// Copied & extended from 56-witness/12-apron-unassume-branch.
+int main() {
+  int i = 0;
+  while (i < 100) {
+    i++;
+  }
+  assert(i == 100);
+
+  int j = 0;
+  while (j < 100) {
+    j++;
+  }
+  assert(j == 100);
+  return 0;
+}
diff --git a/tests/regression/56-witness/70-apron-unassume-set-tokens.yml b/tests/regression/56-witness/70-apron-unassume-set-tokens.yml
new file mode 100644
index 0000000000..1fdc29067c
--- /dev/null
+++ b/tests/regression/56-witness/70-apron-unassume-set-tokens.yml
@@ -0,0 +1,59 @@
+- entry_type: invariant_set
+  metadata:
+    format_version: "0.1"
+    uuid: 0a72f7b3-7826-4f68-bc7b-25425e95946e
+    creation_time: 2022-07-26T09:11:03Z
+    producer:
+      name: Goblint
+      version: heads/yaml-witness-unassume-0-g48503c690-dirty
+      command_line: '''./goblint'' ''--enable'' ''dbg.debug'' ''--enable'' ''dbg.regression''
+        ''--html'' ''--set'' ''ana.activated[+]'' ''apron'' ''--enable'' ''witness.yaml.enabled''
+        ''70-apron-unassume-set-tokens.c'''
+    task:
+      input_files:
+      - 70-apron-unassume-set-tokens.c
+      input_file_hashes:
+        70-apron-unassume-set-tokens.c: 71e40ed99b5217343d0831e293e7207e5bd30ce53f6ab73f0c1ef6ced1afcc60
+      data_model: LP64
+      language: C
+  content:
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 70-apron-unassume-set-tokens.c
+        file_hash: 71e40ed99b5217343d0831e293e7207e5bd30ce53f6ab73f0c1ef6ced1afcc60
+        line: 8
+        column: 3
+        function: main
+      value: 99LL - (long long )i >= 0LL
+      format: c_expression
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 70-apron-unassume-set-tokens.c
+        file_hash: 71e40ed99b5217343d0831e293e7207e5bd30ce53f6ab73f0c1ef6ced1afcc60
+        line: 8
+        column: 3
+        function: main
+      value: (long long )i >= 0LL
+      format: c_expression
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 70-apron-unassume-set-tokens.c
+        file_hash: 71e40ed99b5217343d0831e293e7207e5bd30ce53f6ab73f0c1ef6ced1afcc60
+        line: 14
+        column: 3
+        function: main
+      value: 99LL - (long long )j >= 0LL
+      format: c_expression
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 70-apron-unassume-set-tokens.c
+        file_hash: 71e40ed99b5217343d0831e293e7207e5bd30ce53f6ab73f0c1ef6ced1afcc60
+        line: 14
+        column: 3
+        function: main
+      value: (long long )j >= 0LL
+      format: c_expression
diff --git a/tests/regression/56-witness/dune b/tests/regression/56-witness/dune
index 215e47deb2..f6694c60ec 100644
--- a/tests/regression/56-witness/dune
+++ b/tests/regression/56-witness/dune
@@ -21,7 +21,8 @@
      (run %{update_suite} hh-ex3 -q)
      (run %{update_suite} bh-ex1-poly -q)
      (run %{update_suite} apron-unassume-precheck -q)
-     (run %{update_suite} apron-tracked-global-annot -q)))))
+     (run %{update_suite} apron-tracked-global-annot -q)
+     (run %{update_suite} apron-unassume-set-tokens -q)))))
 
 (cram
  (deps (glob_files *.c) (glob_files ??-*.yml)))
diff --git a/tests/regression/cfg/foo.t/run.t b/tests/regression/cfg/foo.t/run.t
index cd890b7a19..19873d7540 100644
--- a/tests/regression/cfg/foo.t/run.t
+++ b/tests/regression/cfg/foo.t/run.t
@@ -67,6 +67,9 @@
     total lines: 6
   [Warning][Deadcode][CWE-571] condition 'a > 0' (possibly inserted by CIL) is always true (foo.c:3:10-3:20)
   [Info][Witness] witness generation summary:
+    location invariants: 8
+    loop invariants: 2
+    flow-insensitive invariants: 0
     total generation entries: 10
 
   $ yamlWitnessStrip < witness.yml
diff --git a/tests/regression/cfg/issue-1356.t/run.t b/tests/regression/cfg/issue-1356.t/run.t
index aee9456b61..d1fcb3c7ef 100644
--- a/tests/regression/cfg/issue-1356.t/run.t
+++ b/tests/regression/cfg/issue-1356.t/run.t
@@ -99,6 +99,9 @@
     dead: 0
     total lines: 13
   [Info][Witness] witness generation summary:
+    location invariants: 0
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 0
 
   $ yamlWitnessStrip < witness.yml
diff --git a/tests/regression/cfg/loops.t/run.t b/tests/regression/cfg/loops.t/run.t
index 6596e7b4a4..1fd19b41fe 100644
--- a/tests/regression/cfg/loops.t/run.t
+++ b/tests/regression/cfg/loops.t/run.t
@@ -219,6 +219,9 @@
     dead: 0
     total lines: 20
   [Info][Witness] witness generation summary:
+    location invariants: 32
+    loop invariants: 21
+    flow-insensitive invariants: 0
     total generation entries: 53
 
   $ yamlWitnessStrip < witness.yml
diff --git a/tests/regression/cfg/pr-758.t/run.t b/tests/regression/cfg/pr-758.t/run.t
index 58bbb88ce4..082c63e860 100644
--- a/tests/regression/cfg/pr-758.t/run.t
+++ b/tests/regression/cfg/pr-758.t/run.t
@@ -93,6 +93,9 @@
     dead: 0
     total lines: 6
   [Info][Witness] witness generation summary:
+    location invariants: 10
+    loop invariants: 2
+    flow-insensitive invariants: 0
     total generation entries: 12
 
   $ yamlWitnessStrip < witness.yml
diff --git a/tests/regression/witness/int.t/run.t b/tests/regression/witness/int.t/run.t
index 6b4784ce32..9448ac7855 100644
--- a/tests/regression/witness/int.t/run.t
+++ b/tests/regression/witness/int.t/run.t
@@ -7,6 +7,9 @@
     dead: 0
     total lines: 10
   [Info][Witness] witness generation summary:
+    location invariants: 3
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 3
 
   $ yamlWitnessStrip < witness.yml
diff --git a/tests/regression/witness/typedef.t/run.t b/tests/regression/witness/typedef.t/run.t
index 55dcc1f911..f9fac0c743 100644
--- a/tests/regression/witness/typedef.t/run.t
+++ b/tests/regression/witness/typedef.t/run.t
@@ -4,6 +4,9 @@
     dead: 0
     total lines: 6
   [Info][Witness] witness generation summary:
+    location invariants: 13
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 13
 
   $ yamlWitnessStrip < witness.yml
@@ -157,6 +160,9 @@
     dead: 0
     total lines: 6
   [Info][Witness] witness generation summary:
+    location invariants: 14
+    loop invariants: 0
+    flow-insensitive invariants: 0
     total generation entries: 14
 
   $ yamlWitnessStrip < witness.yml
diff --git a/tests/util/dune b/tests/util/dune
index 0e32304d4f..e43d21c25d 100644
--- a/tests/util/dune
+++ b/tests/util/dune
@@ -1,7 +1,8 @@
 (executables
- (names yamlWitnessStrip yamlWitnessStripDiff)
+ (names yamlWitnessStrip yamlWitnessStripDiff multilibConfigure)
  (libraries
    batteries.unthreaded
+   goblint-cil
    goblint_std
    goblint_lib
    yaml
@@ -9,3 +10,7 @@
    goblint.build-info.dune)
  (flags :standard -open Goblint_std)
  (preprocess (pps ppx_deriving.std)))
+
+(rule
+ (target multilibAvailable)
+ (action (with-stdout-to %{target} (run ./multilibConfigure.exe))))
diff --git a/tests/util/multilibConfigure.ml b/tests/util/multilibConfigure.ml
new file mode 100644
index 0000000000..96cf9a706a
--- /dev/null
+++ b/tests/util/multilibConfigure.ml
@@ -0,0 +1,4 @@
+open GoblintCil
+
+let () =
+  Printf.printf "%B" (Option.is_some Machdep.gcc32 && Option.is_some Machdep.gcc64)