diff --git a/.github/workflows/docker.yml b/.github/workflows/docker.yml
index 1ef104db29..36568e6cb2 100644
--- a/.github/workflows/docker.yml
+++ b/.github/workflows/docker.yml
@@ -38,10 +38,10 @@ jobs:
         uses: actions/checkout@v4
 
       - name: Set up Docker Buildx
-        uses: docker/setup-buildx-action@v2 # needed for GitHub Actions Cache in build-push-action
+        uses: docker/setup-buildx-action@v3 # needed for GitHub Actions Cache in build-push-action
 
       - name: Log in to the Container registry
-        uses: docker/login-action@v2
+        uses: docker/login-action@v3
         with:
           registry: ${{ env.REGISTRY }}
           username: ${{ github.actor }}
@@ -49,7 +49,7 @@ jobs:
 
       - name: Extract metadata (tags, labels) for Docker
         id: meta
-        uses: docker/metadata-action@v4
+        uses: docker/metadata-action@v5
         with:
           images: ${{ env.REGISTRY }}/${{ env.IMAGE_NAME }}
           tags: |
@@ -59,7 +59,7 @@ jobs:
 
       - name: Build Docker image
         id: build
-        uses: docker/build-push-action@v4
+        uses: docker/build-push-action@v5
         with:
           context: .
           load: true # load into docker instead of immediately pushing
@@ -72,7 +72,7 @@ jobs:
         run: docker run --rm -v $(pwd):/data ${{ env.REGISTRY }}/${{ env.IMAGE_NAME }}:${{ steps.meta.outputs.version }} /data/tests/regression/04-mutex/01-simple_rc.c # run image by version in case multiple tags
 
       - name: Push Docker image
-        uses: docker/build-push-action@v4
+        uses: docker/build-push-action@v5
         with:
           context: .
           push: true
diff --git a/.github/workflows/unlocked.yml b/.github/workflows/unlocked.yml
index 15cd9138d8..6c23c7cdd4 100644
--- a/.github/workflows/unlocked.yml
+++ b/.github/workflows/unlocked.yml
@@ -18,6 +18,7 @@ jobs:
           - ubuntu-latest
           - macos-latest
         ocaml-compiler:
+          - 5.0.x
           - ocaml-variants.4.14.0+options,ocaml-option-flambda
           - 4.14.x
           - 4.13.x
@@ -211,11 +212,11 @@ jobs:
         uses: actions/checkout@v4
 
       - name: Set up Docker Buildx
-        uses: docker/setup-buildx-action@v2 # needed for GitHub Actions Cache in build-push-action
+        uses: docker/setup-buildx-action@v3 # needed for GitHub Actions Cache in build-push-action
 
       - name: Build dev Docker image
         id: build
-        uses: docker/build-push-action@v4
+        uses: docker/build-push-action@v5
         with:
           context: .
           target: dev
diff --git a/CHANGELOG.md b/CHANGELOG.md
index a126514852..97cc399133 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,10 +1,10 @@
-## v2.2.0
-* TODO OCaml 5 (#1003, #1137).
-* TODO Library #1138
-* TODO refactor race #1136
+## v2.2.1
+* Bump batteries lower bound to 3.5.0.
+* Fix flaky dead code elimination transformation test.
 
+## v2.2.0
 * Add `setjmp`/`longjmp` analysis (#887, #970, #1015, #1019).
-* Refactor race analysis to lazy distribution (#1084, #1089, #1016).
+* Refactor race analysis to lazy distribution (#1084, #1089, #1136, #1016).
 * Add thread-unsafe library function call analysis (#723, #1082).
 * Add mutex type analysis and mutex API analysis (#800, #839, #1073).
 * Add interval set domain and string literals domain (#901, #966, #994, #1048).
@@ -19,8 +19,8 @@
 * Fix many incremental analysis issues (#627, #836, #835, #841, #932, #678, #942, #949, #950, #957, #955, #954, #960, #959, #1004, #558, #1010, #1091).
 * Fix server mode for abstract debugging (#983, #990, #997, #1000, #1001, #1013, #1018, #1017, #1026, #1027).
 * Add documentation for configuration JSON schema and OCaml API (#999, #1054, #1055, #1053).
-* Add many library function specifications (#962, #996, #1028, #1079, #1121, #1135).
-* Add OCaml 5.0 support (#945).
+* Add many library function specifications (#962, #996, #1028, #1079, #1121, #1135, #1138).
+* Add OCaml 5.0 support (#1003, #945, #1162).
 
 ## v2.1.0
 Functionally equivalent to Goblint in SV-COMP 2023.
diff --git a/README.md b/README.md
index b03b7bbe36..4d97baa842 100644
--- a/README.md
+++ b/README.md
@@ -13,6 +13,7 @@ Documentation can be browsed on [Read the Docs](https://goblint.readthedocs.io/e
 
 ## Installing
 Both for using an up-to-date version of Goblint or developing it, the best way is to install from source by cloning this repository.
+For benchmarking Goblint, please follow the [Benchmarking guide on Read the Docs](https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/).
 
 ### Linux
 1. Install [opam](https://opam.ocaml.org/doc/Install.html).
diff --git a/docs/developer-guide/releasing.md b/docs/developer-guide/releasing.md
index f6bfbb459e..69ffcb2461 100644
--- a/docs/developer-guide/releasing.md
+++ b/docs/developer-guide/releasing.md
@@ -45,13 +45,20 @@
     10. Check that analysis works: `goblint -v tests/regression/04-mutex/01-simple_rc.c`.
     11. Exit Docker container.
 
-12. Create a GitHub release with the git tag: `DUNE_RELEASE_DELEGATE=github-dune-release-delegate dune-release publish distrib`.
+12. Temporarily enable Zenodo GitHub webhook.
+
+    This is because we only want numbered version releases to automatically add a new version to our Zenodo artifact.
+    Other tags (like SV-COMP or paper artifacts) have manually created Zenodo artifacts anyway and thus shouldn't add new versions to the main Zenodo artifact.
+
+13. Create a GitHub release with the git tag: `DUNE_RELEASE_DELEGATE=github-dune-release-delegate dune-release publish distrib`.
 
     Explicitly specify `distrib` because we don't want to publish OCaml API docs.
     Environment variable workaround for the package having a Read the Docs `doc` URL (see <https://github.com/ocamllabs/dune-release/issues/154>).
 
-13. Create an opam package: `dune-release opam pkg`.
-14. Submit the opam package to opam-repository: `dune-release opam submit`.
+14. Re-disable Zenodo GitHub webhook.
+
+15. Create an opam package: `dune-release opam pkg`.
+16. Submit the opam package to opam-repository: `dune-release opam submit`.
 
 
 ## SV-COMP
@@ -104,15 +111,9 @@
 ### After all preruns
 
 1. Push git tag from last prerun: `git push origin svcompXY`.
-2. Temporarily disable Zenodo webhook.
-
-    This is because we don't want a new out-of-place version of Goblint in our Zenodo artifact.
-    A separate Zenodo artifact for the SV-COMP version can be created later if tool paper is submitted.
-
-3. Create GitHub release from the git tag and attach latest submitted archive as a download.
-4. Manually run `docker` workflow on `svcompXY` git tag and targeting `svcompXY` Docker tag.
+2. Create GitHub release from the git tag and attach latest submitted archive as a download.
+3. Manually run `docker` workflow on `svcompXY` git tag and targeting `svcompXY` Docker tag.
 
     This is because the usual `docker` workflow only handles semver releases.
 
-5. Re-enable Zenodo webhook.
-6. Release new semver version on opam. See above.
+4. Release new semver version on opam. See above.
diff --git a/docs/user-guide/benchmarking.md b/docs/user-guide/benchmarking.md
index 44811b61a5..5417375bdb 100644
--- a/docs/user-guide/benchmarking.md
+++ b/docs/user-guide/benchmarking.md
@@ -1,6 +1,31 @@
 # Benchmarking
+The following best practices should be followed when benchmarking Goblint.
+This is to ensure valid, reproducible and representative benchmarking results.
 
-To achieve reproducible builds and the best performance for benchmarking, it is recommended to compile Goblint using the `release` option:
+# External benchmarking
+External users should choose the version of Goblint to evaluate or benchmark as follows:
+
+1. Use the newest version release.
+
+    The version from git `master` branch or any other intermediate git commit come without any guarantees.
+    They are bleeding-edge and haven't gone through validation like the version releases.
+
+    SV-COMP releases are highly preferable since they've gone through rigorous validation in SV-COMP.
+
+2. Download the corresponding version from a Zenodo artifact or by checking out the respective git tag. **Do not install directly from opam repository!**
+
+    Goblint pins optimized versions of some dependencies which cannot be done on the opam repository releases.
+    Thus, using the latter would yield unrepresentative results.
+
+    Zenodo artifacts come with DOIs, which make them ideal for citation.
+
+3. Use OCaml 4.14. **Do not use OCaml 5!**
+
+    OCaml 5 has significant performance regressions, which yield unrepresentative benchmarking results.
+    Goblint's `make setup` installs the correct OCaml version into a new opam switch.
+
+# Release build
+To achieve the best performance for benchmarking, Goblint should be compiled using the `release` option:
 
 ```sh
 make release
diff --git a/dune-project b/dune-project
index b8b8481c97..4a9cd8e3c1 100644
--- a/dune-project
+++ b/dune-project
@@ -24,8 +24,8 @@
   (synopsis "Static analysis framework for C")
   (depends
     (ocaml (>= 4.10))
-    (goblint-cil (>= 2.0.1)) ; 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.4.0))
+    (goblint-cil (>= 2.0.2)) ; 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.0))
     (zarith (>= 1.8))
     (yojson (>= 2.0.0))
     (qcheck-core (>= 0.19))
diff --git a/goblint.opam b/goblint.opam
index a20df919d0..661222805b 100644
--- a/goblint.opam
+++ b/goblint.opam
@@ -21,8 +21,8 @@ bug-reports: "https://github.com/goblint/analyzer/issues"
 depends: [
   "dune" {>= "3.6"}
   "ocaml" {>= "4.10"}
-  "goblint-cil" {>= "2.0.1"}
-  "batteries" {>= "3.4.0"}
+  "goblint-cil" {>= "2.0.2"}
+  "batteries" {>= "3.5.0"}
   "zarith" {>= "1.8"}
   "yojson" {>= "2.0.0"}
   "qcheck-core" {>= "0.19"}
@@ -74,10 +74,12 @@ 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!
 available: os-distribution != "alpine" & arch != "arm64"
-pin-depends: [
-  [ "goblint-cil.2.0.1" "git+https://github.com/goblint/cil.git#4df989fe625d91ce07d94afe1d85b3b5c6cdd63e" ]
+# pin-depends: [
+  # published goblint-cil 2.0.2 is currently up-to-date, so no pin needed
+  # [ "goblint-cil.2.0.2" "git+https://github.com/goblint/cil.git#98598d94f796a63751e5a9d39c6b3a9fe1f32330" ]
   # 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" ]
-  # TODO: add back after release, only pinned for CI stability
-  [ "apron.v0.9.13" "git+https://github.com/antoinemine/apron.git#1a8e91062c0d7d1e80333d19d5a432332bbbaec8"]
+  # [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
+# ]
+post-messages: [
+  "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}
 ]
diff --git a/goblint.opam.locked b/goblint.opam.locked
index acb49a7b14..bb59c41dd1 100644
--- a/goblint.opam.locked
+++ b/goblint.opam.locked
@@ -21,7 +21,7 @@ doc: "https://goblint.readthedocs.io/en/latest/"
 bug-reports: "https://github.com/goblint/analyzer/issues"
 depends: [
   "angstrom" {= "0.15.0"}
-  "apron" {= "v0.9.13"}
+  "apron" {= "v0.9.14~beta.2"}
   "arg-complete" {= "0.1.0"}
   "astring" {= "0.8.5"}
   "base-bigarray" {= "base"}
@@ -56,22 +56,22 @@ depends: [
   "dune-private-libs" {= "3.6.1"}
   "dune-site" {= "3.6.1"}
   "dyn" {= "3.6.1"}
+  "fileutils" {= "0.6.4"}
   "fmt" {= "0.9.0"}
   "fpath" {= "0.7.3"}
-  "goblint-cil" {= "2.0.1"}
+  "goblint-cil" {= "2.0.2"}
   "integers" {= "0.7.0"}
   "json-data-encoding" {= "0.12.1"}
   "jsonrpc" {= "1.15.0~5.0preview1"}
-  "fileutils" {= "0.6.4"}
   "logs" {= "0.7.0"}
-  "mlgmpidl" {= "1.2.14"}
+  "mlgmpidl" {= "1.2.15"}
   "num" {= "1.4"}
   "ocaml" {= "4.14.0"}
-  "ocaml-variants" {= "4.14.0+options"}
   "ocaml-compiler-libs" {= "v0.12.4"}
   "ocaml-config" {= "2"}
   "ocaml-option-flambda" {= "1"}
   "ocaml-syntax-shims" {= "1.0.0"}
+  "ocaml-variants" {= "4.14.0+options"}
   "ocamlbuild" {= "0.14.2"}
   "ocamlfind" {= "1.9.5"}
   "odoc" {= "2.2.0" & with-doc}
@@ -125,18 +125,6 @@ available: os-distribution != "alpine" & arch != "arm64"
 conflicts: [
   "result" {< "1.5"}
 ]
-# TODO: manually reordered to avoid opam pin crash: https://github.com/ocaml/opam/issues/4936
-pin-depends: [
-  [
-    "goblint-cil.2.0.1"
-    "git+https://github.com/goblint/cil.git#4df989fe625d91ce07d94afe1d85b3b5c6cdd63e"
-  ]
-  [
-    "apron.v0.9.13"
-    "git+https://github.com/antoinemine/apron.git#1a8e91062c0d7d1e80333d19d5a432332bbbaec8"
-  ]
-  [
-    "ppx_deriving.5.2.1"
-    "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6"
-  ]
+post-messages: [
+  "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}
 ]
diff --git a/goblint.opam.template b/goblint.opam.template
index b7f5a7abff..6259c4d498 100644
--- a/goblint.opam.template
+++ b/goblint.opam.template
@@ -1,10 +1,12 @@
 # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
 # also remember to generate/adjust goblint.opam.locked!
 available: os-distribution != "alpine" & arch != "arm64"
-pin-depends: [
-  [ "goblint-cil.2.0.1" "git+https://github.com/goblint/cil.git#4df989fe625d91ce07d94afe1d85b3b5c6cdd63e" ]
+# pin-depends: [
+  # published goblint-cil 2.0.2 is currently up-to-date, so no pin needed
+  # [ "goblint-cil.2.0.2" "git+https://github.com/goblint/cil.git#98598d94f796a63751e5a9d39c6b3a9fe1f32330" ]
   # 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" ]
-  # TODO: add back after release, only pinned for CI stability
-  [ "apron.v0.9.13" "git+https://github.com/antoinemine/apron.git#1a8e91062c0d7d1e80333d19d5a432332bbbaec8"]
+  # [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
+# ]
+post-messages: [
+  "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}
 ]
diff --git a/gobview b/gobview
index c3dcfaba97..b373d06174 160000
--- a/gobview
+++ b/gobview
@@ -1 +1 @@
-Subproject commit c3dcfaba97a1df72f027e5dad317e2c201ce5e4b
+Subproject commit b373d06174667537b671f3122daf4ebd4b195aea
diff --git a/make.sh b/make.sh
index 788289c5ed..af1411a8d3 100755
--- a/make.sh
+++ b/make.sh
@@ -8,7 +8,7 @@ opam_setup() {
   set -x
   opam init -y -a --bare $SANDBOXING # sandboxing is disabled in travis and docker
   opam update
-  opam switch -y create . --deps-only ocaml-variants.4.14.0+options ocaml-option-flambda --locked
+  opam switch -y create . --deps-only --packages=ocaml-variants.4.14.0+options,ocaml-option-flambda --locked
 }
 
 rule() {
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 912e298143..e30729e2d0 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -1099,12 +1099,12 @@ struct
 
   let eval_funvar ctx fval: Queries.AD.t =
     let fp = eval_fv (Analyses.ask_of_ctx ctx) ctx.global ctx.local fval in
-    if AD.is_top fp then begin
+    if AD.is_top fp then (
       if AD.cardinal fp = 1 then
-        (M.warn ~category:Unsound "Unknown call to function %a." d_exp fval;)
+        M.warn ~category:Imprecise ~tags:[Category Call] "Unknown call to function %a." d_exp fval
       else
-        (M.warn ~category:Imprecise "Function pointer %a may contain unknown functions." d_exp fval;)
-    end;
+        M.warn ~category:Imprecise ~tags:[Category Call] "Function pointer %a may contain unknown functions." d_exp fval
+    );
     fp
 
   (** Evaluate expression as address.
@@ -1962,7 +1962,7 @@ struct
     end
 
   let special_unknown_invalidate ctx ask gs st f args =
-    (if CilType.Varinfo.equal f dummyFunDec.svar then M.warn ~category:Imprecise "Unknown function ptr called");
+    (if CilType.Varinfo.equal f dummyFunDec.svar then M.warn ~category:Imprecise ~tags:[Category Call] "Unknown function ptr called");
     let desc = LF.find f in
     let shallow_addrs = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = false } args in
     let deep_addrs = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = true } args in
diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml
index 096d50b89b..70c6ed9101 100644
--- a/src/analyses/baseInvariant.ml
+++ b/src/analyses/baseInvariant.ml
@@ -410,6 +410,18 @@ struct
           meet_bin c c
         else
           a, b
+      | BAnd as op ->
+        (* we only attempt to refine a here *)
+        let a =
+          match ID.to_int b with
+          | Some x when BI.equal x BI.one ->
+            (match ID.to_bool c with
+             | Some true -> ID.meet a (ID.of_congruence ikind (Z.one, Z.of_int 2))
+             | Some false -> ID.meet a (ID.of_congruence ikind (Z.zero, Z.of_int 2))
+             | None -> if M.tracing then M.tracel "inv" "Unhandled case for operator x %a 1 = %a\n" d_binop op ID.pretty c; a)
+          | _ -> if M.tracing then M.tracel "inv" "Unhandled case for operator x %a %a = %a\n" d_binop op ID.pretty b ID.pretty c; a
+        in
+        a, b
       | op ->
         if M.tracing then M.tracel "inv" "Unhandled operator %a\n" d_binop op;
         a, b
@@ -545,8 +557,8 @@ struct
     in
     let eval e st = eval_rv a gs st e in
     let eval_bool e st = match eval e st with Int i -> ID.to_bool i | _ -> None in
-    let unroll_fk_of_exp e = 
-      match unrollType (Cilfacade.typeOf e) with 
+    let unroll_fk_of_exp e =
+      match unrollType (Cilfacade.typeOf e) with
       | TFloat (fk, _) -> fk
       | _ -> failwith "value which was expected to be a float is of different type?!"
     in
@@ -700,8 +712,8 @@ struct
               begin match t with
                 | TInt (ik, _) ->
                   begin match x with
-                    | ((Var v), offs) -> 
-                      if M.tracing then M.trace "invSpecial" "qry Result: %a\n" Queries.ML.pretty (ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs))); 
+                    | ((Var v), offs) ->
+                      if M.tracing then M.trace "invSpecial" "qry Result: %a\n" Queries.ML.pretty (ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs)));
                       let tv_opt = ID.to_bool c in
                       begin match tv_opt with
                         | Some tv ->
@@ -735,12 +747,12 @@ struct
               begin match t with
                 | TFloat (fk, _) ->
                   begin match x with
-                    | ((Var v), offs) -> 
-                      if M.tracing then M.trace "invSpecial" "qry Result: %a\n" Queries.ML.pretty (ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs))); 
+                    | ((Var v), offs) ->
+                      if M.tracing then M.trace "invSpecial" "qry Result: %a\n" Queries.ML.pretty (ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs)));
                       begin match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs)) with
                         | `Lifted (Ceil (ret_fk, xFloat)) -> inv_exp (Float (FD.inv_ceil (FD.cast_to ret_fk c))) xFloat st
                         | `Lifted (Floor (ret_fk, xFloat)) -> inv_exp (Float (FD.inv_floor (FD.cast_to ret_fk c))) xFloat st
-                        | `Lifted (Fabs (ret_fk, xFloat)) -> 
+                        | `Lifted (Fabs (ret_fk, xFloat)) ->
                           let inv = FD.inv_fabs (FD.cast_to ret_fk c) in
                           if FD.is_bot inv then
                             raise Analyses.Deadcode
diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml
index 6003f69bf9..137a3103a5 100644
--- a/src/analyses/libraryFunctions.ml
+++ b/src/analyses/libraryFunctions.ml
@@ -102,6 +102,8 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("vprintf", unknown [drop "format" [r]; drop "vlist" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *)
     ("vfprintf", unknown [drop "stream" [r_deep; w_deep]; drop "format" [r]; drop "vlist" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *)
     ("vsprintf", unknown [drop "buffer" [w]; drop "format" [r]; drop "vlist" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *)
+    ("vasprintf", unknown [drop "strp" [w]; drop "format" [r]; drop "ap" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *)
+    ("vsnprintf", unknown [drop "str" [w]; drop "size" []; drop "format" [r]; drop "ap" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *)
     ("mktime", unknown [drop "tm" [r;w]]);
     ("ctime", unknown ~attrs:[ThreadUnsafe] [drop "rm" [r]]);
     ("clearerr", unknown [drop "stream" [w]]);
@@ -289,6 +291,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("nftw", unknown ~attrs:[ThreadUnsafe] [drop "dirpath" [r]; drop "fn" [s]; drop "nopenfd" []; drop "flags" []]); (* TODO: use Call instead of Spawn *)
     ("getaddrinfo", unknown [drop "node" [r]; drop "service" [r]; drop "hints" [r_deep]; drop "res" [w]]); (* only write res non-deep because it doesn't write to existing fields of res *)
     ("fnmatch", unknown [drop "pattern" [r]; drop "string" [r]; drop "flags" []]);
+    ("realpath", unknown [drop "path" [r]; drop "resolved_path" [w]]);
   ]
 
 (** Pthread functions. *)
@@ -825,6 +828,19 @@ let pcre_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("pcre_version", unknown []);
   ]
 
+let zlib_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
+    ("inflate", unknown [drop "strm" [r_deep; w_deep]; drop "flush" []]);
+    ("inflateInit2", unknown [drop "strm" [r_deep; w_deep]; drop "windowBits" []]);
+    ("inflateInit2_", unknown [drop "strm" [r_deep; w_deep]; drop "windowBits" []; drop "version" [r]; drop "stream_size" []]);
+    ("inflateEnd", unknown [drop "strm" [f_deep]]);
+  ]
+
+let liblzma_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
+    ("lzma_code", unknown [drop "strm" [r_deep; w_deep]; drop "action" []]);
+    ("lzma_auto_decoder", unknown [drop "strm" [r_deep; w_deep]; drop "memlimit" []; drop "flags" []]);
+    ("lzma_end", unknown [drop "strm" [r_deep; w_deep; f_deep]]);
+  ]
+
 let libraries = Hashtbl.of_list [
     ("c", c_descs_list @ math_descs_list);
     ("posix", posix_descs_list);
@@ -838,6 +854,8 @@ let libraries = Hashtbl.of_list [
     ("ncurses", ncurses_descs_list);
     ("zstd", zstd_descs_list);
     ("pcre", pcre_descs_list);
+    ("zlib", zlib_descs_list);
+    ("liblzma", liblzma_descs_list);
   ]
 
 let activated_library_descs: (string, LibraryDesc.t) Hashtbl.t ResettableLazy.t =
@@ -1072,7 +1090,6 @@ let invalidate_actions = [
     "usleep", readsAll;
     "svc_run", writesAll;(*unsafe*)
     "dup", readsAll; (*safe*)
-    "vsnprintf", writesAllButFirst 3 readsAll; (*drop 3*)
     "__builtin___vsnprintf", writesAllButFirst 3 readsAll; (*drop 3*)
     "__builtin___vsnprintf_chk", writesAllButFirst 3 readsAll; (*drop 3*)
     "strcasecmp", readsAll; (*safe*)
diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml
index fabd655811..9c2272fabb 100644
--- a/src/analyses/raceAnalysis.ml
+++ b/src/analyses/raceAnalysis.ml
@@ -225,9 +225,9 @@ struct
     | _ ->
       ()
 
-  let side_access ctx (conf, w, loc, e, a) ((memoroot, offset) as memo) =
+  let side_access ctx acc ((memoroot, offset) as memo) =
     if !AnalysisState.should_warn then
-      ctx.sideg (V.access memoroot) (G.create_access (OffsetTrie.singleton offset (`Lifted (Access.AS.singleton (conf, w, loc, e, a)))));
+      ctx.sideg (V.access memoroot) (G.create_access (OffsetTrie.singleton offset (`Lifted (Access.AS.singleton acc))));
     side_vars ctx memo
 
   (** Side-effect empty access set for prefix-type_suffix race checking. *)
@@ -304,22 +304,22 @@ struct
 
   let event ctx e octx =
     match e with
-    | Events.Access {exp=e; ad; kind; reach} when ThreadFlag.is_currently_multi (Analyses.ask_of_ctx ctx) -> (* threadflag query in post-threadspawn ctx *)
+    | Events.Access {exp; ad; kind; reach} when ThreadFlag.is_currently_multi (Analyses.ask_of_ctx ctx) -> (* threadflag query in post-threadspawn ctx *)
       (* must use original (pre-assign, etc) ctx queries *)
       let conf = 110 in
       let module AD = Queries.AD in
       let part_access (vo:varinfo option): MCPAccess.A.t =
         (*partitions & locks*)
-        Obj.obj (octx.ask (PartAccess (Memory {exp=e; var_opt=vo; kind})))
+        Obj.obj (octx.ask (PartAccess (Memory {exp; var_opt=vo; kind})))
       in
-      let loc = Option.get !Node.current_node in
+      let node = Option.get !Node.current_node in
       let add_access conf voffs =
-        let a = part_access (Option.map fst voffs) in
-        Access.add ~side:(side_access octx (conf, kind, loc, e, a)) ~side_empty:(side_access_empty octx) e voffs;
+        let acc = part_access (Option.map fst voffs) in
+        Access.add ~side:(side_access octx {conf; kind; node; exp; acc}) ~side_empty:(side_access_empty octx) exp voffs;
       in
       let add_access_struct conf ci =
-        let a = part_access None in
-        Access.add_one ~side:(side_access octx (conf, kind, loc, e, a)) (`Type (TSComp (ci.cstruct, ci.cname, [])), `NoOffset)
+        let acc = part_access None in
+        Access.add_one ~side:(side_access octx {conf; kind; node; exp; acc}) (`Type (TSComp (ci.cstruct, ci.cname, [])), `NoOffset)
       in
       let has_escaped g = octx.ask (Queries.MayEscape g) in
       (* The following function adds accesses to the lval-set ls
@@ -345,7 +345,7 @@ struct
           (* the case where the points-to set is non top and contains unknown values *)
           let includes_uk = ref false in
           (* now we need to access all fields that might be pointed to: is this correct? *)
-          begin match octx.ask (ReachableUkTypes e) with
+          begin match octx.ask (ReachableUkTypes exp) with
             | ts when Queries.TS.is_top ts ->
               includes_uk := true
             | ts ->
@@ -370,12 +370,13 @@ struct
     (* perform shallow and deep invalidate according to Library descriptors *)
     let desc = LibraryFunctions.find f in
     if List.mem LibraryDesc.ThreadUnsafe desc.attrs then (
-      let e = Lval (Var f, NoOffset) in
+      let exp = Lval (Var f, NoOffset) in
       let conf = 110 in
-      let loc = Option.get !Node.current_node in
+      let kind = AccessKind.Call in
+      let node = Option.get !Node.current_node in
       let vo = Some f in
-      let a = Obj.obj (ctx.ask (PartAccess (Memory {exp=e; var_opt=vo; kind=Call}))) in
-      side_access ctx (conf, Call, loc, e, a) ((`Var f), `NoOffset) ;
+      let acc = Obj.obj (ctx.ask (PartAccess (Memory {exp; var_opt=vo; kind}))) in
+      side_access ctx {conf; kind; node; exp; acc} ((`Var f), `NoOffset) ;
     );
     ctx.local
 
diff --git a/src/analyses/threadAnalysis.ml b/src/analyses/threadAnalysis.ml
index d6a93744bc..1e679a4707 100644
--- a/src/analyses/threadAnalysis.ml
+++ b/src/analyses/threadAnalysis.ml
@@ -32,13 +32,21 @@ struct
 
   let rec is_not_unique ctx tid =
     let (rep, parents, _) = ctx.global tid in
-    let n = TS.cardinal parents in
-    (* A thread is not unique if it is
-      * a) repeatedly created,
-      * b) created in multiple threads, or
-      * c) created by a thread that is itself multiply created.
-      * Note that starting threads have empty ancestor sets! *)
-    rep || n > 1 || n > 0 && is_not_unique ctx (TS.choose parents)
+    if rep then
+      true (* repeatedly created *)
+    else (
+      let n = TS.cardinal parents in
+      if n > 1 then
+        true (* created in multiple threads *)
+      else if n > 0 then (
+        (* created by single thread *)
+        let parent = TS.choose parents in
+        (* created by itself thread-recursively or by a thread that is itself multiply created *)
+        T.equal tid parent || is_not_unique ctx parent (* equal check needed to avoid infinte self-recursion *)
+      )
+      else
+        false (* no ancestors, starting thread *)
+    )
 
   let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
     let desc = LibraryFunctions.find f in
diff --git a/src/cdomains/intDomain.ml b/src/cdomains/intDomain.ml
index 5417598360..748df62300 100644
--- a/src/cdomains/intDomain.ml
+++ b/src/cdomains/intDomain.ml
@@ -514,7 +514,7 @@ module Size = struct (* size in bits as int, range as int64 *)
 
   let cast t x = (* TODO: overflow is implementation-dependent! *)
     if t = IBool then
-      (* C11 6.3.1.2 Boolean type *) 
+      (* C11 6.3.1.2 Boolean type *)
       if Z.equal x Z.zero then Z.zero else Z.one
     else
       let a,b = range t in
@@ -826,7 +826,19 @@ struct
       | _              -> (top_of ik,{underflow=true; overflow=true})
 
   let bitxor = bit (fun _ik -> Ints_t.bitxor)
-  let bitand = bit (fun _ik -> Ints_t.bitand)
+
+  let bitand ik i1 i2 =
+    match is_bot i1, is_bot i2 with
+    | true, true -> bot_of ik
+    | true, _
+    | _   , true -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show i1) (show i2)))
+    | _ ->
+      match to_int i1, to_int i2 with
+      | Some x, Some y -> (try of_int ik (Ints_t.bitand x y) |> fst with Division_by_zero -> top_of ik)
+      | _, Some y when Ints_t.equal y Ints_t.zero -> of_int ik Ints_t.zero |> fst
+      | _, Some y when Ints_t.equal y Ints_t.one -> of_interval ik (Ints_t.zero, Ints_t.one) |> fst
+      | _ -> top_of ik
+
   let bitor  = bit (fun _ik -> Ints_t.bitor)
 
   let bit1 f ik i1 =
@@ -1978,7 +1990,7 @@ struct
   let top_of ik = `Excluded (S.empty (), size ik)
   let cast_to ?torg ?no_ov ik = function
     | `Excluded (s,r) ->
-      let r' = size ik in 
+      let r' = size ik in
         if R.leq r r' then (* upcast -> no change *)
           `Excluded (s, r)
         else if ik = IBool then (* downcast to bool *)
@@ -1986,7 +1998,7 @@ struct
             `Definite (BI.one)
           else
             `Excluded (S.empty(), r')
-        else 
+        else
           (* downcast: may overflow *)
           (* let s' = S.map (BigInt.cast_to ik) s in *)
           (* We want to filter out all i in s' where (t)x with x in r could be i. *)
@@ -2282,7 +2294,28 @@ struct
   let ge ik x y = le ik y x
 
   let bitnot = lift1 BigInt.bitnot
-  let bitand = lift2 BigInt.bitand
+
+  let bitand ik x y = norm ik (match x,y with
+      (* We don't bother with exclusion sets: *)
+      | `Excluded _, `Definite i ->
+        (* Except in two special cases *)
+        if BigInt.equal i BigInt.zero then
+          `Definite BigInt.zero
+        else if BigInt.equal i BigInt.one then
+          of_interval IBool (BigInt.zero, BigInt.one)
+        else
+          top ()
+      | `Definite _, `Excluded _
+      | `Excluded _, `Excluded _ -> top ()
+      (* The good case: *)
+      | `Definite x, `Definite y ->
+        (try `Definite (BigInt.bitand x y) with | Division_by_zero -> top ())
+      | `Bot, `Bot -> `Bot
+      | _ ->
+        (* If only one of them is bottom, we raise an exception that eval_rv will catch *)
+        raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y))))
+
+
   let bitor  = lift2 BigInt.bitor
   let bitxor = lift2 BigInt.bitxor
 
@@ -3134,7 +3167,7 @@ struct
 
   (** The implementation of the bit operations could be improved based on the master’s thesis
       'Abstract Interpretation and Abstract Domains' written by Stefan Bygde.
-      see: https://www.dsi.unive.it/~avp/domains.pdf *)
+      see: http://www.es.mdh.se/pdf_publications/948.pdf *)
   let bit2 f ik x y = match x, y with
     | None, None -> None
     | None, _ | _, None -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y)))
@@ -3144,7 +3177,19 @@ struct
 
   let bitor ik x y = bit2 Ints_t.bitor ik x y
 
-  let bitand ik x y = bit2 Ints_t.bitand ik x y
+  let bitand ik x y =  match x, y with
+    | None, None -> None
+    | None, _ | _, None -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y)))
+    | Some (c, m), Some (c', m') ->
+      if (m =: Ints_t.zero && m' =: Ints_t.zero) then
+        (* both arguments constant *)
+        Some (Ints_t.bitand c c', Ints_t.zero)
+      else if m' =: Ints_t.zero && c' =: Ints_t.one && Ints_t.rem m (Ints_t.of_int 2) =: Ints_t.zero then
+        (* x & 1  and  x == c (mod 2*z) *)
+        (* Value is equal to LSB of c *)
+        Some (Ints_t.bitand c c', Ints_t.zero)
+      else
+        top ()
 
   let bitxor ik x y = bit2 Ints_t.bitxor ik x y
 
@@ -3154,8 +3199,8 @@ struct
     | None, _ | _, None -> raise (ArithmeticOnIntegerBot (Printf.sprintf "%s op %s" (show x) (show y)))
     | Some (c1, m1), Some(c2, m2) ->
       if m2 =: Ints_t.zero then
-        if (c2 |: m1) then
-          Some(c1 %: c2,Ints_t.zero)
+        if (c2 |: m1) && (c1 %: c2 =: Ints_t.zero || m1 =: Ints_t.zero || not (Cil.isSigned ik)) then
+          Some(c1 %: c2, Ints_t.zero)
         else
           normalize ik (Some(c1, (Ints_t.gcd m1 c2)))
       else
diff --git a/src/cdomains/valueDomain.ml b/src/cdomains/valueDomain.ml
index 9d894b6b34..cba4b04c18 100644
--- a/src/cdomains/valueDomain.ml
+++ b/src/cdomains/valueDomain.ml
@@ -824,6 +824,8 @@ struct
   (* Funny, this does not compile without the final type annotation! *)
   let rec eval_offset (ask: VDQ.t) f (x: t) (offs:offs) (exp:exp option) (v:lval option) (t:typ): t =
     let rec do_eval_offset (ask:VDQ.t) f (x:t) (offs:offs) (exp:exp option) (l:lval option) (o:offset option) (v:lval option) (t:typ): t =
+      if M.tracing then M.traceli "eval_offset" "do_eval_offset %a %a (%a)\n" pretty x Offs.pretty offs (Pretty.docOpt (CilType.Exp.pretty ())) exp;
+      let r =
       match x, offs with
       | Blob((va, _, orig) as c), `Index (_, ox) ->
         begin
@@ -886,6 +888,9 @@ struct
             | Top -> M.info ~category:Imprecise "Trying to read an index, but the array is unknown"; top ()
             | _ -> M.warn ~category:Imprecise ~tags:[Category Program] "Trying to read an index, but was not given an array (%a)" pretty x; top ()
           end
+      in
+      if M.tracing then M.traceu "eval_offset" "do_eval_offset -> %a\n" pretty r;
+      r
     in
     let l, o = match exp with
       | Some(Lval (x,o)) -> Some ((x, NoOffset)), Some(o)
diff --git a/src/domains/access.ml b/src/domains/access.ml
index 675d1c2e72..fa6446df16 100644
--- a/src/domains/access.ml
+++ b/src/domains/access.ml
@@ -16,8 +16,8 @@ let is_ignorable_type (t: typ): bool =
   | TComp ({ cname = "__pthread_mutex_s" | "__pthread_rwlock_arch_t" | "__jmp_buf_tag" | "_pthread_cleanup_buffer" | "__pthread_cleanup_frame" | "__cancel_jmp_buf_tag"; _}, _) -> true
   | TComp ({ cname; _}, _) when String.starts_with_stdlib ~prefix:"__anon" cname ->
     begin match Cilfacade.split_anoncomp_name cname with
-      | (true, ("__once_flag" | "__pthread_unwind_buf_t" | "__cancel_jmp_buf"), _) -> true (* anonstruct *)
-      | (false, ("pthread_mutexattr_t" | "pthread_condattr_t" | "pthread_barrierattr_t"), _) -> true (* anonunion *)
+      | (true, Some ("__once_flag" | "__pthread_unwind_buf_t" | "__cancel_jmp_buf"), _) -> true (* anonstruct *)
+      | (false, Some ("pthread_mutexattr_t" | "pthread_condattr_t" | "pthread_barrierattr_t"), _) -> true (* anonunion *)
       | _ -> false
     end
   | TComp ({ cname = "lock_class_key"; _ }, _) -> true
@@ -329,12 +329,18 @@ and distribute_access_type f = function
 module A =
 struct
   include Printable.Std
-  type t = int * AccessKind.t * Node.t * CilType.Exp.t * MCPAccess.A.t [@@deriving eq, ord, hash]
+  type t = {
+    conf : int;
+    kind : AccessKind.t;
+    node : Node.t;
+    exp : CilType.Exp.t;
+    acc : MCPAccess.A.t;
+  } [@@deriving eq, ord, hash]
 
   let name () = "access"
 
-  let pretty () (conf, kind, node, e, lp) =
-    Pretty.dprintf "%d, %a, %a, %a, %a" conf AccessKind.pretty kind CilType.Location.pretty (Node.location node) CilType.Exp.pretty e MCPAccess.A.pretty lp
+  let pretty () {conf; kind; node; exp; acc} =
+    Pretty.dprintf "%d, %a, %a, %a, %a" conf AccessKind.pretty kind CilType.Location.pretty (Node.location node) CilType.Exp.pretty exp MCPAccess.A.pretty acc
 
   include Printable.SimplePretty (
     struct
@@ -343,10 +349,8 @@ struct
     end
     )
 
-  let conf (conf, _, _, _, _) = conf
-
-  let relift (conf, kind, node, e, a) =
-    (conf, kind, node, e, MCPAccess.A.relift a)
+  let relift {conf; kind; node; exp; acc} =
+    {conf; kind; node; exp; acc = MCPAccess.A.relift acc}
 end
 
 module AS =
@@ -354,17 +358,17 @@ struct
   include SetDomain.Make (A)
 
   let max_conf accs =
-    accs |> elements |> List.map A.conf |> (List.max ~cmp:Int.compare)
+    accs |> elements |> List.map (fun {A.conf; _} -> conf) |> (List.max ~cmp:Int.compare)
 end
 
 
 (* Check if two accesses may race and if yes with which confidence *)
-let may_race (conf,(kind: AccessKind.t),loc,e,a) (conf2,(kind2: AccessKind.t),loc2,e2,a2) =
+let may_race A.{kind; acc; _} A.{kind=kind2; acc=acc2; _} =
   if kind = Read && kind2 = Read then
     false (* two read/read accesses do not race *)
   else if not (get_bool "ana.race.free") && (kind = Free || kind2 = Free) then
     false
-  else if not (MCPAccess.A.may_race a a2) then
+  else if not (MCPAccess.A.may_race acc acc2) then
     false (* analysis-specific information excludes race *)
   else
     true
@@ -487,7 +491,7 @@ let race_conf accs =
   if AS.cardinal accs = 1 then ( (* singleton component *)
     let acc = AS.choose accs in
     if may_race acc acc then (* self-race *)
-      Some (A.conf acc)
+      Some (acc.conf)
     else
       None
   )
@@ -516,9 +520,8 @@ let print_accesses memo grouped_accs =
   let allglobs = get_bool "allglobs" in
   let race_threshold = get_int "warn.race-threshold" in
   let msgs race_accs =
-    let h (conf,kind,node,e,a) =
-      let d_msg () = dprintf "%a with %a (conf. %d)" AccessKind.pretty kind MCPAccess.A.pretty a conf in
-      let doc = dprintf "%t  (exp: %a)" d_msg d_exp e in
+    let h A.{conf; kind; node; exp; acc} =
+      let doc = dprintf "%a with %a (conf. %d)  (exp: %a)" AccessKind.pretty kind MCPAccess.A.pretty acc conf d_exp exp in
       (doc, Some (Messages.Location.Node node))
     in
     AS.elements race_accs
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index 26fdfac606..47be7458c1 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -776,16 +776,16 @@ struct
           end
         else begin
           let geq = if var_arg then ">=" else "" in
-          M.warn ~tags:[CWE 685] "Potential call to function %a with wrong number of arguments (expected: %s%d, actual: %d). This call will be ignored." CilType.Varinfo.pretty f geq p_length arg_length;
+          M.warn ~category:Unsound ~tags:[Category Call; CWE 685] "Potential call to function %a with wrong number of arguments (expected: %s%d, actual: %d). This call will be ignored." CilType.Varinfo.pretty f geq p_length arg_length;
           None
         end
       | _ ->
-        M.warn  ~category:Call "Something that is not a function (%a) is called." CilType.Varinfo.pretty f;
+        M.warn ~category:Call "Something that is not a function (%a) is called." CilType.Varinfo.pretty f;
         None
     in
     let funs = List.filter_map one_function functions in
     if [] = funs then begin
-      M.warn ~category:Unsound "No suitable function to be called at call site. Continuing with state before call.";
+      M.warn ~category:Unsound ~tags:[Category Call] "No suitable function to be called at call site. Continuing with state before call.";
       d (* because LevelSliceLifter *)
     end else
       common_joins ctx funs !r !spawns
diff --git a/src/maingoblint.ml b/src/maingoblint.ml
index 8944d87ea0..155faa0e76 100644
--- a/src/maingoblint.ml
+++ b/src/maingoblint.ml
@@ -417,10 +417,9 @@ let parse_preprocessed preprocessed =
 
   let goblint_cwd = GobFpath.cwd () in
   let get_ast_and_record_deps (preprocessed_file, task_opt) =
-    let transform_file (path_str, system_header) = match path_str with
-      | "<built-in>" | "<command-line>" ->
+    let transform_file (path_str, system_header) = if Str.string_match (Str.regexp "<.+>") path_str 0 then
         (path_str, system_header) (* ignore special "paths" *)
-      | _ ->
+      else
         let path = Fpath.v path_str in
         let path' = if get_bool "pre.transform-paths" then (
             let cwd_opt =
@@ -584,19 +583,19 @@ let do_gobview cilfile =
       let file_dir = Fpath.(run_dir / "files") in
       GobSys.mkdir_or_exists file_dir;
       let file_loc = Hashtbl.create 113 in
-      let counter = ref 0 in
-      let copy path =
+      let copy (path, i) =
         let name, ext = Fpath.split_ext (Fpath.base path) in
-        let unique_name = Fpath.add_ext ext (Fpath.add_ext (string_of_int !counter) name) in
-        counter := !counter + 1;
+        let unique_name = Fpath.add_ext ext (Fpath.add_ext (string_of_int i) name) in
         let dest = Fpath.(file_dir // unique_name) in
         let gobview_path = match Fpath.relativize ~root:run_dir dest with
           | Some p -> Fpath.to_string p
           | None -> failwith "The gobview directory should be a prefix of the paths of c files copied to the gobview directory" in
         Hashtbl.add file_loc (Fpath.to_string path) gobview_path;
-        FileUtil.cp [Fpath.to_string path] (Fpath.to_string dest) in
+        FileUtil.cp [Fpath.to_string path] (Fpath.to_string dest)
+      in
       let source_paths = Preprocessor.FpathH.to_list Preprocessor.dependencies |> List.concat_map (fun (_, m) -> Fpath.Map.fold (fun p _ acc -> p::acc) m []) in
-      List.iter copy source_paths;
+      let source_file_paths = List.filteri_map (fun i e -> if Fpath.is_file_path e then Some (e, i) else None) source_paths in
+      List.iter copy source_file_paths;
       Serialize.marshal file_loc (Fpath.(run_dir / "file_loc.marshalled"));
       (* marshal timing statistics *)
       let stats = Fpath.(run_dir / "stats.marshalled") in
diff --git a/src/solvers/sLRphased.ml b/src/solvers/sLRphased.ml
index f4c3389f1d..c120a7bc6c 100644
--- a/src/solvers/sLRphased.ml
+++ b/src/solvers/sLRphased.ml
@@ -73,7 +73,7 @@ module Make =
         let effects = ref Set.empty in
         let side y d =
           assert (not (S.Dom.is_bot d));
-          trace "sol" "SIDE: Var: %a\nVal: %a\n" S.Var.pretty_trace y S.Dom.pretty d;
+          if tracing then trace "sol" "SIDE: Var: %a\nVal: %a\n" S.Var.pretty_trace y S.Dom.pretty d;
           let first = not (Set.mem y !effects) in
           effects := Set.add y !effects;
           if first then (
@@ -109,11 +109,11 @@ module Make =
           if wpx then
             if b then
               let nar = narrow old tmp in
-              trace "sol" "NARROW: Var: %a\nOld: %a\nNew: %a\nWiden: %a\n" S.Var.pretty_trace x S.Dom.pretty old S.Dom.pretty tmp S.Dom.pretty nar;
+              if tracing then trace "sol" "NARROW: Var: %a\nOld: %a\nNew: %a\nWiden: %a\n" S.Var.pretty_trace x S.Dom.pretty old S.Dom.pretty tmp S.Dom.pretty nar;
               nar
             else
               let wid = S.Dom.widen old (S.Dom.join old tmp) in
-              trace "sol" "WIDEN: Var: %a\nOld: %a\nNew: %a\nWiden: %a\n" S.Var.pretty_trace x S.Dom.pretty old S.Dom.pretty tmp S.Dom.pretty wid;
+              if tracing then trace "sol" "WIDEN: Var: %a\nOld: %a\nNew: %a\nWiden: %a\n" S.Var.pretty_trace x S.Dom.pretty old S.Dom.pretty tmp S.Dom.pretty wid;
               wid
           else
             tmp
@@ -163,7 +163,7 @@ module Make =
       and sides x =
         let w = try HM.find set x with Not_found -> VS.empty in
         let v = Enum.fold (fun d z -> try S.Dom.join d (HPM.find rho' (z,x)) with Not_found -> d) (S.Dom.bot ()) (VS.enum w)
-        in trace "sol" "SIDES: Var: %a\nVal: %a\n" S.Var.pretty_trace x S.Dom.pretty v; v
+        in if tracing then trace "sol" "SIDES: Var: %a\nVal: %a\n" S.Var.pretty_trace x S.Dom.pretty v; v
       and eq x get set =
         eval_rhs_event x;
         match S.system x with
diff --git a/src/solvers/sLRterm.ml b/src/solvers/sLRterm.ml
index d4f4671c46..eb11447d11 100644
--- a/src/solvers/sLRterm.ml
+++ b/src/solvers/sLRterm.ml
@@ -64,14 +64,14 @@ module SLR3term =
           HM.replace rho  x (S.Dom.bot ());
           HM.replace infl x (VS.add x VS.empty);
           let c = if side then count_side else count in
-          trace "sol" "INIT: Var: %a with prio %d\n" S.Var.pretty_trace x !c;
+          if tracing then trace "sol" "INIT: Var: %a with prio %d\n" S.Var.pretty_trace x !c;
           HM.replace key x !c; decr c
         end
       in
       let sides x =
         let w = try HM.find set x with Not_found -> VS.empty in
         let v = Enum.fold (fun d z -> try S.Dom.join d (HPM.find rho' (z,x)) with Not_found -> d) (S.Dom.bot ()) (VS.enum w) in
-        trace "sol" "SIDES: Var: %a\nVal: %a\n" S.Var.pretty_trace x S.Dom.pretty v; v
+        if tracing then trace "sol" "SIDES: Var: %a\nVal: %a\n" S.Var.pretty_trace x S.Dom.pretty v; v
       in
       let rec iterate b_old prio =
         if H.size !q = 0 || min_key q > prio then ()
@@ -122,7 +122,7 @@ module SLR3term =
           )
           *)
           (* if S.Dom.is_bot d then print_endline "BOT" else *)
-          trace "sol" "SIDE: Var: %a\nVal: %a\n" S.Var.pretty_trace y S.Dom.pretty d;
+          if tracing then trace "sol" "SIDE: Var: %a\nVal: %a\n" S.Var.pretty_trace y S.Dom.pretty d;
           let first = not (Set.mem y !effects) in
           effects := Set.add y !effects;
           if first then (
@@ -156,17 +156,17 @@ module SLR3term =
           if wpx then
             if S.Dom.leq tmp old then (
               let nar = narrow old tmp in
-              trace "sol" "NARROW1: Var: %a\nOld: %a\nNew: %a\nNarrow: %a" S.Var.pretty_trace x S.Dom.pretty old S.Dom.pretty tmp S.Dom.pretty nar;
+              if tracing then trace "sol" "NARROW1: Var: %a\nOld: %a\nNew: %a\nNarrow: %a" S.Var.pretty_trace x S.Dom.pretty old S.Dom.pretty tmp S.Dom.pretty nar;
               nar, true
             ) else
             if b_old then (
               let nar = narrow old tmp in
-              trace "sol" "NARROW2: Var: %a\nOld: %a\nNew: %a\nNarrow: %a" S.Var.pretty_trace x S.Dom.pretty old S.Dom.pretty tmp S.Dom.pretty nar;
+              if tracing then trace "sol" "NARROW2: Var: %a\nOld: %a\nNew: %a\nNarrow: %a" S.Var.pretty_trace x S.Dom.pretty old S.Dom.pretty tmp S.Dom.pretty nar;
               nar, true
             )
             else (
               let wid = S.Dom.widen old (S.Dom.join old tmp) in
-              trace "sol" "WIDEN: Var: %a\nOld: %a\nNew: %a\nWiden: %a" S.Var.pretty_trace x S.Dom.pretty old S.Dom.pretty tmp S.Dom.pretty wid;
+              if tracing then trace "sol" "WIDEN: Var: %a\nOld: %a\nNew: %a\nWiden: %a" S.Var.pretty_trace x S.Dom.pretty old S.Dom.pretty tmp S.Dom.pretty wid;
               wid, false
             )
           else
diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml
index 29ad301292..07edc632c7 100644
--- a/src/solvers/td3.ml
+++ b/src/solvers/td3.ml
@@ -327,7 +327,7 @@ module Base =
               else
                 box old eqd
           in
-          if tracing then trace "sol" "Var: %a (wp: %b)\nOld value: %a\nNew value: %a\n" S.Var.pretty_trace x wp S.Dom.pretty old S.Dom.pretty wpd;
+          if tracing then trace "sol" "Var: %a (wp: %b)\nOld value: %a\nEqd: %a\nNew value: %a\n" S.Var.pretty_trace x wp S.Dom.pretty old S.Dom.pretty eqd S.Dom.pretty wpd;
           if cache then (
             if tracing then trace "cache" "cache size %d for %a\n" (HM.length l) S.Var.pretty_trace x;
             cache_sizes := HM.length l :: !cache_sizes;
diff --git a/src/util/cilfacade.ml b/src/util/cilfacade.ml
index c77d2cd738..eb7330aa19 100644
--- a/src/util/cilfacade.ml
+++ b/src/util/cilfacade.ml
@@ -342,22 +342,23 @@ let makeBinOp binop e1 e2 =
   let (_, e) = Cabs2cil.doBinOp binop e1 t1 e2 t2 in
   e
 
-let anoncomp_name_regexp = Str.regexp {|^__anon\(struct\|union\)_\(.+\)_\([0-9]+\)$|}
+let anoncomp_name_regexp = Str.regexp {|^__anon\(struct\|union\)\(_\(.+\)\)?_\([0-9]+\)$|}
 
 let split_anoncomp_name name =
   (* __anonunion_pthread_mutexattr_t_488594144 *)
+  (* __anonunion_50 *)
   if Str.string_match anoncomp_name_regexp name 0 then (
     let struct_ = match Str.matched_group 1 name with
       | "struct" -> true
       | "union" -> false
       | _ -> assert false
     in
-    let name' = Str.matched_group 2 name in
-    let id = int_of_string (Str.matched_group 3 name) in
+    let name' = try Some (Str.matched_group 3 name) with Not_found -> None in
+    let id = int_of_string (Str.matched_group 4 name) in
     (struct_, name', id)
   )
   else
-    invalid_arg "Cilfacade.split_anoncomp_name"
+    invalid_arg ("Cilfacade.split_anoncomp_name: " ^ name)
 
 (** Pretty-print typsig like typ, because
     {!d_typsig} prints with CIL constructors. *)
@@ -376,7 +377,7 @@ let rec pretty_typsig_like_typ (nameOpt: Pretty.doc option) () ts =
     | _ -> pa
   in
   match ts with
-  | TSBase t -> dn_type () t
+  | TSBase t -> defaultCilPrinter#pType nameOpt () t
   | TSComp (cstruct, cname, a) ->
     let su = if cstruct then "struct" else "union" in
     text (su ^ " " ^ cname ^ " ")
diff --git a/src/util/options.schema.json b/src/util/options.schema.json
index 1ef73378fb..1b9c7d3fd5 100644
--- a/src/util/options.schema.json
+++ b/src/util/options.schema.json
@@ -1285,7 +1285,9 @@
               "sv-comp",
               "ncurses",
               "zstd",
-              "pcre"
+              "pcre",
+              "zlib",
+              "liblzma"
             ]
           },
           "default": [
diff --git a/tests/regression/03-practical/31-zstd-cctxpool-blobs.c b/tests/regression/03-practical/31-zstd-cctxpool-blobs.c
new file mode 100644
index 0000000000..40e448eb22
--- /dev/null
+++ b/tests/regression/03-practical/31-zstd-cctxpool-blobs.c
@@ -0,0 +1,29 @@
+#include <stdlib.h>
+#include <pthread.h>
+
+struct ZSTD_CCtx_s {
+  int bmi2;
+};
+
+typedef struct ZSTD_CCtx_s ZSTD_CCtx;
+
+typedef struct {
+  ZSTD_CCtx* cctx[1];
+} ZSTDMT_CCtxPool;
+
+void *t_fun(void *arg) {
+  return NULL;
+}
+
+int main() {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL); // enter multithreaded
+
+  ZSTDMT_CCtxPool* const cctxPool = calloc(1, sizeof(ZSTDMT_CCtxPool));
+  cctxPool->cctx[0] = malloc(sizeof(ZSTD_CCtx));
+  if (!cctxPool->cctx[0]) // TODO NOWARN
+    __goblint_check(1); // TODO reachable
+  else
+    __goblint_check(1); // TODO reachable
+  return 0;
+}
diff --git a/tests/regression/09-regions/40-zstd-thread-pool-region.c b/tests/regression/09-regions/40-zstd-thread-pool-region.c
new file mode 100644
index 0000000000..13baf5ec3f
--- /dev/null
+++ b/tests/regression/09-regions/40-zstd-thread-pool-region.c
@@ -0,0 +1,34 @@
+// SKIP PARAM: --set ana.activated[+] region
+// FIXPOINT
+#include<stdlib.h>
+#include<pthread.h>
+#include<goblint.h>
+
+typedef struct POOL_job_s {
+    void *opaque;
+} POOL_job;
+
+typedef struct POOL_ctx_s {
+    POOL_job *queue;
+} POOL_ctx;
+
+POOL_ctx* ctx_global;
+
+POOL_ctx* POOL_create(size_t numThreads, size_t queueSize)
+{
+    POOL_ctx* ctx_create;
+    ctx_create = (POOL_ctx*)malloc(sizeof(POOL_ctx));
+    ctx_create->queue = (POOL_job*)malloc(queueSize * sizeof(POOL_job));
+
+    int r; // rand
+    if (r)
+        ctx_global = ctx_create; // pretend escape
+    return ctx_create;
+}
+
+int main() {
+    while (1) {
+        POOL_ctx *ctx_main;
+        ctx_main = POOL_create(20, 10);
+    }
+}
diff --git a/tests/regression/10-synch/07-thread_self_create.c b/tests/regression/10-synch/07-thread_self_create.c
new file mode 100644
index 0000000000..473a26a25b
--- /dev/null
+++ b/tests/regression/10-synch/07-thread_self_create.c
@@ -0,0 +1,15 @@
+// PARAM: --set ana.activated[+] thread
+// Checks termination of thread analysis with a thread who is its own single parent.
+#include <pthread.h>
+
+void *t_fun(void *arg) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  return 0;
+}
diff --git a/tests/regression/37-congruence/06-refinements.c b/tests/regression/37-congruence/06-refinements.c
index c0b7b0564c..38bf9458cc 100644
--- a/tests/regression/37-congruence/06-refinements.c
+++ b/tests/regression/37-congruence/06-refinements.c
@@ -5,14 +5,15 @@ int main() {
     int top;
     int i = 0;
     if(top % 17 == 3) {
-        __goblint_check(top%17 ==3);
+        __goblint_check(top%17 ==3); //TODO (Refine top to be positive above, and reuse information in %)
         if(top %17 != 3) {
             i = 12;
         } else {
 
         }
     }
-    __goblint_check(i ==0);
+    __goblint_check(i ==0); // TODO
+    i = 0;
 
     if(top % 17 == 0) {
         __goblint_check(top%17 == 0);
diff --git a/tests/regression/37-congruence/07-refinements-o.c b/tests/regression/37-congruence/07-refinements-o.c
index 44f21b7c8c..49148d6683 100644
--- a/tests/regression/37-congruence/07-refinements-o.c
+++ b/tests/regression/37-congruence/07-refinements-o.c
@@ -32,15 +32,16 @@ int main() {
     int top;
     int i = 0;
     if(top % 17 == 3) {
-        __goblint_check(top%17 ==3);
+        __goblint_check(top%17 ==3); //TODO (Refine top to be positive above, and reuse information in %)
         if(top %17 != 3) {
             i = 12;
         } else {
 
         }
     }
-    __goblint_check(i ==0);
+    __goblint_check(i ==0); //TODO
 
+    i = 0;
     if(top % 17 == 0) {
         __goblint_check(top%17 == 0);
         if(top %17 != 0) {
diff --git a/tests/regression/37-congruence/11-overflow-signed.c b/tests/regression/37-congruence/11-overflow-signed.c
index 29599fe246..031d88ce45 100644
--- a/tests/regression/37-congruence/11-overflow-signed.c
+++ b/tests/regression/37-congruence/11-overflow-signed.c
@@ -12,8 +12,8 @@ int basic(){
 	{
 		if (b % two_pow_16 == 5)
 		{
-			__goblint_check(a % two_pow_16 == 3);
-			__goblint_check(b % two_pow_16 == 5);
+			__goblint_check(a % two_pow_16 == 3); //TODO (Refine a to be positive above, and reuse information in %)
+			__goblint_check(b % two_pow_16 == 5); //TODO (Refine a to be positive above, and reuse information in %)
 
 			unsigned int e = a * b;
 			__goblint_check(e % two_pow_16 == 15); // UNKNOWN!
@@ -35,7 +35,7 @@ int special(){
 
 	if (a % two_pow_18 == two_pow_17)
 	{
-		__goblint_check(a % two_pow_18 == two_pow_17);
+		__goblint_check(a % two_pow_18 == two_pow_17); //TODO (Refine a to be positive above, and reuse information in %)
 
 		unsigned int e = a * a;
 		__goblint_check(e == 0); //UNKNOWN!
diff --git a/tests/regression/37-congruence/13-bitand.c b/tests/regression/37-congruence/13-bitand.c
new file mode 100644
index 0000000000..500fb9d1cc
--- /dev/null
+++ b/tests/regression/37-congruence/13-bitand.c
@@ -0,0 +1,46 @@
+// PARAM: --enable ana.int.congruence --set sem.int.signed_overflow assume_none
+#include <goblint.h>
+
+int main()
+{
+	// Assuming modulo expression
+
+	unsigned long x;
+	__goblint_assume(x % 2 == 1);
+	__goblint_check(x % 2 == 1);
+	__goblint_check(x & 1);
+
+	long xx;
+	__goblint_assume(xx % 2 == 1);
+	__goblint_check(xx % 2 == 1); //TODO (Refine xx to be positive above, and reuse information in %)
+	__goblint_check(xx & 1);
+
+	long y;
+	__goblint_assume(y % 2 == 0);
+	__goblint_check(y % 2 == 0);
+	__goblint_check(y & 1); //FAIL
+
+	long z;
+	__goblint_check(z & 1); //UNKNOWN!
+	__goblint_assume(z % 8 == 1);
+	__goblint_check(z & 1);
+
+	long xz;
+	__goblint_assume(xz % 3 == 1);
+	__goblint_check(xz & 1); //UNKNOWN!
+	__goblint_assume(xz % 6 == 1);
+	__goblint_check(xz & 1);
+
+	// Assuming bitwise expression
+	// Does NOT actually lead to modulo information, as negative values may also have their last bit set!
+
+	long a;
+	__goblint_assume(a & 1);
+	__goblint_check(a % 2 == 1); //UNKNOWN!
+	__goblint_check(a & 1);
+
+	int b;
+	__goblint_assume(b & 1);
+	__goblint_check(b % 2 == 1); //UNKNOWN!
+	__goblint_check(b & 1);
+}
diff --git a/tests/regression/37-congruence/14-negative.c b/tests/regression/37-congruence/14-negative.c
new file mode 100644
index 0000000000..eae8307ab1
--- /dev/null
+++ b/tests/regression/37-congruence/14-negative.c
@@ -0,0 +1,15 @@
+// PARAM: --enable ana.int.congruence --set sem.int.signed_overflow assume_none
+#include <goblint.h>
+
+int main()
+{
+	int top;
+
+	int c = -5;
+	if (top)
+	{
+		c = -7;
+	}
+	__goblint_check(c % 2 == 1); //UNKNOWN! (Does not hold at runtime)
+	__goblint_check(c % 2 == -1); //TODO (Track information that c is negative)
+}
diff --git a/tests/regression/68-longjmp/52-races.c b/tests/regression/68-longjmp/52-races.c
new file mode 100644
index 0000000000..4cde97d954
--- /dev/null
+++ b/tests/regression/68-longjmp/52-races.c
@@ -0,0 +1,35 @@
+// PARAM: --enable ana.int.interval
+#include <stdio.h>
+#include <stdlib.h>
+#include <setjmp.h>
+#include <pthread.h>
+
+jmp_buf env_buffer;
+int global = 0;
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&mutex1);
+  global = 3; // NORACE
+  pthread_mutex_unlock(&mutex1);
+  return NULL;
+}
+
+int bar() {
+   pthread_mutex_lock(&mutex1);
+   longjmp(env_buffer, 2);
+   pthread_mutex_unlock(&mutex1);
+   return 8;
+}
+
+int main() {
+   pthread_t id;
+   pthread_create(&id, NULL, t_fun, NULL);
+
+   if(!setjmp( env_buffer )) {
+      bar();
+   }
+
+   global = 5; // NORACE
+   pthread_mutex_unlock(&mutex1);
+}
diff --git a/tests/regression/68-longjmp/53-races-no.c b/tests/regression/68-longjmp/53-races-no.c
new file mode 100644
index 0000000000..4692f6ca18
--- /dev/null
+++ b/tests/regression/68-longjmp/53-races-no.c
@@ -0,0 +1,36 @@
+// PARAM: --enable ana.int.interval
+#include <stdio.h>
+#include <stdlib.h>
+#include <setjmp.h>
+#include <pthread.h>
+
+jmp_buf env_buffer;
+int global = 0;
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&mutex1);
+  global = 3; // NORACE
+  pthread_mutex_unlock(&mutex1);
+  return NULL;
+}
+
+int bar() {
+   pthread_mutex_lock(&mutex1);
+   if(global ==3) {
+      longjmp(env_buffer, 2);
+   }
+   return 8;
+}
+
+int main() {
+   pthread_t id;
+   pthread_create(&id, NULL, t_fun, NULL);
+
+   if(!setjmp( env_buffer )) {
+      bar();
+   }
+
+   global = 5; // NORACE
+   pthread_mutex_unlock(&mutex1);
+}
diff --git a/tests/regression/68-longjmp/54-races-actually.c b/tests/regression/68-longjmp/54-races-actually.c
new file mode 100644
index 0000000000..62423cd884
--- /dev/null
+++ b/tests/regression/68-longjmp/54-races-actually.c
@@ -0,0 +1,50 @@
+// PARAM: --enable ana.int.interval
+#include <stdio.h>
+#include <stdlib.h>
+#include <setjmp.h>
+#include <pthread.h>
+
+jmp_buf env_buffer;
+int global = 0;
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&mutex1);
+  global = 3; // RACE
+  pthread_mutex_unlock(&mutex1);
+  return NULL;
+}
+
+int bar() {
+   pthread_mutex_lock(&mutex1);
+   if(global == 3) {
+      longjmp(env_buffer, 2);
+   } else {
+      longjmp(env_buffer, 4);
+   }
+   return 8;
+}
+
+int main() {
+   pthread_t id;
+   pthread_create(&id, NULL, t_fun, NULL);
+   int n = 0;
+
+   switch(setjmp( env_buffer )) {
+      case 0:
+         bar();
+         break;
+      case 2:
+         n=1;
+         pthread_mutex_unlock(&mutex1);
+         break;
+      default:
+         break;
+   }
+
+   global = 5; //RACE
+
+   if(n == 0) {
+      pthread_mutex_unlock(&mutex1);
+   }
+}
diff --git a/tests/regression/68-longjmp/55-races-no-return.c b/tests/regression/68-longjmp/55-races-no-return.c
new file mode 100644
index 0000000000..850fc54fa5
--- /dev/null
+++ b/tests/regression/68-longjmp/55-races-no-return.c
@@ -0,0 +1,50 @@
+// PARAM: --enable ana.int.interval
+#include <stdio.h>
+#include <stdlib.h>
+#include <setjmp.h>
+#include <pthread.h>
+
+jmp_buf env_buffer;
+int global = 0;
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&mutex1);
+  global = 3; //NORACE
+  pthread_mutex_unlock(&mutex1);
+  return NULL;
+}
+
+int bar() {
+   pthread_mutex_lock(&mutex1);
+   if(global == 7) {
+      longjmp(env_buffer, 2);
+   } else {
+      longjmp(env_buffer, 4);
+   }
+   return 8;
+}
+
+int main() {
+   pthread_t id;
+   pthread_create(&id, NULL, t_fun, NULL);
+   int n = 0;
+
+   switch(setjmp( env_buffer )) {
+      case 0:
+         bar();
+         break;
+      case 2:
+         n=1;
+         pthread_mutex_unlock(&mutex1);
+         break;
+      default:
+         break;
+   }
+
+   global = 5; //NORACE
+
+   if(n == 0) {
+      pthread_mutex_unlock(&mutex1);
+   }
+}
diff --git a/tests/regression/70-transform/02-deadcode.t b/tests/regression/70-transform/02-deadcode.t
index ed3cd80e17..03a46b891e 100644
--- a/tests/regression/70-transform/02-deadcode.t
+++ b/tests/regression/70-transform/02-deadcode.t
@@ -210,15 +210,15 @@
 
 Transformation still works with 'exp.mincfg', but can not find all dead code; test against the diff.
 Macintosh's diff(1) adds whitespace after the function names, strip with sed.
-  $ diff -p -U0 "$(./transform.sh --file $args 02-deadcode.c)" "$(./transform.sh --file $args --enable exp.mincfg 02-deadcode.c)" | sed 's/[[:blank:]]*$//' | tail +3
-  @@ -13,0 +14,3 @@ int basic1(int n )
+  $ diff -U0 "$(./transform.sh --file $args 02-deadcode.c)" "$(./transform.sh --file $args --enable exp.mincfg 02-deadcode.c)" | sed 's/[[:blank:]]*$//' | tail -n +3
+  @@ -13,0 +14,3 @@
   +  if (n < 0) {
   +    return (0);
   +  }
-  @@ -54,0 +58,2 @@ int one_branch_dead(int x )
+  @@ -54,0 +58,2 @@
   +  } else {
   +    return (7 - x);
-  @@ -65,0 +71,8 @@ int uncalled_but_referenced_function(int
+  @@ -65,0 +71,8 @@
   +int uncalled1(void)
   +{
   +
@@ -227,17 +227,17 @@ Macintosh's diff(1) adds whitespace after the function names, strip with sed.
   +
   +}
   +}
-  @@ -79,0 +93,5 @@ int conditional_call_in_loop(int x )
+  @@ -79,0 +93,5 @@
   +    if (i > 7) {
   +      {
   +      uncalled1();
   +      }
   +    }
-  @@ -151,0 +170,4 @@ int loop_dead_on_break(int z )
+  @@ -151,0 +170,4 @@
   +    {
   +    s += s;
   +    i ++;
   +    }
-  @@ -203,0 +226,2 @@ int main(void)
+  @@ -203,0 +226,2 @@
   +  uncalled1();
   +  uncalled_but_referenced_function(3);
diff --git a/unittest/mainTest.ml b/unittest/mainTest.ml
index df67340309..642e495d50 100644
--- a/unittest/mainTest.ml
+++ b/unittest/mainTest.ml
@@ -8,6 +8,7 @@ let all_tests = ("" >:::
     LvalTest.test ();
     CompilationDatabaseTest.tests;
     LibraryDslTest.tests;
+    CilfacadeTest.tests;
     (* etc *)
     "domaintest" >::: QCheck_ounit.to_ounit2_test_list Maindomaintest.all_testsuite;
     IntOpsTest.tests;
diff --git a/unittest/util/cilfacadeTest.ml b/unittest/util/cilfacadeTest.ml
new file mode 100644
index 0000000000..482a502824
--- /dev/null
+++ b/unittest/util/cilfacadeTest.ml
@@ -0,0 +1,14 @@
+open Goblint_lib
+open OUnit2
+open Cilfacade
+
+let test_split_anoncomp_name _ =
+  let assert_equal = assert_equal ~printer:[%show: bool * string option * int] in
+  assert_equal (false, Some "pthread_mutexattr_t", 488594144) (split_anoncomp_name "__anonunion_pthread_mutexattr_t_488594144");
+  assert_equal (true, Some "__once_flag", 1234) (split_anoncomp_name "__anonstruct___once_flag_1234");
+  assert_equal (false, None, 50) (split_anoncomp_name "__anonunion_50")
+
+let tests =
+  "cilfacadeTest" >::: [
+    "split_anoncomp_name" >:: test_split_anoncomp_name;
+  ]