diff --git a/.github/workflows/coverage.yml b/.github/workflows/coverage.yml
index d4fc872620..7f6d5a1cfb 100644
--- a/.github/workflows/coverage.yml
+++ b/.github/workflows/coverage.yml
@@ -18,7 +18,7 @@ jobs:
         os:
           - ubuntu-latest
         ocaml-compiler:
-          - ocaml-variants.4.14.0+options,ocaml-option-flambda # matches opam lock file
+          - ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
           # don't add any other because they won't be used
 
     runs-on: ${{ matrix.os }}
@@ -35,10 +35,9 @@ jobs:
           # otherwise setup-ocaml pins non-locked dependencies
           # https://github.com/ocaml/setup-ocaml/issues/166
           OPAMLOCKED: locked
-        uses: ocaml/setup-ocaml@v2
+        uses: ocaml/setup-ocaml@v3
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
-          opam-depext-flags: --with-test # doesn't work (https://github.com/ocaml/opam/issues/5836)
 
       - name: Install graph-easy # TODO: remove if depext --with-test works
         if: ${{ matrix.os == 'ubuntu-latest' }}
diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml
index 242acef3de..c5b414a741 100644
--- a/.github/workflows/docs.yml
+++ b/.github/workflows/docs.yml
@@ -18,7 +18,7 @@ jobs:
         os:
           - ubuntu-latest
         ocaml-compiler:
-          - ocaml-variants.4.14.0+options,ocaml-option-flambda # matches opam lock file
+          - ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
           # don't add any other because they won't be used
 
     runs-on: ${{ matrix.os }}
@@ -35,7 +35,7 @@ jobs:
           # otherwise setup-ocaml pins non-locked dependencies
           # https://github.com/ocaml/setup-ocaml/issues/166
           OPAMLOCKED: locked
-        uses: ocaml/setup-ocaml@v2
+        uses: ocaml/setup-ocaml@v3
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
 
diff --git a/.github/workflows/indentation.yml b/.github/workflows/indentation.yml
index e22e674301..96ef5ee56a 100644
--- a/.github/workflows/indentation.yml
+++ b/.github/workflows/indentation.yml
@@ -25,7 +25,7 @@ jobs:
           fetch-depth: 0
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
-        uses: ocaml/setup-ocaml@v2
+        uses: ocaml/setup-ocaml@v3
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
 
diff --git a/.github/workflows/locked.yml b/.github/workflows/locked.yml
index 18935725ca..4f892ea419 100644
--- a/.github/workflows/locked.yml
+++ b/.github/workflows/locked.yml
@@ -20,7 +20,7 @@ jobs:
           - ubuntu-latest
           - macos-13
         ocaml-compiler:
-          - ocaml-variants.4.14.0+options,ocaml-option-flambda # matches opam lock file
+          - ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
           # don't add any other because they won't be used
 
     runs-on: ${{ matrix.os }}
@@ -37,10 +37,9 @@ jobs:
           # otherwise setup-ocaml pins non-locked dependencies
           # https://github.com/ocaml/setup-ocaml/issues/166
           OPAMLOCKED: locked
-        uses: ocaml/setup-ocaml@v2
+        uses: ocaml/setup-ocaml@v3
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
-          opam-depext-flags: --with-test # doesn't work (https://github.com/ocaml/opam/issues/5836)
 
       - name: Install graph-easy # TODO: remove if depext --with-test works
         if: ${{ matrix.os == 'ubuntu-latest' }}
@@ -73,7 +72,7 @@ jobs:
         os:
           - ubuntu-latest
         ocaml-compiler:
-          - ocaml-variants.4.14.0+options,ocaml-option-flambda # matches opam lock file
+          - ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
           # don't add any other because they won't be used
 
     runs-on: ${{ matrix.os }}
@@ -87,10 +86,9 @@ jobs:
           # otherwise setup-ocaml pins non-locked dependencies
           # https://github.com/ocaml/setup-ocaml/issues/166
           OPAMLOCKED: locked
-        uses: ocaml/setup-ocaml@v2
+        uses: ocaml/setup-ocaml@v3
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
-          opam-depext-flags: --with-test # doesn't work (https://github.com/ocaml/opam/issues/5836)
 
       - name: Install graph-easy # TODO: remove if depext --with-test works
         if: ${{ matrix.os == 'ubuntu-latest' }}
@@ -116,7 +114,7 @@ jobs:
         os:
           - ubuntu-latest
         ocaml-compiler:
-          - ocaml-variants.4.14.0+options,ocaml-option-flambda # matches opam lock file
+          - ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
           # don't add any other because they won't be used
         node-version:
           - 14
@@ -132,7 +130,7 @@ jobs:
           # otherwise setup-ocaml pins non-locked dependencies
           # https://github.com/ocaml/setup-ocaml/issues/166
           OPAMLOCKED: locked
-        uses: ocaml/setup-ocaml@v2
+        uses: ocaml/setup-ocaml@v3
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
 
diff --git a/.github/workflows/unlocked.yml b/.github/workflows/unlocked.yml
index f1bd399a17..0c4433d0af 100644
--- a/.github/workflows/unlocked.yml
+++ b/.github/workflows/unlocked.yml
@@ -21,7 +21,7 @@ jobs:
           - 5.2.x
           - 5.1.x
           - 5.0.x
-          - ocaml-variants.4.14.0+options,ocaml-option-flambda
+          - ocaml-variants.4.14.2+options,ocaml-option-flambda
           - 4.14.x
         apron:
           - false
@@ -33,6 +33,8 @@ jobs:
           - os: ubuntu-latest
             ocaml-compiler: 4.14.x
             z3: true
+          - os: macos-latest
+            ocaml-compiler: 4.14.x
 
     # customize name to use readable string for apron instead of just a boolean
     # workaround for missing ternary operator: https://github.com/actions/runner/issues/409
@@ -45,10 +47,9 @@ jobs:
         uses: actions/checkout@v4
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
-        uses: ocaml/setup-ocaml@v2
+        uses: ocaml/setup-ocaml@v3
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
-          opam-depext-flags: --with-test # doesn't work (https://github.com/ocaml/opam/issues/5836)
 
       - name: Install graph-easy # TODO: remove if depext --with-test works
         if: ${{ matrix.os == 'ubuntu-latest' }}
@@ -92,7 +93,7 @@ jobs:
           - ubuntu-latest
           - macos-13
         ocaml-compiler:
-          - ocaml-variants.4.14.0+options,ocaml-option-flambda # matches opam lock file, downgrade deps step
+          - ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file, downgrade deps step
 
     name: lower-bounds (${{ matrix.os }}, ${{ matrix.ocaml-compiler }}, downgrade)
 
@@ -109,7 +110,6 @@ jobs:
         uses: ocaml/setup-ocaml@v2
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
-          opam-depext-flags: --with-test # doesn't work (https://github.com/ocaml/opam/issues/5836)
 
       - name: Install graph-easy # TODO: remove if depext --with-test works
         if: ${{ matrix.os == 'ubuntu-latest' }}
@@ -133,7 +133,7 @@ jobs:
       - name: Downgrade dependencies
         # must specify ocaml-base-compiler again to prevent it from being downgraded
         # prevent num downgrade to avoid dune/jbuilder error: https://github.com/ocaml/dune/issues/5280
-        run: opam install $(opam exec -- opam-0install --prefer-oldest goblint ocaml-variants.4.14.0+options ocaml-option-flambda num.1.5)
+        run: opam install $(opam exec -- opam-0install --prefer-oldest goblint ocaml-variants.4.14.2+options ocaml-option-flambda num.1.5)
 
       - name: Build
         run: ./make.sh nat
@@ -190,7 +190,7 @@ jobs:
           - ubuntu-latest
           - macos-13
         ocaml-compiler:
-          - ocaml-variants.4.14.0+options,ocaml-option-flambda # matches opam lock file
+          - ocaml-variants.4.14.2+options,ocaml-option-flambda # matches opam lock file
 
     runs-on: ${{ matrix.os }}
 
@@ -199,10 +199,9 @@ jobs:
         uses: actions/checkout@v4
 
       - name: Set up OCaml ${{ matrix.ocaml-compiler }}
-        uses: ocaml/setup-ocaml@v2
+        uses: ocaml/setup-ocaml@v3
         with:
           ocaml-compiler: ${{ matrix.ocaml-compiler }}
-          opam-depext-flags: --with-test # doesn't work (https://github.com/ocaml/opam/issues/5836)
 
       - name: Install graph-easy # TODO: remove if depext --with-test works
         if: ${{ matrix.os == 'ubuntu-latest' }}
diff --git a/.zenodo.json b/.zenodo.json
index 22705c2d9c..1e71573948 100644
--- a/.zenodo.json
+++ b/.zenodo.json
@@ -23,6 +23,11 @@
       "affiliation": "Technische Universität München",
       "orcid": "0009-0009-9644-7475"
     },
+    {
+      "name": "Holter, Karoliine",
+      "affiliation": "University of Tartu",
+      "orcid": "0009-0008-3725-4131"
+    },
     {
       "name": "Vogler, Ralf",
       "affiliation": "Technische Universität München"
diff --git a/CHANGELOG.md b/CHANGELOG.md
index d285480259..420cc7145e 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,22 @@
+## v2.4.0
+* Remove unmaintained analyses: spec, file (#1281).
+* Add linear two-variable equalities analysis (#1297, #1412, #1466).
+* Add callstring, loopfree callstring and context gas analyses (#1038, #1340, #1379, #1427, #1439).
+* Add non-relational thread-modular value analyses with thread IDs (#1366, #1398, #1399).
+* Add NULL byte array domain (#1076).
+* Fix spurious overflow warnings from internal evaluations (#1406, #1411, #1511).
+* Refactor non-definite mutex handling to fix unsoundness (#1430, #1500, #1503, #1409).
+* Fix non-relational thread-modular value analysis unsoundness with ambiguous points-to sets (#1457, #1458).
+* 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).
+* Fix many locations in witnesses (#1355, #1372, #1400, #1403).
+* Improve output readability (#1294, #1312, #1405, #1497).
+* Refactor logging (#1117).
+* Modernize all library function specifications (#1029, #688, #1174, #1289, #1447, #1487).
+* Remove OCaml 4.10, 4.11, 4.12 and 4.13 support (#1448).
+
 ## v2.3.0
 Functionally equivalent to Goblint in SV-COMP 2024.
 
diff --git a/CITATION.cff b/CITATION.cff
index 25d46cf762..7a93859c54 100644
--- a/CITATION.cff
+++ b/CITATION.cff
@@ -21,6 +21,10 @@ authors: # same authors as in .zenodo.json and dune-project
     family-names: Tilscher
     affiliation: "Technische Universität München"
     orcid: "https://orcid.org/0009-0009-9644-7475"
+  - given-names: Karoliine
+    family-names: Holter
+    affiliation: "University of Tartu"
+    orcid: "https://orcid.org/0009-0008-3725-4131"
   - given-names: Ralf
     family-names: Vogler
     affiliation: "Technische Universität München"
diff --git a/bench/basic/benchSet.ml b/bench/basic/benchSet.ml
index 14eb03be82..ae38c156da 100644
--- a/bench/basic/benchSet.ml
+++ b/bench/basic/benchSet.ml
@@ -73,7 +73,7 @@ let () =
         ]
       );
       "const" @> lazy (
-        let args = ((fun x -> 42), set1) in
+        let args = ((fun _ -> 42), set1) in
         throughputN 1 [
           ("map1", map1, args);
           ("map2", map2, args);
diff --git a/conf/examples/medium-program.json b/conf/examples/medium-program.json
index 2c1e7c7346..5afc1aa2f8 100644
--- a/conf/examples/medium-program.json
+++ b/conf/examples/medium-program.json
@@ -9,6 +9,7 @@
       "base",
       "threadid",
       "threadflag",
+      "threadreturn",
       "mallocWrapper",
       "mutexEvents",
       "mutex",
@@ -18,6 +19,7 @@
       "expRelation",
       "mhp",
       "assert",
+      "pthreadMutexType",
       "var_eq",
       "symb_locks",
       "region",
diff --git a/conf/examples/very-precise.json b/conf/examples/very-precise.json
index 2197335eaf..074d448a85 100644
--- a/conf/examples/very-precise.json
+++ b/conf/examples/very-precise.json
@@ -22,6 +22,7 @@
       "base",
       "threadid",
       "threadflag",
+      "threadreturn",
       "mallocWrapper",
       "mutexEvents",
       "mutex",
@@ -31,6 +32,7 @@
       "expRelation",
       "mhp",
       "assert",
+      "pthreadMutexType",
       "var_eq",
       "symb_locks",
       "region",
diff --git a/conf/svcomp-validate.json b/conf/svcomp-validate.json
new file mode 100644
index 0000000000..a234aeb0d5
--- /dev/null
+++ b/conf/svcomp-validate.json
@@ -0,0 +1,142 @@
+{
+  "ana": {
+    "sv-comp": {
+      "enabled": true,
+      "functions": true
+    },
+    "int": {
+      "def_exc": true,
+      "enums": false,
+      "interval": true
+    },
+    "float": {
+      "interval": 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
+    },
+    "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"
+      }
+    },
+    "race": {
+      "free": false,
+      "call": false
+    },
+    "autotune": {
+      "enabled": true,
+      "activated": [
+        "singleThreaded",
+        "mallocWrappers",
+        "noRecursiveIntervals",
+        "enums",
+        "congruence",
+        "octagon",
+        "wideningThresholds",
+        "loopUnrollHeuristic",
+        "memsafetySpecification",
+        "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/docs/developer-guide/releasing.md b/docs/developer-guide/releasing.md
index d875c0d3bf..7530d9ad20 100644
--- a/docs/developer-guide/releasing.md
+++ b/docs/developer-guide/releasing.md
@@ -24,6 +24,8 @@
 
     All changes must be committed because the working tree is not checked.
 
+    The warning `[FAIL] opam field doc cannot be parsed by dune-release` is fine and can be ignored (see <https://github.com/ocamllabs/dune-release/issues/154>).
+
 8. Check that "unlocked" workflow passes on GitHub Actions.
 
     It can be run manually on the release branch for checking.
@@ -36,12 +38,13 @@
     1. Pull Docker image: `docker pull ocaml/opam:ubuntu-22.04-ocaml-4.14` (or newer).
     2. Extract distribution archive.
     3. Run Docker container in extracted directory: `docker run -it --rm -v $(pwd):/goblint ocaml/opam:ubuntu-22.04-ocaml-4.14` (or newer).
-    4. Navigate to distribution archive inside Docker container: `cd /goblint`.
-    5. Install and test package from distribution archive: `opam-2.1 install --with-test .`.
-    6. Activate opam environment: `eval $(opam env)`.
-    7. Check version: `goblint --version`.
-    8. Check that analysis works: `goblint -v tests/regression/04-mutex/01-simple_rc.c`.
-    9. Exit Docker container.
+    4. Update opam-repository from git: `opam-2.1 repository add git git+https://github.com/ocaml/opam-repository.git && opam-2.1 update`.
+    5. Navigate to distribution archive inside Docker container: `cd /goblint`.
+    6. Install and test package from distribution archive: `opam-2.1 install --with-test .`.
+    7. Activate opam environment: `eval $(opam env)`.
+    8. Check version: `goblint --version`.
+    9. Check that analysis works: `goblint -v tests/regression/04-mutex/01-simple_rc.c`.
+    10. Exit Docker container.
 
 12. Temporarily enable Zenodo GitHub webhook.
 
diff --git a/docs/user-guide/assumptions.md b/docs/user-guide/assumptions.md
index f77e3b5097..33284ccc00 100644
--- a/docs/user-guide/assumptions.md
+++ b/docs/user-guide/assumptions.md
@@ -17,3 +17,22 @@ _NB! This list is likely incomplete._
 
     See [PR #1414](https://github.com/goblint/analyzer/pull/1414).
 
+2.  Pointer arithmetic does not overflow.
+
+    [C11's N1570][n1570] at 6.5.6.8 states that
+
+    > When an expression that has integer type is added to or subtracted from a pointer, the result has the type of the pointer operand.
+    > [...]
+    > the evaluation shall not produce an overflow; otherwise, the behavior is undefined.
+
+    after a long list of defined behaviors.
+
+    Goblint does not report overflow and out-of-bounds pointer arithmetic (when the pointer _is not dereferenced_).
+    This affects the overflow analysis (SV-COMP no-overflow property) in the `base` analysis.
+
+    This _does not_ affect the `memOutOfBounds` analysis (SV-COMP valid-memsafety property), which is for undefined behavior from _dereferencing_ such out-of-bounds pointers.
+
+    See [PR #1511](https://github.com/goblint/analyzer/pull/1511).
+
+
+[n1570]: https://www.open-std.org/jtc1/sc22/wg14/www/docs/n1570.pdf
diff --git a/dune-project b/dune-project
index 878abd3b4f..54915cf964 100644
--- a/dune-project
+++ b/dune-project
@@ -15,23 +15,38 @@
 (source (github goblint/analyzer))
 (homepage "https://goblint.in.tum.de")
 (documentation "https://goblint.readthedocs.io/en/latest/")
-(authors "Simmo Saan" "Michael Schwarz" "Julian Erhard" "Sarah Tilscher" "Ralf Vogler" "Kalmer Apinis" "Vesal Vojdani" ) ; same authors as in .zenodo.json and CITATION.cff
+(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")
 (license MIT)
 
 (package
   (name goblint)
   (synopsis "Static analysis framework for C")
+  (description "\
+Goblint is a sound static analysis framework for C programs using abstract interpretation.
+It specializes in thread-modular verification of multi-threaded programs, especially regarding data races.
+Goblint includes analyses for assertions, overflows, deadlocks, etc and can be extended with new analyses.
+")
+  (tags (
+    "program analysis"
+    "program verification"
+    "static analysis"
+    "abstract interpretation"
+    "C"
+    "data race analysis"
+    "concurrency"))
   (depends
     (ocaml (>= 4.14))
-    (goblint-cil (>= 2.0.3)) ; 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.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.
     (batteries (>= 3.5.1))
     (zarith (>= 1.10))
     (yojson (>= 2.0.0))
     (qcheck-core (>= 0.19))
-    ppx_deriving
+    (ppx_deriving (>= 6.0.2))
     (ppx_deriving_hash (>= 0.1.2))
     (ppx_deriving_yojson (>= 3.7.0))
+    (ppx_blob (>= 0.8.0))
+    (ppxlib (>= 0.30.0)) ; ppx_easy_deriving
     (ounit2 :with-test)
     (qcheck-ounit :with-test)
     (odoc :with-doc)
@@ -54,7 +69,7 @@
     conf-gcc ; ensures opam-repository CI installs real gcc from homebrew on MacOS
   )
   (depopts
-    apron
+    (apron (>= v0.9.15))
     z3
   )
   (conflicts
diff --git a/goblint.opam b/goblint.opam
index 692625c965..565d1fab5b 100644
--- a/goblint.opam
+++ b/goblint.opam
@@ -1,6 +1,11 @@
 # This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
 synopsis: "Static analysis framework for C"
+description: """
+Goblint is a sound static analysis framework for C programs using abstract interpretation.
+It specializes in thread-modular verification of multi-threaded programs, especially regarding data races.
+Goblint includes analyses for assertions, overflows, deadlocks, etc and can be extended with new analyses.
+"""
 maintainer: [
   "Simmo Saan <simmo.saan@gmail.com>"
   "Michael Schwarz <michael.schwarz93@gmail.com>"
@@ -11,25 +16,37 @@ authors: [
   "Michael Schwarz"
   "Julian Erhard"
   "Sarah Tilscher"
+  "Karoliine Holter"
   "Ralf Vogler"
   "Kalmer Apinis"
   "Vesal Vojdani"
 ]
 license: "MIT"
+tags: [
+  "program analysis"
+  "program verification"
+  "static analysis"
+  "abstract interpretation"
+  "C"
+  "data race analysis"
+  "concurrency"
+]
 homepage: "https://goblint.in.tum.de"
 doc: "https://goblint.readthedocs.io/en/latest/"
 bug-reports: "https://github.com/goblint/analyzer/issues"
 depends: [
   "dune" {>= "3.7"}
   "ocaml" {>= "4.14"}
-  "goblint-cil" {>= "2.0.3"}
+  "goblint-cil" {>= "2.0.4"}
   "batteries" {>= "3.5.1"}
   "zarith" {>= "1.10"}
   "yojson" {>= "2.0.0"}
   "qcheck-core" {>= "0.19"}
-  "ppx_deriving"
+  "ppx_deriving" {>= "6.0.2"}
   "ppx_deriving_hash" {>= "0.1.2"}
   "ppx_deriving_yojson" {>= "3.7.0"}
+  "ppx_blob" {>= "0.8.0"}
+  "ppxlib" {>= "0.30.0"}
   "ounit2" {with-test}
   "qcheck-ounit" {with-test}
   "odoc" {with-doc}
@@ -51,7 +68,10 @@ depends: [
   "benchmark" {with-test}
   "conf-gcc"
 ]
-depopts: ["apron" "z3"]
+depopts: [
+  "apron" {>= "v0.9.15"}
+  "z3"
+]
 conflicts: [
   "result" {< "1.5"}
   "ez-conf-lib" {= "1"}
@@ -75,12 +95,9 @@ build: [
 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"
+available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
 pin-depends: [
-  # published goblint-cil 2.0.3 is currently up-to-date, so no pin needed
-  [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#ae3a4949d478fad77e004c6fe15a7c83427df59f" ]
-  # 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" ]
+  [ "goblint-cil.2.0.4" "git+https://github.com/goblint/cil.git#04b8a45a7d20425c7b6c8abe1ad094abc063922b" ]
 ]
 depexts: [
   ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test}
@@ -88,3 +105,7 @@ depexts: [
 post-messages: [
   "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}
 ]
+x-ci-accept-failures: [
+  "macos-homebrew" # newer MacOS headers cannot be parsed (https://github.com/ocaml/opam-repository/pull/26307#issuecomment-2258080206)
+  "opensuse-tumbleweed" # not GNU diff, so some cram tests fail (https://discuss.ocaml.org/t/opensuse-and-opam-tests/14641/2)
+]
diff --git a/goblint.opam.locked b/goblint.opam.locked
index f8de683948..28dd8e17e9 100644
--- a/goblint.opam.locked
+++ b/goblint.opam.locked
@@ -12,6 +12,7 @@ authors: [
   "Michael Schwarz"
   "Julian Erhard"
   "Sarah Tilscher"
+  "Karoliine Holter"
   "Ralf Vogler"
   "Kalmer Apinis"
   "Vesal Vojdani"
@@ -21,89 +22,95 @@ homepage: "https://goblint.in.tum.de"
 doc: "https://goblint.readthedocs.io/en/latest/"
 bug-reports: "https://github.com/goblint/analyzer/issues"
 depends: [
-  "angstrom" {= "0.15.0"}
-  "apron" {= "v0.9.14~beta.2"}
+  "angstrom" {= "0.16.0"}
+  "apron" {= "v0.9.15"}
   "arg-complete" {= "0.1.0"}
   "astring" {= "0.8.5"}
   "base-bigarray" {= "base"}
   "base-bytes" {= "base"}
   "base-threads" {= "base"}
   "base-unix" {= "base"}
-  "batteries" {= "3.6.0"}
+  "batteries" {= "3.8.0"}
   "benchmark" {= "1.6" & with-test}
   "bigarray-compat" {= "1.1.0"}
-  "bigstringaf" {= "0.9.0"}
+  "bigstringaf" {= "0.9.1"}
   "bos" {= "0.2.1"}
-  "camlidl" {= "1.11"}
+  "camlidl" {= "1.12"}
   "camlp-streams" {= "5.0.1"}
   "catapult" {= "0.2"}
   "catapult-file" {= "0.2"}
-  "cmdliner" {= "1.1.1" & with-doc}
-  "conf-autoconf" {= "0.1"}
+  "cmdliner" {= "1.3.0" & with-doc}
+  "conf-autoconf" {= "0.2"}
+  "conf-findutils" {= "1"}
   "conf-gcc" {= "1.0"}
   "conf-gmp" {= "4"}
-  "conf-mpfr" {= "3"}
+  "conf-gmp-paths" {= "1"}
+  "conf-mpfr-paths" {= "1"}
   "conf-perl" {= "2"}
-  "conf-pkg-config" {= "2"}
   "conf-ruby" {= "1.0.0" & with-test}
-  "conf-which" {= "1"}
   "cppo" {= "1.6.9"}
   "cpu" {= "2.0.0"}
-  "csexp" {= "1.5.1"}
-  "ctypes" {= "0.20.1"}
-  "dune" {= "3.7.1"}
-  "dune-build-info" {= "3.7.1"}
-  "dune-configurator" {= "3.7.1"}
-  "dune-private-libs" {= "3.7.1"}
-  "dune-site" {= "3.7.1"}
-  "dyn" {= "3.7.1"}
+  "crunch" {= "3.3.1" & with-doc}
+  "csexp" {= "1.5.2"}
+  "cstruct" {= "6.2.0"}
+  "ctypes" {= "0.22.0"}
+  "dune" {= "3.16.0"}
+  "dune-build-info" {= "3.16.0"}
+  "dune-configurator" {= "3.16.0"}
+  "dune-private-libs" {= "3.16.0"}
+  "dune-site" {= "3.16.0"}
+  "dyn" {= "3.16.0"}
+  "ez-conf-lib" {= "2"}
   "fileutils" {= "0.6.4"}
   "fmt" {= "0.9.0"}
   "fpath" {= "0.7.3"}
-  "goblint-cil" {= "2.0.3"}
+  "goblint-cil" {= "2.0.4"}
+  "hex" {= "1.5.0"}
   "integers" {= "0.7.0"}
-  "json-data-encoding" {= "0.12.1"}
-  "jsonrpc" {= "1.15.0~5.0preview1"}
+  "json-data-encoding" {= "1.0.1"}
+  "jsonrpc" {= "1.17.0"}
   "logs" {= "0.7.0"}
-  "mlgmpidl" {= "1.2.15"}
-  "num" {= "1.4"}
-  "ocaml" {= "4.14.0"}
+  "mlgmpidl" {= "1.3.0"}
+  "num" {= "1.5"}
+  "ocaml" {= "4.14.2"}
   "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}
-  "odoc-parser" {= "2.0.0" & with-doc}
-  "ordering" {= "3.7.1"}
-  "ounit2" {= "2.2.6" & with-test}
-  "pp" {= "1.1.2"}
+  "ocaml-variants" {= "4.14.2+options"}
+  "ocamlbuild" {= "0.14.3"}
+  "ocamlfind" {= "1.9.6"}
+  "odoc" {= "2.4.2" & with-doc}
+  "odoc-parser" {= "2.4.2" & with-doc}
+  "ordering" {= "3.16.0"}
+  "ounit2" {= "2.2.7" & with-test}
+  "pp" {= "1.2.0"}
+  "ppx_blob" {= "0.9.0"}
   "ppx_derivers" {= "1.2.1"}
-  "ppx_deriving" {= "5.2.1"}
+  "ppx_deriving" {= "6.0.2"}
   "ppx_deriving_hash" {= "0.1.2"}
-  "ppx_deriving_yojson" {= "3.7.0"}
-  "ppxlib" {= "0.28.0"}
-  "qcheck-core" {= "0.20"}
-  "qcheck-ounit" {= "0.20" & with-test}
-  "re" {= "1.10.4" & with-doc}
-  "result" {= "1.5"}
+  "ppx_deriving_yojson" {= "3.8.0"}
+  "ppxlib" {= "0.32.1"}
+  "ptime" {= "1.1.0" & with-doc}
+  "qcheck-core" {= "0.21.3"}
+  "qcheck-ounit" {= "0.21.3" & with-test}
+  "re" {= "1.11.0" & with-doc}
+  "result" {= "1.5" & with-doc}
   "rresult" {= "0.7.0"}
   "seq" {= "base"}
-  "sexplib0" {= "v0.15.1"}
-  "sha" {= "1.15.2"}
+  "sexplib0" {= "v0.16.0"}
+  "sha" {= "1.15.4"}
   "stdlib-shims" {= "0.3.0"}
-  "stdune" {= "3.7.1"}
+  "stdune" {= "3.16.0"}
   "stringext" {= "1.6.0"}
-  "topkg" {= "1.0.6"}
-  "tyxml" {= "4.5.0" & with-doc}
-  "uri" {= "4.2.0"}
+  "topkg" {= "1.0.7"}
+  "tyxml" {= "4.6.0" & with-doc}
+  "uri" {= "4.4.0"}
   "uuidm" {= "0.9.8"}
   "uutf" {= "1.0.3" & with-doc}
-  "yaml" {= "3.1.0"}
-  "yojson" {= "2.0.2"}
-  "zarith" {= "1.12"}
+  "yaml" {= "3.2.0"}
+  "yojson" {= "2.2.1"}
+  "zarith" {= "1.13"}
 ]
 build: [
   ["dune" "subst"] {dev}
@@ -122,7 +129,7 @@ build: [
   ["dune" "install" "-p" name "--create-install-files" name]
 ]
 dev-repo: "git+https://github.com/goblint/analyzer.git"
-available: os-distribution != "alpine" & arch != "arm64"
+available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
 conflicts: [
   "result" {< "1.5"}
   "ez-conf-lib" {= "1"}
@@ -130,15 +137,23 @@ conflicts: [
 post-messages: [
   "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}
 ]
-# TODO: manually reordered to avoid opam pin crash: https://github.com/ocaml/opam/issues/4936
 pin-depends: [
   [
-    "goblint-cil.2.0.3"
-    "git+https://github.com/goblint/cil.git#ae3a4949d478fad77e004c6fe15a7c83427df59f"
-  ]
-  [
-    "ppx_deriving.5.2.1"
-    "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6"
+    "goblint-cil.2.0.4"
+    "git+https://github.com/goblint/cil.git#04b8a45a7d20425c7b6c8abe1ad094abc063922b"
   ]
 ]
 depexts: ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test}
+description: """\
+Goblint is a sound static analysis framework for C programs using abstract interpretation.
+It specializes in thread-modular verification of multi-threaded programs, especially regarding data races.
+Goblint includes analyses for assertions, overflows, deadlocks, etc and can be extended with new analyses."""
+tags: [
+  "program analysis"
+  "program verification"
+  "static analysis"
+  "abstract interpretation"
+  "C"
+  "data race analysis"
+  "concurrency"
+]
diff --git a/goblint.opam.template b/goblint.opam.template
index 2d5ef10bc9..9f29ceb7a5 100644
--- a/goblint.opam.template
+++ b/goblint.opam.template
@@ -1,11 +1,8 @@
 # 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"
+available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
 pin-depends: [
-  # published goblint-cil 2.0.3 is currently up-to-date, so no pin needed
-  [ "goblint-cil.2.0.3" "git+https://github.com/goblint/cil.git#ae3a4949d478fad77e004c6fe15a7c83427df59f" ]
-  # 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" ]
+  [ "goblint-cil.2.0.4" "git+https://github.com/goblint/cil.git#04b8a45a7d20425c7b6c8abe1ad094abc063922b" ]
 ]
 depexts: [
   ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test}
@@ -13,3 +10,7 @@ depexts: [
 post-messages: [
   "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}
 ]
+x-ci-accept-failures: [
+  "macos-homebrew" # newer MacOS headers cannot be parsed (https://github.com/ocaml/opam-repository/pull/26307#issuecomment-2258080206)
+  "opensuse-tumbleweed" # not GNU diff, so some cram tests fail (https://discuss.ocaml.org/t/opensuse-and-opam-tests/14641/2)
+]
diff --git a/gobview b/gobview
index 72abbb576b..76e42c34d3 160000
--- a/gobview
+++ b/gobview
@@ -1 +1 @@
-Subproject commit 72abbb576b8ffc8759dcfa31501738f6b561b05a
+Subproject commit 76e42c34d36bd2ab6900efd661a972ba4824f065
diff --git a/make.sh b/make.sh
index 5b55e51beb..0f76759065 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 --packages=ocaml-variants.4.14.0+options,ocaml-option-flambda --locked
+  opam switch -y create . --deps-only --packages=ocaml-variants.4.14.2+options,ocaml-option-flambda --locked
 }
 
 rule() {
diff --git a/scripts/creduce/privPrecCompare.sh b/scripts/creduce/privPrecCompare.sh
index fdc5f9219d..2165112924 100755
--- a/scripts/creduce/privPrecCompare.sh
+++ b/scripts/creduce/privPrecCompare.sh
@@ -22,7 +22,7 @@ for PRIV in "${PRIVS[@]}"; do
     PRIVDUMP="$OUTDIR/$PRIV"
     LOG="$OUTDIR/$PRIV.log"
     rm -f $PRIVDUMP
-    $GOBLINTDIR/goblint --sets exp.privatization $PRIV --sets exp.priv-prec-dump $PRIVDUMP $OPTS -v --enable warn.debug &> $LOG
+    $GOBLINTDIR/goblint --set exp.privatization $PRIV --set exp.priv-prec-dump $PRIVDUMP $OPTS -v --enable warn.debug &> $LOG
     grep -F "Function definition missing" $LOG && exit 1
 done
 
diff --git a/scripts/goblint-lib-modules.py b/scripts/goblint-lib-modules.py
index 017530f838..ba25a1403c 100755
--- a/scripts/goblint-lib-modules.py
+++ b/scripts/goblint-lib-modules.py
@@ -42,6 +42,10 @@
     "Goblint_build_info",
     "Dune_build_info",
 
+    # ppx-s
+    "Ppx_deriving_printable",
+    "Ppx_deriving_lattice",
+
     "MessageCategory", # included in Messages
     "PreValueDomain", # included in ValueDomain
 
diff --git a/scripts/privPrecCompare.sh b/scripts/privPrecCompare.sh
index c5b9f2c01e..2b09fb80b5 100755
--- a/scripts/privPrecCompare.sh
+++ b/scripts/privPrecCompare.sh
@@ -10,7 +10,7 @@ mkdir -p $OUTDIR
 for PRIV in "${PRIVS[@]}"; do
     echo $PRIV
     PRIVDUMP="$OUTDIR/$PRIV"
-    ./goblint --sets exp.privatization $PRIV --sets exp.priv-prec-dump $PRIVDUMP "$@"
+    ./goblint --set exp.privatization $PRIV --set exp.priv-prec-dump $PRIVDUMP "$@"
 done
 
 PRIVDUMPS=("${PRIVS[*]/#/$OUTDIR/}") # why [*] here?
diff --git a/scripts/test-gobview.py b/scripts/test-gobview.py
index f5961108d7..10808a9b62 100644
--- a/scripts/test-gobview.py
+++ b/scripts/test-gobview.py
@@ -6,6 +6,7 @@
 from webdriver_manager.chrome import ChromeDriverManager
 from selenium.webdriver.common.by import By
 from selenium.webdriver.chrome.options import Options
+from selenium.webdriver.common.desired_capabilities import DesiredCapabilities
 from threading import Thread
 import subprocess
 
@@ -17,6 +18,11 @@
 # cleanup
 def cleanup(browser, thread):
   print("cleanup")
+
+  # print messages
+  for entry in browser.get_log('browser'):
+    print(entry)
+
   browser.close()
   p.kill()
   thread.join()
@@ -35,6 +41,8 @@ def serve():
 print("starting installation of browser\n")
 options = Options()
 options.add_argument('headless')
+# options.set_capability("loggingPrefs", { 'browser':'ALL' })
+options.set_capability("goog:loggingPrefs", { 'browser':'ALL' })
 browser = webdriver.Chrome(service=Service(ChromeDriverManager().install()),options=options)
 print("finished webdriver installation \n")
 browser.maximize_window()
diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml
index a42d78d71a..cb8e8731d9 100644
--- a/src/analyses/apron/relationAnalysis.apron.ml
+++ b/src/analyses/apron/relationAnalysis.apron.ml
@@ -295,7 +295,7 @@ struct
     (* there should be smarter ways to do this, e.g. by keeping track of which values are written etc. ... *)
     (* See, e.g, Beckschulze E, Kowalewski S, Brauer J (2012) Access-based localization for octagons. Electron Notes Theor Comput Sci 287:29–40 *)
     (* Also, a local *)
-    let vname = Apron.Var.to_string var in
+    let vname = GobApron.Var.show var in
     let locals = fundec.sformals @ fundec.slocals in
     match List.find_opt (fun v -> VM.var_name (Local v) = vname) locals with (* TODO: optimize *)
     | None -> true
@@ -418,7 +418,7 @@ struct
     in
     let any_local_reachable = any_local_reachable fundec reachable_from_args in
     let arg_vars = f.sformals |> List.filter (RD.Tracked.varinfo_tracked) |> List.map RV.arg in
-    if M.tracing then M.tracel "combine-rel" "relation remove vars: %a" (docList (fun v -> Pretty.text (Apron.Var.to_string v))) arg_vars;
+    if M.tracing then M.tracel "combine-rel" "relation remove vars: %a" (docList (GobApron.Var.pretty ())) arg_vars;
     RD.remove_vars_with new_fun_rel arg_vars; (* fine to remove arg vars that also exist in caller because unify from new_rel adds them back with proper constraints *)
     let tainted = f_ask.f Queries.MayBeTainted in
     let tainted_vars = TaintPartialContexts.conv_varset tainted in
@@ -756,7 +756,7 @@ struct
 
   let sync ctx reason =
     (* After the solver is finished, store the results (for later comparison) *)
-    if !AnalysisState.postsolving then begin
+    if !AnalysisState.postsolving && GobConfig.get_string "exp.relation.prec-dump" <> "" then begin
       let keep_local = GobConfig.get_bool "ana.relation.invariant.local" in
       let keep_global = GobConfig.get_bool "ana.relation.invariant.global" in
 
diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml
index 3ecfb713d7..ff771e692e 100644
--- a/src/analyses/apron/relationPriv.apron.ml
+++ b/src/analyses/apron/relationPriv.apron.ml
@@ -33,8 +33,8 @@ module type S =
        the state when following conditional guards. *)
     val write_global: ?invariant:bool -> Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> relation_components_t -> varinfo -> varinfo -> relation_components_t
 
-    val lock: Q.ask -> (V.t -> G.t) -> relation_components_t -> LockDomain.Addr.t -> relation_components_t
-    val unlock: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> relation_components_t -> LockDomain.Addr.t -> relation_components_t
+    val lock: Q.ask -> (V.t -> G.t) -> relation_components_t -> LockDomain.MustLock.t -> relation_components_t
+    val unlock: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> relation_components_t -> LockDomain.MustLock.t -> relation_components_t
 
     val sync: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> relation_components_t -> [`Normal | `Join | `JoinCall | `Return | `Init | `Thread] -> relation_components_t
 
@@ -483,7 +483,7 @@ struct
 
   let startstate () = ()
 
-  let atomic_mutex = LockDomain.Addr.of_var LibraryFunctions.verifier_atomic_var
+  let atomic_mutex = LockDomain.MustLock.of_var LibraryFunctions.verifier_atomic_var
 
   let get_m_with_mutex_inits ask getg m =
     let get_m = getg (V.mutex m) in
@@ -503,7 +503,7 @@ struct
     in
     let get_mutex_inits = getg V.mutex_inits in
     let get_mutex_inits' = RD.keep_vars get_mutex_inits [g_var] in
-    if not (RD.mem_var get_mutex_inits' g_var) then (* TODO: is this just a workaround for an escape bug? https://github.com/goblint/analyzer/pull/1354/files#r1498882657 *)
+    if RD.mem_var get_mutex_global_g g_var && not (RD.mem_var get_mutex_inits' g_var) then (* TODO: is this just a workaround for an escape bug? https://github.com/goblint/analyzer/pull/1354/files#r1498882657 *)
       (* This is an escaped variable whose value was never side-effected to get_mutex_inits' *)
       get_mutex_global_g
     else
@@ -589,9 +589,9 @@ struct
   let write_escape = write_global_internal ~skip_meet:true
 
   let lock ask getg (st: relation_components_t) m =
-    let atomic = Param.handle_atomic && LockDomain.Addr.equal m (atomic_mutex) in
+    let atomic = Param.handle_atomic && LockDomain.MustLock.equal m atomic_mutex in
     (* TODO: somehow actually unneeded here? *)
-    if not atomic && Locksets.(not (Lockset.mem m (current_lockset ask))) then (
+    if not atomic && Locksets.(not (MustLockset.mem m (current_lockset ask))) then (
       let rel = st.rel in
       let get_m = get_m_with_mutex_inits ask getg m in
       (* Additionally filter get_m in case it contains variables it no longer protects. E.g. in 36/22. *)
@@ -604,7 +604,7 @@ struct
       st (* sound w.r.t. recursive lock *)
 
   let unlock ask getg sideg (st: relation_components_t) m: relation_components_t =
-    let atomic = Param.handle_atomic && LockDomain.Addr.equal m (atomic_mutex) in
+    let atomic = Param.handle_atomic && LockDomain.MustLock.equal m atomic_mutex in
     let rel = st.rel in
     if not atomic then (
       let rel_side = keep_only_protected_globals ask m rel in
@@ -721,7 +721,7 @@ module type ClusterArg = functor (RD: RelationDomain.RD) ->
 sig
   module LRD: Lattice.S
 
-  val keep_only_protected_globals: Q.ask -> LockDomain.Addr.t -> LRD.t -> LRD.t
+  val keep_only_protected_globals: Q.ask -> LockDomain.MustLock.t -> LRD.t -> LRD.t
   val keep_global: varinfo -> LRD.t -> LRD.t
 
   val lock: RD.t -> LRD.t -> LRD.t -> RD.t
@@ -980,7 +980,7 @@ struct
 
   let get_m_with_mutex_inits inits ask getg m =
     let get_m = get_relevant_writes ask m (G.mutex @@ getg (V.mutex m)) in
-    if M.tracing then M.traceli "relationpriv" "get_m_with_mutex_inits %a\n  get=%a" LockDomain.Addr.pretty m LRD.pretty get_m;
+    if M.tracing then M.traceli "relationpriv" "get_m_with_mutex_inits %a\n  get=%a" LockDomain.MustLock.pretty m LRD.pretty get_m;
     let r =
       if not inits then
         get_m
@@ -993,7 +993,7 @@ struct
     if M.tracing then M.traceu "relationpriv" "-> %a" LRD.pretty r;
     r
 
-  let atomic_mutex = LockDomain.Addr.of_var LibraryFunctions.verifier_atomic_var
+  let atomic_mutex = LockDomain.MustLock.of_var LibraryFunctions.verifier_atomic_var
 
   let get_mutex_global_g_with_mutex_inits inits ask getg g =
     let get_mutex_global_g =
@@ -1106,8 +1106,8 @@ struct
       {rel = rel_local; priv = (W.add g w,lmust,l)} (* Keep write local as if it were protected by the atomic section. *)
 
   let lock ask getg (st: relation_components_t) m =
-    let atomic = Param.handle_atomic && LockDomain.Addr.equal m (atomic_mutex) in
-    if not atomic && Locksets.(not (Lockset.mem m (current_lockset ask))) then (
+    let atomic = Param.handle_atomic && LockDomain.MustLock.equal m atomic_mutex in
+    if not atomic && Locksets.(not (MustLockset.mem m (current_lockset ask))) then (
       let rel = st.rel in
       let _,lmust,l = st.priv in
       let lm = LLock.mutex m in
@@ -1130,7 +1130,7 @@ struct
     RD.keep_filter oct protected
 
   let unlock ask getg sideg (st: relation_components_t) m: relation_components_t =
-    let atomic = Param.handle_atomic && LockDomain.Addr.equal m (atomic_mutex) in
+    let atomic = Param.handle_atomic && LockDomain.MustLock.equal m atomic_mutex in
     let rel = st.rel in
     let w,lmust,l = st.priv in
     if not atomic then (
@@ -1314,7 +1314,7 @@ struct
     r
 
   let lock ask getg st m =
-    if M.tracing then M.traceli "relationpriv" "lock %a" LockDomain.Addr.pretty m;
+    if M.tracing then M.traceli "relationpriv" "lock %a" LockDomain.MustLock.pretty m;
     if M.tracing then M.trace "relationpriv" "st: %a" RelComponents.pretty st;
     let getg x =
       let r = getg x in
@@ -1326,7 +1326,7 @@ struct
     r
 
   let unlock ask getg sideg st m =
-    if M.tracing then M.traceli "relationpriv" "unlock %a" LockDomain.Addr.pretty m;
+    if M.tracing then M.traceli "relationpriv" "unlock %a" LockDomain.MustLock.pretty m;
     if M.tracing then M.trace "relationpriv" "st: %a" RelComponents.pretty st;
     let getg x =
       let r = getg x in
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 102e22b5a7..a69b3a2b23 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -261,6 +261,8 @@ struct
       (* adds n to the last offset *)
       let rec addToOffset n (t:typ option) = function
         | `Index (i, `NoOffset) ->
+          (* Binary operations on pointer types should not generate warnings in SV-COMP *)
+          GobRef.wrap AnalysisState.executing_speculative_computations true @@ fun () ->
           (* If we have arrived at the last Offset and it is an Index, we add our integer to it *)
           `Index(IdxDom.add i (iDtoIdx n), `NoOffset)
         | `Field (f, `NoOffset) ->
@@ -2043,7 +2045,7 @@ struct
       List.map mpt exps
     )
 
-  let invalidate ?(deep=true) ~ctx (st:store) (exps: exp list): store =
+  let invalidate ~(must: bool) ?(deep=true) ~ctx (st:store) (exps: exp list): store =
     if M.tracing && exps <> [] then M.tracel "invalidate" "Will invalidate expressions [%a]" (d_list ", " d_plainexp) exps;
     if exps <> [] then M.info ~category:Imprecise "Invalidating expressions: %a" (d_list ", " d_exp) exps;
     (* To invalidate a single address, we create a pair with its corresponding
@@ -2070,7 +2072,15 @@ struct
       let vs = List.map (Tuple3.third) invalids' in
       M.tracel "invalidate" "Setting addresses [%a] to values [%a]" (d_list ", " AD.pretty) addrs (d_list ", " VD.pretty) vs
     );
-    set_many ~ctx st invalids'
+    (* copied from set_many *)
+    let f (acc: store) ((lval:AD.t),(typ:Cil.typ),(value:value)): store =
+      let acc' = set ~ctx acc lval typ value in
+      if must then
+        acc'
+      else
+        D.join acc acc'
+    in
+    List.fold_left f st invalids'
 
 
   let make_entry ?(thread=false) (ctx:(D.t, G.t, C.t, V.t) Analyses.ctx) fundec args: D.t =
@@ -2166,7 +2176,7 @@ struct
       end
     | _, _ when get_bool "sem.unknown_function.spawn" ->
       (* TODO: Remove sem.unknown_function.spawn check because it is (and should be) really done in LibraryFunctions.
-         But here we consider all non-ThreadCrate functions also unknown, so old-style LibraryFunctions access
+         But here we consider all non-ThreadCreate functions also unknown, so old-style LibraryFunctions access
          definitions using `Write would still spawn because they are not truly unknown functions (missing from LibraryFunctions).
          Need this to not have memmove spawn in SV-COMP. *)
       let shallow_args = LibraryDesc.Accesses.find desc.accs { kind = Spawn; deep = false } args in
@@ -2209,8 +2219,8 @@ struct
     in
     (* TODO: what about escaped local variables? *)
     (* invalidate arguments and non-static globals for unknown functions *)
-    let st' = invalidate ~deep:false ~ctx ctx.local shallow_addrs in
-    invalidate ~deep:true ~ctx st' deep_addrs
+    let st' = invalidate ~must:false ~deep:false ~ctx ctx.local shallow_addrs in
+    invalidate ~must:false ~deep:true ~ctx st' deep_addrs
 
   let check_invalid_mem_dealloc ctx special_fn ptr =
     let has_non_heap_var = AD.exists (function
@@ -2300,7 +2310,7 @@ struct
     let invalidate_ret_lv st = match lv with
       | Some lv ->
         if M.tracing then M.tracel "invalidate" "Invalidating lhs %a for function call %s" d_plainlval lv f.vname;
-        invalidate ~deep:false ~ctx st [Cil.mkAddrOrStartOf lv]
+        invalidate ~must:true ~deep:false ~ctx st [Cil.mkAddrOrStartOf lv]
       | None -> st
     in
     let addr_type_of_exp exp =
@@ -2634,14 +2644,14 @@ struct
         | Int n when GobOption.exists (Z.equal Z.zero) (ID.to_int n) -> st
         | Address ret_a ->
           begin match eval_rv ~ctx st id with
-            | Thread a when ValueDomain.Threads.is_top a -> invalidate ~ctx st [ret_var]
+            | Thread a when ValueDomain.Threads.is_top a -> invalidate ~must:true ~ctx st [ret_var]
             | Thread a ->
               let v = List.fold VD.join (VD.bot ()) (List.map (fun x -> G.thread (ctx.global (V.thread x))) (ValueDomain.Threads.elements a)) in
               (* TODO: is this type right? *)
               set ~ctx st ret_a (Cilfacade.typeOf ret_var) v
-            | _      -> invalidate ~ctx st [ret_var]
+            | _      -> invalidate ~must:true ~ctx st [ret_var]
           end
-        | _      -> invalidate ~ctx st [ret_var]
+        | _      -> invalidate ~must:true ~ctx st [ret_var]
       in
       let st' = invalidate_ret_lv st' in
       Priv.thread_join (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) id st'
diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml
index efa0575bf4..08413d54b1 100644
--- a/src/analyses/basePriv.ml
+++ b/src/analyses/basePriv.ml
@@ -28,8 +28,8 @@ sig
    * the state when following conditional guards. *)
   val write_global: ?invariant:bool -> Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseComponents (D).t -> varinfo -> VD.t -> BaseComponents (D).t
 
-  val lock: Q.ask -> (V.t -> G.t) -> BaseComponents (D).t -> LockDomain.Addr.t -> BaseComponents (D).t
-  val unlock: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseComponents (D).t -> LockDomain.Addr.t -> BaseComponents (D).t
+  val lock: Q.ask -> (V.t -> G.t) -> BaseComponents (D).t -> LockDomain.MustLock.t -> BaseComponents (D).t
+  val unlock: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseComponents (D).t -> LockDomain.MustLock.t -> BaseComponents (D).t
 
   val sync: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseComponents (D).t -> [`Normal | `Join | `JoinCall | `Return | `Init | `Thread] -> BaseComponents (D).t
 
@@ -191,7 +191,7 @@ struct
     let get_mutex_inits = getg V.mutex_inits in
     let is_in_Gm x _ = is_protected_by ask m x in
     let get_mutex_inits' = CPA.filter is_in_Gm get_mutex_inits in
-    if M.tracing then M.tracel "priv" "get_m_with_mutex_inits %a:\n  get_m: %a\n  get_mutex_inits: %a\n  get_mutex_inits': %a" LockDomain.Addr.pretty m CPA.pretty get_m CPA.pretty get_mutex_inits CPA.pretty get_mutex_inits';
+    if M.tracing then M.tracel "priv" "get_m_with_mutex_inits %a:\n  get_m: %a\n  get_mutex_inits: %a\n  get_mutex_inits': %a" LockDomain.MustLock.pretty m CPA.pretty get_m CPA.pretty get_mutex_inits CPA.pretty get_mutex_inits';
     CPA.join get_m get_mutex_inits'
 
   (** [get_m_with_mutex_inits] optimized for implementation-specialized [read_global]. *)
@@ -281,7 +281,7 @@ struct
      cpa' *)
 
   let lock ask getg (st: BaseComponents (D).t) m =
-    if Locksets.(not (Lockset.mem m (current_lockset ask))) then (
+    if Locksets.(not (MustLockset.mem m (current_lockset ask))) then (
       let get_m = get_m_with_mutex_inits ask getg m in
       (* Really we want is_unprotected, but pthread_cond_wait emits unlock-lock events,
          where our (necessary) original context still has the mutex,
@@ -292,7 +292,7 @@ struct
          No other privatization uses is_unprotected, so this hack is only needed here. *)
       let is_in_V x _ = is_protected_by ask m x && is_unprotected_without ask x m in
       let cpa' = CPA.filter is_in_V get_m in
-      if M.tracing then M.tracel "priv" "PerMutexOplusPriv.lock m=%a cpa'=%a" LockDomain.Addr.pretty m CPA.pretty cpa';
+      if M.tracing then M.tracel "priv" "PerMutexOplusPriv.lock m=%a cpa'=%a" LockDomain.MustLock.pretty m CPA.pretty cpa';
       {st with cpa = CPA.fold CPA.add cpa' st.cpa}
     )
     else
@@ -301,7 +301,7 @@ struct
   let unlock ask getg sideg (st: BaseComponents (D).t) m =
     let is_in_Gm x _ = is_protected_by ask m x in
     let side_m_cpa = CPA.filter is_in_Gm st.cpa in
-    if M.tracing then M.tracel "priv" "PerMutexOplusPriv.unlock m=%a side_m_cpa=%a" LockDomain.Addr.pretty m CPA.pretty side_m_cpa;
+    if M.tracing then M.tracel "priv" "PerMutexOplusPriv.unlock m=%a side_m_cpa=%a" LockDomain.MustLock.pretty m CPA.pretty side_m_cpa;
     sideg (V.mutex m) side_m_cpa;
     st
 
@@ -384,14 +384,14 @@ struct
      cpa' *)
 
   let lock (ask: Queries.ask) getg (st: BaseComponents (D).t) m =
-    if Locksets.(not (Lockset.mem m (current_lockset ask))) then (
+    if Locksets.(not (MustLockset.mem m (current_lockset ask))) then (
       let get_m = get_m_with_mutex_inits ask getg m in
       (* Additionally filter get_m in case it contains variables it no longer protects. *)
       let is_in_Gm x _ = is_protected_by ask m x in
       let get_m = CPA.filter is_in_Gm get_m in
       let long_meet m1 m2 = CPA.long_map2 VD.meet m1 m2 in
       let meet = long_meet st.cpa get_m in
-      if M.tracing then M.tracel "priv" "LOCK %a:\n  get_m: %a\n  meet: %a" LockDomain.Addr.pretty m CPA.pretty get_m CPA.pretty meet;
+      if M.tracing then M.tracel "priv" "LOCK %a:\n  get_m: %a\n  meet: %a" LockDomain.MustLock.pretty m CPA.pretty get_m CPA.pretty meet;
       {st with cpa = meet}
     )
     else
@@ -537,7 +537,7 @@ struct
     {st with cpa = cpa'; priv = (W.add x w,LMust.add lm lmust,l')}
 
   let lock (ask: Queries.ask) getg (st: BaseComponents (D).t) m =
-    if Locksets.(not (Lockset.mem m (current_lockset ask))) then (
+    if Locksets.(not (MustLockset.mem m (current_lockset ask))) then (
       let _,lmust,l = st.priv in
       let lm = LLock.mutex m in
       let get_m = get_m_with_mutex_inits (not (LMust.mem lm lmust)) ask getg m in
@@ -764,7 +764,7 @@ struct
 
   let unlock ask getg sideg (st: BaseComponents (D).t) m =
     let sideg = Wrapper.sideg ask sideg in
-    let atomic = Param.handle_atomic && LockDomain.Addr.equal m (LockDomain.Addr.of_var LibraryFunctions.verifier_atomic_var) in
+    let atomic = Param.handle_atomic && LockDomain.MustLock.equal m (LockDomain.MustLock.of_var LibraryFunctions.verifier_atomic_var) in
     (* TODO: what about G_m globals in cpa that weren't actually written? *)
     CPA.fold (fun x v (st: BaseComponents (D).t) ->
         if is_protected_by ask m x then ( (* is_in_Gm *)
@@ -868,12 +868,12 @@ struct
 
   module GWeak =
   struct
-    include MapDomain.MapBot (Lockset) (WeakRange)
+    include MapDomain.MapBot (MustLockset) (WeakRange)
     let name () = "weak"
   end
   module GSync =
   struct
-    include MapDomain.MapBot (Lockset) (SyncRange)
+    include MapDomain.MapBot (MustLockset) (SyncRange)
     let name () = "synchronized"
   end
   module G =
@@ -929,7 +929,7 @@ struct
   let invariant_vars ask getg st =
     let module VS = Set.Make (CilType.Varinfo) in
     let s = current_lockset ask in
-    Lockset.fold (fun m acc ->
+    MustLockset.fold (fun m acc ->
         GSync.fold (fun s' cpa' acc ->
             SyncRange.fold_sync_vars VS.add cpa' acc
           ) (G.sync (getg (V.mutex m))) acc
@@ -1008,7 +1008,7 @@ struct
   let read_global ask getg (st: BaseComponents (D).t) x =
     let s = current_lockset ask in
     GWeak.fold (fun s' tm acc ->
-        if Lockset.disjoint s s' then
+        if MustLockset.disjoint s s' then
           ThreadMap.fold (fun t' v acc ->
               VD.join v acc
             ) tm acc
@@ -1028,7 +1028,7 @@ struct
   let lock ask getg (st: BaseComponents (D).t) m =
     let s = current_lockset ask in
     let cpa' = GSync.fold (fun s' cpa' acc ->
-        if Lockset.disjoint s s' then
+        if MustLockset.disjoint s s' then
           CPA.join cpa' acc
         else
           acc
@@ -1037,13 +1037,13 @@ struct
     {st with cpa = cpa'}
 
   let unlock ask getg sideg (st: BaseComponents (D).t) m =
-    let s = Lockset.remove m (current_lockset ask) in
+    let s = MustLockset.remove m (current_lockset ask) in
     let t = current_thread ask in
     let side_cpa = CPA.filter (fun x _ ->
         GWeak.fold (fun s' tm acc ->
             (* TODO: swap 2^M and T partitioning for lookup by t here first? *)
             let v = ThreadMap.find t tm in
-            (Lockset.mem m s' && not (VD.is_bot v)) || acc
+            (MustLockset.mem m s' && not (VD.is_bot v)) || acc
           ) (G.weak (getg (V.global x))) false
       ) st.cpa
     in
@@ -1070,7 +1070,7 @@ struct
   let read_global ask getg (st: BaseComponents (D).t) x =
     let s = current_lockset ask in
     GWeak.fold (fun s' v acc ->
-        if Lockset.disjoint s s' then
+        if MustLockset.disjoint s s' then
           VD.join v acc
         else
           acc
@@ -1087,7 +1087,7 @@ struct
   let lock ask getg (st: BaseComponents (D).t) m =
     let s = current_lockset ask in
     let cpa' = GSync.fold (fun s' cpa' acc ->
-        if Lockset.disjoint s s' then
+        if MustLockset.disjoint s s' then
           CPA.join cpa' acc
         else
           acc
@@ -1096,10 +1096,10 @@ struct
     {st with cpa = cpa'}
 
   let unlock ask getg sideg (st: BaseComponents (D).t) m =
-    let s = Lockset.remove m (current_lockset ask) in
+    let s = MustLockset.remove m (current_lockset ask) in
     let side_cpa = CPA.filter (fun x _ ->
         GWeak.fold (fun s' v acc ->
-            (Lockset.mem m s' && not (VD.is_bot v)) || acc
+            (MustLockset.mem m s' && not (VD.is_bot v)) || acc
           ) (G.weak (getg (V.global x))) false
       ) st.cpa
     in
@@ -1142,7 +1142,7 @@ struct
   let read_global ask getg (st: BaseComponents (D).t) x =
     let s = current_lockset ask in
     GWeak.fold (fun s' v acc ->
-        if Lockset.disjoint s s' then
+        if MustLockset.disjoint s s' then
           VD.join v acc
         else
           acc
@@ -1163,7 +1163,7 @@ struct
   let lock ask getg (st: BaseComponents (D).t) m =
     let s = current_lockset ask in
     let cpa' = GSync.fold (fun s' cpa' acc ->
-        if Lockset.disjoint s s' then
+        if MustLockset.disjoint s s' then
           CPA.join cpa' acc
         else
           acc
@@ -1172,7 +1172,7 @@ struct
     {st with cpa = cpa'}
 
   let unlock ask getg sideg (st: BaseComponents (D).t) m =
-    let s = Lockset.remove m (current_lockset ask) in
+    let s = MustLockset.remove m (current_lockset ask) in
     let is_in_W x _ = W.mem x st.priv in
     let side_cpa = CPA.filter is_in_W st.cpa in
     sideg (V.mutex m) (G.create_sync (GSync.singleton s side_cpa));
@@ -1193,7 +1193,7 @@ struct
     if Param.side_effect_global_init then (
       CPA.fold (fun x v (st: BaseComponents (D).t) ->
           if is_global ask x then (
-            sideg (V.global x) (G.create_weak (GWeak.singleton (Lockset.empty ()) v));
+            sideg (V.global x) (G.create_weak (GWeak.singleton (MustLockset.empty ()) v));
             {st with priv = W.add x st.priv} (* TODO: is this add necessary? *)
           )
           else
@@ -1216,13 +1216,13 @@ struct
 
   module DV =
   struct
-    include MapDomain.MapBot_LiftTop (Lock) (MustVars)
+    include MapDomain.MapBot_LiftTop (LockDomain.MustLock) (MustVars)
     let name () = "V"
   end
 
   module L =
   struct
-    include MapDomain.MapBot_LiftTop (Lock) (MinLocksets)
+    include MapDomain.MapBot_LiftTop (LockDomain.MustLock) (MinLocksets)
     let name () = "L"
   end
 end
@@ -1246,7 +1246,7 @@ struct
 
   let startstate () = (DV.bot (), L.bot ())
 
-  let lockset_init = Lockset.top ()
+  let lockset_init = MustLockset.all ()
 
   let distr_init getg x v =
     if get_bool "exp.priv-distr-init" then
@@ -1265,7 +1265,7 @@ struct
           let syncs = UnwrappedG.sync (getg (V.mutex m)) in
           MinLocksets.fold (fun b acc ->
               GSync.fold (fun s' cpa' acc ->
-                  if Lockset.disjoint b s' then
+                  if MustLockset.disjoint b s' then
                     let v = CPA.find x cpa' in
                     VD.join v acc
                   else
@@ -1278,7 +1278,7 @@ struct
     in
     let weaks = UnwrappedG.weak (getg (V.global x)) in
     let d_weak = GWeak.fold (fun s' v acc ->
-        if Lockset.disjoint s s' then
+        if MustLockset.disjoint s s' then
           VD.join v acc
         else
           acc
@@ -1325,7 +1325,7 @@ struct
   let unlock ask getg sideg (st: BaseComponents (D).t) m =
     let sideg = Wrapper.sideg ask sideg in
     let getg = Wrapper.getg ask getg in
-    let s = Lockset.remove m (current_lockset ask) in
+    let s = MustLockset.remove m (current_lockset ask) in
     let is_in_G x _ = is_global ask x in
     let side_cpa = CPA.filter is_in_G st.cpa in
     let side_cpa = CPA.mapi (fun x v ->
@@ -1380,13 +1380,13 @@ struct
 
   module GWeakW =
   struct
-    include MapDomain.MapBot (Lockset) (VD)
+    include MapDomain.MapBot (MustLockset) (VD)
 
     let fold_weak f m a = fold (fun _ v a -> f v a) m a
   end
   module GSyncW =
   struct
-    include MapDomain.MapBot (Lockset) (LockCenteredBase.CPA)
+    include MapDomain.MapBot (MustLockset) (LockCenteredBase.CPA)
 
     let fold_sync_vars f m a =
       fold (fun _ cpa a ->
@@ -1418,11 +1418,11 @@ struct
 
   let startstate () = (W.bot (), P.top ())
 
-  let lockset_init = Lockset.top ()
+  let lockset_init = MustLockset.all ()
 
   let distr_init getg x v =
     if get_bool "exp.priv-distr-init" then
-      let v_init = GWeakW.find lockset_init (GWeak.find (Lockset.empty ()) (UnwrappedG.weak (getg (V.global x)))) in
+      let v_init = GWeakW.find lockset_init (GWeak.find (MustLockset.empty ()) (UnwrappedG.weak (getg (V.global x)))) in
       VD.join v v_init
     else
       v
@@ -1433,13 +1433,13 @@ struct
     let (w, p) = st.priv in
     let p_x = P.find x p in
     let d_cpa = CPA.find x st.cpa in
-    let d_sync = Lockset.fold (fun m acc ->
-        if MinLocksets.exists (fun s''' -> not (Lockset.mem m s''')) p_x then
+    let d_sync = MustLockset.fold (fun m acc ->
+        if MinLocksets.exists (fun s''' -> not (MustLockset.mem m s''')) p_x then
           let syncs = UnwrappedG.sync (getg (V.mutex m)) in
           GSync.fold (fun s' gsyncw' acc ->
-              if Lockset.disjoint s s' then
+              if MustLockset.disjoint s s' then
                 GSyncW.fold (fun w' cpa' acc ->
-                    if MinLocksets.exists (fun s'' -> Lockset.disjoint s'' w') p_x then
+                    if MinLocksets.exists (fun s'' -> MustLockset.disjoint s'' w') p_x then
                       let v = CPA.find x cpa' in
                       VD.join v acc
                     else
@@ -1454,9 +1454,9 @@ struct
     in
     let weaks = UnwrappedG.weak (getg (V.global x)) in
     let d_weak = GWeak.fold (fun s' gweakw' acc ->
-        if Lockset.disjoint s s' then
+        if MustLockset.disjoint s s' then
           GWeakW.fold (fun w' v acc ->
-              if MinLocksets.exists (fun s'' -> Lockset.disjoint s'' w') p_x then
+              if MinLocksets.exists (fun s'' -> MustLockset.disjoint s'' w') p_x then
                 VD.join v acc
               else
                 acc
@@ -1496,10 +1496,10 @@ struct
   let unlock ask getg sideg (st: BaseComponents (D).t) m =
     let getg = Wrapper.getg ask getg in
     let sideg = Wrapper.sideg ask sideg in
-    let s = Lockset.remove m (current_lockset ask) in
+    let s = MustLockset.remove m (current_lockset ask) in
     let (w, p) = st.priv in
     let p' = P.map (fun s' -> MinLocksets.add s s') p in
-    if M.tracing then M.traceli "priv" "unlock %a %a" Lock.pretty m CPA.pretty st.cpa;
+    if M.tracing then M.traceli "priv" "unlock %a %a" LockDomain.MustLock.pretty m CPA.pretty st.cpa;
     let side_gsyncw = CPA.fold (fun x v acc ->
         if is_global ask x then (
           let w_x = W.find x w in
@@ -1512,7 +1512,7 @@ struct
           acc
       ) st.cpa (GSyncW.bot ())
     in
-    if M.tracing then M.traceu "priv" "unlock %a %a" Lock.pretty m GSyncW.pretty side_gsyncw;
+    if M.tracing then M.traceu "priv" "unlock %a %a" LockDomain.MustLock.pretty m GSyncW.pretty side_gsyncw;
     sideg (V.mutex m) (UnwrappedG.create_sync (GSync.singleton s side_gsyncw));
     {st with priv = (w, p')}
 
@@ -1533,7 +1533,7 @@ struct
         if EscapeDomain.EscapedVars.mem x escaped then (
           let (w, p) = st.priv in
           let p' = P.add x (MinLocksets.singleton s) p in
-          sideg (V.global x) (UnwrappedG.create_weak (GWeak.singleton (Lockset.empty ()) (GWeakW.singleton lockset_init v)));
+          sideg (V.global x) (UnwrappedG.create_weak (GWeak.singleton (MustLockset.empty ()) (GWeakW.singleton lockset_init v)));
           {st with cpa = CPA.remove x st.cpa; priv = (w, p')}
         )
         else
@@ -1544,7 +1544,7 @@ struct
     let sideg = Wrapper.sideg ask sideg in
     CPA.fold (fun x v (st: BaseComponents (D).t) ->
         if is_global ask x then (
-          sideg (V.global x) (UnwrappedG.create_weak (GWeak.singleton (Lockset.empty ()) (GWeakW.singleton lockset_init v)));
+          sideg (V.global x) (UnwrappedG.create_weak (GWeak.singleton (MustLockset.empty ()) (GWeakW.singleton lockset_init v)));
           {st with cpa = CPA.remove x st.cpa}
         )
         else
@@ -1574,11 +1574,11 @@ struct
 
   let startstate () = ((W.bot (), P.top ()), (DV.bot (), L.bot ()))
 
-  let lockset_init = Lockset.top ()
+  let lockset_init = MustLockset.all ()
 
   let distr_init getg x v =
     if get_bool "exp.priv-distr-init" then
-      let v_init = GWeakW.find lockset_init (GWeak.find (Lockset.empty ()) (UnwrappedG.weak (getg (V.global x)))) in
+      let v_init = GWeakW.find lockset_init (GWeak.find (MustLockset.empty ()) (UnwrappedG.weak (getg (V.global x)))) in
       VD.join v v_init
     else
       v
@@ -1594,9 +1594,9 @@ struct
           let syncs = UnwrappedG.sync (getg (V.mutex m)) in
           MinLocksets.fold (fun b acc ->
               GSync.fold (fun s' gsyncw' acc ->
-                  if Lockset.disjoint b s' then
+                  if MustLockset.disjoint b s' then
                     GSyncW.fold (fun w' cpa' acc ->
-                        if MinLocksets.exists (fun s'' -> Lockset.disjoint s'' w') p_x then
+                        if MinLocksets.exists (fun s'' -> MustLockset.disjoint s'' w') p_x then
                           let v = CPA.find x cpa' in
                           VD.join v acc
                         else
@@ -1612,9 +1612,9 @@ struct
     in
     let weaks = UnwrappedG.weak (getg (V.global x)) in
     let d_m_weak = GWeak.fold (fun s' gweakw' acc ->
-        if Lockset.disjoint s s' then
+        if MustLockset.disjoint s s' then
           GWeakW.fold (fun w' v acc ->
-              if MinLocksets.exists (fun s'' -> Lockset.disjoint s'' w') p_x then
+              if MinLocksets.exists (fun s'' -> MustLockset.disjoint s'' w') p_x then
                 VD.join v acc
               else
                 acc
@@ -1624,13 +1624,13 @@ struct
       ) weaks (VD.bot ())
     in
     let d_m = VD.join d_m_sync d_m_weak in
-    let d_g_sync = Lockset.fold (fun m acc ->
-        if MinLocksets.exists (fun s''' -> not (Lockset.mem m s''')) p_x then
+    let d_g_sync = MustLockset.fold (fun m acc ->
+        if MinLocksets.exists (fun s''' -> not (MustLockset.mem m s''')) p_x then
           let syncs = UnwrappedG.sync (getg (V.mutex m)) in
           GSync.fold (fun s' gsyncw' acc ->
-              if Lockset.disjoint s s' then
+              if MustLockset.disjoint s s' then
                 GSyncW.fold (fun w' cpa' acc ->
-                    if MinLocksets.exists (fun s'' -> Lockset.disjoint s'' w') p_x then
+                    if MinLocksets.exists (fun s'' -> MustLockset.disjoint s'' w') p_x then
                       let v = CPA.find x cpa' in
                       VD.join v acc
                     else
@@ -1682,7 +1682,7 @@ struct
   let unlock ask getg sideg (st: BaseComponents (D).t) m =
     let getg = Wrapper.getg ask getg in
     let sideg = Wrapper.sideg ask sideg in
-    let s = Lockset.remove m (current_lockset ask) in
+    let s = MustLockset.remove m (current_lockset ask) in
     let ((w, p), vl) = st.priv in
     let p' = P.map (fun s' -> MinLocksets.add s s') p in
     let side_gsyncw = CPA.fold (fun x v acc ->
@@ -1716,7 +1716,7 @@ struct
         if EscapeDomain.EscapedVars.mem x escaped then (
           let ((w, p), (vv, l)) = st.priv in
           let p' = P.add x (MinLocksets.singleton s) p in
-          sideg (V.global x) (UnwrappedG.create_weak (GWeak.singleton (Lockset.empty ()) (GWeakW.singleton lockset_init v)));
+          sideg (V.global x) (UnwrappedG.create_weak (GWeak.singleton (MustLockset.empty ()) (GWeakW.singleton lockset_init v)));
           {st with cpa = CPA.remove x st.cpa; priv = ((w, p'), (vv, l))}
         )
         else
@@ -1727,7 +1727,7 @@ struct
     let sideg = Wrapper.sideg ask sideg in
     CPA.fold (fun x v (st: BaseComponents (D).t) ->
         if is_global ask x then (
-          sideg (V.global x) (UnwrappedG.create_weak (GWeak.singleton (Lockset.empty ()) (GWeakW.singleton lockset_init v)));
+          sideg (V.global x) (UnwrappedG.create_weak (GWeak.singleton (MustLockset.empty ()) (GWeakW.singleton lockset_init v)));
           {st with cpa = CPA.remove x st.cpa}
         )
         else
@@ -1836,7 +1836,7 @@ struct
     r
 
   let lock ask getg st m =
-    if M.tracing then M.traceli "priv" "lock %a" LockDomain.Addr.pretty m;
+    if M.tracing then M.traceli "priv" "lock %a" LockDomain.MustLock.pretty m;
     if M.tracing then M.trace "priv" "st: %a" BaseComponents.pretty st;
     let getg x =
       let r = getg x in
@@ -1848,7 +1848,7 @@ struct
     r
 
   let unlock ask getg sideg st m =
-    if M.tracing then M.traceli "priv" "unlock %a" LockDomain.Addr.pretty m;
+    if M.tracing then M.traceli "priv" "unlock %a" LockDomain.MustLock.pretty m;
     if M.tracing then M.trace "priv" "st: %a" BaseComponents.pretty st;
     let getg x =
       let r = getg x in
diff --git a/src/analyses/basePriv.mli b/src/analyses/basePriv.mli
index 87b17e5ad0..40e50c2a69 100644
--- a/src/analyses/basePriv.mli
+++ b/src/analyses/basePriv.mli
@@ -17,8 +17,8 @@ sig
   val read_global: Queries.ask -> (V.t -> G.t) -> BaseDomain.BaseComponents (D).t -> varinfo -> BaseDomain.VD.t
   val write_global: ?invariant:bool -> Queries.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseDomain.BaseComponents (D).t -> varinfo -> BaseDomain.VD.t -> BaseDomain.BaseComponents (D).t
 
-  val lock: Queries.ask -> (V.t -> G.t) -> BaseDomain.BaseComponents (D).t -> LockDomain.Addr.t -> BaseDomain.BaseComponents (D).t
-  val unlock: Queries.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseDomain.BaseComponents (D).t -> LockDomain.Addr.t -> BaseDomain.BaseComponents (D).t
+  val lock: Queries.ask -> (V.t -> G.t) -> BaseDomain.BaseComponents (D).t -> LockDomain.MustLock.t -> BaseDomain.BaseComponents (D).t
+  val unlock: Queries.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseDomain.BaseComponents (D).t -> LockDomain.MustLock.t -> BaseDomain.BaseComponents (D).t
 
   val sync: Queries.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> BaseDomain.BaseComponents (D).t -> [`Normal | `Join | `JoinCall | `Return | `Init | `Thread] -> BaseDomain.BaseComponents (D).t
 
diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml
index 1ece8dcc60..003cdfa96c 100644
--- a/src/analyses/commonPriv.ml
+++ b/src/analyses/commonPriv.ml
@@ -110,7 +110,7 @@ module MutexGlobals =
 struct
   module VMutex =
   struct
-    include LockDomain.Addr
+    include LockDomain.MustLock
     let name () = "mutex"
   end
   module VMutexInits = Printable.UnitConf (struct let name = "MUTEX_INITS" end)
@@ -148,23 +148,14 @@ end
 
 module Locksets =
 struct
-  module Lock =
-  struct
-    include LockDomain.Addr
-    let name () = "lock"
-  end
-
-  module Lockset = SetDomain.ToppedSet (Lock) (struct let topname = "All locks" end)
-
-  module MustLockset = SetDomain.Reverse (Lockset)
+  module MustLockset = LockDomain.MustLockset
 
-  let current_lockset (ask: Q.ask): Lockset.t =
+  let current_lockset (ask: Q.ask): MustLockset.t =
     (* TODO: remove this global_init workaround *)
     if !AnalysisState.global_initialization then
-      Lockset.empty ()
+      MustLockset.empty ()
     else
-      let mls = ask.f Queries.MustLockset in
-      LockDomain.MustLockset.fold (fun ml acc -> Lockset.add (Addr (LockDomain.MustLock.to_mval ml)) acc) mls (Lockset.empty ()) (* TODO: use MustLockset as Lockset *)
+      ask.f Queries.MustLockset
 
   (* TODO: reversed SetDomain.Hoare *)
   module MinLocksets = HoareDomain.Set_LiftTop (MustLockset) (struct let topname = "All locksets" end) (* reverse Lockset because Hoare keeps maximal, but we need minimal *)
@@ -189,7 +180,7 @@ struct
     let name () = "P"
 
     (* TODO: change MinLocksets.exists/top instead? *)
-    let find x p = find_opt x p |? MinLocksets.singleton (Lockset.empty ()) (* ensure exists has something to check for thread returns *)
+    let find x p = find_opt x p |? MinLocksets.singleton (MustLockset.empty ()) (* ensure exists has something to check for thread returns *)
   end
 end
 
@@ -270,7 +261,7 @@ struct
 
   module LLock =
   struct
-    include Printable.Either (Locksets.Lock) (struct include CilType.Varinfo let name () = "global" end)
+    include Printable.Either (LockDomain.MustLock) (struct include CilType.Varinfo let name () = "global" end)
     let mutex m = `Left m
     let global x = `Right x
   end
@@ -333,7 +324,7 @@ let lift_lock (ask: Q.ask) f st (addr: LockDomain.Addr.t) =
   match addr with
   | UnknownPtr -> st
   | Addr (v, _) when ask.f (IsMultiple v) -> st
-  | Addr mv when LockDomain.Mval.is_definite mv -> f st addr
+  | Addr mv when LockDomain.Mval.is_definite mv -> f st (LockDomain.MustLock.of_mval mv)
   | Addr _
   | NullPtr
   | StrPtr _ -> st
@@ -348,16 +339,16 @@ let lift_unlock (ask: Q.ask) f st (addr: LockDomain.Addr.t) =
   | UnknownPtr ->
     LockDomain.MustLockset.fold (fun ml st ->
         (* call privatization's unlock only with definite lock *)
-        f st (LockDomain.Addr.Addr (LockDomain.MustLock.to_mval ml)) (* TODO: no conversion *)
+        f st ml
       ) (ask.f MustLockset) st
   | StrPtr _
   | NullPtr -> st
-  | Addr mv when LockDomain.Mval.is_definite mv -> f st addr
+  | Addr mv when LockDomain.Mval.is_definite mv -> f st (LockDomain.MustLock.of_mval mv)
   | Addr mv ->
     LockDomain.MustLockset.fold (fun ml st ->
         if LockDomain.MustLock.semantic_equal_mval ml mv = Some false then
           st
         else
           (* call privatization's unlock only with definite lock *)
-          f st (Addr (LockDomain.MustLock.to_mval ml)) (* TODO: no conversion *)
+          f st ml
       ) (ask.f MustLockset) st
diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml
index b44795b6da..9b6aa4f4ca 100644
--- a/src/analyses/mutexAnalysis.ml
+++ b/src/analyses/mutexAnalysis.ml
@@ -209,15 +209,14 @@ struct
       MustLockset.disjoint held_locks protecting
     | Queries.MayBePublicWithout _ when MustLocksetRW.is_all ls -> false
     | Queries.MayBePublicWithout {global=v; write; without_mutex; protection} ->
-      let held_locks = MustLocksetRW.to_must_lockset @@ fst @@ Arg.remove' ctx ~warn:false without_mutex in
+      let held_locks = MustLockset.remove without_mutex (MustLocksetRW.to_must_lockset ls) in
       let protecting = protecting ~write protection v in
       (* TODO: unsound in 29/24, why did we do this before? *)
       (* if Mutexes.mem verifier_atomic (Lockset.export_locks (Lockset.remove (without_mutex, true) ctx.local)) then
         false
       else *)
       MustLockset.disjoint held_locks protecting
-    | Queries.MustBeProtectedBy {mutex = Addr mutex_mv; global=v; write; protection} when Mval.is_definite mutex_mv -> (* only definite Addrs can be in must-locksets to begin with, anything else cannot protect anything *)
-      let ml = LockDomain.MustLock.of_mval mutex_mv in
+    | Queries.MustBeProtectedBy {mutex = ml; global=v; write; protection} ->
       let protecting = protecting ~write protection v in
       (* TODO: unsound in 29/24, why did we do this before? *)
       (* if LockDomain.Addr.equal mutex (LockDomain.Addr.of_var LF.verifier_atomic_var) then
diff --git a/src/analyses/mutexEventsAnalysis.ml b/src/analyses/mutexEventsAnalysis.ml
index c5339e68cf..5ea0afc809 100644
--- a/src/analyses/mutexEventsAnalysis.ml
+++ b/src/analyses/mutexEventsAnalysis.ml
@@ -5,7 +5,6 @@
 module M = Messages
 module Addr = ValueDomain.Addr
 module LF = LibraryFunctions
-open Batteries
 open GoblintCil
 open Analyses
 open GobConfig
@@ -52,12 +51,12 @@ struct
 
   let return ctx exp fundec : D.t =
     (* deprecated but still valid SV-COMP convention for atomic block *)
-    if get_bool "ana.sv-comp.functions" && String.starts_with fundec.svar.vname "__VERIFIER_atomic_" then
+    if get_bool "ana.sv-comp.functions" && String.starts_with fundec.svar.vname ~prefix:"__VERIFIER_atomic_" then
       ctx.emit (Events.Unlock (LockDomain.Addr.of_var LF.verifier_atomic_var))
 
   let body ctx f : D.t =
     (* deprecated but still valid SV-COMP convention for atomic block *)
-    if get_bool "ana.sv-comp.functions" && String.starts_with f.svar.vname "__VERIFIER_atomic_" then
+    if get_bool "ana.sv-comp.functions" && String.starts_with f.svar.vname ~prefix:"__VERIFIER_atomic_" then
       ctx.emit (Events.Lock (LockDomain.Addr.of_var LF.verifier_atomic_var, true))
 
   let special (ctx: (unit, _, _, _) ctx) lv f arglist : D.t =
diff --git a/src/analyses/mutexTypeAnalysis.ml b/src/analyses/mutexTypeAnalysis.ml
index 441f2e9953..4a993bbd7d 100644
--- a/src/analyses/mutexTypeAnalysis.ml
+++ b/src/analyses/mutexTypeAnalysis.ml
@@ -12,16 +12,17 @@ struct
 
   let name () = "pthreadMutexType"
 
-  (* Removing indexes here avoids complicated lookups and allows to have the LVals as vars here, at the price that different types of mutexes in arrays are not dinstinguished *)
-  module O = Offset.Unit
-
-  module V = struct
-    include Printable.Prod(CilType.Varinfo)(O) (* TODO: use Mval.Unit *)
+  module V =
+  struct
+    (* Removing indexes here avoids complicated lookups and allows to have the LVals as vars here, at the price that different types of mutexes in arrays are not dinstinguished *)
+    include Mval.Unit
     let is_write_only _ = false
   end
 
   module G = MAttr
 
+  module O = Offset.Unit
+
   (* transfer functions *)
   let assign ctx (lval:lval) (rval:exp) : D.t =
     match lval with
diff --git a/src/analyses/unassumeAnalysis.ml b/src/analyses/unassumeAnalysis.ml
index 265e9c6925..8f8892b8be 100644
--- a/src/analyses/unassumeAnalysis.ml
+++ b/src/analyses/unassumeAnalysis.ml
@@ -71,21 +71,11 @@ struct
         | _ -> ()
       );
 
-    let loc_of_location (location: YamlWitnessType.Location.t): Cil.location = {
-      file = location.file_name;
-      line = location.line;
-      column = location.column;
-      byte = -1;
-      endLine = -1;
-      endColumn = -1;
-      endByte = -1;
-      synthetic = false;
-    }
-    in
-
     let yaml = match Yaml_unix.of_file (Fpath.v (GobConfig.get_string "witness.yaml.unassume")) with
       | Ok yaml -> yaml
-      | Error (`Msg m) -> failwith ("Yaml_unix.of_file: " ^ m)
+      | Error (`Msg m) ->
+        Logs.error "Yaml_unix.of_file: %s" m;
+        Svcomp.errorwith "witness missing"
     in
     let yaml_entries = yaml |> GobYaml.list |> BatResult.get_ok in
 
@@ -123,7 +113,7 @@ struct
       in
 
       let unassume_location_invariant (location_invariant: YamlWitnessType.LocationInvariant.t) =
-        let loc = loc_of_location location_invariant.location in
+        let loc = YamlWitness.loc_of_location location_invariant.location in
         let inv = location_invariant.location_invariant.string in
         let msgLoc: M.Location.t = CilLocation loc in
 
@@ -135,7 +125,7 @@ struct
       in
 
       let unassume_loop_invariant (loop_invariant: YamlWitnessType.LoopInvariant.t) =
-        let loc = loc_of_location loop_invariant.location in
+        let loc = YamlWitness.loc_of_location loop_invariant.location in
         let inv = loop_invariant.loop_invariant.string in
         let msgLoc: M.Location.t = CilLocation loc in
 
@@ -185,7 +175,7 @@ struct
       in
 
       let unassume_precondition_loop_invariant (precondition_loop_invariant: YamlWitnessType.PreconditionLoopInvariant.t) =
-        let loc = loc_of_location precondition_loop_invariant.location in
+        let loc = YamlWitness.loc_of_location precondition_loop_invariant.location in
         let pre = precondition_loop_invariant.precondition.string in
         let inv = precondition_loop_invariant.loop_invariant.string in
         let msgLoc: M.Location.t = CilLocation loc in
@@ -200,7 +190,7 @@ struct
       let unassume_invariant_set (invariant_set: YamlWitnessType.InvariantSet.t) =
 
         let unassume_location_invariant (location_invariant: YamlWitnessType.InvariantSet.LocationInvariant.t) =
-          let loc = loc_of_location location_invariant.location in
+          let loc = YamlWitness.loc_of_location location_invariant.location in
           let inv = location_invariant.value in
           let msgLoc: M.Location.t = CilLocation loc in
 
@@ -212,7 +202,7 @@ struct
         in
 
         let unassume_loop_invariant (loop_invariant: YamlWitnessType.InvariantSet.LoopInvariant.t) =
-          let loc = loc_of_location loop_invariant.location in
+          let loc = YamlWitness.loc_of_location loop_invariant.location in
           let inv = loop_invariant.value in
           let msgLoc: M.Location.t = CilLocation loc in
 
diff --git a/src/autoTune.ml b/src/autoTune.ml
index 434b4fb0b2..0def6021fa 100644
--- a/src/autoTune.ml
+++ b/src/autoTune.ml
@@ -68,6 +68,7 @@ let functionArgs fd = (ResettableLazy.force functionCallMaps).argLists |> Functi
 
 let findMallocWrappers () =
   let isMalloc f =
+    Goblint_backtrace.wrap_val ~mark:(Cilfacade.FunVarinfo f) @@ fun () ->
     if LibraryFunctions.is_special f then (
       let desc = LibraryFunctions.find f in
       match functionArgs f with
@@ -104,7 +105,7 @@ let rec setCongruenceRecursive fd depth neigbourFunction =
          | exception Not_found -> () (* Happens for __goblint_bounded *)
       )
       (FunctionSet.filter (*for extern and builtin functions there is no function definition in CIL*)
-         (fun x -> not (isExtern x.vstorage || BatString.starts_with x.vname "__builtin"))
+         (fun x -> not (isExtern x.vstorage || String.starts_with x.vname ~prefix:"__builtin"))
          (neigbourFunction fd.svar)
       )
     ;
@@ -153,6 +154,7 @@ let disableIntervalContextsInRecursiveFunctions () =
 
 let hasFunction pred =
   let relevant_static var =
+    Goblint_backtrace.wrap_val ~mark:(Cilfacade.FunVarinfo var) @@ fun () ->
     if LibraryFunctions.is_special var then
       let desc = LibraryFunctions.find var in
       GobOption.exists (fun args -> pred (desc.special args)) (functionArgs var)
@@ -160,6 +162,7 @@ let hasFunction pred =
       false
   in
   let relevant_dynamic var =
+    Goblint_backtrace.wrap_val ~mark:(Cilfacade.FunVarinfo var) @@ fun () ->
     if LibraryFunctions.is_special var then
       let desc = LibraryFunctions.find var in
       (* We don't really have arguments at hand, so we cheat and just feed it a list of MyCFG.unknown_exp of appropriate length *)
@@ -186,7 +189,7 @@ let enableAnalyses anas =
 (*escape is also still enabled, because otherwise we get a warning*)
 (*does not consider dynamic calls!*)
 
-let notNeccessaryThreadAnalyses = ["race"; "deadlock"; "maylocks"; "symb_locks"; "thread"; "threadid"; "threadJoins"; "threadreturn"; "mhp"; "region"]
+let notNeccessaryThreadAnalyses = ["race"; "deadlock"; "maylocks"; "symb_locks"; "thread"; "threadid"; "threadJoins"; "threadreturn"; "mhp"; "region"; "pthreadMutexType"]
 let reduceThreadAnalyses () =
   let isThreadCreate = function
     | LibraryDesc.ThreadCreate _ -> true
diff --git a/src/build-info/dune b/src/build-info/dune
index 5a64b399a4..1dd74c192c 100644
--- a/src/build-info/dune
+++ b/src/build-info/dune
@@ -8,14 +8,13 @@
 (library
   (name goblint_build_info)
   (public_name goblint.build-info)
-  (libraries batteries.unthreaded)
   (virtual_modules dune_build_info))
 
 (rule
   (target configVersion.ml)
   (mode (promote (until-clean) (only configVersion.ml))) ; replace existing file in source tree, even if releasing (only overrides)
   (deps (universe)) ; do not cache, always regenerate
-  (action (pipe-stdout (bash "git describe --all --long --dirty || echo \"n/a\"") (with-stdout-to %{target} (bash "xargs printf '(* Automatically regenerated, changes do not persist! *)\nlet version = \"%s\"'")))))
+  (action (pipe-stdout (bash "git describe --all --long --dirty || echo \"n/a\"") (with-stdout-to %{target} (bash "xargs printf '(* Automatically regenerated, changes do not persist! *)\nlet version = Sys.opaque_identity \"%s\"'")))))
 
 (rule
   (target configProfile.ml)
@@ -31,7 +30,7 @@
   (target configDatetime.ml)
   (mode (promote (until-clean) (only configDatetime.ml))) ; replace existing file in source tree, even if releasing (only overrides)
   (deps (universe)) ; do not cache, always regenerate
-  (action (pipe-stdout (bash "date +\"%Y-%m-%dT%H:%M:%S\" || echo \"n/a\"") (with-stdout-to %{target} (bash "xargs printf '(* Automatically regenerated, changes do not persist! *)\nlet datetime = \"%s\"'")))))
+  (action (pipe-stdout (bash "date +\"%Y-%m-%dT%H:%M:%S\" || echo \"n/a\"") (with-stdout-to %{target} (bash "xargs printf '(* Automatically regenerated, changes do not persist! *)\nlet datetime = Sys.opaque_identity \"%s\"'")))))
 
 (env
   (_
diff --git a/src/build-info/goblint_build_info.ml b/src/build-info/goblint_build_info.ml
index 14e30a1b36..d2600c94ad 100644
--- a/src/build-info/goblint_build_info.ml
+++ b/src/build-info/goblint_build_info.ml
@@ -18,7 +18,7 @@ let release_commit = "%%VCS_COMMIT_ID%%"
 (** Goblint version. *)
 let version =
   let commit = ConfigVersion.version in
-  if BatString.starts_with release_version "%" then
+  if String.starts_with release_version ~prefix:"%" then
     commit
   else (
     let commit =
diff --git a/src/cdomain/value/cdomains/floatDomain.ml b/src/cdomain/value/cdomains/floatDomain.ml
index 0977c68890..7c77b954b4 100644
--- a/src/cdomain/value/cdomains/floatDomain.ml
+++ b/src/cdomain/value/cdomains/floatDomain.ml
@@ -1134,7 +1134,7 @@ module FloatDomTupleImpl = struct
   module F1 = FloatIntervalImplLifted
   open Batteries
 
-  type t = F1.t option [@@deriving to_yojson, eq, ord]
+  type t = F1.t option [@@deriving eq, ord, hash]
 
   let name () = "floatdomtuple"
 
@@ -1181,10 +1181,6 @@ module FloatDomTupleImpl = struct
     Option.map_default identity ""
       (mapp { fp= (fun (type a) (module F : FloatDomain with type t = a) x -> F.name () ^ ":" ^ F.show x); } x)
 
-  let hash x =
-    Option.map_default identity 0
-      (mapp { fp= (fun (type a) (module F : FloatDomain with type t = a) -> F.hash); } x)
-
   let of_const fkind =
     create { fi= (fun (type a) (module F : FloatDomain with type t = a) -> F.of_const fkind); }
 
diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index c525732d3b..a0e9a38f37 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -582,6 +582,59 @@ module IntervalArith (Ints_t : IntOps.IntOps) = struct
     List.exists (Z.equal l) ts
 end
 
+module IntInvariant =
+struct
+  let of_int e ik x =
+    if get_bool "witness.invariant.exact" then
+      Invariant.of_exp Cil.(BinOp (Eq, e, kintegerCilint ik x, intType))
+    else
+      Invariant.none
+
+  let of_incl_list e ik ps =
+    match ps with
+    | [_; _] when ik = IBool && not (get_bool "witness.invariant.inexact-type-bounds") ->
+      assert (List.mem Z.zero ps);
+      assert (List.mem Z.one ps);
+      Invariant.none
+    | [_] when get_bool "witness.invariant.exact" ->
+      Invariant.none
+    | _ :: _ :: _
+    | [_] | [] ->
+      List.fold_left (fun a x ->
+          let i = Invariant.of_exp Cil.(BinOp (Eq, e, kintegerCilint ik x, intType)) in
+          Invariant.(a || i) [@coverage off] (* bisect_ppx cannot handle redefined (||) *)
+        ) (Invariant.bot ()) ps
+
+  let of_interval_opt e ik = function
+    | (Some x1, Some x2) when Z.equal x1 x2 ->
+      of_int e ik x1
+    | x1_opt, x2_opt ->
+      let (min_ik, max_ik) = Size.range ik in
+      let inexact_type_bounds = get_bool "witness.invariant.inexact-type-bounds" in
+      let i1 =
+        match x1_opt, inexact_type_bounds with
+        | Some x1, false when Z.equal min_ik x1 -> Invariant.none
+        | Some x1, _ -> Invariant.of_exp Cil.(BinOp (Le, kintegerCilint ik x1, e, intType))
+        | None, _ -> Invariant.none
+      in
+      let i2 =
+        match x2_opt, inexact_type_bounds with
+        | Some x2, false when Z.equal x2 max_ik -> Invariant.none
+        | Some x2, _ -> Invariant.of_exp Cil.(BinOp (Le, e, kintegerCilint ik x2, intType))
+        | None, _ -> Invariant.none
+      in
+      Invariant.(i1 && i2)
+
+  let of_interval e ik (x1, x2) =
+    of_interval_opt e ik (Some x1, Some x2)
+
+  let of_excl_list e ik ns =
+    List.fold_left (fun a x ->
+        let i = Invariant.of_exp Cil.(BinOp (Ne, e, kintegerCilint ik x, intType)) in
+        Invariant.(a && i)
+      ) (Invariant.top ()) ns
+end
+
 module IntervalFunctor (Ints_t : IntOps.IntOps): SOverflow with type int_t = Ints_t.t and type t = (Ints_t.t * Ints_t.t) option =
 struct
   let name () = "intervals"
@@ -915,21 +968,10 @@ struct
       else if Ints_t.compare y2 x1 <= 0 then of_bool ik false
       else top_bool
 
-  let invariant_ikind e ik x =
-    match x with
-    | Some (x1, x2) when Ints_t.compare x1 x2 = 0 ->
-      if get_bool "witness.invariant.exact" then
-        let x1 = Ints_t.to_bigint x1 in
-        Invariant.of_exp Cil.(BinOp (Eq, e, kintegerCilint ik x1, intType))
-      else
-        Invariant.top ()
+  let invariant_ikind e ik = function
     | Some (x1, x2) ->
-      let (min_ik, max_ik) = range ik in
-      let (x1', x2') = BatTuple.Tuple2.mapn (Ints_t.to_bigint) (x1, x2) in
-      let inexact_type_bounds = get_bool "witness.invariant.inexact-type-bounds" in
-      let i1 = if inexact_type_bounds || Ints_t.compare min_ik x1 <> 0 then Invariant.of_exp Cil.(BinOp (Le, kintegerCilint ik x1', e, intType)) else Invariant.none in
-      let i2 = if inexact_type_bounds || Ints_t.compare x2 max_ik <> 0 then Invariant.of_exp Cil.(BinOp (Le, e, kintegerCilint ik x2', intType)) else Invariant.none in
-      Invariant.(i1 && i2)
+      let (x1', x2') = BatTuple.Tuple2.mapn Ints_t.to_bigint (x1, x2) in
+      IntInvariant.of_interval e ik (x1', x2')
     | None -> Invariant.none
 
   let arbitrary ik =
@@ -2297,25 +2339,14 @@ struct
   let invariant_ikind e ik (x:t) =
     match x with
     | `Definite x ->
-      if get_bool "witness.invariant.exact" then
-        Invariant.of_exp Cil.(BinOp (Eq, e, kintegerCilint ik x, intType))
-      else
-        Invariant.top ()
+      IntInvariant.of_int e ik x
     | `Excluded (s, r) ->
       (* Emit range invariant if tighter than ikind bounds.
          This can be more precise than interval, which has been widened. *)
       let (rmin, rmax) = (Exclusion.min_of_range r, Exclusion.max_of_range r) in
-      let (ikmin, ikmax) =
-        let ikr = size ik in
-        (Exclusion.min_of_range ikr, Exclusion.max_of_range ikr)
-      in
-      let inexact_type_bounds = get_bool "witness.invariant.inexact-type-bounds" in
-      let imin = if inexact_type_bounds || Z.compare ikmin rmin <> 0 then Invariant.of_exp Cil.(BinOp (Le, kintegerCilint ik rmin, e, intType)) else Invariant.none in
-      let imax = if inexact_type_bounds || Z.compare rmax ikmax <> 0 then Invariant.of_exp Cil.(BinOp (Le, e, kintegerCilint ik rmax, intType)) else Invariant.none in
-      S.fold (fun x a ->
-          let i = Invariant.of_exp Cil.(BinOp (Ne, e, kintegerCilint ik x, intType)) in
-          Invariant.(a && i)
-        ) s Invariant.(imin && imax)
+      let ri = IntInvariant.of_interval e ik (rmin, rmax) in
+      let si = IntInvariant.of_excl_list e ik (S.elements s) in
+      Invariant.(ri && si)
     | `Bot -> Invariant.none
 
   let arbitrary ik =
@@ -2731,32 +2762,16 @@ module Enums : S with type int_t = Z.t = struct
   let ne ik x y = c_lognot ik (eq ik x y)
 
   let invariant_ikind e ik x =
-    let inexact_type_bounds = get_bool "witness.invariant.inexact-type-bounds" in
     match x with
-    | Inc ps when not inexact_type_bounds && ik = IBool && is_top_of ik x ->
-      Invariant.none
     | Inc ps ->
-      if BISet.cardinal ps > 1 || get_bool "witness.invariant.exact" then
-        BISet.fold (fun x a ->
-            let i = Invariant.of_exp Cil.(BinOp (Eq, e, kintegerCilint ik x, intType)) in
-            Invariant.(a || i) [@coverage off] (* bisect_ppx cannot handle redefined (||) *)
-          ) ps (Invariant.bot ())
-      else
-        Invariant.top ()
+      IntInvariant.of_incl_list e ik (BISet.elements ps)
     | Exc (ns, r) ->
       (* Emit range invariant if tighter than ikind bounds.
          This can be more precise than interval, which has been widened. *)
       let (rmin, rmax) = (Exclusion.min_of_range r, Exclusion.max_of_range r) in
-      let (ikmin, ikmax) =
-        let ikr = size ik in
-        (Exclusion.min_of_range ikr, Exclusion.max_of_range ikr)
-      in
-      let imin = if inexact_type_bounds || Z.compare ikmin rmin <> 0 then Invariant.of_exp Cil.(BinOp (Le, kintegerCilint ik rmin, e, intType)) else Invariant.none in
-      let imax = if inexact_type_bounds || Z.compare rmax ikmax <> 0 then Invariant.of_exp Cil.(BinOp (Le, e, kintegerCilint ik rmax, intType)) else Invariant.none in
-      BISet.fold (fun x a ->
-          let i = Invariant.of_exp Cil.(BinOp (Ne, e, kintegerCilint ik x, intType)) in
-          Invariant.(a && i)
-        ) ns Invariant.(imin && imax)
+      let ri = IntInvariant.of_interval e ik (rmin, rmax) in
+      let nsi = IntInvariant.of_excl_list e ik (BISet.elements ns) in
+      Invariant.(ri && nsi)
 
 
   let arbitrary ik =
@@ -2779,7 +2794,7 @@ module Enums : S with type int_t = Z.t = struct
     | Inc e, Some (c, m) -> Inc (BISet.filter (contains c m) e)
     | _ -> a
 
-  let refine_with_interval ik a b = a
+  let refine_with_interval ik a b = a (* TODO: refine inclusion (exclusion?) set *)
 
   let refine_with_excl_list ik a b =
     match b with
@@ -3243,10 +3258,7 @@ struct
     match x with
     | x when is_top x -> Invariant.top ()
     | Some (c, m) when m =: Z.zero ->
-      if get_bool "witness.invariant.exact" then
-        Invariant.of_exp Cil.(BinOp (Eq, e, Cil.kintegerCilint ik c, intType))
-      else
-        Invariant.top ()
+      IntInvariant.of_int e ik c
     | Some (c, m) ->
       let open Cil in
       let (c, m) = BatTuple.Tuple2.mapn (fun a -> kintegerCilint ik a) (c, m) in
@@ -3338,7 +3350,7 @@ module IntDomTupleImpl = struct
   module I5 = IntervalSetFunctor (IntOps.BigIntOps)
 
   type t = I1.t option * I2.t option * I3.t option * I4.t option * I5.t option
-  [@@deriving to_yojson, eq, ord]
+  [@@deriving eq, ord, hash]
 
   let name () = "intdomtuple"
 
@@ -3524,7 +3536,7 @@ module IntDomTupleImpl = struct
     let merge ps =
       let (vs, rs) = List.split ps in
       let (mins, maxs) = List.split rs in
-      (List.concat vs, (List.min mins, List.max maxs))
+      (List.concat vs |> List.sort_uniq Z.compare, (List.min mins, List.max maxs))
     in
     mapp2 { fp2 = fun (type a) (module I:SOverflow with type t = a and type int_t = int_t) -> I.to_excl_list } x |> flat merge
 
@@ -3565,7 +3577,7 @@ module IntDomTupleImpl = struct
     in
     [(fun (a, b, c, d, e) -> refine_with_excl_list ik (a, b, c, d, e) (to_excl_list (a, b, c, d, e)));
      (fun (a, b, c, d, e) -> refine_with_incl_list ik (a, b, c, d, e) (to_incl_list (a, b, c, d, e)));
-     (fun (a, b, c, d, e) -> maybe refine_with_interval ik (a, b, c, d, e) b);
+     (fun (a, b, c, d, e) -> maybe refine_with_interval ik (a, b, c, d, e) b); (* TODO: get interval across all domains with minimal and maximal *)
      (fun (a, b, c, d, e) -> maybe refine_with_congruence ik (a, b, c, d, e) d)]
 
   let refine ik ((a, b, c, d, e) : t ) : t =
@@ -3665,7 +3677,6 @@ module IntDomTupleImpl = struct
            |> to_list
            |> String.concat "; "
   let to_yojson = [%to_yojson: Yojson.Safe.t list] % to_list % mapp { fp = fun (type a) (module I:SOverflow with type t = a) x -> I.to_yojson x }
-  let hash = List.fold_left (lxor) 0 % to_list % mapp { fp = fun (type a) (module I:SOverflow with type t = a) -> I.hash }
 
   (* `map/opt_map` are used by `project` *)
   let opt_map b f =
@@ -3778,19 +3789,47 @@ module IntDomTupleImpl = struct
     | Some v when not (GobConfig.get_bool "dbg.full-output") -> BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" (Z.to_string v)
     | _ -> BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" (show x)
 
-  let invariant_ikind e ik x =
-    match to_int x with
-    | Some v ->
-      if get_bool "witness.invariant.exact" then
-        (* If definite, output single equality instead of every subdomain repeating same equality *)
-        Invariant.of_exp Cil.(BinOp (Eq, e, kintegerCilint ik v, intType))
-      else
-        Invariant.top ()
-    | None ->
-      let is = to_list (mapp { fp = fun (type a) (module I:SOverflow with type t = a) -> I.invariant_ikind e ik } x)
-      in List.fold_left (fun a i ->
+  let invariant_ikind e ik ((_, _, _, x_cong, x_intset) as x) =
+    (* TODO: do refinement before to ensure incl_list being more precise than intervals, etc (https://github.com/goblint/analyzer/pull/1517#discussion_r1693998515), requires refine functions to actually refine that *)
+    let simplify_int fallback =
+      match to_int x with
+      | Some v ->
+        (* If definite, output single equality instead of every subdomain repeating same equality (or something less precise). *)
+        IntInvariant.of_int e ik v
+      | None ->
+        fallback ()
+    in
+    let simplify_all () =
+      match to_incl_list x with
+      | Some ps ->
+        (* If inclusion set, output disjunction of equalities because it subsumes interval(s), exclusion set and congruence. *)
+        IntInvariant.of_incl_list e ik ps
+      | None ->
+        (* Get interval bounds from all domains (intervals and exclusion set ranges). *)
+        let min = minimal x in
+        let max = maximal x in
+        let ns = Option.map fst (to_excl_list x) |? [] in (* Ignore exclusion set bit range, known via interval bounds already. *)
+        (* "Refine" out-of-bounds exclusions for simpler output. *)
+        let ns = Option.map_default (fun min -> List.filter (Z.leq min) ns) ns min in
+        let ns = Option.map_default (fun max -> List.filter (Z.geq max) ns) ns max in
+        Invariant.(
+          IntInvariant.of_interval_opt e ik (min, max) && (* Output best interval bounds once instead of multiple subdomains repeating them (or less precise ones). *)
+          IntInvariant.of_excl_list e ik ns &&
+          Option.map_default (I4.invariant_ikind e ik) Invariant.none x_cong && (* Output congruence as is. *)
+          Option.map_default (I5.invariant_ikind e ik) Invariant.none x_intset (* Output interval sets as is. *)
+        )
+    in
+    let simplify_none () =
+      let is = to_list (mapp { fp = fun (type a) (module I:SOverflow with type t = a) -> I.invariant_ikind e ik } x) in
+      List.fold_left (fun a i ->
           Invariant.(a && i)
         ) (Invariant.top ()) is
+    in
+    match GobConfig.get_string "ana.base.invariant.int.simplify" with
+    | "none" -> simplify_none ()
+    | "int" -> simplify_int simplify_none
+    | "all" -> simplify_int simplify_all
+    | _ -> assert false
 
   let arbitrary ik = QCheck.(set_print show @@ tup5 (option (I1.arbitrary ik)) (option (I2.arbitrary ik)) (option (I3.arbitrary ik)) (option (I4.arbitrary ik)) (option (I5.arbitrary ik)))
 
diff --git a/src/cdomain/value/cdomains/mutexAttrDomain.ml b/src/cdomain/value/cdomains/mutexAttrDomain.ml
index ea9696d26f..e12818c2c1 100644
--- a/src/cdomain/value/cdomains/mutexAttrDomain.ml
+++ b/src/cdomain/value/cdomains/mutexAttrDomain.ml
@@ -25,7 +25,7 @@ let recursive_int = lazy (
   let res = ref (Z.of_int 2) in (* Use OS X as the default, it doesn't have the enum *)
   GoblintCil.iterGlobals !Cilfacade.current_file (function
       | GEnumTag (einfo, _) ->
-        List.iter (fun (name, exp, _) ->
+        List.iter (fun (name, _, exp, _) ->
             if name = "PTHREAD_MUTEX_RECURSIVE" then
               res := Option.get @@ GoblintCil.getInteger exp
           ) einfo.eitems
diff --git a/src/cdomain/value/cdomains/offset.ml b/src/cdomain/value/cdomains/offset.ml
index 9c9c5c3333..e8cba0afc5 100644
--- a/src/cdomain/value/cdomains/offset.ml
+++ b/src/cdomain/value/cdomains/offset.ml
@@ -213,7 +213,7 @@ struct
         let bits_offset, _size = GoblintCil.bitsOffset (TComp (field.fcomp, [])) field_as_offset  in
         let bits_offset = idx_of_int bits_offset in
         let remaining_offset = offset_to_index_offset ~typ:field.ftype o in
-        Idx.add bits_offset remaining_offset
+        GobRef.wrap AnalysisState.executing_speculative_computations true @@ fun () -> Idx.add bits_offset remaining_offset
       | `Index (x, o) ->
         let (item_typ, item_size_in_bits) =
           match Option.map unrollType typ with
@@ -223,9 +223,10 @@ struct
           | _ ->
             (None, Idx.top ())
         in
-        let bits_offset = Idx.mul item_size_in_bits x in
+        (* Binary operations on offsets should not generate overflow warnings in SV-COMP *)
+        let bits_offset = GobRef.wrap AnalysisState.executing_speculative_computations true @@ fun () -> Idx.mul item_size_in_bits x in
         let remaining_offset = offset_to_index_offset ?typ:item_typ o in
-        Idx.add bits_offset remaining_offset
+        GobRef.wrap AnalysisState.executing_speculative_computations true @@ fun () -> Idx.add bits_offset remaining_offset
     in
     offset_to_index_offset ?typ offs
 
diff --git a/src/cdomain/value/domains/invariantCil.ml b/src/cdomain/value/domains/invariantCil.ml
index 813ec25818..f41d48ab61 100644
--- a/src/cdomain/value/domains/invariantCil.ml
+++ b/src/cdomain/value/domains/invariantCil.ml
@@ -88,7 +88,7 @@ class exp_contains_anon_type_visitor = object
   inherit nopCilVisitor
   method! vtype (t: typ) =
     match t with
-    | TComp ({cname; _}, _) when BatString.starts_with_stdlib ~prefix:"__anon" cname ->
+    | TComp ({cname; _}, _) when String.starts_with ~prefix:"__anon" cname ->
       raise Stdlib.Exit
     | _ ->
       DoChildren
@@ -102,7 +102,7 @@ let exp_contains_anon_type =
 
 
 (* TODO: synchronize magic constant with BaseDomain *)
-let var_is_heap {vname; _} = BatString.starts_with vname "(alloc@"
+let var_is_heap {vname; _} = String.starts_with vname ~prefix:"(alloc@"
 
 let reset_lazy () =
   ResettableLazy.reset exclude_vars_regexp
diff --git a/src/cdomain/value/util/wideningThresholds.ml b/src/cdomain/value/util/wideningThresholds.ml
index 0d93be76ff..939ed9482f 100644
--- a/src/cdomain/value/util/wideningThresholds.ml
+++ b/src/cdomain/value/util/wideningThresholds.ml
@@ -121,6 +121,7 @@ class extractInvariantsVisitor (exps) = object
   method! vinst (i: instr) =
     match i with
     | Call (_, Lval (Var f, NoOffset), args, _, _) when LibraryFunctions.is_special f ->
+      Goblint_backtrace.wrap_val ~mark:(Cilfacade.FunVarinfo f) @@ fun () ->
       let desc = LibraryFunctions.find f in
       begin match desc.special args with
         | Assert { exp; _ } ->
diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml
index 7e60cce74b..06268130b2 100644
--- a/src/cdomains/apron/affineEqualityDomain.apron.ml
+++ b/src/cdomains/apron/affineEqualityDomain.apron.ml
@@ -6,7 +6,6 @@
     Matrices are modeled as proposed by Karr: Each variable is assigned to a column and each row represents a linear affine relationship that must hold at the corresponding program point.
     The apron environment is hereby used to organize the order of columns and variables. *)
 
-open Batteries
 open GoblintCil
 open Pretty
 module M = Messages
@@ -181,7 +180,7 @@ struct
             else if Z.lt coeff Z.minus_one then Z.to_string coeff
             else Format.asprintf "+%s" (Z.to_string coeff)
           in
-          coeff_str ^ Var.to_string var
+          coeff_str ^ Var.show var
       in
       let const_to_str vl =
         if Z.equal vl Z.zero then
@@ -193,7 +192,7 @@ struct
       in
       let res = (String.concat "" @@ Array.to_list @@ Array.map dim_to_str vars)
                 ^ (const_to_str arr.(Array.length arr - 1)) ^ "=0" in
-      if String.starts_with res "+" then
+      if String.starts_with res ~prefix:"+" then
         Str.string_after res 1
       else
         res
@@ -203,11 +202,10 @@ struct
     | Some m when Matrix.is_empty m -> "⊤"
     | Some m ->
       let constraint_list = List.init (Matrix.num_rows m) (fun i -> vec_to_constraint (conv_to_ints @@ Matrix.get_row m i) t.env) in
-      Format.asprintf "%s" ("[|"^ (String.concat "; " constraint_list) ^"|]")
+      "[|"^ (String.concat "; " constraint_list) ^"|]"
 
   let pretty () (x:t) = text (show x)
-  let printXml f x = BatPrintf.fprintf f "<value>\n<map>\n<key>\nmatrix\n</key>\n<value>\n%s</value>\n<key>\nenv\n</key>\n<value>\n%s</value>\n</map>\n</value>\n" (XmlUtil.escape (Format.asprintf "%s" (show x) )) (XmlUtil.escape (Format.asprintf "%a" (Environment.print: Format.formatter -> Environment.t -> unit) (x.env)))
-
+  let printXml f x = BatPrintf.fprintf f "<value>\n<map>\n<key>\nmatrix\n</key>\n<value>\n%s</value>\n<key>\nenv\n</key>\n<value>\n%a</value>\n</map>\n</value>\n" (XmlUtil.escape (show x)) Environment.printXml x.env
   let eval_interval ask = Bounds.bound_texpr
 
   let name () = "affeq"
@@ -257,7 +255,7 @@ struct
   let meet t1 t2 = timing_wrap "meet" (meet t1) t2
 
   let leq t1 t2 =
-    let env_comp = Environment.compare t1.env t2.env in (* Apron's Environment.compare has defined return values. *)
+    let env_comp = Environment.cmp t1.env t2.env in (* Apron's Environment.cmp has defined return values. *)
     if env_comp = -2 || env_comp > 0 then
       (* -2:  environments are not compatible (a variable has different types in the 2 environements *)
       (* -1: if env1 is a subset of env2,  (OK)  *)
@@ -334,7 +332,7 @@ struct
     else
       match Option.get a.d, Option.get b.d with
       | x, y when is_top_env a || is_top_env b -> {d = Some (Matrix.empty ()); env = Environment.lce a.env b.env}
-      | x, y when (Environment.compare a.env b.env <> 0) ->
+      | x, y when (Environment.cmp a.env b.env <> 0) ->
         let sup_env = Environment.lce a.env b.env in
         let mod_x = dim_add (Environment.dimchange a.env sup_env) x in
         let mod_y = dim_add (Environment.dimchange b.env sup_env) y in
@@ -370,7 +368,7 @@ struct
   let remove_rels_with_var x var env inplace = timing_wrap "remove_rels_with_var" (remove_rels_with_var x var env) inplace
 
   let forget_vars t vars =
-    if is_bot t || is_top_env t || List.is_empty vars then
+    if is_bot t || is_top_env t || vars = [] then
       t
     else
       let m = Option.get t.d in
@@ -430,8 +428,8 @@ struct
 
   let assign_exp ask t var exp no_ov =
     let res = assign_exp ask t var exp no_ov in
-    if M.tracing then M.tracel "ops" "assign_exp t:\n %s \n var: %s \n exp: %a\n no_ov: %b -> \n %s"
-        (show t) (Var.to_string var) d_exp exp (Lazy.force no_ov) (show res) ;
+    if M.tracing then M.tracel "ops" "assign_exp t:\n %s \n var: %a \n exp: %a\n no_ov: %b -> \n %s"
+        (show t) Var.pretty var d_exp exp (Lazy.force no_ov) (show res);
     res
 
   let assign_var (t: VarManagement(Vc)(Mx).t) v v' =
@@ -441,7 +439,7 @@ struct
 
   let assign_var t v v' =
     let res = assign_var t v v' in
-    if M.tracing then M.tracel "ops" "assign_var t:\n %s \n v: %s \n v': %s\n -> %s" (show t) (Var.to_string v) (Var.to_string v') (show res) ;
+    if M.tracing then M.tracel "ops" "assign_var t:\n %s \n v: %a \n v': %a\n -> %s" (show t) Var.pretty v Var.pretty v' (show res);
     res
 
   let assign_var_parallel t vv's =
@@ -499,7 +497,7 @@ struct
 
   let substitute_exp ask t var exp no_ov =
     let res = substitute_exp ask t var exp no_ov in
-    if M.tracing then M.tracel "ops" "Substitute_expr t: \n %s \n var: %s \n exp: %a \n -> \n %s" (show t) (Var.to_string var) d_exp exp (show res);
+    if M.tracing then M.tracel "ops" "Substitute_expr t: \n %s \n var: %a \n exp: %a \n -> \n %s" (show t) Var.pretty var d_exp exp (show res);
     res
 
   let substitute_exp ask t var exp no_ov = timing_wrap "substitution" (substitute_exp ask t var exp) no_ov
diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml
index d0ef268ca6..03ac3ed3f0 100644
--- a/src/cdomains/apron/apronDomain.apron.ml
+++ b/src/cdomains/apron/apronDomain.apron.ml
@@ -283,7 +283,7 @@ struct
   let assign_exp_with ask nd v e no_ov =
     match Convert.texpr1_of_cil_exp ask nd (A.env nd) e no_ov with
     | texpr1 ->
-      if M.tracing then M.trace "apron" "assign_exp converted: %s" (Format.asprintf "%a" Texpr1.print texpr1);
+      if M.tracing then M.trace "apron" "assign_exp converted: %a" Texpr1.pretty texpr1;
       A.assign_texpr_with Man.mgr nd v texpr1 None
     | exception Convert.Unsupported_CilExp _ ->
       if M.tracing then M.trace "apron" "assign_exp unsupported";
@@ -442,7 +442,7 @@ struct
   let invariant _ = []
 
   let show (x:t) =
-    Format.asprintf "%a (env: %a)" A.print x (Environment.print: Format.formatter -> Environment.t -> unit) (A.env x)
+    GobFormat.asprintf "%a (env: %a)" A.print x Environment.pp (A.env x)
   let pretty () (x:t) = text (show x)
 
   let equal x y =
@@ -451,10 +451,10 @@ struct
   let hash (x:t) =
     A.hash Man.mgr x
 
-  let compare (x:t) y: int =
-    (* there is no A.compare, but polymorphic compare should delegate to Abstract0 and Environment compare's implemented in Apron's C *)
-    Stdlib.compare x y
-  let printXml f x = BatPrintf.fprintf f "<value>\n<map>\n<key>\nconstraints\n</key>\n<value>\n%s</value>\n<key>\nenv\n</key>\n<value>\n%s</value>\n</map>\n</value>\n" (XmlUtil.escape (Format.asprintf "%a" A.print x)) (XmlUtil.escape (Format.asprintf "%a" (Environment.print: Format.formatter -> Environment.t -> unit) (A.env x)))
+  let compare (x: t) (y: t): int =
+    failwith "Apron.Abstract1 doesn't have total order" (* https://github.com/antoinemine/apron/issues/99 *)
+
+  let printXml f x = BatPrintf.fprintf f "<value>\n<map>\n<key>\nconstraints\n</key>\n<value>\n%s</value>\n<key>\nenv\n</key>\n<value>\n%a</value>\n</map>\n</value>\n" (XmlUtil.escape (GobFormat.asprint A.print x)) Environment.printXml (A.env x)
 
   let to_yojson (x: t) =
     let constraints =
@@ -463,11 +463,9 @@ struct
       |> Lincons1Set.elements
       |> List.map (fun lincons1 -> `String (Lincons1.show lincons1))
     in
-    let env = `String (Format.asprintf "%a" (Environment.print: Format.formatter -> Environment.t -> unit) (A.env x))
-    in
     `Assoc [
       ("constraints", `List constraints);
-      ("env", env);
+      ("env", Environment.to_yojson (A.env x));
     ]
 
   let unify x y =
@@ -533,9 +531,9 @@ struct
     | _ ->
       begin match Convert.tcons1_of_cil_exp ask d (A.env d) e negate no_ov with
         | tcons1 ->
-          if M.tracing then M.trace "apron" "assert_constraint %a %s" d_exp e (Format.asprintf "%a" Tcons1.print tcons1);
+          if M.tracing then M.trace "apron" "assert_constraint %a %a" d_exp e Tcons1.pretty tcons1;
           if M.tracing then M.trace "apron" "assert_constraint st: %a" D.pretty d;
-          if M.tracing then M.trace "apron" "assert_constraint tcons1: %s" (Format.asprintf "%a" Tcons1.print tcons1);
+          if M.tracing then M.trace "apron" "assert_constraint tcons1: %a" Tcons1.pretty tcons1;
           let r = meet_tcons ask d tcons1 e in
           if M.tracing then M.trace "apron" "assert_constraint r: %a" D.pretty r;
           r
@@ -598,7 +596,7 @@ struct
     let x_cons = A.to_lincons_array Man.mgr x_j in
     let y_cons = A.to_lincons_array Man.mgr y_j in
     let try_add_con j con1 =
-      if M.tracing then M.tracei "apron" "try_add_con %s" (Format.asprintf "%a" (Lincons1.print: Format.formatter -> Lincons1.t -> unit) con1);
+      if M.tracing then M.tracei "apron" "try_add_con %a" Lincons1.pretty con1;
       let t = meet_lincons j con1 in
       let t_x = A.change_environment Man.mgr t x_env false in
       let t_y = A.change_environment Man.mgr t y_env false in
@@ -637,7 +635,7 @@ struct
       in
       let env_exists_mem_con1 env con1 =
         let r = env_exists_mem_con1 env con1 in
-        if M.tracing then M.trace "apron" "env_exists_mem_con1 %s %s -> %B" (Format.asprintf "%a" (Environment.print: Format.formatter -> Environment.t -> unit) env) (Lincons1.show con1) r;
+        if M.tracing then M.trace "apron" "env_exists_mem_con1 %a %a -> %B" Environment.pretty env Lincons1.pretty con1 r;
         r
       in
       (* Heuristically reorder constraints to pass 36/12 with singlethreaded->multithreaded mode switching. *)
diff --git a/src/cdomains/apron/gobApron.apron.ml b/src/cdomains/apron/gobApron.apron.ml
index e202a88c60..fbb1fe9ec5 100644
--- a/src/cdomains/apron/gobApron.apron.ml
+++ b/src/cdomains/apron/gobApron.apron.ml
@@ -1,6 +1,19 @@
 open Batteries
 include Apron
 
+module Scalar =
+struct
+  include Scalar
+
+  let pp = print
+  include Printable.SimpleFormat (
+    struct
+      type nonrec t = t
+      let pp = pp
+    end
+    )
+end
+
 module Coeff =
 struct
   include Coeff
@@ -11,6 +24,15 @@ end
 module Var =
 struct
   include Var
+
+  let pp = print
+  include Printable.SimpleFormat (
+    struct
+      type nonrec t = t
+      let pp = pp
+    end
+    )
+
   let equal x y = Var.compare x y = 0
 end
 
@@ -18,8 +40,17 @@ module Lincons1 =
 struct
   include Lincons1
 
-  let show = Format.asprintf "%a" print
-  let compare x y = String.compare (show x) (show y) (* HACK *)
+  let pp = print
+  include Printable.SimpleFormat (
+    struct
+      type nonrec t = t
+      let pp = pp
+    end
+    )
+
+  let compare x y =
+    (* TODO: implement proper total Lincons1 order *)
+    String.compare (show x) (show y) (* HACK *)
 
   let num_vars x =
     (* Apron.Linexpr0.get_size returns some internal nonsense, so we count ourselves. *)
@@ -43,12 +74,63 @@ struct
     |> of_enum
 end
 
+module Texpr1 =
+struct
+  include Texpr1
+
+  let pp = print
+  include Printable.SimpleFormat (
+    struct
+      type nonrec t = t
+      let pp = pp
+    end
+    )
+
+  module Expr =
+  struct
+    type t = expr
+
+    let pp = print_expr
+    include Printable.SimpleFormat (
+      struct
+        type nonrec t = t
+        let pp = pp
+      end
+      )
+  end
+end
+
+module Tcons1 =
+struct
+  include Tcons1
+
+  let pp = print
+  include Printable.SimpleFormat (
+    struct
+      type nonrec t = t
+      let pp = pp
+    end
+    )
+end
+
 (** A few code elements for environment changes from functions as remove_vars etc. have been moved to sharedFunctions as they are needed in a similar way inside affineEqualityDomain.
     A module that includes various methods used by variable handling operations such as add_vars, remove_vars etc. in apronDomain and affineEqualityDomain. *)
 module Environment =
 struct
   include Environment
 
+  let pp: Format.formatter -> Environment.t -> unit = Environment.print
+  include Printable.SimpleFormat (
+    struct
+      type nonrec t = t
+      let pp = pp
+    end
+    )
+
+  let compare (x: t) (y: t): int =
+    (* TODO: implement total Environment order in OCaml *)
+    failwith "Apron.Environment doesn't have total order" (* https://github.com/antoinemine/apron/issues/99 *)
+
   let ivars_only env =
     let ivs, fvs = Environment.vars env in
     assert (Array.length fvs = 0); (* shouldn't ever contain floats *)
diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml
index 5558bc2c96..c1ca3661a5 100644
--- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml
+++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml
@@ -11,7 +11,7 @@ open Batteries
 open GoblintCil
 open Pretty
 module M = Messages
-open Apron
+open GobApron
 open VectorMatrix
 
 module Mpqf = SharedFunctions.Mpqf
@@ -158,7 +158,7 @@ module EqualitiesConjunction = struct
             let (newref,offs,divi) = (get_rhs d head) in
             let (coeff,y) = BatOption.get newref in
             let (y,yrhs) = inverse head (coeff,y,offs,divi) in (* reassemble yrhs out of components *)
-            let shifted_cluster =  (List.fold (fun map i -> 
+            let shifted_cluster =  (List.fold (fun map i ->
                 let irhs = (get_rhs d i) in (* old entry is i = irhs *)
                 Rhs.subst yrhs y irhs |>    (* new entry for i is irhs [yrhs/y] *)
                 set_rhs map i
@@ -222,7 +222,7 @@ module EqualitiesConjunction = struct
        | Some (coeff,j), ((Some (coeff1,h1), o1, divi1) as oldi)->
          (match get_rhs ts j with
           (* ts[x_j]=o2/d2             ========>  ... *)
-          | (None            , o2, divi2) -> 
+          | (None            , o2, divi2) ->
             let newxi  = Rhs.subst (None,o2,divi2) j (Some (coeff,j),offs,divi) in
             let newxh1 = snd @@ inverse i (coeff1,h1,o1,divi1) in
             let newxh1 = Rhs.subst newxi i newxh1 in
@@ -251,7 +251,7 @@ module EqualitiesConjunction = struct
     else (* var_i = var_i, i.e. it may occur on the rhs of other equalities *)
       (* so now, we transform with the inverse of the transformer: *)
       let inv = snd (inverse i (coeff,j,offs,divi)) in
-      IntMap.fold (fun k v acc -> 
+      IntMap.fold (fun k v acc ->
           match v with
           | (Some (c,x),o,d) when x=i-> set_rhs acc k (Rhs.subst inv i v)
           | _ -> acc
@@ -281,7 +281,7 @@ struct
     let multiply a b =
       (* if one of them is a constant, then multiply. Otherwise, the expression is not linear *)
       match a, b with
-      | [(None,coeff, divi)], c 
+      | [(None,coeff, divi)], c
       | c, [(None,coeff, divi)] -> multiply_with_Q coeff divi c
       | _ -> raise NotLinearExpr
     in
@@ -314,7 +314,7 @@ struct
     | x -> Some(x)
 
   (** convert and simplify (wrt. reference variables) a texpr into a tuple of a list of monomials (coeff,varidx,divi) and a (constant/divi) *)
-  let simplified_monomials_from_texp (t: t) texp = 
+  let simplified_monomials_from_texp (t: t) texp =
     BatOption.bind (monomials_from_texp t texp)
       (fun monomiallist ->
          let d = Option.get t.d in
@@ -323,7 +323,7 @@ struct
            | None -> let gcdee = Z.gcd adiv divi in exprcache,(Z.(aconst*divi/gcdee + offs*adiv/gcdee),Z.lcm adiv divi)
            | Some (coeff,idx) -> let (somevar,someoffs,somedivi)=Rhs.subst (EConj.get_rhs d idx) idx (v,offs,divi) in (* normalize! *)
              let newcache = Option.map_default (fun (coef,ter) -> IMap.add ter Q.((IMap.find_default zero ter exprcache) + make coef somedivi) exprcache) exprcache somevar in
-             let gcdee = Z.gcd adiv divi in 
+             let gcdee = Z.gcd adiv divi in
              (newcache,(Z.(aconst*divi/gcdee + offs*adiv/gcdee),Z.lcm adiv divi))
          in
          let (expr,constant) = List.fold_left accumulate_constants (IMap.empty,(Z.zero,Z.one)) monomiallist in (* abstract simplification of the guard wrt. reference variables *)
@@ -331,7 +331,7 @@ struct
 
   let simplified_monomials_from_texp (t: t) texp =
     let res = simplified_monomials_from_texp t texp in
-    if M.tracing then M.tracel "from_texp" "%s %s -> %s" (EConj.show @@ snd @@ BatOption.get t.d) (Format.asprintf "%a" Texpr1.print_expr texp)
+    if M.tracing then M.tracel "from_texp" "%s %a -> %s" (EConj.show @@ snd @@ BatOption.get t.d) Texpr1.Expr.pretty texp
         (BatOption.map_default (fun (l,(o,d)) -> List.fold_right (fun (a,x,b) acc -> Printf.sprintf "%s*var_%d/%s + %s" (Z.to_string a) x (Z.to_string b) acc) l ((Z.to_string o)^"/"^(Z.to_string d))) "" res);
     res
 
@@ -339,7 +339,7 @@ struct
     BatOption.bind (simplified_monomials_from_texp t texp )
       (fun (sum_of_terms, (constant,divisor)) ->
          (match sum_of_terms with
-          | [] -> Some (None, constant,divisor) 
+          | [] -> Some (None, constant,divisor)
           | [(coeff,var,divi)] -> Some (Rhs.canonicalize (Some (Z.mul divisor coeff,var), Z.mul constant divi,Z.mul divisor divi))
           |_ -> None))
 
@@ -361,7 +361,7 @@ struct
     else
       match simplify_to_ref_and_offset t (Texpr1.to_expr texpr) with
       | Some (None, offset, divisor) when Z.equal (Z.rem offset divisor) Z.zero -> let res = Z.div offset divisor in
-        (if M.tracing then M.tracel "bounds" "min: %s max: %s" (IntOps.BigIntOps.to_string res) (IntOps.BigIntOps.to_string res);
+        (if M.tracing then M.tracel "bounds" "min: %a max: %a" GobZ.pretty res GobZ.pretty res;
          Some res, Some res)
       | _ -> None, None
 
@@ -424,7 +424,7 @@ struct
         EConj.show_formatted (show_var varM.env) (snd arr) ^ (to_subscript @@ fst arr)
 
   let pretty () (x:t) = text (show x)
-  let printXml f x = BatPrintf.fprintf f "<value>\n<map>\n<key>\nequalities\n</key>\n<value>\n%s</value>\n<key>\nenv\n</key>\n<value>\n%s</value>\n</map>\n</value>\n" (XmlUtil.escape (Format.asprintf "%s" (show x) )) (XmlUtil.escape (Format.asprintf "%a" (Environment.print: Format.formatter -> Environment.t -> unit) (x.env)))
+  let printXml f x = BatPrintf.fprintf f "<value>\n<map>\n<key>\nequalities\n</key>\n<value>\n%s</value>\n<key>\nenv\n</key>\n<value>\n%a</value>\n</map>\n</value>\n" (XmlUtil.escape (show x)) Environment.printXml x.env
   let eval_interval ask = Bounds.bound_texpr
 
   let meet_with_one_conj t i (var, o, divi) =
@@ -447,7 +447,7 @@ struct
     let t1 = change_d t1 sup_env ~add:true ~del:false in
     let t2 = change_d t2 sup_env ~add:true ~del:false in
     match t1.d, t2.d with
-    | Some d1', Some d2' -> 
+    | Some d1', Some d2' ->
       EConj.IntMap.fold (fun lhs rhs map -> meet_with_one_conj map lhs rhs) (snd d2') t1 (* even on sparse d2, this will chose the relevant conjs to meet with*)
     | _ -> {d = None; env = sup_env}
 
@@ -459,7 +459,7 @@ struct
   let meet t1 t2 = timing_wrap "meet" (meet t1) t2
 
   let leq t1 t2 =
-    let env_comp = Environment.compare t1.env t2.env in (* Apron's Environment.compare has defined return values. *)
+    let env_comp = Environment.cmp t1.env t2.env in (* Apron's Environment.cmp has defined return values. *)
     let implies ts i (var, offs, divi) =
       let tuple_cmp = Tuple3.eq (Option.eq ~eq:(Tuple2.eq (Z.equal) (Int.equal))) (Z.equal) (Z.equal) in
       match var with
@@ -489,7 +489,7 @@ struct
          - lhs itself
          - criteria A and B that characterize equivalence class, depending on the reference variable and the affine expression parameters wrt. each EConj
          - rhs1
-         - rhs2 
+         - rhs2
            however, we have to account for the sparseity of EConj maps by manually patching holes with default values *)
       let joinfunction lhs rhs1 rhs2 =
         (
@@ -516,15 +516,15 @@ struct
       let varentry ci offi ch offh xh =
         let (coeff,off,d) = Q.(ci,(offi*ch)-(ci*offh),ch) in (* compute new rhs in Q *)
         let (coeff,off,d) = Z.(coeff.num*d.den*off.den,off.num*d.den*coeff.den,d. num*coeff.den*off.den) in (* convert that back into Z *)
-        Rhs.canonicalize (Some(coeff,xh),off,d) 
+        Rhs.canonicalize (Some(coeff,xh),off,d)
       in
       (* ci1 = a*ch1+b /\ ci2 = a*ch2+b *)
       (* ===> a = (ci1-ci2)/(ch1-ch2) b = ci2-a*ch2 *)
-      let constentry ci1 ci2 ch1 ch2 xh = 
+      let constentry ci1 ci2 ch1 ch2 xh =
         let a = Q.((ci1-ci2) / (ch1-ch2)) in
         let b = Q.(ci2 - a*ch2) in
         Rhs.canonicalize (Some (Z.(a.num*b.den),xh),Z.(b.num*a.den) ,Z.(a.den*b.den) ) in
-      let iterate map l = 
+      let iterate map l =
         match l with
         | (_, _, _, rhs                  , rhs'                 ) :: t when Rhs.equal rhs rhs' -> List.fold (fun acc (x,_,_,rh,_)      -> EConj.set_rhs acc x rh) map l
         | (h, _, _, ((Some (ch,_),oh,dh)), ((Some _,_,_)       )) :: t -> List.fold (fun acc (i,_,_,(monom,oi,di),_)         -> EConj.set_rhs acc i (varentry   Q.(make (fst@@Option.get monom) di)   Q.(make oi di)   Q.(make ch dh)   Q.(make oh dh)   h)) map t
@@ -543,7 +543,7 @@ struct
     | Some x, Some y when is_top a || is_top b ->
       let new_env = Environment.lce a.env b.env in
       top_of new_env
-    | Some x, Some y when (Environment.compare a.env b.env <> 0) ->
+    | Some x, Some y when (Environment.cmp a.env b.env <> 0) ->
       let sup_env = Environment.lce a.env b.env in
       let mod_x = dim_add (Environment.dimchange a.env sup_env) x in
       let mod_y = dim_add (Environment.dimchange b.env sup_env) y in
@@ -630,8 +630,8 @@ struct
 
   let assign_exp ask t var exp no_ov =
     let res = assign_exp ask t var exp no_ov in
-    if M.tracing then M.tracel "ops" "assign_exp t:\n %s \n var: %s \n exp: %a\n no_ov: %b -> \n %s"
-        (show t) (Var.to_string var) d_exp exp (Lazy.force no_ov) (show res) ;
+    if M.tracing then M.tracel "ops" "assign_exp t:\n %s \n var: %a \n exp: %a\n no_ov: %b -> \n %s"
+        (show t) Var.pretty var d_exp exp (Lazy.force no_ov) (show res);
     res
 
   let assign_var (t: VarManagement.t) v v' =
@@ -640,7 +640,7 @@ struct
 
   let assign_var t v v' =
     let res = assign_var t v v' in
-    if M.tracing then M.tracel "ops" "assign_var t:\n %s \n v: %s \n v': %s\n -> %s" (show t) (Var.to_string v) (Var.to_string v') (show res) ;
+    if M.tracing then M.tracel "ops" "assign_var t:\n %s \n v: %a \n v': %a\n -> %s" (show t) Var.pretty v Var.pretty v' (show res);
     res
 
   (** Parallel assignment of variables.
@@ -693,7 +693,7 @@ struct
 
   let substitute_exp ask t var exp no_ov =
     let res = substitute_exp ask t var exp no_ov in
-    if M.tracing then M.tracel "ops" "Substitute_expr t: \n %s \n var: %s \n exp: %a \n -> \n %s" (show t) (Var.to_string var) d_exp exp (show res);
+    if M.tracing then M.tracel "ops" "Substitute_expr t: \n %s \n var: %a \n exp: %a \n -> \n %s" (show t) Var.pretty var d_exp exp (show res);
     res
 
   let substitute_exp ask t var exp no_ov = timing_wrap "substitution" (substitute_exp ask t var exp) no_ov
diff --git a/src/cdomains/apron/relationDomain.apron.ml b/src/cdomains/apron/relationDomain.apron.ml
index 9b1eff0c64..3b7226889f 100644
--- a/src/cdomains/apron/relationDomain.apron.ml
+++ b/src/cdomains/apron/relationDomain.apron.ml
@@ -146,7 +146,7 @@ end
 type ('a, 'b) relcomponents_t = {
   rel: 'a;
   priv: 'b;
-} [@@deriving eq, ord, hash, to_yojson]
+} [@@deriving eq, ord, hash, to_yojson, relift, lattice]
 
 module RelComponents (D3: S3) (PrivD: Lattice.S):
 sig
@@ -155,13 +155,11 @@ sig
 end =
 struct
   module RD = D3
-  type t = (RD.t, PrivD.t) relcomponents_t [@@deriving eq, ord, hash, to_yojson]
+  type t = (RD.t, PrivD.t) relcomponents_t [@@deriving eq, ord, hash, to_yojson, relift, lattice]
 
   include Printable.Std
   open Pretty
 
-  let relift {rel; priv} = {rel = RD.relift rel; priv = PrivD.relift priv}
-
   let show r =
     let first  = RD.show r.rel in
     let third  = PrivD.show r.priv in
@@ -185,26 +183,11 @@ struct
     let tr = QCheck.pair (RD.arbitrary ()) (PrivD.arbitrary ()) in
     QCheck.map ~rev:to_tuple of_tuple tr
 
-  let bot () = {rel = RD.bot (); priv = PrivD.bot ()}
-  let is_bot {rel; priv} = RD.is_bot rel && PrivD.is_bot priv
-  let top () = {rel = RD.top (); priv = PrivD.bot ()}
-  let is_top {rel; priv} = RD.is_top rel && PrivD.is_top priv
-
-  let leq {rel=x1; priv=x3 } {rel=y1; priv=y3} =
-    RD.leq x1 y1 && PrivD.leq x3 y3
-
   let pretty_diff () (({rel=x1; priv=x3}:t),({rel=y1; priv=y3}:t)): Pretty.doc =
     if not (RD.leq x1 y1) then
       RD.pretty_diff () (x1,y1)
     else
       PrivD.pretty_diff () (x3,y3)
-
-  let op_scheme op1 op3 {rel=x1; priv=x3} {rel=y1; priv=y3}: t =
-    {rel = op1 x1 y1; priv = op3 x3 y3 }
-  let join = op_scheme RD.join PrivD.join
-  let meet = op_scheme RD.meet PrivD.meet
-  let widen = op_scheme RD.widen PrivD.widen
-  let narrow = op_scheme RD.narrow PrivD.narrow
 end
 
 
diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml
index 8c94c996b0..86b5f2770f 100644
--- a/src/cdomains/apron/sharedFunctions.apron.ml
+++ b/src/cdomains/apron/sharedFunctions.apron.ml
@@ -6,7 +6,8 @@ open GobApron
 
 module M = Messages
 
-let int_of_scalar ?round (scalar: Scalar.t) =
+
+let int_of_scalar ?(scalewith=Z.one) ?round (scalar: Scalar.t) =
   if Scalar.is_infty scalar <> 0 then (* infinity means unbounded *)
     None
   else
@@ -20,23 +21,26 @@ let int_of_scalar ?round (scalar: Scalar.t) =
         | None when Stdlib.Float.is_integer f -> Some f
         | None -> None
       in
-      Z.of_float f
+      Z.(of_float f * scalewith)
     | Mpqf scalar -> (* octMPQ, boxMPQ, polkaMPQ *)
       let n = Mpqf.get_num scalar in
       let d = Mpqf.get_den scalar in
+      let scale = Z_mlgmpidl.mpz_of_z scalewith in
       let+ z =
         if Mpzf.cmp_int d 1 = 0 then (* exact integer (denominator 1) *)
-          Some n
+          Some (Mpzf.mul scale n)
         else
           begin match round with
-            | Some `Floor -> Some (Mpzf.fdiv_q n d) (* floor division *)
-            | Some `Ceil -> Some (Mpzf.cdiv_q n d) (* ceiling division *)
-            | None -> None
+            | Some `Floor -> Some (Mpzf.mul scale (Mpzf.fdiv_q n d)) (* floor division *)
+            | Some `Ceil ->  Some (Mpzf.mul scale (Mpzf.cdiv_q n d)) (* ceiling division *)
+            | None -> let product = Mpzf.mul scale n in if Mpz.divisible_p product d then
+                Some (Mpzf.divexact product d) (* scale, preferably with common denominator *)
+              else None
           end
       in
       Z_mlgmpidl.z_of_mpzf z
     | _ ->
-      failwith ("int_of_scalar: unsupported: " ^ Scalar.to_string scalar)
+      failwith ("int_of_scalar: unsupported: " ^ Scalar.show scalar)
 
 
 module type ConvertArg =
@@ -136,7 +140,7 @@ struct
             let expr =
               (** simplify asks for a constant value of some subexpression e, similar to a constant fold. In particular but not exclusively
                   this query is answered by the 2 var equalities domain itself. This normalizes arbitrary expressions to a point where they
-                  might be able to be represented by means of 2 var equalities 
+                  might be able to be represented by means of 2 var equalities
 
                   This simplification happens during a time, when there are temporary variables a#in and a#out part of the expression,
                   but are not represented in the ctx, thus queries may result in top for these variables. Wrapping this in speculative
@@ -196,7 +200,7 @@ struct
     in
     let exp = Cil.constFold false exp in
     let res = conv exp in
-    if M.tracing then M.trace "relation" "texpr1_expr_of_cil_exp: %a -> %s (%b)" d_plainexp exp (Format.asprintf "%a" Texpr1.print_expr res) (Lazy.force no_ov);
+    if M.tracing then M.trace "relation" "texpr1_expr_of_cil_exp: %a -> %a (%b)" d_plainexp exp Texpr1.Expr.pretty res (Lazy.force no_ov);
     res
 
   let texpr1_of_cil_exp ask d env e no_ov =
@@ -245,11 +249,11 @@ module CilOfApron (V: SV) =
 struct
   exception Unsupported_Linexpr1
 
-  let cil_exp_of_linexpr1 (linexpr1:Linexpr1.t) =
+  let cil_exp_of_linexpr1 ?scalewith (linexpr1:Linexpr1.t) =
     let longlong = TInt(ILongLong,[]) in
     let coeff_to_const consider_flip (c:Coeff.union_5) = match c with
       | Scalar c ->
-        (match int_of_scalar c with
+        (match int_of_scalar ?scalewith c with
          | Some i ->
            let ci,truncation = truncateCilint ILongLong i in
            if truncation = NoTruncation then
@@ -263,15 +267,14 @@ struct
                else
                  Const (CInt(i,ILongLong,None)), false
            else
-             (M.warn ~category:Analyzer "Invariant Apron: coefficient is not int: %s" (Scalar.to_string c); raise Unsupported_Linexpr1)
+             (M.warn ~category:Analyzer "Invariant Apron: coefficient is not int: %a" Scalar.pretty c; raise Unsupported_Linexpr1)
          | None -> raise Unsupported_Linexpr1)
       | _ -> raise Unsupported_Linexpr1
     in
     let expr = ref (fst @@ coeff_to_const false (Linexpr1.get_cst linexpr1)) in
     let append_summand (c:Coeff.union_5) v =
       match V.to_cil_varinfo v with
-      | Some vinfo ->
-        (* TODO: What to do with variables that have a type that cannot be stored into ILongLong to avoid overflows? *)
+      | Some vinfo when IntDomain.Size.is_cast_injective ~from_type:vinfo.vtype ~to_type:(TInt(ILongLong,[]))   ->
         let var = Cilfacade.mkCast ~e:(Lval(Var vinfo,NoOffset)) ~newt:longlong in
         let coeff, flip = coeff_to_const true c in
         let prod = BinOp(Mult, coeff, var, longlong) in
@@ -279,17 +282,45 @@ struct
           expr := BinOp(MinusA,!expr,prod,longlong)
         else
           expr := BinOp(PlusA,!expr,prod,longlong)
-      | None -> M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil var: %s"  (Var.to_string v); raise Unsupported_Linexpr1
+      | None -> M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil var: %a" Var.pretty v; raise Unsupported_Linexpr1
+      | _ -> M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil var in overflow preserving manner: %a" Var.pretty v; raise Unsupported_Linexpr1
     in
     Linexpr1.iter append_summand linexpr1;
     !expr
 
 
+  let lcm_den linexpr1 =
+    let exception UnsupportedScalar
+    in
+    let frac_of_scalar scalar =
+      if Scalar.is_infty scalar <> 0 then (* infinity means unbounded *)
+        None
+      else match scalar with
+        | Float f -> if Stdlib.Float.is_integer f then Some (Q.of_float f) else None
+        | Mpqf f -> Some (Z_mlgmpidl.q_of_mpqf f)
+        | _ -> raise UnsupportedScalar
+    in
+    let extract_den (c:Coeff.union_5) =
+      match c with
+      | Scalar c -> BatOption.map Q.den (frac_of_scalar c)
+      | _ -> None
+    in
+    let lcm_denom = ref (BatOption.default Z.one (extract_den (Linexpr1.get_cst linexpr1))) in
+    let lcm_coeff (c:Coeff.union_5) _ =
+      match (extract_den c) with
+      | Some z -> lcm_denom := Z.lcm z !lcm_denom
+      | _      -> ()
+    in
+    try
+      Linexpr1.iter lcm_coeff linexpr1; !lcm_denom
+    with UnsupportedScalar -> Z.one
+
   let cil_exp_of_lincons1 (lincons1:Lincons1.t) =
     let zero = Cil.kinteger ILongLong 0 in
     try
       let linexpr1 = Lincons1.get_linexpr1 lincons1 in
-      let cilexp = cil_exp_of_linexpr1 linexpr1 in
+      let common_denominator = lcm_den linexpr1 in
+      let cilexp = cil_exp_of_linexpr1 ~scalewith:common_denominator linexpr1 in
       match Lincons1.get_typ lincons1 with
       | EQ -> Some (Cil.constFold false @@ BinOp(Eq, cilexp, zero, TInt(IInt,[])))
       | SUPEQ -> Some (Cil.constFold false @@ BinOp(Ge, cilexp, zero, TInt(IInt,[])))
diff --git a/src/cdomains/baseDomain.ml b/src/cdomains/baseDomain.ml
index 1be0fb8c1e..64b5a174e8 100644
--- a/src/cdomains/baseDomain.ml
+++ b/src/cdomains/baseDomain.ml
@@ -38,7 +38,7 @@ type 'a basecomponents_t = {
   deps: PartDeps.t;
   weak: WeakUpdates.t;
   priv: 'a;
-} [@@deriving eq, ord, hash]
+} [@@deriving eq, ord, hash, relift, lattice]
 
 
 module BaseComponents (PrivD: Lattice.S):
@@ -47,7 +47,7 @@ sig
   val op_scheme: (CPA.t -> CPA.t -> CPA.t) -> (PartDeps.t -> PartDeps.t -> PartDeps.t) -> (WeakUpdates.t -> WeakUpdates.t -> WeakUpdates.t) -> (PrivD.t -> PrivD.t -> PrivD.t) -> t -> t -> t
 end =
 struct
-  type t = PrivD.t basecomponents_t [@@deriving eq, ord, hash]
+  type t = PrivD.t basecomponents_t [@@deriving eq, ord, hash, relift, lattice]
 
   include Printable.Std
   open Pretty
@@ -90,14 +90,6 @@ struct
     let tr = QCheck.quad (CPA.arbitrary ()) (PartDeps.arbitrary ()) (WeakUpdates.arbitrary ()) (PrivD.arbitrary ()) in
     QCheck.map ~rev:to_tuple of_tuple tr
 
-  let bot () = { cpa = CPA.bot (); deps = PartDeps.bot (); weak = WeakUpdates.bot (); priv = PrivD.bot ()}
-  let is_bot {cpa; deps; weak; priv} = CPA.is_bot cpa && PartDeps.is_bot deps && WeakUpdates.is_bot weak && PrivD.is_bot priv
-  let top () = {cpa = CPA.top (); deps = PartDeps.top ();  weak = WeakUpdates.top () ; priv = PrivD.top ()}
-  let is_top {cpa; deps; weak; priv} = CPA.is_top cpa && PartDeps.is_top deps && WeakUpdates.is_top weak && PrivD.is_top priv
-
-  let leq {cpa=x1; deps=x2; weak=x3; priv=x4 } {cpa=y1; deps=y2; weak=y3; priv=y4} =
-    CPA.leq x1 y1 && PartDeps.leq x2 y2 && WeakUpdates.leq x3 y3 && PrivD.leq x4 y4
-
   let pretty_diff () (({cpa=x1; deps=x2; weak=x3; priv=x4}:t),({cpa=y1; deps=y2; weak=y3; priv=y4}:t)): Pretty.doc =
     if not (CPA.leq x1 y1) then
       CPA.pretty_diff () (x1,y1)
@@ -110,13 +102,6 @@ struct
 
   let op_scheme op1 op2 op3 op4 {cpa=x1; deps=x2; weak=x3; priv=x4} {cpa=y1; deps=y2; weak=y3; priv=y4}: t =
     {cpa = op1 x1 y1; deps = op2 x2 y2; weak = op3 x3 y3; priv = op4 x4 y4 }
-  let join = op_scheme CPA.join PartDeps.join WeakUpdates.join PrivD.join
-  let meet = op_scheme CPA.meet PartDeps.meet WeakUpdates.meet PrivD.meet
-  let widen = op_scheme CPA.widen PartDeps.widen WeakUpdates.widen PrivD.widen
-  let narrow = op_scheme CPA.narrow PartDeps.narrow WeakUpdates.narrow PrivD.narrow
-
-  let relift {cpa; deps; weak; priv} =
-    {cpa = CPA.relift cpa; deps = PartDeps.relift deps; weak = WeakUpdates.relift weak; priv = PrivD.relift priv}
 end
 
 module type ExpEvaluator =
diff --git a/src/cdomains/lockDomain.ml b/src/cdomains/lockDomain.ml
index 35d73e5f28..08353f4795 100644
--- a/src/cdomains/lockDomain.ml
+++ b/src/cdomains/lockDomain.ml
@@ -24,6 +24,8 @@ struct
     else
       Some false
 
+  let of_var v: t = (v, `NoOffset)
+
   let of_mval ((v, o): Mval.t): t =
     (v, Offset.Poly.map_indices (fun i -> IndexDomain.to_int i |> Option.get) o)
 
diff --git a/src/cdomains/mHP.ml b/src/cdomains/mHP.ml
index f58b7d2e92..433486d4e0 100644
--- a/src/cdomains/mHP.ml
+++ b/src/cdomains/mHP.ml
@@ -11,10 +11,7 @@ type t = {
   tid: ThreadIdDomain.ThreadLifted.t;
   created: ConcDomain.ThreadSet.t;
   must_joined: ConcDomain.ThreadSet.t;
-} [@@deriving eq, ord, hash]
-
-let relift {tid; created; must_joined} =
-  {tid = ThreadIdDomain.ThreadLifted.relift tid; created = ConcDomain.ThreadSet.relift created; must_joined = ConcDomain.ThreadSet.relift must_joined}
+} [@@deriving eq, ord, hash, relift]
 
 let current (ask:Queries.ask) =
   {
diff --git a/src/cdomains/pthreadDomain.ml b/src/cdomains/pthreadDomain.ml
index 2c12689dcf..8862a768bc 100644
--- a/src/cdomains/pthreadDomain.ml
+++ b/src/cdomains/pthreadDomain.ml
@@ -25,7 +25,7 @@ end
 module D = struct
   include Printable.StdLeaf
 
-  type t = { tid : Tid.t; pred : Pred.t; ctx : Ctx.t } [@@deriving eq, ord, hash, to_yojson]
+  type t = { tid : Tid.t; pred : Pred.t; ctx : Ctx.t } [@@deriving eq, ord, hash, relift, to_yojson, lattice]
 
   (** printing *)
   let show x =
@@ -35,26 +35,15 @@ module D = struct
       (Pred.show x.pred)
       (Ctx.show x.ctx)
 
-  include Printable.SimpleShow(struct type nonrec t = t let show = show end) (* TODO: overrides derived to_yojson *)
+  include Printable.SimpleShow (struct
+      type nonrec t = t
+      let show = show
+    end) (* TODO: overrides derived to_yojson *)
 
   let name () = "pthread state"
 
   let make tid pred ctx = { tid; pred; ctx }
-  let bot () = { tid = Tid.bot (); pred = Pred.bot (); ctx = Ctx.bot () }
-  let is_bot x = Tid.is_bot x.tid && Pred.is_bot x.pred && Ctx.is_bot x.ctx
   let any_is_bot x = Tid.is_bot x.tid || Pred.is_bot x.pred
-  let top () = { tid = Tid.top (); pred = Pred.top (); ctx = Ctx.top () }
-  let is_top x = Tid.is_top x.tid && Pred.is_top x.pred && Ctx.is_top x.ctx
-
-  let leq x y = Tid.leq x.tid y.tid && Pred.leq x.pred y.pred && Ctx.leq x.ctx y.ctx
-
-  let op_scheme op1 op2 op3 x y : t =
-    { tid = op1 x.tid y.tid; pred = op2 x.pred y.pred; ctx = op3 x.ctx y.ctx }
-
-  let join = op_scheme Tid.join Pred.join Ctx.join
-  let widen = join
-  let meet = op_scheme Tid.meet Pred.meet Ctx.meet
-  let narrow = meet
 
   let pretty_diff () (x,y) =
     if not (Tid.leq x.tid y.tid) then
diff --git a/src/common/domains/printable.ml b/src/common/domains/printable.ml
index 1a642c932a..93d3f99edc 100644
--- a/src/common/domains/printable.ml
+++ b/src/common/domains/printable.ml
@@ -88,6 +88,20 @@ struct
   let to_yojson x = `String (show x)
 end
 
+module type Formatable =
+sig
+  type t
+  val pp: Format.formatter -> t -> unit
+end
+
+module SimpleFormat (P: Formatable) =
+struct
+  let show x = GobFormat.asprint P.pp x
+  let pretty () x = text (show x)
+  let printXml f x = BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" (XmlUtil.escape (show x))
+  let to_yojson x = `String (show x)
+end
+
 
 module type Name = sig val name: string end
 module UnitConf (N: Name) =
@@ -465,7 +479,7 @@ module ProdConf (C: ProdConfiguration) (Base1: S) (Base2: S)=
 struct
   include C
 
-  type t = Base1.t * Base2.t [@@deriving eq, ord, hash]
+  type t = Base1.t * Base2.t [@@deriving eq, ord, hash, relift]
 
   include Std
 
@@ -504,8 +518,6 @@ struct
     `Assoc [ (Base1.name (), Base1.to_yojson x); (Base2.name (), Base2.to_yojson y) ]
 
   let arbitrary () = QCheck.pair (Base1.arbitrary ()) (Base2.arbitrary ())
-
-  let relift (x,y) = (Base1.relift x, Base2.relift y)
 end
 
 module Prod = ProdConf (struct let expand_fst = true let expand_snd = true end)
@@ -513,7 +525,7 @@ module ProdSimple = ProdConf (struct let expand_fst = false let expand_snd = fal
 
 module Prod3 (Base1: S) (Base2: S) (Base3: S) =
 struct
-  type t = Base1.t * Base2.t * Base3.t [@@deriving eq, ord, hash]
+  type t = Base1.t * Base2.t * Base3.t [@@deriving eq, ord, hash, relift]
   include Std
 
   let show (x,y,z) =
@@ -555,40 +567,10 @@ struct
 
   let name () = Base1.name () ^ " * " ^ Base2.name () ^ " * " ^ Base3.name ()
 
-  let relift (x,y,z) = (Base1.relift x, Base2.relift y, Base3.relift z)
   let arbitrary () = QCheck.triple (Base1.arbitrary ()) (Base2.arbitrary ()) (Base3.arbitrary ())
 end
 
-module Prod4 (Base1: S) (Base2: S) (Base3: S) (Base4: S) = struct
-  type t = Base1.t * Base2.t * Base3.t * Base4.t [@@deriving eq, ord, hash]
-  include Std
-
-  let show (x,y,z,w) = "(" ^ Base1.show x ^ ", " ^ Base2.show y ^ ", " ^ Base3.show z ^ ", " ^ Base4.show w ^ ")"
-
-  let pretty () (x,y,z,w) =
-    text "(" ++
-    Base1.pretty () x
-    ++ text ", " ++
-    Base2.pretty () y
-    ++ text ", " ++
-    Base3.pretty () z
-    ++ text ", " ++
-    Base4.pretty () w
-    ++ text ")"
-
-  let printXml f (x,y,z,w) =
-    BatPrintf.fprintf f "<value>\n<map>\n<key>\n%s\n</key>\n%a<key>\n%s\n</key>\n%a<key>\n%s\n</key>\n%a<key>\n%s\n</key>\n%a</map>\n</value>\n" (XmlUtil.escape (Base1.name ())) Base1.printXml x (XmlUtil.escape (Base2.name ())) Base2.printXml y (XmlUtil.escape (Base3.name ())) Base3.printXml z (XmlUtil.escape (Base4.name ())) Base4.printXml w
-
-  let to_yojson (x, y, z, w) =
-    `Assoc [ (Base1.name (), Base1.to_yojson x); (Base2.name (), Base2.to_yojson y); (Base3.name (), Base3.to_yojson z); (Base4.name (), Base4.to_yojson w) ]
-
-  let name () = Base1.name () ^ " * " ^ Base2.name () ^ " * " ^ Base3.name () ^ " * " ^ Base4.name ()
-
-  let relift (x,y,z,w) = (Base1.relift x, Base2.relift y, Base3.relift z, Base4.relift w)
-  let arbitrary () = QCheck.quad (Base1.arbitrary ()) (Base2.arbitrary ()) (Base3.arbitrary ()) (Base4.arbitrary ())
-end
-
-module PQueue (Base: S) = 
+module PQueue (Base: S) =
 struct
   type t = Base.t BatDeque.dq
   include Std
@@ -604,22 +586,22 @@ struct
     let rec loop n q =
       match BatDeque.front q with
       | None -> ()
-      | Some (x, xs) -> (BatPrintf.fprintf f "<key>%d</key>\n%a\n" n Base.printXml x; 
+      | Some (x, xs) -> (BatPrintf.fprintf f "<key>%d</key>\n%a\n" n Base.printXml x;
                          loop (n+1) (xs))
     in
     BatPrintf.fprintf f "<value>\n<map>\n";
-    loop 0 xs; 
+    loop 0 xs;
     BatPrintf.fprintf f "</map>\n</value>\n"
 
   let to_yojson q = `List (BatDeque.to_list @@ BatDeque.map (Base.to_yojson) q)
   let hash q = BatDeque.fold_left (fun acc x -> (acc + 71) * (Base.hash x)) 11 q
   let equal q1 q2 = BatDeque.eq ~eq:Base.equal q1 q2
-  let compare q1 q2 = 
+  let compare q1 q2 =
     match BatDeque.front q1, BatDeque.front q2 with
     | None, None -> 0
     | None, Some(_, _) -> -1
     | Some(_, _), None -> 1
-    | Some(a1, q1'), Some(a2, q2') -> 
+    | Some(a1, q1'), Some(a2, q2') ->
       let c = Base.compare a1 a2 in
       if c <> 0 then c
       else compare q1' q2'
diff --git a/src/common/dune b/src/common/dune
index 0cded0bdf9..e5aeddde7f 100644
--- a/src/common/dune
+++ b/src/common/dune
@@ -11,6 +11,7 @@
    goblint_logs
    goblint_config
    goblint_tracing
+   goblint_backtrace
    goblint-cil
    fpath
    yojson
@@ -23,7 +24,8 @@
   (pps
     ppx_deriving.std
     ppx_deriving_hash
-    ppx_deriving_yojson))
+    ppx_deriving_yojson
+    ppx_deriving_printable))
  (instrumentation (backend bisect_ppx)))
 
 (documentation)
diff --git a/src/common/util/cilType.ml b/src/common/util/cilType.ml
index a484a228bd..91368052b3 100644
--- a/src/common/util/cilType.ml
+++ b/src/common/util/cilType.ml
@@ -79,8 +79,8 @@ struct
 
   let of_yojson = function
     | `Assoc l ->
-      begin match List.assoc_opt "file" l, List.assoc_opt "line" l, List.assoc_opt "column" l, List.assoc_opt "byte" l with
-        | Some (`String file), Some (`Int line), Some (`Int column), Some (`Int byte) ->
+      begin match List.assoc_opt "file" l, List.assoc_opt "line" l, List.assoc_opt "column" l, Option.value ~default:(`Int (-1)) (List.assoc_opt "byte" l) with
+        | Some (`String file), Some (`Int line), Some (`Int column), `Int byte ->
           let loc = {file; line; column; byte; endLine = -1; endColumn = -1; endByte = -1; synthetic = false} in
           begin match List.assoc_opt "endLine" l, List.assoc_opt "endColumn" l, List.assoc_opt "endByte" l with
             | Some (`Int endLine), Some (`Int endColumn), Some (`Int endByte) ->
@@ -698,6 +698,7 @@ struct
     | AAddrOf of t
     | AIndex of t * t
     | AQuestion of t * t * t
+    | AAssign of t * t
   [@@deriving eq, ord, hash]
 
   let name () = "attrparam"
diff --git a/src/common/util/cilfacade.ml b/src/common/util/cilfacade.ml
index 99430ee8b6..d520d250e2 100644
--- a/src/common/util/cilfacade.ml
+++ b/src/common/util/cilfacade.ml
@@ -6,6 +6,14 @@ module E = Errormsg
 
 include Cilfacade0
 
+type Goblint_backtrace.mark += FunVarinfo of varinfo
+
+let () = Goblint_backtrace.register_mark_printer (function
+    | FunVarinfo var ->
+      Some ("function " ^ CilType.Varinfo.show var)
+    | _ -> None (* for other marks *)
+  )
+
 (** Command for assigning an id to a varinfo. All varinfos directly created by Goblint should be modified by this method *)
 let create_var (var: varinfo) =
   (* Hack: using negative integers should preempt conflicts with ids generated by CIL *)
@@ -734,7 +742,7 @@ let add_function_declarations (file: Cil.file): unit =
   let functions, non_functions = List.partition (fun g -> match g with GFun _ -> true | _ -> false) globals in
   let upto_last_type, non_types = GobList.until_last_with (fun g -> match g with GType _ -> true | _ -> false) non_functions in
   let declaration_from_GFun f = match f with
-    | GFun (f, _) when BatString.starts_with_stdlib ~prefix:"__builtin" f.svar.vname ->
+    | GFun (f, _) when String.starts_with ~prefix:"__builtin" f.svar.vname ->
       (* Builtin functions should not occur in asserts generated, so there is no need to add declarations for them.*)
       None
     | GFun (f, _) ->
diff --git a/src/common/util/gobFormat.ml b/src/common/util/gobFormat.ml
index 3cda0a4758..8f26ff0087 100644
--- a/src/common/util/gobFormat.ml
+++ b/src/common/util/gobFormat.ml
@@ -19,3 +19,12 @@ let pp_set_ansi_color_tags ppf =
   Format.pp_set_mark_tags ppf true
 
 let pp_print_nothing (ppf: Format.formatter) () = ()
+
+let pp_infinity = 1000000001 (* Exact value not exposed before OCaml 5.2, but use the smallest value permitted by documentation. *)
+
+let pp_set_infinite_geometry = Format.pp_set_geometry ~max_indent:(pp_infinity - 2) ~margin:(pp_infinity - 1)
+
+let asprintf (fmt: ('a, Format.formatter, unit, string) format4): 'a =
+  Format.asprintf ("%t" ^^ fmt) pp_set_infinite_geometry
+
+let asprint pp x = asprintf "%a" pp x (* eta-expanded to bypass value restriction *)
diff --git a/src/config/options.schema.json b/src/config/options.schema.json
index acf85abed9..7b07c3ca35 100644
--- a/src/config/options.schema.json
+++ b/src/config/options.schema.json
@@ -344,7 +344,7 @@
           "default": [
             "expRelation", "base", "threadid", "threadflag", "threadreturn",
             "escape", "mutexEvents", "mutex", "access", "race", "mallocWrapper", "mhp",
-            "assert"
+            "assert", "pthreadMutexType"
           ]
         },
         "path_sens": {
@@ -807,6 +807,20 @@
                   "type": "string",
                   "enum": ["once", "fixpoint"],
                   "default": "once"
+                },
+                "int": {
+                  "title": "ana.base.invariant.int",
+                  "type": "object",
+                  "properties": {
+                    "simplify": {
+                      "title": "ana.base.invariant.int.simplify",
+                      "description": "How much to simplify int domain invariants. Value \"int\" only simplifies definite integers. Without int domain refinement \"all\" might not be maximally precise.",
+                      "type": "string",
+                      "enum": ["none", "int", "all"],
+                      "default": "all"
+                    }
+                  },
+                  "additionalProperties": false
                 }
               },
               "additionalProperties": false
@@ -1561,6 +1575,26 @@
           "description": "Output filename for transformations that output a transformed file.",
           "type":"string",
           "default": "transformed.c"
+        },
+        "assert" : {
+          "title": "trans.assert",
+          "type": "object",
+          "properties": {
+            "function": {
+              "title": "trans.assert.function",
+              "description": "Function to use for assertions in output.",
+              "type": "string",
+              "enum": ["assert", "__goblint_check", "__VERIFIER_assert"],
+              "default": "__VERIFIER_assert"
+            },
+            "wrap-atomic": {
+              "title": "trans.assert.wrap-atomic",
+              "description": "Wrap assertions in __VERIFIER_atomic_begin and __VERIFIER_atomic_end.",
+              "type": "boolean",
+              "default": true
+            }
+          },
+          "additionalProperties": false
         }
       },
       "additionalProperties": false
@@ -2574,7 +2608,8 @@
                   "precondition_loop_invariant",
                   "loop_invariant_certificate",
                   "precondition_loop_invariant_certificate",
-                  "invariant_set"
+                  "invariant_set",
+                  "violation_sequence"
                 ]
               },
               "default": [
diff --git a/src/domain/dune b/src/domain/dune
index 85e69a6246..ce4cdcb1a5 100644
--- a/src/domain/dune
+++ b/src/domain/dune
@@ -14,7 +14,8 @@
   (pps
     ppx_deriving.std
     ppx_deriving_hash
-    ppx_deriving_yojson))
+    ppx_deriving_yojson
+    ppx_deriving_lattice))
  (instrumentation (backend bisect_ppx)))
 
 (documentation)
diff --git a/src/domain/lattice.ml b/src/domain/lattice.ml
index 99322c09d8..f29cb8217d 100644
--- a/src/domain/lattice.ml
+++ b/src/domain/lattice.ml
@@ -277,6 +277,8 @@ struct
   let narrow x y =
     match (x,y) with
     | (`Lifted x, `Lifted y) -> `Lifted (Base.narrow x y)
+    | (_, `Bot) -> `Bot
+    | (`Top, y) -> y
     | _ -> x
 end
 
@@ -337,6 +339,8 @@ struct
     | (`Lifted x, `Lifted y) ->
       (try `Lifted (Base.narrow x y)
        with Uncomparable -> `Bot)
+    | (_, `Bot) -> `Bot
+    | (`Top, y) -> y
     | _ -> x
 end
 
@@ -408,6 +412,8 @@ struct
     match (x,y) with
     | (`Lifted1 x, `Lifted1 y) -> `Lifted1 (Base1.narrow x y)
     | (`Lifted2 x, `Lifted2 y) -> `Lifted2 (Base2.narrow x y)
+    | (_, `Bot) -> `Bot
+    | (`Top, y) -> y
     | _ -> x
 
 end
@@ -416,27 +422,17 @@ module Lift2 = Lift2Conf (Printable.DefaultConf)
 
 module ProdConf (C: Printable.ProdConfiguration) (Base1: S) (Base2: S) =
 struct
-  include Printable.ProdConf (C) (Base1) (Base2)
-
-  let bot () = (Base1.bot (), Base2.bot ())
-  let is_bot (x1,x2) = Base1.is_bot x1 && Base2.is_bot x2
-  let top () = (Base1.top (), Base2.top ())
-  let is_top (x1,x2) = Base1.is_top x1 && Base2.is_top x2
-
-  let leq (x1,x2) (y1,y2) = Base1.leq x1 y1 && Base2.leq x2 y2
+  open struct (* open to avoid leaking P and causing conflicts *)
+    module P = Printable.ProdConf (C) (Base1) (Base2)
+  end
+  type t = Base1.t * Base2.t [@@deriving lattice]
+  include (P: module type of P with type t := t)
 
   let pretty_diff () ((x1,x2:t),(y1,y2:t)): Pretty.doc =
     if Base1.leq x1 y1 then
       Base2.pretty_diff () (x2,y2)
     else
       Base1.pretty_diff () (x1,y1)
-
-  let op_scheme op1 op2 (x1,x2) (y1,y2): t = (op1 x1 y1, op2 x2 y2)
-  let join = op_scheme Base1.join Base2.join
-  let meet = op_scheme Base1.meet Base2.meet
-  let narrow = op_scheme Base1.narrow Base2.narrow
-  let widen = op_scheme Base1.widen Base2.widen
-
 end
 
 
@@ -445,14 +441,11 @@ module ProdSimple = ProdConf (struct let expand_fst = false let expand_snd = fal
 
 module Prod3 (Base1: S) (Base2: S) (Base3: S) =
 struct
-  include Printable.Prod3 (Base1) (Base2) (Base3)
-
-  let bot () = (Base1.bot (), Base2.bot (), Base3.bot ())
-  let is_bot (x1,x2,x3) = Base1.is_bot x1 && Base2.is_bot x2 && Base3.is_bot x3
-  let top () = (Base1.top (), Base2.top (), Base3.top ())
-  let is_top (x1,x2,x3) = Base1.is_top x1 && Base2.is_top x2 && Base3.is_top x3
-
-  let leq (x1,x2,x3) (y1,y2,y3) = Base1.leq x1 y1 && Base2.leq x2 y2 && Base3.leq x3 y3
+  open struct (* open to avoid leaking P and causing conflicts *)
+    module P = Printable.Prod3 (Base1) (Base2) (Base3)
+  end
+  type t = Base1.t * Base2.t * Base3.t [@@deriving lattice]
+  include (P: module type of P with type t := t)
 
   let pretty_diff () ((x1,x2,x3:t),(y1,y2,y3:t)): Pretty.doc =
     if not (Base1.leq x1 y1) then
@@ -461,39 +454,6 @@ struct
       Base2.pretty_diff () (x2,y2)
     else
       Base3.pretty_diff () (x3,y3)
-
-  let op_scheme op1 op2 op3 (x1,x2,x3) (y1,y2,y3): t = (op1 x1 y1, op2 x2 y2, op3 x3 y3)
-  let join = op_scheme Base1.join Base2.join Base3.join
-  let meet = op_scheme Base1.meet Base2.meet Base3.meet
-  let widen = op_scheme Base1.widen Base2.widen Base3.widen
-  let narrow = op_scheme Base1.narrow Base2.narrow Base3.narrow
-end
-
-module Prod4 (Base1: S) (Base2: S) (Base3: S) (Base4: S) =
-struct
-  include Printable.Prod4 (Base1) (Base2) (Base3) (Base4)
-
-  let bot () = (Base1.bot (), Base2.bot (), Base3.bot (), Base4.bot ())
-  let is_bot (x1,x2,x3,x4) = Base1.is_bot x1 && Base2.is_bot x2 && Base3.is_bot x3 && Base4.is_bot x4
-  let top () = (Base1.top (), Base2.top (), Base3.top (), Base4.top ())
-  let is_top (x1,x2,x3,x4) = Base1.is_top x1 && Base2.is_top x2 && Base3.is_top x3 && Base4.is_top x4
-  let leq (x1,x2,x3,x4) (y1,y2,y3,y4) = Base1.leq x1 y1 && Base2.leq x2 y2 && Base3.leq x3 y3 && Base4.leq x4 y4
-
-  let pretty_diff () ((x1,x2,x3,x4:t),(y1,y2,y3,y4:t)): Pretty.doc =
-    if not (Base1.leq x1 y1) then
-      Base1.pretty_diff () (x1,y1)
-    else if not (Base2.leq x2 y2) then
-      Base2.pretty_diff () (x2,y2)
-    else if not (Base3.leq x3 y3) then
-      Base3.pretty_diff () (x3,y3)
-    else
-      Base4.pretty_diff () (x4,y4)
-
-  let op_scheme op1 op2 op3 op4 (x1,x2,x3,x4) (y1,y2,y3,y4): t = (op1 x1 y1, op2 x2 y2, op3 x3 y3, op4 x4 y4)
-  let join = op_scheme Base1.join Base2.join Base3.join Base4.join
-  let meet = op_scheme Base1.meet Base2.meet Base3.meet Base4.meet
-  let widen = op_scheme Base1.widen Base2.widen Base3.widen Base4.widen
-  let narrow = op_scheme Base1.narrow Base2.narrow Base3.narrow Base4.narrow
 end
 
 module LiftBot (Base : S) =
@@ -539,6 +499,7 @@ struct
   let narrow x y =
     match (x,y) with
     | (`Lifted x, `Lifted y) -> `Lifted (Base.narrow x y)
+    | (_, `Bot) -> `Bot
     | _ -> x
 end
 
@@ -580,6 +541,7 @@ struct
   let narrow x y =
     match (x,y) with
     | (`Lifted x, `Lifted y) -> `Lifted (Base.narrow x y)
+    | (`Top, y) -> y
     | _ -> x
 
   let pretty_diff () (x,y) =
diff --git a/src/domain/setDomain.ml b/src/domain/setDomain.ml
index 9b545a78ee..c552363f3d 100644
--- a/src/domain/setDomain.ml
+++ b/src/domain/setDomain.ml
@@ -184,7 +184,7 @@ struct
     end
     )
 
-  let hash x = fold (fun x y -> y + Base.hash x) x 0
+  let hash x = fold (fun x y -> 13 * y + Base.hash x) x 0
 
   let relift x = map Base.relift x
 
diff --git a/src/domains/access.ml b/src/domains/access.ml
index c35fb3a16d..f7ce68a18b 100644
--- a/src/domains/access.ml
+++ b/src/domains/access.ml
@@ -1,6 +1,5 @@
 (** Memory accesses and their manipulation. *)
 
-open Batteries
 open GoblintCil
 open Pretty
 open GobConfig
@@ -12,7 +11,7 @@ module M = Messages
 
 let is_ignorable_comp_name = function
   | "__pthread_mutex_s" | "__pthread_rwlock_arch_t" | "__jmp_buf_tag" | "_pthread_cleanup_buffer" | "__pthread_cleanup_frame" | "__cancel_jmp_buf_tag" | "_IO_FILE" -> true
-  | cname when String.starts_with_stdlib ~prefix:"__anon" cname ->
+  | cname when String.starts_with ~prefix:"__anon" cname ->
     begin match Cilfacade.split_anoncomp_name cname with
       | (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 *)
@@ -385,7 +384,7 @@ and distribute_access_exp f = function
 
 and distribute_access_type f = function
   | TArray (et, len, _) ->
-    Option.may (distribute_access_exp f) len;
+    Option.iter (distribute_access_exp f) len;
     distribute_access_type f et
 
   | TVoid _
@@ -434,7 +433,7 @@ struct
   include SetDomain.Make (A)
 
   let max_conf accs =
-    accs |> elements |> List.map (fun {A.conf; _} -> conf) |> (List.max ~cmp:Int.compare)
+    accs |> elements |> List.map (fun {A.conf; _} -> conf) |> (BatList.max ~cmp:Int.compare)
 end
 
 
@@ -583,7 +582,7 @@ let incr_summary ~safe ~vulnerable ~unsafe grouped_accs =
     |> List.filter_map race_conf
     |> (function
         | [] -> None
-        | confs -> Some (List.max confs)
+        | confs -> Some (BatList.max confs)
       )
   in
   match safety with
diff --git a/src/domains/queries.ml b/src/domains/queries.ml
index 1ceb91ef1d..5fbb244874 100644
--- a/src/domains/queries.ml
+++ b/src/domains/queries.ml
@@ -49,8 +49,8 @@ end
 
 (* Helper definitions for deriving complex parts of Any.compare below. *)
 type maybepublic = {global: CilType.Varinfo.t; write: bool; protection: Protection.t} [@@deriving ord, hash]
-type maybepublicwithout = {global: CilType.Varinfo.t; write: bool; without_mutex: PreValueDomain.Addr.t; protection: Protection.t} [@@deriving ord, hash]
-type mustbeprotectedby = {mutex: PreValueDomain.Addr.t; global: CilType.Varinfo.t; write: bool; protection: Protection.t} [@@deriving ord, hash]
+type maybepublicwithout = {global: CilType.Varinfo.t; write: bool; without_mutex: LockDomain.MustLock.t; protection: Protection.t} [@@deriving ord, hash]
+type mustbeprotectedby = {mutex: LockDomain.MustLock.t; global: CilType.Varinfo.t; write: bool; protection: Protection.t} [@@deriving ord, hash]
 type mustprotectedvars = {mutex: LockDomain.MustLock.t; write: bool} [@@deriving ord, hash]
 type access =
   | Memory of {exp: CilType.Exp.t; var_opt: CilType.Varinfo.t option; kind: AccessKind.t} (** Memory location access (race). *)
diff --git a/src/dune b/src/dune
index 5265821b5a..a307a237ae 100644
--- a/src/dune
+++ b/src/dune
@@ -71,7 +71,7 @@
   (flags :standard -open Goblint_std -open Goblint_logs)
   (ocamlopt_flags :standard -no-float-const-prop)
   (preprocess
-    (pps ppx_deriving.std ppx_deriving_hash ppx_deriving_yojson ppx_blob))
+    (pps ppx_deriving.std ppx_deriving_hash ppx_deriving_yojson ppx_blob ppx_deriving_printable ppx_deriving_lattice))
   (instrumentation (backend bisect_ppx))
 )
 
diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
index 1ea01c99fb..717507802f 100644
--- a/src/framework/analyses.ml
+++ b/src/framework/analyses.ml
@@ -14,8 +14,7 @@ type fundecs = fundec list * fundec list * fundec list
 
 module Var =
 struct
-  type t = Node.t [@@deriving eq, ord, hash]
-  let relift = Node.relift
+  type t = Node.t [@@deriving eq, ord, hash, relift]
 
   let printXml f n =
     let l = Node.location n in
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index e0e36801ed..7df4167acd 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -713,11 +713,13 @@ struct
 
   let tf_assign var edge prev_node lv e getl sidel getg sideg d =
     let ctx, r, spawns = common_ctx var edge prev_node d getl sidel getg sideg in
-    common_join ctx (S.assign ctx lv e) !r !spawns
+    let d = S.assign ctx lv e in (* Force transfer function to be evaluated before dereferencing in common_join argument. *)
+    common_join ctx d !r !spawns
 
   let tf_vdecl var edge prev_node v getl sidel getg sideg d =
     let ctx, r, spawns = common_ctx var edge prev_node d getl sidel getg sideg in
-    common_join ctx (S.vdecl ctx v) !r !spawns
+    let d = S.vdecl ctx v in (* Force transfer function to be evaluated before dereferencing in common_join argument. *)
+    common_join ctx d !r !spawns
 
   let normal_return r fd ctx sideg =
     let spawning_return = S.return ctx r fd in
@@ -732,7 +734,7 @@ struct
 
   let tf_ret var edge prev_node ret fd getl sidel getg sideg d =
     let ctx, r, spawns = common_ctx var edge prev_node d getl sidel getg sideg in
-    let d =
+    let d = (* Force transfer function to be evaluated before dereferencing in common_join argument. *)
       if (CilType.Fundec.equal fd MyCFG.dummy_func ||
           List.mem fd.svar.vname (get_string_list "mainfun")) &&
          get_bool "kernel"
@@ -747,11 +749,13 @@ struct
     let c: unit -> S.C.t = snd var |> Obj.obj in
     side_context sideg fd (c ());
     let ctx, r, spawns = common_ctx var edge prev_node d getl sidel getg sideg in
-    common_join ctx (S.body ctx fd) !r !spawns
+    let d = S.body ctx fd in (* Force transfer function to be evaluated before dereferencing in common_join argument. *)
+    common_join ctx d !r !spawns
 
   let tf_test var edge prev_node e tv getl sidel getg sideg d =
     let ctx, r, spawns = common_ctx var edge prev_node d getl sidel getg sideg in
-    common_join ctx (S.branch ctx e tv) !r !spawns
+    let d = S.branch ctx e tv in (* Force transfer function to be evaluated before dereferencing in common_join argument. *)
+    common_join ctx d !r !spawns
 
   let tf_normal_call ctx lv e (f:fundec) args getl sidel getg sideg =
     let combine (cd, fc, fd) =
@@ -870,11 +874,13 @@ struct
 
   let tf_asm var edge prev_node getl sidel getg sideg d =
     let ctx, r, spawns = common_ctx var edge prev_node d getl sidel getg sideg in
-    common_join ctx (S.asm ctx) !r !spawns
+    let d = S.asm ctx in (* Force transfer function to be evaluated before dereferencing in common_join argument. *)
+    common_join ctx d !r !spawns
 
   let tf_skip var edge prev_node getl sidel getg sideg d =
     let ctx, r, spawns = common_ctx var edge prev_node d getl sidel getg sideg in
-    common_join ctx (S.skip ctx) !r !spawns
+    let d = S.skip ctx in (* Force transfer function to be evaluated before dereferencing in common_join argument. *)
+    common_join ctx d !r !spawns
 
   let tf var getl sidel getg sideg prev_node edge d =
     begin match edge with
diff --git a/src/framework/control.ml b/src/framework/control.ml
index 05fad90caf..5e92282210 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -357,6 +357,7 @@ struct
     (* real beginning of the [analyze] function *)
     if get_bool "ana.sv-comp.enabled" then
       Witness.init (module FileCfg); (* TODO: move this out of analyze_loop *)
+    YamlWitness.init ();
 
     AnalysisState.global_initialization := true;
     GobConfig.earlyglobs := get_bool "exp.earlyglobs";
@@ -789,15 +790,19 @@ struct
     );
 
     (* Before SV-COMP, so result can depend on YAML witness validation. *)
-    if get_string "witness.yaml.validate" <> "" then (
-      let module YWitness = YamlWitness.Validator (R) in
-      YWitness.validate ()
-    );
+    let yaml_validate_result =
+      if get_string "witness.yaml.validate" <> "" then (
+        let module YWitness = YamlWitness.Validator (R) in
+        Some (YWitness.validate ())
+      )
+      else
+        None
+    in
 
     if get_bool "ana.sv-comp.enabled" then (
       (* SV-COMP and witness generation *)
       let module WResult = Witness.Result (R) in
-      WResult.write entrystates
+      WResult.write yaml_validate_result entrystates
     );
 
     if get_bool "witness.yaml.enabled" then (
diff --git a/src/goblint.ml b/src/goblint.ml
index a687badb8e..52b9bbdfc0 100644
--- a/src/goblint.ml
+++ b/src/goblint.ml
@@ -83,6 +83,11 @@ let main () =
     Logs.error "%s" (MessageUtil.colorize ~fd:Unix.stderr ("{RED}Analysis was aborted because it reached the set timeout of " ^ get_string "dbg.timeout" ^ " or was signalled SIGPROF!"));
     Goblint_timing.teardown_tef ();
     exit 124
+  | Svcomp.Error msg ->
+    do_stats ();
+    Witness.print_svcomp_result ("ERROR (" ^ msg ^ ")");
+    Goblint_timing.teardown_tef ();
+    exit 1
 
 (* We do this since the evaluation order of top-level bindings is not defined, but we want `main` to run after all the other side-effects (e.g. registering analyses/solvers) have happened. *)
 let () = at_exit main
diff --git a/src/incremental/compareAST.ml b/src/incremental/compareAST.ml
index f3de153658..5ac7a90706 100644
--- a/src/incremental/compareAST.ml
+++ b/src/incremental/compareAST.ml
@@ -73,7 +73,7 @@ let forward_list_equal ?(propF = (&&>>)) f l1 l2 ~(rename_mapping: rename_mappin
 let compare_name (a: string) (b: string) =
   let anon_struct = "__anonstruct_" in
   let anon_union = "__anonunion_" in
-  if a = b then true else BatString.(starts_with a anon_struct && starts_with b anon_struct || starts_with a anon_union && starts_with b anon_union)
+  if a = b then true else String.(starts_with a ~prefix:anon_struct && starts_with b ~prefix:anon_struct || starts_with a ~prefix:anon_union && starts_with b ~prefix:anon_union)
 
 let rec eq_constant ~(rename_mapping: rename_mapping) ~(acc: (typ * typ) list) (a: constant) (b: constant) : bool * rename_mapping =
   match a, b with
@@ -178,8 +178,8 @@ and eq_typ_acc ?(fun_parameter_name_comparison_enabled: bool = true) (a: typ) (b
   if Messages.tracing then Messages.traceu "compareast" "eq_typ_acc %a vs %a" d_type a d_type b;
   (r, updated_rename_mapping)
 
-and eq_eitems (a: string * exp * location) (b: string * exp * location) ~(rename_mapping: rename_mapping) ~(acc: (typ * typ) list) = match a, b with
-    (name1, exp1, _l1), (name2, exp2, _l2) -> (name1 = name2, rename_mapping) &&>> eq_exp exp1 exp2 ~acc
+and eq_eitems (a: string * attributes * exp * location) (b: string * attributes * exp * location) ~(rename_mapping: rename_mapping) ~(acc: (typ * typ) list) = match a, b with
+    (name1, attr1, exp1, _l1), (name2, attr2, exp2, _l2) -> (name1 = name2, rename_mapping) &&>> forward_list_equal (eq_attribute ~acc) attr1 attr2 &&>> eq_exp exp1 exp2 ~acc
 (* Ignore location *)
 
 and eq_enuminfo (a: enuminfo) (b: enuminfo) ~(rename_mapping: rename_mapping) ~(acc: (typ * typ) list) =
@@ -210,6 +210,7 @@ and eq_attrparam (a: attrparam) (b: attrparam) ~(rename_mapping: rename_mapping)
   | AAddrOf attrparam1, AAddrOf attrparam2 -> eq_attrparam attrparam1 attrparam2 ~rename_mapping ~acc
   | AIndex (left1, right1), AIndex (left2, right2) -> eq_attrparam left1 left2 ~rename_mapping ~acc &&>> eq_attrparam right1 right2 ~acc
   | AQuestion (left1, middle1, right1), AQuestion (left2, middle2, right2) -> eq_attrparam left1 left2 ~rename_mapping ~acc &&>> eq_attrparam middle1 middle2 ~acc &&>> eq_attrparam right1 right2 ~acc
+  | AAssign (left1, right1), AAssign (left2, right2) -> eq_attrparam left1 left2 ~rename_mapping ~acc &&>> eq_attrparam right1 right2 ~acc
   | a, b -> a = b, rename_mapping
 
 and eq_attribute (a: attribute) (b: attribute) ~(acc: (typ * typ) list) ~(rename_mapping: rename_mapping) = match a, b with
diff --git a/src/incremental/makefileUtil.ml b/src/incremental/makefileUtil.ml
index 9a17122f5e..33cd8f64c9 100644
--- a/src/incremental/makefileUtil.ml
+++ b/src/incremental/makefileUtil.ml
@@ -39,7 +39,7 @@ let find_file_by_suffix (dir: Fpath.t) (file_name_suffix: string) =
     | (h::t) -> let f = Fpath.to_string h in
       if Sys.file_exists f && Sys.is_directory f
       then (Queue.add h dirs; search dir t)
-      else if Batteries.String.ends_with (Fpath.filename h) file_name_suffix then h else search dir t
+      else if String.ends_with (Fpath.filename h) ~suffix:file_name_suffix then h else search dir t
     | [] ->
       if Queue.is_empty dirs then failwith ("find_file_by_suffix found no files with suffix "^file_name_suffix^" in "^ Fpath.to_string dir)
       else let d = Queue.take dirs in search d (list_files d)
diff --git a/src/ppx/dune b/src/ppx/dune
new file mode 100644
index 0000000000..ff757cb8ca
--- /dev/null
+++ b/src/ppx/dune
@@ -0,0 +1 @@
+(include_subdirs no)
diff --git a/src/ppx/lattice/dune b/src/ppx/lattice/dune
new file mode 100644
index 0000000000..862298be13
--- /dev/null
+++ b/src/ppx/lattice/dune
@@ -0,0 +1,5 @@
+(library
+ (name ppx_deriving_lattice)
+ (kind ppx_deriver)
+ (libraries ppxlib ppx_easy_deriving)
+ (preprocess (pps ppxlib.metaquot)))
diff --git a/src/ppx/lattice/ppx_deriving_lattice.ml b/src/ppx/lattice/ppx_deriving_lattice.ml
new file mode 100644
index 0000000000..e78e88644a
--- /dev/null
+++ b/src/ppx/lattice/ppx_deriving_lattice.ml
@@ -0,0 +1,97 @@
+open Ppxlib
+open Ppx_easy_deriving
+
+module LeqArg: Product.Reduce.Conjunctive.S =
+struct
+  let name = "leq"
+end
+
+module LeqDeriver = Deriver.Make (Product.Reduce2.Make (Product.Reduce.Conjunctive.Make (LeqArg)))
+let leq_deriving = LeqDeriver.register ()
+
+
+module JoinArg: Product.Map2.S =
+struct
+  let name = "join"
+end
+
+module JoinDeriver = Deriver.Make (Product.Map2.Make (JoinArg))
+let join_deriving = JoinDeriver.register ()
+
+
+module MeetArg: Product.Map2.S =
+struct
+  let name = "meet"
+end
+
+module MeetDeriver = Deriver.Make (Product.Map2.Make (MeetArg))
+let meet_deriving = MeetDeriver.register ()
+
+
+module WidenArg: Product.Map2.S =
+struct
+  let name = "widen"
+end
+
+module WidenDeriver = Deriver.Make (Product.Map2.Make (WidenArg))
+let widen_deriving = WidenDeriver.register ()
+
+
+module NarrowArg: Product.Map2.S =
+struct
+  let name = "narrow"
+end
+
+module NarrowDeriver = Deriver.Make (Product.Map2.Make (NarrowArg))
+let narrow_deriving = NarrowDeriver.register ()
+
+
+module BotArg: Product.Create.S =
+struct
+  let name = "bot"
+  let typ ~loc _ = [%type: unit]
+end
+
+module BotDeriver = Deriver.Make (Product.Create.Make (BotArg))
+let bot_deriving = BotDeriver.register ()
+
+
+module IsBotArg: Product.Reduce.Conjunctive.S =
+struct
+  let name = "is_bot"
+end
+
+module IsBotDeriver = Deriver.Make (Product.Reduce1.Make (Product.Reduce.Conjunctive.Make (IsBotArg)))
+let is_bot_deriving = IsBotDeriver.register ()
+
+
+module TopArg: Product.Create.S =
+struct
+  let name = "top"
+  let typ ~loc _ = [%type: unit]
+end
+
+module TopDeriver = Deriver.Make (Product.Create.Make (TopArg))
+let top_deriving = TopDeriver.register ()
+
+
+module IsTopArg: Product.Reduce.Conjunctive.S =
+struct
+  let name = "is_top"
+end
+
+module IsTopDeriver = Deriver.Make (Product.Reduce1.Make (Product.Reduce.Conjunctive.Make (IsTopArg)))
+let is_top_deriving = IsTopDeriver.register ()
+
+
+let _ = Ppxlib.Deriving.add_alias "lattice" [
+    leq_deriving;
+    join_deriving;
+    meet_deriving;
+    widen_deriving;
+    narrow_deriving;
+    bot_deriving;
+    is_bot_deriving;
+    top_deriving;
+    is_top_deriving;
+  ]
diff --git a/src/ppx/printable/dune b/src/ppx/printable/dune
new file mode 100644
index 0000000000..8e08232de6
--- /dev/null
+++ b/src/ppx/printable/dune
@@ -0,0 +1,5 @@
+(library
+ (name ppx_deriving_printable)
+ (kind ppx_deriver)
+ (libraries ppxlib ppx_easy_deriving)
+ (preprocess (pps ppxlib.metaquot)))
diff --git a/src/ppx/printable/ppx_deriving_printable.ml b/src/ppx/printable/ppx_deriving_printable.ml
new file mode 100644
index 0000000000..75fd5044fe
--- /dev/null
+++ b/src/ppx/printable/ppx_deriving_printable.ml
@@ -0,0 +1,16 @@
+open Ppx_easy_deriving
+
+module ReliftArg: Product.Map1.S =
+struct
+  let name = "relift"
+end
+
+(* TODO: Map1 should also do variants *)
+module ReliftDeriver = Deriver.Make (Product.Map1.Make (ReliftArg))
+let relift_deriving = ReliftDeriver.register ()
+
+
+(* TODO: needs https://github.com/ocaml-ppx/ppxlib/pull/124 to include eq, ord, hash *)
+(* let _ = Ppxlib.Deriving.add_alias "printable" [
+       relift_deriving;
+     ] *)
diff --git a/src/transform/evalAssert.ml b/src/transform/evalAssert.ml
index eab06222ef..8f858d09df 100644
--- a/src/transform/evalAssert.ml
+++ b/src/transform/evalAssert.ml
@@ -22,12 +22,8 @@ open Formatcil
         will be removed and they will fail on the next iteration
 *)
 
-module EvalAssert = struct
-  (* should asserts be surrounded by __VERIFIER_atomic_{begin,end}? *)
-  let surroundByAtomic = true
-
-  (* Cannot use Cilfacade.name_fundecs as assert() is external and has no fundec *)
-  let ass = makeVarinfo true "__VERIFIER_assert" (TVoid [])
+module EvalAssert =
+struct
   let atomicBegin = makeVarinfo true "__VERIFIER_atomic_begin" (TVoid [])
   let atomicEnd = makeVarinfo true "__VERIFIER_atomic_end" (TVoid [])
 
@@ -39,10 +35,16 @@ module EvalAssert = struct
     val emit_after_lock = GobConfig.get_bool "witness.invariant.after-lock"
     val emit_other = GobConfig.get_bool "witness.invariant.other"
 
+    (* Cannot use Cilfacade.name_fundecs as assert() is external and has no fundec *)
+    val assert_function = makeVarinfo true (GobConfig.get_string "trans.assert.function") (TVoid [])
+    (* should asserts be surrounded by __VERIFIER_atomic_{begin,end}? *)
+    val surroundByAtomic = GobConfig.get_bool "trans.assert.wrap-atomic"
+
     method! vstmt s =
       let is_lock exp args =
         match exp with
         | Lval(Var v,_) when LibraryFunctions.is_special v ->
+          Goblint_backtrace.wrap_val ~mark:(Cilfacade.FunVarinfo v) @@ fun () ->
           let desc = LibraryFunctions.find v in
           (match desc.special args with
            | Lock _ -> true
@@ -59,7 +61,7 @@ module EvalAssert = struct
         match (ask ~node loc).f (Queries.Invariant context) with
         | `Lifted e ->
           let es = WitnessUtil.InvariantExp.process_exp e in
-          let asserts = List.map (fun e -> cInstr ("%v:assert (%e:exp);") loc [("assert", Fv ass); ("exp", Fe e)]) es in
+          let asserts = List.map (fun e -> cInstr ("%v:assert (%e:exp);") loc [("assert", Fv assert_function); ("exp", Fe e)]) es in
           if surroundByAtomic then
             let abegin = (cInstr ("%v:__VERIFIER_atomic_begin();") loc [("__VERIFIER_atomic_begin", Fv atomicBegin)]) in
             let aend = (cInstr ("%v:__VERIFIER_atomic_end();") loc [("__VERIFIER_atomic_end", Fv atomicEnd)]) in
diff --git a/src/util/backtrace/goblint_backtrace.ml b/src/util/backtrace/goblint_backtrace.ml
index 29198c27ea..513753bddb 100644
--- a/src/util/backtrace/goblint_backtrace.ml
+++ b/src/util/backtrace/goblint_backtrace.ml
@@ -36,6 +36,15 @@ let protect ~(mark: unit -> mark) ~(finally: unit -> unit) work =
     add_mark work_exn (mark ());
     Printexc.raise_with_backtrace work_exn work_bt
 
+(* Copied & modified from protect. *)
+let wrap_val ~(mark:mark) work =
+  try
+    work ()
+  with work_exn ->
+    let work_bt = Printexc.get_raw_backtrace () in
+    add_mark work_exn mark;
+    Printexc.raise_with_backtrace work_exn work_bt
+
 
 let mark_printers: (mark -> string option) list ref = ref []
 
diff --git a/src/util/backtrace/goblint_backtrace.mli b/src/util/backtrace/goblint_backtrace.mli
index e2b6ed2913..e53bfd826a 100644
--- a/src/util/backtrace/goblint_backtrace.mli
+++ b/src/util/backtrace/goblint_backtrace.mli
@@ -24,6 +24,9 @@ val add_mark: exn -> mark -> unit
 val protect: mark:(unit -> mark) -> finally:(unit -> unit) -> (unit -> 'a) -> 'a
 (** {!Fun.protect} with additional [~mark] addition to all exceptions. *)
 
+val wrap_val: mark:mark -> (unit -> 'a) -> 'a
+(** {!protect} with [~mark] value and without [~finally]. *)
+
 val print_marktrace: out_channel -> exn -> unit
 (** Print trace of marks of an exception.
 
diff --git a/src/util/library/libraryFunctions.ml b/src/util/library/libraryFunctions.ml
index 4e678c926e..25a90da2d3 100644
--- a/src/util/library/libraryFunctions.ml
+++ b/src/util/library/libraryFunctions.ml
@@ -712,7 +712,7 @@ let linux_userspace_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("__errno", unknown []);
     ("__errno_location", unknown []);
     ("__h_errno_location", unknown []);
-    ("__printf_chk", unknown [drop "flag" []; drop "format" [r]]);
+    ("__printf_chk", unknown (drop "flag" [] :: drop "format" [r] :: VarArgs (drop' [r])));
     ("__fprintf_chk", unknown (drop "stream" [r_deep; w_deep] :: drop "flag" [] :: drop "format" [r] :: VarArgs (drop' [r])));
     ("__vfprintf_chk", unknown [drop "stream" [r_deep; w_deep]; drop "flag" []; drop "format" [r]; drop "ap" [r_deep]]);
     ("sysinfo", unknown [drop "info" [w_deep]]);
@@ -1246,7 +1246,7 @@ let libraries =
       descs_tbl
     ) libraries
 
-let all_library_descs: (string, LibraryDesc.t) Hashtbl.t =
+let _all_library_descs: (string, LibraryDesc.t) Hashtbl.t =
   Hashtbl.fold (fun _ descs_tbl acc ->
       Hashtbl.merge (fun name desc1 desc2 ->
           match desc1, desc2 with
diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml
index 47c95da8e8..b63645ab17 100644
--- a/src/util/loopUnrolling.ml
+++ b/src/util/loopUnrolling.ml
@@ -306,6 +306,7 @@ class loopUnrollingCallVisitor = object
 
   method! vinst = function
     | Call (_,Lval ((Var info), NoOffset),args,_,_) when LibraryFunctions.is_special info -> (
+        Goblint_backtrace.wrap_val ~mark:(Cilfacade.FunVarinfo info) @@ fun () ->
         let desc = LibraryFunctions.find info in
         match desc.special args with
         | Malloc _
diff --git a/src/vendor/ppx_blob/LICENSE.txt b/src/vendor/ppx_blob/LICENSE.txt
deleted file mode 100644
index 00d2e135a7..0000000000
--- a/src/vendor/ppx_blob/LICENSE.txt
+++ /dev/null
@@ -1,24 +0,0 @@
-This is free and unencumbered software released into the public domain.
-
-Anyone is free to copy, modify, publish, use, compile, sell, or
-distribute this software, either in source code form or as a compiled
-binary, for any purpose, commercial or non-commercial, and by any
-means.
-
-In jurisdictions that recognize copyright laws, the author or authors
-of this software dedicate any and all copyright interest in the
-software to the public domain. We make this dedication for the benefit
-of the public at large and to the detriment of our heirs and
-successors. We intend this dedication to be an overt act of
-relinquishment in perpetuity of all present and future rights to this
-software under copyright law.
-
-THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
-EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
-MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
-IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY CLAIM, DAMAGES OR
-OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
-ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
-OTHER DEALINGS IN THE SOFTWARE.
-
-For more information, please refer to <http://unlicense.org/>
\ No newline at end of file
diff --git a/src/vendor/ppx_blob/README.md b/src/vendor/ppx_blob/README.md
deleted file mode 100644
index fdd7448a32..0000000000
--- a/src/vendor/ppx_blob/README.md
+++ /dev/null
@@ -1 +0,0 @@
-ppx_blob fix for `(lang dune 3.0)` vendored from <https://github.com/johnwhitington/ppx_blob/pull/24>.
diff --git a/src/vendor/ppx_blob/src/dune b/src/vendor/ppx_blob/src/dune
deleted file mode 100644
index 112b1d07c0..0000000000
--- a/src/vendor/ppx_blob/src/dune
+++ /dev/null
@@ -1,5 +0,0 @@
-(library
- (name ppx_blob)
- ; (public_name ppx_blob)
- (kind ppx_rewriter)
- (libraries ppxlib))
\ No newline at end of file
diff --git a/src/vendor/ppx_blob/src/ppx_blob.ml b/src/vendor/ppx_blob/src/ppx_blob.ml
deleted file mode 100644
index 622a99f8f6..0000000000
--- a/src/vendor/ppx_blob/src/ppx_blob.ml
+++ /dev/null
@@ -1,35 +0,0 @@
-open Ppxlib
-
-let location_errorf ~loc =
-  Format.ksprintf (fun err ->
-      raise (Ocaml_common.Location.Error (Ocaml_common.Location.error ~loc err))
-    )
-
-let find_file_path ~loc file_name =
-  let dirname = loc.Ocaml_common.Location.loc_start.pos_fname |> Filename.dirname in
-  let relative_path = Filename.concat dirname file_name in
-  List.find Sys.file_exists [relative_path; file_name]
-
-let get_blob ~loc file_name =
-  try
-    let file_path = find_file_path ~loc file_name in
-    let c = open_in_bin file_path in
-    let s = String.init (in_channel_length c) (fun _ -> input_char c) in
-    close_in c;
-    s
-  with _ ->
-    location_errorf ~loc "[%%blob] could not find or load file %s" file_name
-
-let expand ~ctxt file_name =
-  let loc = Expansion_context.Extension.extension_point_loc ctxt in
-  Ast_builder.Default.estring ~loc (get_blob ~loc file_name)
-
-let extension =
-  Extension.V3.declare "blob" Extension.Context.expression
-    Ast_pattern.(single_expr_payload (estring __))
-    expand
-
-let rule = Ppxlib.Context_free.Rule.extension extension
-
-;;
-Driver.register_transformation ~rules:[rule] "ppx_blob"
\ No newline at end of file
diff --git a/src/vendor/ppx_easy_deriving/LICENSE.md b/src/vendor/ppx_easy_deriving/LICENSE.md
new file mode 100644
index 0000000000..ae6337b11b
--- /dev/null
+++ b/src/vendor/ppx_easy_deriving/LICENSE.md
@@ -0,0 +1,21 @@
+MIT License
+
+Copyright (c) 2023 Simmo Saan
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.
diff --git a/src/vendor/ppx_easy_deriving/README.md b/src/vendor/ppx_easy_deriving/README.md
new file mode 100644
index 0000000000..99a5e7e140
--- /dev/null
+++ b/src/vendor/ppx_easy_deriving/README.md
@@ -0,0 +1,4 @@
+# ppx_easy_deriving
+
+Goblint vendors a subset of the unreleased [ppx_easy_deriving](https://github.com/sim642/ppx_easy_deriving) library.
+It only includes products, excluding simples and variants.
diff --git a/src/vendor/ppx_easy_deriving/deriver.ml b/src/vendor/ppx_easy_deriving/deriver.ml
new file mode 100644
index 0000000000..533a77959c
--- /dev/null
+++ b/src/vendor/ppx_easy_deriving/deriver.ml
@@ -0,0 +1,100 @@
+open Ppxlib
+open Ast_builder.Default
+
+include Deriver_intf
+
+module Make (Arg: Intf.S): S =
+struct
+  let attr = Attribute.declare (Printf.sprintf "deriving.%s.%s" Arg.name Arg.name) Attribute.Context.core_type Ast_pattern.(single_expr_payload __) (fun expr -> expr)
+
+  let unit ~loc = Arg.tuple ~loc []
+
+  let rec expr ~loc ~quoter ct =
+    match Attribute.get attr ct with
+    | Some expr ->
+      Expansion_helpers.Quoter.quote quoter expr
+    | None ->
+      match ct with
+      | [%type: unit] ->
+        unit ~loc
+      | {ptyp_desc = Ptyp_constr ({txt = lid; loc}, args); _} ->
+        let ident = pexp_ident ~loc {loc; txt = Expansion_helpers.mangle_lid (Prefix Arg.name) lid} in
+        let ident = Expansion_helpers.Quoter.quote quoter ident in
+        let apply_args = List.map (fun ct ->
+            (Nolabel, expr ~loc ~quoter ct)
+          ) args
+        in
+        pexp_apply ~loc ident apply_args
+      | {ptyp_desc = Ptyp_tuple elems; _} ->
+        expr_tuple ~loc ~quoter elems
+      | {ptyp_desc = Ptyp_var name; _} ->
+        evar ~loc ("poly_" ^ name)
+      | _ ->
+        pexp_extension ~loc (Location.error_extensionf ~loc "unsupported core type")
+
+  and expr_record ~loc ~quoter (lds: label_declaration list) =
+    let les = List.map (fun {pld_name = {txt = label; _}; pld_type; _} ->
+        (Lident label, expr ~loc ~quoter pld_type)
+      ) lds
+    in
+    Arg.record ~loc les
+
+  and expr_tuple ~loc ~quoter elems =
+    let es = List.map (expr ~loc ~quoter) elems in
+    Arg.tuple ~loc es
+
+  let expr_declaration ~loc ~quoter = function
+    | {ptype_kind = Ptype_abstract; ptype_manifest = Some ct; _} ->
+      expr ~loc ~quoter ct
+    | {ptype_kind = Ptype_abstract; _} ->
+      pexp_extension ~loc (Location.error_extensionf ~loc "unsupported abstract type")
+    | {ptype_kind = Ptype_variant constrs; _} ->
+      pexp_extension ~loc (Location.error_extensionf ~loc "unsupported variant type")
+    | {ptype_kind = Ptype_open; _} ->
+      pexp_extension ~loc (Location.error_extensionf ~loc "unsupported open type")
+    | {ptype_kind = Ptype_record fields; _} ->
+      expr_record ~loc ~quoter fields
+
+  let typ ~loc td =
+    let ct = Ppx_deriving.core_type_of_type_decl td in
+    Ppx_deriving.poly_arrow_of_type_decl
+      (Arg.typ ~loc)
+      td
+      (Arg.typ ~loc ct)
+
+  let generate_impl ~ctxt (_rec_flag, type_declarations) =
+    let loc = Expansion_context.Deriver.derived_item_loc ctxt in
+    let vbs = List.map (fun td ->
+        let quoter = Expansion_helpers.Quoter.create () in
+        let expr = expr_declaration ~loc ~quoter td in
+        let expr = Expansion_helpers.Quoter.sanitize quoter expr in
+        let expr = Ppx_deriving.poly_fun_of_type_decl td expr in
+        let ct = typ ~loc td in
+        let pat = ppat_var ~loc {loc; txt = Expansion_helpers.mangle_type_decl (Prefix Arg.name) td} in
+        let pat = ppat_constraint ~loc pat ct in
+        Ast_helper.Vb.mk ~loc ~attrs:[Ppx_deriving.attr_warning [%expr "-39"]] pat expr
+      ) type_declarations
+    in
+    [Ast_helper.Str.value ~loc Recursive vbs]
+
+  let generate_intf ~ctxt (_rec_flag, type_declarations) =
+    let loc = Expansion_context.Deriver.derived_item_loc ctxt in
+    List.map (fun td ->
+        let ct = typ ~loc td in
+        let val_ = Ast_helper.Val.mk ~loc {loc; txt = Expansion_helpers.mangle_type_decl (Prefix Arg.name) td} ct in
+        Ast_helper.Sig.value ~loc val_
+      ) type_declarations
+
+  let impl_generator = Deriving.Generator.V2.make_noarg generate_impl
+  let intf_generator = Deriving.Generator.V2.make_noarg generate_intf
+  let extension ~loc ~path:_ ct =
+    let quoter = Expansion_helpers.Quoter.create () in
+    let expr = expr ~loc ~quoter ct in
+    Expansion_helpers.Quoter.sanitize quoter expr
+
+  let register () =
+    Deriving.add Arg.name
+      ~sig_type_decl:intf_generator
+      ~str_type_decl:impl_generator
+      ~extension
+end
diff --git a/src/vendor/ppx_easy_deriving/deriver.mli b/src/vendor/ppx_easy_deriving/deriver.mli
new file mode 100644
index 0000000000..a8238f6f6f
--- /dev/null
+++ b/src/vendor/ppx_easy_deriving/deriver.mli
@@ -0,0 +1,3 @@
+(** Registerable deriver. *)
+
+include Deriver_intf.Deriver (** @inline *)
diff --git a/src/vendor/ppx_easy_deriving/deriver_intf.ml b/src/vendor/ppx_easy_deriving/deriver_intf.ml
new file mode 100644
index 0000000000..565a6aef38
--- /dev/null
+++ b/src/vendor/ppx_easy_deriving/deriver_intf.ml
@@ -0,0 +1,13 @@
+module type S =
+sig
+  val register: unit -> Ppxlib.Deriving.t
+  (** Register deriver with ppxlb. *)
+end
+
+module type Deriver =
+sig
+  module type S = S
+
+  module Make (_: Intf.S): S
+  (** Make registerable deriver. *)
+end
diff --git a/src/vendor/ppx_easy_deriving/dune b/src/vendor/ppx_easy_deriving/dune
new file mode 100644
index 0000000000..7d50a56e43
--- /dev/null
+++ b/src/vendor/ppx_easy_deriving/dune
@@ -0,0 +1,4 @@
+(library
+ (name ppx_easy_deriving)
+ (libraries ppxlib ppx_deriving.api)
+ (preprocess (pps ppxlib.metaquot)))
diff --git a/src/vendor/ppx_easy_deriving/intf.ml b/src/vendor/ppx_easy_deriving/intf.ml
new file mode 100644
index 0000000000..b30c7c36a0
--- /dev/null
+++ b/src/vendor/ppx_easy_deriving/intf.ml
@@ -0,0 +1,64 @@
+(** Main interfaces. *)
+
+open Ppxlib
+
+(** Deriver name interface. *)
+module type Name =
+sig
+  val name: string
+  (** Deriver name.
+
+      For example, with the name "equal":
+      + Use [[@@deriving equal]] after a type definition.
+      + The derived value/function is [val equal: ...] (if the type is named [t]) or [val equal_ty: ...] (otherwise if the type is named [ty]).
+      + Use [[@equal ...]] after a type expression to override the underlying value/function used for it.
+      + Use [[%equal: ty]] as an expression for the value/function of type [ty]. *)
+end
+
+(** Deriver base interface. *)
+module type Base =
+sig
+  include Name
+  val typ: loc:location -> core_type -> core_type
+  (** Derived value/function type for a given type.
+
+      For example, "equal" deriver would map [t] to [t -> t -> bool]. *)
+end
+
+module Tuple =
+struct
+
+  (** Tuple deriver interface. *)
+  module type S =
+  sig
+    include Base
+    val tuple: loc:location -> expression list -> expression
+    (** Compose derived values/functions for tuple elements into derived value/function for the tuple. *)
+  end
+end
+
+module Record =
+struct
+
+  (** Record deriver interface. *)
+  module type S =
+  sig
+    include Base
+    val record: loc:location -> (longident * expression) list -> expression
+    (** Compose derived values/functions for record fields into derived value/function for the record. *)
+  end
+end
+
+module Full =
+struct
+
+  (** Full deriver interface. *)
+  module type S =
+  sig
+    include Tuple.S
+    include Record.S
+  end
+end
+
+module type S = Full.S
+(** Deriver interface. *)
diff --git a/src/vendor/ppx_easy_deriving/pat_exp.ml b/src/vendor/ppx_easy_deriving/pat_exp.ml
new file mode 100644
index 0000000000..a9d43d07e6
--- /dev/null
+++ b/src/vendor/ppx_easy_deriving/pat_exp.ml
@@ -0,0 +1,46 @@
+open Ppxlib
+open Ast_builder.Default
+
+type t =
+  | Record of (longident * t) list
+  | Tuple of t list
+  | Unit
+  | Base of string
+let create_record ~prefix ls =
+  Record (List.mapi (fun i l -> (l, Base (prefix ^ string_of_int (i + 1)))) ls)
+let create_tuple ~prefix n =
+  match n with
+  | 0 -> Unit
+  | 1 -> Base (prefix ^ "1")
+  | n -> Tuple (List.init n (fun i -> Base (prefix ^ string_of_int (i + 1))))
+let rec to_pat ~loc = function
+  | Record xs ->
+    ppat_record ~loc (List.map (fun (l, x) ->
+        (Located.mk ~loc l, to_pat ~loc x)
+      ) xs) Closed
+  | Tuple xs ->
+    ppat_tuple ~loc (List.map (to_pat ~loc) xs)
+  | Unit ->
+    [%pat? ()]
+  | Base s ->
+    ppat_var ~loc (Located.mk ~loc s)
+let rec to_exps ~loc = function
+  | Record xs ->
+    List.flatten (List.map (fun (_, x) -> to_exps ~loc x) xs)
+  | Tuple xs ->
+    List.flatten (List.map (to_exps ~loc) xs)
+  | Unit ->
+    []
+  | Base s ->
+    [pexp_ident ~loc {loc; txt = Lident s}]
+let rec to_exp ~loc = function
+  | Record xs ->
+    pexp_record ~loc (List.map (fun (l, x) ->
+        (Located.mk ~loc l, to_exp ~loc x)
+      ) xs) None
+  | Tuple xs ->
+    pexp_tuple ~loc (List.map (to_exp ~loc) xs)
+  | Unit ->
+    [%expr ()]
+  | Base s ->
+    pexp_ident ~loc {loc; txt = Lident s}
diff --git a/src/vendor/ppx_easy_deriving/pat_exp.mli b/src/vendor/ppx_easy_deriving/pat_exp.mli
new file mode 100644
index 0000000000..a4878afa81
--- /dev/null
+++ b/src/vendor/ppx_easy_deriving/pat_exp.mli
@@ -0,0 +1,16 @@
+(** Common representation of patterns and expressions. *)
+
+open Ppxlib
+
+type t =
+  | Record of (longident * t) list
+  | Tuple of t list
+  | Unit
+  | Base of string
+
+val create_record: prefix:string -> longident list -> t
+val create_tuple: prefix:string -> int -> t
+
+val to_pat: loc:location -> t -> pattern
+val to_exps: loc:location -> t -> expression list
+val to_exp: loc:location -> t -> expression
diff --git a/src/vendor/ppx_easy_deriving/ppx_easy_deriving.ml b/src/vendor/ppx_easy_deriving/ppx_easy_deriving.ml
new file mode 100644
index 0000000000..a490f33557
--- /dev/null
+++ b/src/vendor/ppx_easy_deriving/ppx_easy_deriving.ml
@@ -0,0 +1,15 @@
+(** Library for easily defining PPX derivers without boilerplate and runtime overhead. *)
+
+(** {1 Interfaces} *)
+
+include Intf (** @inline *)
+
+
+(** {1 Deriver} *)
+
+module Deriver = Deriver
+
+
+(** {1 Easier constructs} *)
+
+module Product = Product
diff --git a/src/vendor/ppx_easy_deriving/product.ml b/src/vendor/ppx_easy_deriving/product.ml
new file mode 100644
index 0000000000..2135552b63
--- /dev/null
+++ b/src/vendor/ppx_easy_deriving/product.ml
@@ -0,0 +1,226 @@
+open Ppxlib
+open Ast_builder.Default
+
+include Product_intf
+
+module type Product_S = S
+
+module Make (P: S): Intf.S =
+struct
+  include P
+
+  let tuple ~loc es =
+    let n = List.length es in
+    let pe_create = Pat_exp.create_tuple n in
+    P.product ~loc ~pe_create es
+
+  let record ~loc les =
+    let ls = List.map fst les in
+    let pe_create = Pat_exp.create_record ls in
+    let es = List.map snd les in
+    P.product ~loc ~pe_create es
+end
+
+module Reduce =
+struct
+  include Reduce
+
+  module Conjunctive =
+  struct
+    include Conjunctive
+
+    module Make (C: S): Reduce.S =
+    struct
+      let name = C.name
+      let typ ~loc _ = [%type: bool]
+      let unit ~loc = [%expr true]
+      let both ~loc e1 e2 = [%expr [%e e1] && [%e e2]]
+    end
+  end
+end
+
+module Reduce1 =
+struct
+  include Reduce1
+
+  module Make (R1: S): Intf.S =
+  struct
+    module P: Product_S =
+    struct
+      let name = R1.name
+      let typ ~loc t = [%type: [%t t] -> [%t R1.typ ~loc t]]
+
+      let product ~loc ~pe_create es =
+        let pe = pe_create ~prefix:"x" in
+        let body =
+          let es = List.map2 (fun e x ->
+              [%expr [%e e] [%e x]]
+            ) es (Pat_exp.to_exps ~loc pe)
+          in
+          Util.reduce ~unit:(R1.unit ~loc) ~both:(R1.both ~loc) es
+        in
+        [%expr fun [%p Pat_exp.to_pat ~loc pe] -> [%e body]]
+    end
+
+    include Make (P)
+  end
+end
+
+module Reduce2 =
+struct
+  include Reduce2
+
+  module Make (R2: S): Intf.S =
+  struct
+    module P: Product_S =
+    struct
+      let name = R2.name
+      let typ ~loc t = [%type: [%t t] -> [%t t] -> [%t R2.typ ~loc t]]
+
+      let product ~loc ~pe_create es =
+        let pel = pe_create ~prefix:"l" in
+        let per = pe_create ~prefix:"r" in
+        let body =
+          let esl = Pat_exp.to_exps ~loc pel in
+          let esr = Pat_exp.to_exps ~loc per in
+          let es = Util.map3 (fun e l r ->
+              [%expr [%e e] [%e l] [%e r]]
+            ) es esl esr
+          in
+          Util.reduce ~unit:(R2.unit ~loc) ~both:(R2.both ~loc) es
+        in
+        let pl = Pat_exp.to_pat ~loc pel in
+        let pr = Pat_exp.to_pat ~loc per in
+        [%expr fun [%p pl] [%p pr] -> [%e body]]
+    end
+
+    include Make (P)
+  end
+end
+
+module Create =
+struct
+  include Create
+
+  module Make (C: S): Intf.S =
+  struct
+    let name = C.name
+    let typ ~loc t = [%type: [%t C.typ ~loc t] -> [%t t]]
+
+    let tuple ~loc es =
+      match es with
+      | [] -> [%expr fun _ -> ()]
+      | [e] -> e
+      | _ :: _ ->
+        let elems = List.map (fun e ->
+            [%expr [%e e] x]
+          ) es
+        in
+        let body = pexp_tuple ~loc elems in
+        [%expr fun x -> [%e body]]
+
+    let record ~loc les =
+      let fields = List.map (fun (l, e) ->
+          (Located.mk ~loc l, [%expr [%e e] x])
+        ) les
+      in
+      let body = pexp_record ~loc fields None in
+      [%expr fun x -> [%e body]]
+  end
+end
+
+module Map1 =
+struct
+  include Map1
+
+  module Make (M1: S): Intf.S =
+  struct
+    let name = M1.name
+    let typ ~loc t = [%type: [%t t] -> [%t t]]
+
+    let tuple ~loc es =
+      let n = List.length es in
+      let pe = Pat_exp.create_tuple ~prefix:"x" n in
+      let elems =
+        List.map2 (fun e x ->
+            [%expr [%e e] [%e x]]
+          ) es (Pat_exp.to_exps ~loc pe)
+      in
+      let body =
+        match elems with
+        | [] -> [%expr ()]
+        | [elem] -> elem
+        | _ :: _ -> pexp_tuple ~loc elems
+      in
+      [%expr fun [%p Pat_exp.to_pat ~loc pe] -> [%e body]]
+
+    let record ~loc les =
+      let ls = List.map fst les in
+      let pe = Pat_exp.create_record ~prefix:"x" ls in
+      let es = List.map snd les in
+      let elems =
+        List.map2 (fun e x ->
+            [%expr [%e e] [%e x]]
+          ) es (Pat_exp.to_exps ~loc pe)
+      in
+      let fields = List.map2 (fun l elem ->
+          (Located.mk ~loc l, elem)
+        ) ls elems
+      in
+      let body = pexp_record ~loc fields None in
+      [%expr fun [%p Pat_exp.to_pat ~loc pe] -> [%e body]]
+  end
+end
+
+module Map2 =
+struct
+  include Map2
+
+  module Make (M2: S): Intf.S =
+  struct
+    let name = M2.name
+    let typ ~loc t = [%type: [%t t] -> [%t t] -> [%t t]]
+
+    let tuple ~loc es =
+      let n = List.length es in
+      let pel = Pat_exp.create_tuple ~prefix:"l" n in
+      let per = Pat_exp.create_tuple ~prefix:"r" n in
+      let elems =
+        let esl = Pat_exp.to_exps ~loc pel in
+        let esr = Pat_exp.to_exps ~loc per in
+        Util.map3 (fun e l r ->
+            [%expr [%e e] [%e l] [%e r]]
+          ) es esl esr
+      in
+      let body =
+        match elems with
+        | [] -> [%expr ()]
+        | [elem] -> elem
+        | _ :: _ -> pexp_tuple ~loc elems
+      in
+      let pl = Pat_exp.to_pat ~loc pel in
+      let pr = Pat_exp.to_pat ~loc per in
+      [%expr fun [%p pl] [%p pr] -> [%e body]]
+
+    let record ~loc les =
+      let ls = List.map fst les in
+      let pel = Pat_exp.create_record ~prefix:"l" ls in
+      let per = Pat_exp.create_record ~prefix:"r" ls in
+      let es = List.map snd les in
+      let elems =
+        let esl = Pat_exp.to_exps ~loc pel in
+        let esr = Pat_exp.to_exps ~loc per in
+        Util.map3 (fun e l r ->
+            [%expr [%e e] [%e l] [%e r]]
+          ) es esl esr
+      in
+      let fields = List.map2 (fun l elem ->
+          (Located.mk ~loc l, elem)
+        ) ls elems
+      in
+      let body = pexp_record ~loc fields None in
+      let pl = Pat_exp.to_pat ~loc pel in
+      let pr = Pat_exp.to_pat ~loc per in
+      [%expr fun [%p pl] [%p pr] -> [%e body]]
+  end
+end
diff --git a/src/vendor/ppx_easy_deriving/product.mli b/src/vendor/ppx_easy_deriving/product.mli
new file mode 100644
index 0000000000..d0b45f106c
--- /dev/null
+++ b/src/vendor/ppx_easy_deriving/product.mli
@@ -0,0 +1,3 @@
+(** Product derivers which unify tuple and record derivers. *)
+
+include Product_intf.Product (** @inline *)
diff --git a/src/vendor/ppx_easy_deriving/product_intf.ml b/src/vendor/ppx_easy_deriving/product_intf.ml
new file mode 100644
index 0000000000..14964bbee7
--- /dev/null
+++ b/src/vendor/ppx_easy_deriving/product_intf.ml
@@ -0,0 +1,132 @@
+open Ppxlib
+
+module type S =
+sig
+  include Intf.Base
+  val product: loc:location -> pe_create:(prefix:string -> Pat_exp.t) -> expression list -> expression
+  (** Compose derived values/functions for product elements into derived value/function for the product.
+
+      @param pe_create factory for patterns/expressions of the actual type. *)
+end
+
+module Reduce =
+struct
+  module type S =
+  sig
+    include Intf.Base
+    val unit: loc:location -> expression
+    (** Derived value/function for [unit] type. *)
+
+    val both: loc:location -> expression -> expression -> expression
+    (** Compose derived values/functions in a product into derived value/function for the pair. *)
+  end
+
+  module Conjunctive =
+  struct
+    module type S = Intf.Name
+  end
+end
+
+module Reduce1 =
+struct
+  module type S = Reduce.S
+end
+
+module Reduce2 =
+struct
+  module type S = Reduce.S
+end
+
+module Create =
+struct
+  module type S =
+  sig
+    include Intf.Base
+  end
+end
+
+module Map1 =
+struct
+  module type S = Intf.Name
+end
+
+module Map2 =
+struct
+  module type S = Intf.Name
+end
+
+module type Product =
+sig
+  module type S = S
+  (** Product deriver interface. *)
+
+  module Make (P: S): Intf.S
+  (** Make deriver from product deriver. *)
+
+  (** Reductions for reducing derivers. *)
+  module Reduce :
+  sig
+    module type S = Reduce.S
+    (** Reduction interface. *)
+
+    (** Conjunctive reduction. *)
+    module Conjunctive :
+    sig
+      module type S = Reduce.Conjunctive.S
+      (** Conjunctive reduction interface. *)
+
+      module Make (C: S): Reduce.S
+      (** Make reduction from conjunctive reduction. *)
+    end
+  end
+
+  (** Unary reducing deriver. *)
+  module Reduce1 :
+  sig
+    module type S = Reduce1.S
+    (** Unary reducing deriver interface. *)
+
+    module Make (R1: S): Intf.S
+    (** Make deriver from unary reducing deriver. *)
+  end
+
+  (** Binary reducing deriver. *)
+  module Reduce2 :
+  sig
+    module type S = Reduce2.S
+    (** Binary reducing deriver interface. *)
+
+    module Make (R2: S): Intf.S
+    (** Make deriver from binary reducing deriver. *)
+  end
+
+  (** Unary creating deriver. *)
+  module Create :
+  sig
+    module type S = Create.S
+    (** Unary creating deriver interface. *)
+
+    module Make (C: S): Intf.S
+    (** Make deriver from unary creating deriver. *)
+  end
+
+  (** Unary mapping deriver. *)
+  module Map1 :
+  sig
+    module type S = Map1.S
+    (** Unary mapping deriver interface. *)
+
+    module Make (M1: S): Intf.S
+    (** Make deriver from unary mapping deriver. *)
+  end
+
+  (** Binary mapping deriver. *)
+  module Map2 :
+  sig
+    module type S = Map2.S
+    (** Binary mapping deriver interface. *)
+
+    module Make (M2: S): Intf.S
+    (** Make deriver from binary mapping deriver. *)
+  end
+end
diff --git a/src/vendor/ppx_easy_deriving/util.ml b/src/vendor/ppx_easy_deriving/util.ml
new file mode 100644
index 0000000000..fbb9d3f642
--- /dev/null
+++ b/src/vendor/ppx_easy_deriving/util.ml
@@ -0,0 +1,12 @@
+let reduce ~unit ~both = function
+  | [] -> unit
+  | [x] -> x
+  | xs ->
+    let xs = List.rev xs in
+    match xs with
+    | x :: xs ->
+      List.fold_right both (List.rev xs) x (* omits hash_empty *)
+    | [] -> assert false
+
+let map3 f l1 l2 l3 =
+  List.map2 (fun x1 (x2, x3) -> f x1 x2 x3) l1 (List.combine l2 l3) (* TODO: optimize *)
diff --git a/src/vendor/ppx_easy_deriving/util.mli b/src/vendor/ppx_easy_deriving/util.mli
new file mode 100644
index 0000000000..0f896e7efc
--- /dev/null
+++ b/src/vendor/ppx_easy_deriving/util.mli
@@ -0,0 +1,8 @@
+(** Utility functions. *)
+
+val reduce: unit:'a -> both:('a -> 'a -> 'a) -> 'a list -> 'a
+(** Reduce a list of values "optimally",
+    i.e. without unnecessary [~unit] and [~both]. *)
+
+val map3: ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
+(** Map three lists into one. *)
diff --git a/src/witness/svcomp.ml b/src/witness/svcomp.ml
index bb887e6cb1..81dbc53760 100644
--- a/src/witness/svcomp.ml
+++ b/src/witness/svcomp.ml
@@ -1,7 +1,6 @@
 (** SV-COMP tasks and results. *)
 
 open GoblintCil
-open Batteries
 
 module Specification = SvcompSpec
 
@@ -27,9 +26,9 @@ let is_error_function f =
 (* TODO: unused, but should be used? *)
 let is_special_function f =
   let loc = f.vdecl in
-  let is_svcomp = String.ends_with loc.file "sv-comp.c" in (* only includes/sv-comp.c functions, not __VERIFIER_assert in benchmark *)
+  let is_svcomp = String.ends_with loc.file ~suffix:"sv-comp.c" in (* only includes/sv-comp.c functions, not __VERIFIER_assert in benchmark *)
   let is_verifier = match f.vname with
-    | fname when String.starts_with fname "__VERIFIER" -> true
+    | fname when String.starts_with fname ~prefix:"__VERIFIER" -> true
     | fname -> is_error_function f
   in
   is_svcomp && is_verifier
@@ -60,6 +59,11 @@ struct
     | Unknown -> "unknown"
 end
 
+exception Error of string
+
+let errorwith s = raise (Error s)
+
+
 module type TaskResult =
 sig
   module Arg: MyARG.S
diff --git a/src/witness/witness.ml b/src/witness/witness.ml
index fb88c2ce7b..7b0213b601 100644
--- a/src/witness/witness.ml
+++ b/src/witness/witness.ml
@@ -690,25 +690,16 @@ struct
       Timing.wrap "graphml witness" (write_file witness_path (module Task)) (module TaskResult)
     )
 
-  let write entrystates =
+  let write yaml_validate_result entrystates =
     match !AnalysisState.verified with
     | Some false -> print_svcomp_result "ERROR (verify)"
     | _ ->
-      if get_string "witness.yaml.validate" <> "" then (
-        match get_bool "witness.yaml.strict" with
-        | true when !YamlWitness.cnt_error > 0 ->
-          print_svcomp_result "ERROR (witness error)"
-        | true when !YamlWitness.cnt_unsupported > 0 ->
-          print_svcomp_result "ERROR (witness unsupported)"
-        | true when !YamlWitness.cnt_disabled > 0 ->
-          print_svcomp_result "ERROR (witness disabled)"
-        | _ when !YamlWitness.cnt_refuted > 0 ->
-          print_svcomp_result (Result.to_string (False None))
-        | _ when !YamlWitness.cnt_unconfirmed > 0 ->
-          print_svcomp_result (Result.to_string Unknown)
-        | _ ->
-          write entrystates
-      )
-      else
+      match yaml_validate_result with
+      | Some (Stdlib.Error msg) ->
+        print_svcomp_result ("ERROR (" ^ msg ^ ")")
+      | Some (Ok (Svcomp.Result.False _ | Unknown as result)) ->
+        print_svcomp_result (Result.to_string result)
+      | Some (Ok True)
+      | None ->
         write entrystates
 end
diff --git a/src/witness/witnessUtil.ml b/src/witness/witnessUtil.ml
index 5d22fd1e83..390e893987 100644
--- a/src/witness/witnessUtil.ml
+++ b/src/witness/witnessUtil.ml
@@ -63,6 +63,7 @@ struct
         List.exists (fun (_, edge) ->
             match edge with
             | Proc (_, Lval (Var fv, NoOffset), args) when LibraryFunctions.is_special fv ->
+              Goblint_backtrace.wrap_val ~mark:(Cilfacade.FunVarinfo fv) @@ fun () ->
               let desc = LibraryFunctions.find fv in
               begin match desc.special args with
                 | Lock _ -> true
@@ -209,7 +210,7 @@ struct
           let typ = TEnum (e, []) in
           let name = "enum " ^ ename in
           Hashtbl.replace genv name (Cabs2cil.EnvTyp typ, loc);
-          List.iter (fun (name, exp, loc) ->
+          List.iter (fun (name, _, exp, loc) ->
               Hashtbl.replace genv name (Cabs2cil.EnvEnum (exp, typ), loc)
             ) eitems
         | Cil.GVar (v, _, loc)
diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index 42254f30de..2bdd2ced4c 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -43,13 +43,20 @@ struct
       specification
     }
 
-  let location ~location:(loc: Cil.location) ~(location_function): Location.t = {
-    file_name = loc.file;
-    file_hash = sha256_file loc.file;
-    line = loc.line;
-    column = loc.column;
-    function_ = location_function;
-  }
+  let location ~location:(loc: Cil.location) ~(location_function): Location.t =
+    let file_hash =
+      match GobConfig.get_string "witness.yaml.format-version" with
+      | "0.1" -> Some (sha256_file loc.file)
+      | "2.0" -> None
+      | _ -> assert false
+    in
+    {
+      file_name = loc.file;
+      file_hash;
+      line = loc.line;
+      column = Some loc.column;
+      function_ = Some location_function;
+    }
 
   let invariant invariant: Invariant.t = {
     string = invariant;
@@ -514,6 +521,26 @@ struct
     Timing.wrap "yaml witness" write ()
 end
 
+let init () =
+  match GobConfig.get_string "witness.yaml.validate" with
+  | "" -> ()
+  | path ->
+    (* Check witness existence before doing the analysis. *)
+    if not (Sys.file_exists path) then (
+      Logs.error "witness.yaml.validate: %s not found" path;
+      Svcomp.errorwith "witness missing"
+    )
+
+let loc_of_location (location: YamlWitnessType.Location.t): Cil.location = {
+  file = location.file_name;
+  line = location.line;
+  column = Option.value location.column ~default:1;
+  byte = -1;
+  endLine = -1;
+  endColumn = -1;
+  endByte = -1;
+  synthetic = false;
+}
 
 module ValidationResult =
 struct
@@ -553,17 +580,6 @@ struct
   module InvariantParser = WitnessUtil.InvariantParser
   module VR = ValidationResult
 
-  let loc_of_location (location: YamlWitnessType.Location.t): Cil.location = {
-    file = location.file_name;
-    line = location.line;
-    column = location.column;
-    byte = -1;
-    endLine = -1;
-    endColumn = -1;
-    endByte = -1;
-    synthetic = false;
-  }
-
   let validate () =
     let location_locator = Locator.create () in
     let loop_locator = Locator.create () in
@@ -581,7 +597,9 @@ struct
 
     let yaml = match Yaml_unix.of_file (Fpath.v (GobConfig.get_string "witness.yaml.validate")) with
       | Ok yaml -> yaml
-      | Error (`Msg m) -> failwith ("Yaml_unix.of_file: " ^ m)
+      | Error (`Msg m) ->
+        Logs.error "Yaml_unix.of_file: %s" m;
+        Svcomp.errorwith "witness missing"
     in
     let yaml_entries = yaml |> GobYaml.list |> BatResult.get_ok in
 
@@ -795,6 +813,15 @@ struct
         None
       in
 
+      let validate_violation_sequence (violation_sequence: YamlWitnessType.ViolationSequence.t) =
+        (* TODO: update cnt-s appropriately (needs access to SV-COMP result pre-witness validation) *)
+        (* Nothing needs to be checked here!
+           If program is correct and we can prove it, we output true, which counts as refutation of violation witness.
+           If program is correct and we cannot prove it, we output unknown.
+           If program is incorrect, we output unknown. *)
+        None
+      in
+
       match entry_type_enabled target_type, entry.entry_type with
       | true, LocationInvariant x ->
         validate_location_invariant x
@@ -804,7 +831,9 @@ struct
         validate_precondition_loop_invariant x
       | true, InvariantSet x ->
         validate_invariant_set x
-      | false, (LocationInvariant _ | LoopInvariant _ | PreconditionLoopInvariant _ | InvariantSet _) ->
+      | true, ViolationSequence x ->
+        validate_violation_sequence x
+      | false, (LocationInvariant _ | LoopInvariant _ | PreconditionLoopInvariant _ | InvariantSet _ | ViolationSequence _) ->
         incr cnt_disabled;
         M.info_noloc ~category:Witness "disabled entry of type %s" target_type;
         None
@@ -840,5 +869,19 @@ struct
 
     let certificate_path = GobConfig.get_string "witness.yaml.certificate" in
     if certificate_path <> "" then
-      yaml_entries_to_file (List.rev yaml_entries') (Fpath.v certificate_path)
+      yaml_entries_to_file (List.rev yaml_entries') (Fpath.v certificate_path);
+
+    match GobConfig.get_bool "witness.yaml.strict" with
+    | true when !cnt_error > 0 ->
+      Error "witness error"
+    | true when !cnt_unsupported > 0 ->
+      Error "witness unsupported"
+    | true when !cnt_disabled > 0 ->
+      Error "witness disabled"
+    | _ when !cnt_refuted > 0 ->
+      Ok (Svcomp.Result.False None)
+    | _ when !cnt_unconfirmed > 0 ->
+      Ok Unknown
+    | _ ->
+      Ok True
 end
diff --git a/src/witness/yamlWitnessType.ml b/src/witness/yamlWitnessType.ml
index 1630e05b69..4fc2029801 100644
--- a/src/witness/yamlWitnessType.ml
+++ b/src/witness/yamlWitnessType.ml
@@ -106,29 +106,45 @@ module Location =
 struct
   type t = {
     file_name: string;
-    file_hash: string;
+    file_hash: string option;
     line: int;
-    column: int;
-    function_: string;
+    column: int option;
+    function_: string option;
   }
   [@@deriving ord]
 
   let to_yaml {file_name; file_hash; line; column; function_} =
-    `O [
-      ("file_name", `String file_name);
-      ("file_hash", `String file_hash);
-      ("line", `Float (float_of_int line));
-      ("column", `Float (float_of_int column));
-      ("function", `String function_);
-    ]
+    `O ([
+        ("file_name", `String file_name);
+      ] @ (match file_hash with
+        | Some file_hash -> [
+            ("file_hash", `String file_hash);
+          ]
+        | None ->
+          []
+      ) @ [
+          ("line", `Float (float_of_int line));
+        ] @ (match column with
+        | Some column -> [
+            ("column", `Float (float_of_int column));
+          ]
+        | None ->
+          []
+      ) @ (match function_ with
+        | Some function_ -> [
+            ("function", `String function_);
+          ]
+        | None ->
+          []
+      ))
 
   let of_yaml y =
     let open GobYaml in
     let+ file_name = y |> find "file_name" >>= to_string
-    and+ file_hash = y |> find "file_hash" >>= to_string
+    and+ file_hash = y |> Yaml.Util.find "file_hash" >>= option_map to_string
     and+ line = y |> find "line" >>= to_int
-    and+ column = y |> find "column" >>= to_int
-    and+ function_ = y |> find "function" >>= to_string in
+    and+ column = y |> Yaml.Util.find "column" >>= option_map to_int
+    and+ function_ = y |> Yaml.Util.find "function" >>= option_map to_string in
     {file_name; file_hash; line; column; function_}
 end
 
@@ -426,6 +442,205 @@ struct
   let entry_type = "precondition_loop_invariant_certificate"
 end
 
+module ViolationSequence =
+struct
+
+  module Constraint =
+  struct
+    type t = {
+      value: string;
+      format: string option;
+    }
+    [@@deriving ord]
+
+    let to_yaml {value; format} =
+      `O ([
+          ("value", `String value);
+        ] @ (match format with
+          | Some format -> [
+              ("format", `String format);
+            ]
+          | None ->
+            []
+        ))
+
+    let of_yaml y =
+      let open GobYaml in
+      let+ value = y |> find "value" >>= to_string
+      and+ format = y |> Yaml.Util.find "format" >>= option_map to_string in
+      {value; format}
+  end
+
+  module Assumption =
+  struct
+    type t = {
+      location: Location.t;
+      action: string;
+      constraint_: Constraint.t;
+    }
+    [@@deriving ord]
+
+    let waypoint_type = "assumption"
+
+    let to_yaml' {location; action; constraint_} =
+      [
+        ("location", Location.to_yaml location);
+        ("action", `String action);
+        ("constraint", Constraint.to_yaml constraint_);
+      ]
+
+    let of_yaml y =
+      let open GobYaml in
+      let+ location = y |> find "location" >>= Location.of_yaml
+      and+ action = y |> find "action" >>= to_string
+      and+ constraint_ = y |> find "constraint" >>= Constraint.of_yaml in
+      {location; action; constraint_}
+  end
+
+  module Target =
+  struct
+    type t = {
+      location: Location.t;
+      action: string;
+    }
+    [@@deriving ord]
+
+    let waypoint_type = "target"
+
+    let to_yaml' {location; action} =
+      [
+        ("location", Location.to_yaml location);
+        ("action", `String action);
+      ]
+
+    let of_yaml y =
+      let open GobYaml in
+      let+ location = y |> find "location" >>= Location.of_yaml
+      and+ action = y |> find "action" >>= to_string in
+      {location; action}
+  end
+
+  module FunctionEnter =
+  struct
+    include Target
+
+    let waypoint_type = "function_enter"
+  end
+
+  module FunctionReturn =
+  struct
+    include Assumption
+
+    let waypoint_type = "function_return"
+  end
+
+  module Branching =
+  struct
+    include Assumption
+
+    let waypoint_type = "branching"
+  end
+
+  (* TODO: could maybe use GADT, but adds ugly existential layer to entry type pattern matching *)
+  module WaypointType =
+  struct
+    type t =
+      | Assumption of Assumption.t
+      | Target of Target.t
+      | FunctionEnter of FunctionEnter.t
+      | FunctionReturn of FunctionReturn.t
+      | Branching of Branching.t
+    [@@deriving ord]
+
+    let waypoint_type = function
+      | Assumption _ -> Assumption.waypoint_type
+      | Target _ -> Target.waypoint_type
+      | FunctionEnter _ -> FunctionEnter.waypoint_type
+      | FunctionReturn _ -> FunctionReturn.waypoint_type
+      | Branching _ -> Branching.waypoint_type
+
+    let to_yaml' = function
+      | Assumption x -> Assumption.to_yaml' x
+      | Target x -> Target.to_yaml' x
+      | FunctionEnter x -> FunctionEnter.to_yaml' x
+      | FunctionReturn x -> FunctionReturn.to_yaml' x
+      | Branching x -> Branching.to_yaml' x
+
+    let of_yaml y =
+      let open GobYaml in
+      let* waypoint_type = y |> find "type" >>= to_string in
+      if waypoint_type = Assumption.waypoint_type then
+        let+ x = y |> Assumption.of_yaml in
+        Assumption x
+      else if waypoint_type = Target.waypoint_type then
+        let+ x = y |> Target.of_yaml in
+        Target x
+      else if waypoint_type = FunctionEnter.waypoint_type then
+        let+ x = y |> FunctionEnter.of_yaml in
+        FunctionEnter x
+      else if waypoint_type = FunctionReturn.waypoint_type then
+        let+ x = y |> FunctionReturn.of_yaml in
+        FunctionReturn x
+      else if waypoint_type = Branching.waypoint_type then
+        let+ x = y |> Branching.of_yaml in
+        Branching x
+      else
+        Error (`Msg "type")
+  end
+
+  module Waypoint =
+  struct
+    type t = {
+      waypoint_type: WaypointType.t;
+    }
+    [@@deriving ord]
+
+    let to_yaml {waypoint_type} =
+      `O [
+        ("waypoint", `O ([
+             ("type", `String (WaypointType.waypoint_type waypoint_type));
+           ] @ WaypointType.to_yaml' waypoint_type)
+        )
+      ]
+
+    let of_yaml y =
+      let open GobYaml in
+      let+ waypoint_type = y |> find "waypoint" >>= WaypointType.of_yaml in
+      {waypoint_type}
+  end
+
+  module Segment =
+  struct
+    type t = {
+      segment: Waypoint.t list;
+    }
+    [@@deriving ord]
+
+    let to_yaml {segment} =
+      `O [("segment", `A (List.map Waypoint.to_yaml segment))]
+
+    let of_yaml y =
+      let open GobYaml in
+      let+ segment = y |> find "segment" >>= list >>= list_map Waypoint.of_yaml in
+      {segment}
+  end
+
+  type t = {
+    content: Segment.t list;
+  }
+  [@@deriving ord]
+
+  let entry_type = "violation_sequence"
+
+  let to_yaml' {content} =
+    [("content", `A (List.map Segment.to_yaml content))]
+
+  let of_yaml y =
+    let open GobYaml in
+    let+ content = y |> find "content" >>= list >>= list_map Segment.of_yaml in
+    {content}
+end
+
 (* TODO: could maybe use GADT, but adds ugly existential layer to entry type pattern matching *)
 module EntryType =
 struct
@@ -437,6 +652,7 @@ struct
     | LoopInvariantCertificate of LoopInvariantCertificate.t
     | PreconditionLoopInvariantCertificate of PreconditionLoopInvariantCertificate.t
     | InvariantSet of InvariantSet.t
+    | ViolationSequence of ViolationSequence.t
   [@@deriving ord]
 
   let entry_type = function
@@ -447,6 +663,7 @@ struct
     | LoopInvariantCertificate _ -> LoopInvariantCertificate.entry_type
     | PreconditionLoopInvariantCertificate _ -> PreconditionLoopInvariantCertificate.entry_type
     | InvariantSet _ -> InvariantSet.entry_type
+    | ViolationSequence _ -> ViolationSequence.entry_type
 
   let to_yaml' = function
     | LocationInvariant x -> LocationInvariant.to_yaml' x
@@ -456,6 +673,7 @@ struct
     | LoopInvariantCertificate x -> LoopInvariantCertificate.to_yaml' x
     | PreconditionLoopInvariantCertificate x -> PreconditionLoopInvariantCertificate.to_yaml' x
     | InvariantSet x -> InvariantSet.to_yaml' x
+    | ViolationSequence x -> ViolationSequence.to_yaml' x
 
   let of_yaml y =
     let open GobYaml in
@@ -481,6 +699,9 @@ struct
     else if entry_type = InvariantSet.entry_type then
       let+ x = y |> InvariantSet.of_yaml in
       InvariantSet x
+    else if entry_type = ViolationSequence.entry_type then
+      let+ x = y |> ViolationSequence.of_yaml in
+      ViolationSequence x
     else
       Error (`Msg "entry_type")
 end
diff --git a/tests/regression/01-cpa/71-widen-sides.c b/tests/regression/01-cpa/71-widen-sides.c
index 522f6fae44..a93124c6e5 100644
--- a/tests/regression/01-cpa/71-widen-sides.c
+++ b/tests/regression/01-cpa/71-widen-sides.c
@@ -1,4 +1,4 @@
-// PARAM: --set ana.ctx_insens "['base', 'mallocWrapper']"  --enable ana.int.interval --sets solvers.td3.side_widen sides-local
+// PARAM: --set ana.ctx_insens "['base', 'mallocWrapper']"  --enable ana.int.interval --set solvers.td3.side_widen sides-local
 #include <goblint.h>
 
 int further(int n) {
diff --git a/tests/regression/36-apron/45-context.c b/tests/regression/36-apron/45-context.c
index 94328af97f..eda945abd5 100644
--- a/tests/regression/36-apron/45-context.c
+++ b/tests/regression/36-apron/45-context.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --enable ana.int.interval --enable ana.relation.context
+// SKIP PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.path_sens[+] threadflag --enable ana.int.interval --enable ana.relation.context
 extern int __VERIFIER_nondet_int();
 
 #include <goblint.h>
diff --git a/tests/regression/36-apron/46-no-context.c b/tests/regression/36-apron/46-no-context.c
index bf115cee24..640784b913 100644
--- a/tests/regression/36-apron/46-no-context.c
+++ b/tests/regression/36-apron/46-no-context.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --enable ana.int.interval --disable ana.relation.context
+// SKIP PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.path_sens[+] threadflag --enable ana.int.interval --disable ana.relation.context
 extern int __VERIFIER_nondet_int();
 
 #include <goblint.h>
diff --git a/tests/regression/36-apron/47-no-context-attribute.c b/tests/regression/36-apron/47-no-context-attribute.c
index 90b58cdc28..cf111f5ffc 100644
--- a/tests/regression/36-apron/47-no-context-attribute.c
+++ b/tests/regression/36-apron/47-no-context-attribute.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --enable ana.int.interval --enable ana.relation.context
+// SKIP PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.path_sens[+] threadflag --enable ana.int.interval --enable ana.relation.context
 extern int __VERIFIER_nondet_int();
 
 #include <goblint.h>
diff --git a/tests/regression/36-apron/48-context-attribute.c b/tests/regression/36-apron/48-context-attribute.c
index 5e5ecf01fe..3304c20388 100644
--- a/tests/regression/36-apron/48-context-attribute.c
+++ b/tests/regression/36-apron/48-context-attribute.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --enable ana.int.interval --disable ana.relation.context
+// SKIP PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.path_sens[+] threadflag --enable ana.int.interval --disable ana.relation.context
 extern int __VERIFIER_nondet_int();
 
 #include <goblint.h>
diff --git a/tests/regression/36-apron/86-branched-thread-creation.c b/tests/regression/36-apron/86-branched-thread-creation.c
index cac0a881a6..91a5411e8f 100644
--- a/tests/regression/36-apron/86-branched-thread-creation.c
+++ b/tests/regression/36-apron/86-branched-thread-creation.c
@@ -40,7 +40,7 @@ int main(void) {
 
   if(!mt) {
     pthread_mutex_lock(&mutex);
-    __goblint_check(g==h); //MAYFAIL
+    __goblint_check(g==h); //FAIL
     pthread_mutex_unlock(&mutex);
   }
 
diff --git a/tests/regression/46-apron2/03-other-assume.c b/tests/regression/46-apron2/03-other-assume.c
index 635911a197..c136d1bde3 100644
--- a/tests/regression/46-apron2/03-other-assume.c
+++ b/tests/regression/46-apron2/03-other-assume.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins --sets ana.relation.privatization mutex-meet-tid
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins --set ana.relation.privatization mutex-meet-tid
 #include <pthread.h>
 #include <goblint.h>
 
diff --git a/tests/regression/46-apron2/04-other-assume-inprec.c b/tests/regression/46-apron2/04-other-assume-inprec.c
index 09b8d150a8..ccf8ecefa1 100644
--- a/tests/regression/46-apron2/04-other-assume-inprec.c
+++ b/tests/regression/46-apron2/04-other-assume-inprec.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins --sets ana.relation.privatization mutex-meet-tid
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[+] threadJoins --set ana.relation.privatization mutex-meet-tid
 #include <pthread.h>
 #include <goblint.h>
 
diff --git a/tests/regression/46-apron2/26-autotune.c b/tests/regression/46-apron2/26-autotune.c
index 96c5c85278..ec8f55fe19 100644
--- a/tests/regression/46-apron2/26-autotune.c
+++ b/tests/regression/46-apron2/26-autotune.c
@@ -1,4 +1,4 @@
-//SKIP PARAM: --enable ana.int.interval --sets sem.int.signed_overflow assume_none --set ana.activated[+] apron --enable ana.autotune.enabled
+//SKIP PARAM: --enable ana.int.interval --set sem.int.signed_overflow assume_none --set ana.activated[+] apron --enable ana.autotune.enabled
 // Check that autotuner disables context for apron as well for recursive calls
 #include <goblint.h>
 
diff --git a/tests/regression/46-apron2/30-autotune-stub.c b/tests/regression/46-apron2/30-autotune-stub.c
index e1b7603c3b..02c80e7d21 100644
--- a/tests/regression/46-apron2/30-autotune-stub.c
+++ b/tests/regression/46-apron2/30-autotune-stub.c
@@ -1,4 +1,4 @@
-//SKIP PARAM: --enable ana.int.interval --sets sem.int.signed_overflow assume_none --set ana.activated[+] apron --enable ana.autotune.enabled
+//SKIP PARAM: --enable ana.int.interval --set sem.int.signed_overflow assume_none --set ana.activated[+] apron --enable ana.autotune.enabled
 // Check that autotuner respect goblint_stub attributes as hints to not track variables.
 #include <goblint.h>
 
diff --git a/tests/regression/46-apron2/90-malloc.c b/tests/regression/46-apron2/90-malloc.c
new file mode 100644
index 0000000000..8780568748
--- /dev/null
+++ b/tests/regression/46-apron2/90-malloc.c
@@ -0,0 +1,21 @@
+// SKIP PARAM: --set ana.activated[+] apron  --set ana.relation.privatization mutex-meet --set ana.apron.domain interval --set sem.int.signed_overflow assume_none
+// Checks that assinging to malloc'ed memory does not cause both branches to be dead
+#include <pthread.h>
+#include <goblint.h>
+void nop(void* arg) {
+}
+
+void main() {
+  pthread_t thread;
+  pthread_create(&thread, 0, &nop, 0);
+
+  long *k = malloc(sizeof(long));
+  *k = 5;
+  if (1)
+    ;
+
+  __goblint_check(*k >= 5); // Reachable and true
+
+  *k = *k+1;
+  __goblint_check(*k >= 5); // Reachable and true
+}
diff --git a/tests/regression/46-apron2/91-malloc-tid.c b/tests/regression/46-apron2/91-malloc-tid.c
new file mode 100644
index 0000000000..36696956e7
--- /dev/null
+++ b/tests/regression/46-apron2/91-malloc-tid.c
@@ -0,0 +1,21 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag  --set ana.relation.privatization mutex-meet-tid --set ana.apron.domain interval --set sem.int.signed_overflow assume_none
+// Checks that assinging to malloc'ed memory does not cause both branches to be dead
+#include <pthread.h>
+#include <goblint.h>
+void nop(void* arg) {
+}
+
+void main() {
+  pthread_t thread;
+  pthread_create(&thread, 0, &nop, 0);
+
+  long *k = malloc(sizeof(long));
+  *k = 5;
+  if (1)
+    ;
+
+  __goblint_check(*k >= 5); // Reachable and true
+
+  *k = *k+1;
+  __goblint_check(*k >= 5); // Reachable and true
+}
diff --git a/tests/regression/46-apron2/92-malloc-atomic.c b/tests/regression/46-apron2/92-malloc-atomic.c
new file mode 100644
index 0000000000..b2f057f6a4
--- /dev/null
+++ b/tests/regression/46-apron2/92-malloc-atomic.c
@@ -0,0 +1,21 @@
+// SKIP PARAM: --set ana.activated[+] apron  --set ana.relation.privatization mutex-meet-atomic --set ana.apron.domain interval --set sem.int.signed_overflow assume_none
+// Checks that assinging to malloc'ed memory does not cause both branches to be dead
+#include <pthread.h>
+#include <goblint.h>
+void nop(void* arg) {
+}
+
+void main() {
+  pthread_t thread;
+  pthread_create(&thread, 0, &nop, 0);
+
+  long *k = malloc(sizeof(long));
+  *k = 5;
+  if (1)
+    ;
+
+  __goblint_check(*k >= 5); // Reachable and true
+
+  *k = *k+1;
+  __goblint_check(*k >= 5); // Reachable and true
+}
diff --git a/tests/regression/55-loop-unrolling/12-loop-no-overflows.c b/tests/regression/55-loop-unrolling/12-loop-no-overflows.c
new file mode 100644
index 0000000000..03554e06c5
--- /dev/null
+++ b/tests/regression/55-loop-unrolling/12-loop-no-overflows.c
@@ -0,0 +1,37 @@
+// PARAM: --enable ana.int.interval_set
+// extracted from SV-COMP task ldv-memsafety/memleaks_test12-2.i
+
+typedef unsigned int size_t;
+struct ldv_list_head {
+    struct ldv_list_head *next, *prev;
+};
+struct ldv_list_head ldv_global_msg_list = {&(ldv_global_msg_list), &(ldv_global_msg_list)};
+struct ldv_msg {
+    void *data;
+    struct ldv_list_head list;
+};
+
+static inline void __ldv_list_del(struct ldv_list_head *prev, struct ldv_list_head *next) {
+    next->prev = prev;
+    prev->next = next;
+}
+
+static inline void ldv_list_del(struct ldv_list_head *entry) {
+    __ldv_list_del(entry->prev, entry->next);
+}
+
+void ldv_msg_free(struct ldv_msg *msg) {
+    free(msg->data);
+    free(msg);
+}
+
+// ldv_destroy_msgs
+void main(void) {
+    struct ldv_msg *msg;
+    struct ldv_msg *n;
+    for (msg = ({ const typeof( ((typeof(*msg) *)0)->list ) *__mptr = ((&ldv_global_msg_list)->next); (typeof(*msg) *)( (char *)__mptr - ((size_t) &((typeof(*msg) *)0)->list) ); }), n = ({ const typeof( ((typeof(*(msg)) *)0)->list ) *__mptr = ((msg)->list.next); (typeof(*(msg)) *)( (char *)__mptr - ((size_t) &((typeof(*(msg)) *)0)->list) ); }); &msg->list != (&ldv_global_msg_list); msg = n, n = ({ const typeof( ((typeof(*(n)) *)0)->list ) *__mptr = ((n)->list.next); (typeof(*(n)) *)( (char *)__mptr - ((size_t) &((typeof(*(n)) *)0)->list) ); })) // NOWARN
+    {
+        ldv_list_del(&msg->list);
+        ldv_msg_free(msg);
+    }
+}
\ No newline at end of file
diff --git a/tests/regression/55-loop-unrolling/13-unrolled-loop-no-overflows.c b/tests/regression/55-loop-unrolling/13-unrolled-loop-no-overflows.c
new file mode 100644
index 0000000000..84700ac9da
--- /dev/null
+++ b/tests/regression/55-loop-unrolling/13-unrolled-loop-no-overflows.c
@@ -0,0 +1,72 @@
+// PARAM: --enable ana.int.interval_set
+// extracted from SV-COMP task ldv-memsafety/memleaks_test12-2.i with --set exp.unrolling-factor 1
+
+typedef unsigned int size_t;
+struct ldv_list_head {
+    struct ldv_list_head *next, *prev;
+};
+struct ldv_list_head ldv_global_msg_list = {&(ldv_global_msg_list), &(ldv_global_msg_list)};
+struct ldv_msg {
+    void *data;
+    struct ldv_list_head list;
+};
+
+__inline static void __ldv_list_del(struct ldv_list_head *prev, struct ldv_list_head *next) {
+    next->prev = prev;
+    prev->next = next;
+    return;
+}
+
+__inline static void ldv_list_del(struct ldv_list_head *entry) {
+    __ldv_list_del(entry->prev, entry->next);
+    return;
+}
+
+void ldv_msg_free(struct ldv_msg *msg) {
+    free(msg->data);
+    free((void *)msg);
+    return;
+}
+
+// ldv_destroy_msgs
+void main(void) {
+    struct ldv_msg *msg;
+    struct ldv_msg *n;
+    struct ldv_list_head const *__mptr;
+    struct ldv_list_head const *__mptr___0;
+    struct ldv_list_head const *__mptr___1;
+
+    __mptr = (struct ldv_list_head const *)ldv_global_msg_list.next;
+    msg = (struct ldv_msg *)((char *)__mptr - (size_t)(&((struct ldv_msg *)0)->list));
+    __mptr___0 = (struct ldv_list_head const *)msg->list.next;
+    n = (struct ldv_msg *)((char *)__mptr___0 - (size_t)(&((struct ldv_msg *)0)->list));
+
+    if (!((unsigned long)(&msg->list) != (unsigned long)(&ldv_global_msg_list))) { // NOWARN
+        goto loop_end;
+    }
+
+    ldv_list_del(&msg->list);
+    ldv_msg_free(msg);
+    msg = n;
+    __mptr___1 = (struct ldv_list_head const *)n->list.next;
+    n = (struct ldv_msg *)((char *)__mptr___1 - (size_t)(&((struct ldv_msg *)0)->list));
+
+    loop_continue_0: /* CIL Label */;
+        {
+            while (1) {
+            while_continue: /* CIL Label */;
+                if (!((unsigned long)(&msg->list) != (unsigned long)(&ldv_global_msg_list))) {
+                    goto while_break;
+                }
+
+                ldv_list_del(&msg->list);
+                ldv_msg_free(msg);
+                msg = n;
+                __mptr___1 = (struct ldv_list_head const *)n->list.next;
+                n = (struct ldv_msg *)((char *)__mptr___1 - (size_t)(&((struct ldv_msg *)0)->list));
+            }
+        while_break: /* CIL Label */;
+        }
+    loop_end: /* CIL Label */;
+    return;
+}
\ No newline at end of file
diff --git a/tests/regression/56-witness/46-top-bool-invariant.t b/tests/regression/56-witness/46-top-bool-invariant.t
index b04d33dda8..741b00966f 100644
--- a/tests/regression/56-witness/46-top-bool-invariant.t
+++ b/tests/regression/56-witness/46-top-bool-invariant.t
@@ -144,7 +144,7 @@ all:
     dead: 0
     total lines: 2
   [Info][Witness] witness generation summary:
-    total generation entries: 3
+    total generation entries: 1
 
   $ yamlWitnessStrip < witness.yml
   - entry_type: location_invariant
@@ -158,28 +158,6 @@ all:
       string: x == (_Bool)0 || x == (_Bool)1
       type: assertion
       format: C
-  - entry_type: location_invariant
-    location:
-      file_name: 46-top-bool-invariant.c
-      file_hash: $FILE_HASH
-      line: 5
-      column: 3
-      function: main
-    location_invariant:
-      string: x <= (_Bool)1
-      type: assertion
-      format: C
-  - entry_type: location_invariant
-    location:
-      file_name: 46-top-bool-invariant.c
-      file_hash: $FILE_HASH
-      line: 5
-      column: 3
-      function: main
-    location_invariant:
-      string: (_Bool)0 <= x
-      type: assertion
-      format: C
 
 all without inexact-type-bounds:
 
diff --git a/tests/regression/58-base-mm-tid/01-tid-toy1.c b/tests/regression/58-base-mm-tid/01-tid-toy1.c
index bc3cd18efa..49e96881d1 100644
--- a/tests/regression/58-base-mm-tid/01-tid-toy1.c
+++ b/tests/regression/58-base-mm-tid/01-tid-toy1.c
@@ -1,4 +1,4 @@
-// PARAM: --set ana.path_sens[+] threadflag --sets ana.base.privatization mutex-meet-tid
+// PARAM: --set ana.path_sens[+] threadflag --set ana.base.privatization mutex-meet-tid
 // Inspired by 36/71
 #include <pthread.h>
 #include <goblint.h>
diff --git a/tests/regression/58-base-mm-tid/15-branched-thread-creation.c b/tests/regression/58-base-mm-tid/15-branched-thread-creation.c
index 3292182adc..c7bb43519f 100644
--- a/tests/regression/58-base-mm-tid/15-branched-thread-creation.c
+++ b/tests/regression/58-base-mm-tid/15-branched-thread-creation.c
@@ -41,7 +41,7 @@ int main(void) {
 
   if(!mt) {
     pthread_mutex_lock(&mutex);
-    __goblint_check(g==h); //MAYFAIL
+    __goblint_check(g==h); //FAIL
     pthread_mutex_unlock(&mutex);
   }
 
diff --git a/tests/regression/58-base-mm-tid/22-other-assume.c b/tests/regression/58-base-mm-tid/22-other-assume.c
index 4f5c73b038..301195ac1f 100644
--- a/tests/regression/58-base-mm-tid/22-other-assume.c
+++ b/tests/regression/58-base-mm-tid/22-other-assume.c
@@ -1,4 +1,4 @@
-// PARAM: --set ana.path_sens[+] threadflag --sets ana.base.privatization mutex-meet-tid
+// PARAM: --set ana.path_sens[+] threadflag --set ana.base.privatization mutex-meet-tid
 // Copy of 46/03 for base
 #include <pthread.h>
 #include <goblint.h>
diff --git a/tests/regression/58-base-mm-tid/23-other-assume-inprec.c b/tests/regression/58-base-mm-tid/23-other-assume-inprec.c
index 37e59d3edf..a4bac04c59 100644
--- a/tests/regression/58-base-mm-tid/23-other-assume-inprec.c
+++ b/tests/regression/58-base-mm-tid/23-other-assume-inprec.c
@@ -1,4 +1,4 @@
-// PARAM: --set ana.path_sens[+] threadflag --sets ana.base.privatization mutex-meet-tid --set ana.activated[+] threadJoins
+// PARAM: --set ana.path_sens[+] threadflag --set ana.base.privatization mutex-meet-tid --set ana.activated[+] threadJoins
 // Copy of 46/04 for base
 #include <pthread.h>
 #include <goblint.h>
diff --git a/tests/regression/66-interval-set-one/51-widen-sides.c b/tests/regression/66-interval-set-one/51-widen-sides.c
index b086baf026..53fe749704 100644
--- a/tests/regression/66-interval-set-one/51-widen-sides.c
+++ b/tests/regression/66-interval-set-one/51-widen-sides.c
@@ -1,4 +1,4 @@
-// PARAM: --set ana.ctx_insens "['base', 'mallocWrapper']"  --enable ana.int.interval_set --sets solvers.td3.side_widen sides-local
+// PARAM: --set ana.ctx_insens "['base', 'mallocWrapper']"  --enable ana.int.interval_set --set solvers.td3.side_widen sides-local
 #include <goblint.h>
 
 int further(int n) {
diff --git a/tests/regression/67-interval-sets-two/16-branched-thread-creation.c b/tests/regression/67-interval-sets-two/16-branched-thread-creation.c
index c309ec8ffd..d97f800621 100644
--- a/tests/regression/67-interval-sets-two/16-branched-thread-creation.c
+++ b/tests/regression/67-interval-sets-two/16-branched-thread-creation.c
@@ -41,7 +41,7 @@ int main(void) {
 
   if(!mt) {
     pthread_mutex_lock(&mutex);
-    __goblint_check(g==h); //MAYFAIL
+    __goblint_check(g==h); //FAIL
     pthread_mutex_unlock(&mutex);
   }
 
diff --git a/tests/regression/cfg/foo.t/run.t b/tests/regression/cfg/foo.t/run.t
index 02f6c1e5e0..cd890b7a19 100644
--- a/tests/regression/cfg/foo.t/run.t
+++ b/tests/regression/cfg/foo.t/run.t
@@ -67,7 +67,7 @@
     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:
-    total generation entries: 15
+    total generation entries: 10
 
   $ yamlWitnessStrip < witness.yml
   - entry_type: loop_invariant
@@ -103,17 +103,6 @@
       string: b == 0
       type: assertion
       format: C
-  - entry_type: location_invariant
-    location:
-      file_name: foo.c
-      file_hash: $FILE_HASH
-      line: 7
-      column: 3
-      function: main
-    location_invariant:
-      string: a != 0
-      type: assertion
-      format: C
   - entry_type: location_invariant
     location:
       file_name: foo.c
@@ -125,17 +114,6 @@
       string: 1 <= a
       type: assertion
       format: C
-  - entry_type: location_invariant
-    location:
-      file_name: foo.c
-      file_hash: $FILE_HASH
-      line: 7
-      column: 3
-      function: main
-    location_invariant:
-      string: 0 <= a
-      type: assertion
-      format: C
   - entry_type: location_invariant
     location:
       file_name: foo.c
@@ -158,17 +136,6 @@
       string: b != 0
       type: assertion
       format: C
-  - entry_type: location_invariant
-    location:
-      file_name: foo.c
-      file_hash: $FILE_HASH
-      line: 5
-      column: 5
-      function: main
-    location_invariant:
-      string: a != 1
-      type: assertion
-      format: C
   - entry_type: location_invariant
     location:
       file_name: foo.c
@@ -202,17 +169,6 @@
       string: b != 0
       type: assertion
       format: C
-  - entry_type: location_invariant
-    location:
-      file_name: foo.c
-      file_hash: $FILE_HASH
-      line: 4
-      column: 5
-      function: main
-    location_invariant:
-      string: a != 0
-      type: assertion
-      format: C
   - entry_type: location_invariant
     location:
       file_name: foo.c
@@ -224,14 +180,3 @@
       string: 1 <= a
       type: assertion
       format: C
-  - entry_type: location_invariant
-    location:
-      file_name: foo.c
-      file_hash: $FILE_HASH
-      line: 4
-      column: 5
-      function: main
-    location_invariant:
-      string: 0 <= a
-      type: assertion
-      format: C
diff --git a/tests/regression/witness/int.t/int.c b/tests/regression/witness/int.t/int.c
new file mode 100644
index 0000000000..4ad15b09ad
--- /dev/null
+++ b/tests/regression/witness/int.t/int.c
@@ -0,0 +1,17 @@
+#include <goblint.h>
+extern int __VERIFIER_nondet_int();
+
+int main() {
+  int i;
+  i = __VERIFIER_nondet_int();
+
+  if (i < 100)
+    __goblint_check(1);
+
+  if (50 < i && i < 100)
+    __goblint_check(1);
+
+  if (i == 42 || i == 5 || i == 101)
+    __goblint_check(1);
+  return 0;
+}
diff --git a/tests/regression/witness/int.t/run.t b/tests/regression/witness/int.t/run.t
new file mode 100644
index 0000000000..6b4784ce32
--- /dev/null
+++ b/tests/regression/witness/int.t/run.t
@@ -0,0 +1,45 @@
+  $ goblint --enable ana.sv-comp.functions --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --enable ana.int.def_exc --enable ana.int.enums --enable ana.int.interval --enable ana.int.congruence --disable ana.int.interval_set --disable witness.invariant.split-conjunction int.c
+  [Success][Assert] Assertion "1" will succeed (int.c:9:5-9:23)
+  [Success][Assert] Assertion "1" will succeed (int.c:12:5-12:23)
+  [Success][Assert] Assertion "1" will succeed (int.c:15:5-15:23)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 10
+    dead: 0
+    total lines: 10
+  [Info][Witness] witness generation summary:
+    total generation entries: 3
+
+  $ yamlWitnessStrip < witness.yml
+  - entry_type: location_invariant
+    location:
+      file_name: int.c
+      file_hash: $FILE_HASH
+      line: 15
+      column: 5
+      function: main
+    location_invariant:
+      string: (i == 5 || i == 42) || i == 101
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: int.c
+      file_hash: $FILE_HASH
+      line: 12
+      column: 5
+      function: main
+    location_invariant:
+      string: 51 <= i && i <= 99
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: int.c
+      file_hash: $FILE_HASH
+      line: 9
+      column: 5
+      function: main
+    location_invariant:
+      string: i <= 99
+      type: assertion
+      format: C
diff --git a/tests/regression/witness/violation.t/correct-hard.c b/tests/regression/witness/violation.t/correct-hard.c
new file mode 100644
index 0000000000..ce2b50a0c0
--- /dev/null
+++ b/tests/regression/witness/violation.t/correct-hard.c
@@ -0,0 +1,9 @@
+void reach_error(){}
+extern int __VERIFIER_nondet_int();
+
+int main() {
+  int x = __VERIFIER_nondet_int();
+  if (x != x)
+    reach_error();
+  return 0;
+}
diff --git a/tests/regression/witness/violation.t/correct-hard.yml b/tests/regression/witness/violation.t/correct-hard.yml
new file mode 100644
index 0000000000..b8af2c2193
--- /dev/null
+++ b/tests/regression/witness/violation.t/correct-hard.yml
@@ -0,0 +1,26 @@
+- entry_type: violation_sequence
+  metadata:
+    format_version: "2.0"
+    uuid: 4412af70-389a-475e-849c-e57e5b92019e
+    creation_time: 2024-06-14T15:35:00+03:00
+    producer:
+      name: Simmo Saan
+      version: n/a
+    task:
+      input_files:
+      - correct-hard.c
+      input_file_hashes:
+        correct-hard.c: 5cc49c1ce5a9aef64286c2a6e57f6955c5f4f9b19b43056507ae87a802802447
+      specification: G ! call(reach_error())
+      data_model: ILP32
+      language: C
+  content:
+  - segment:
+    - waypoint:
+        type: target
+        action: follow
+        location:
+          file_name: correct-hard.c
+          line: 7
+          column: 5
+          function: main
diff --git a/tests/regression/witness/violation.t/correct.c b/tests/regression/witness/violation.t/correct.c
new file mode 100644
index 0000000000..30f58a2f7e
--- /dev/null
+++ b/tests/regression/witness/violation.t/correct.c
@@ -0,0 +1,5 @@
+void reach_error(){}
+
+int main() {
+  return 0;
+}
diff --git a/tests/regression/witness/violation.t/correct.yml b/tests/regression/witness/violation.t/correct.yml
new file mode 100644
index 0000000000..1f1d4f41da
--- /dev/null
+++ b/tests/regression/witness/violation.t/correct.yml
@@ -0,0 +1,26 @@
+- entry_type: violation_sequence
+  metadata:
+    format_version: "2.0"
+    uuid: 4412af70-389a-475e-849c-e57e5b92019d
+    creation_time: 2024-06-14T15:35:00+03:00
+    producer:
+      name: Simmo Saan
+      version: n/a
+    task:
+      input_files:
+      - correct.c
+      input_file_hashes:
+        correct.c: 6f760cf7f33fc152738bf3514fe623cc94e52cad9ddc2f0e744595ce0de07530
+      specification: G ! call(reach_error())
+      data_model: ILP32
+      language: C
+  content:
+  - segment:
+    - waypoint:
+        type: target
+        action: follow
+        location:
+          file_name: correct.c
+          line: 4
+          column: 3
+          function: main
diff --git a/tests/regression/witness/violation.t/incorrect.c b/tests/regression/witness/violation.t/incorrect.c
new file mode 100644
index 0000000000..ff56fa2ef4
--- /dev/null
+++ b/tests/regression/witness/violation.t/incorrect.c
@@ -0,0 +1,6 @@
+void reach_error(){}
+
+int main() {
+  reach_error();
+  return 0;
+}
diff --git a/tests/regression/witness/violation.t/incorrect.yml b/tests/regression/witness/violation.t/incorrect.yml
new file mode 100644
index 0000000000..dd57ce3ca1
--- /dev/null
+++ b/tests/regression/witness/violation.t/incorrect.yml
@@ -0,0 +1,26 @@
+- entry_type: violation_sequence
+  metadata:
+    format_version: "2.0"
+    uuid: 4412af70-389a-475e-849c-e57e5b92019c
+    creation_time: 2024-06-14T15:35:00+03:00
+    producer:
+      name: Simmo Saan
+      version: n/a
+    task:
+      input_files:
+      - incorrect.c
+      input_file_hashes:
+        incorrect.c: 1af4fd9e76418e4b95af9950b58248127e7c2d9eb791e1c9b92da53952e0fca2
+      specification: G ! call(reach_error())
+      data_model: ILP32
+      language: C
+  content:
+  - segment:
+    - waypoint:
+        type: target
+        action: follow
+        location:
+          file_name: incorrect.c
+          line: 4
+          column: 3
+          function: main
diff --git a/tests/regression/witness/violation.t/run.t b/tests/regression/witness/violation.t/run.t
new file mode 100644
index 0000000000..1fc408635e
--- /dev/null
+++ b/tests/regression/witness/violation.t/run.t
@@ -0,0 +1,57 @@
+Violation witness for a correct program can be refuted by proving the program correct and returning `true`:
+
+  $ goblint --enable ana.sv-comp.enabled --set witness.yaml.entry-types[+] violation_sequence --set ana.specification "CHECK( init(main()), LTL(G ! call(reach_error())) )" correct.c --set witness.yaml.validate correct.yml
+  [Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
+  [Warning][Deadcode] Function 'reach_error' is uncalled: 1 LLoC (correct.c:1:1-1:20)
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 2
+    dead: 1 (1 in uncalled functions)
+    total lines: 3
+  [Info][Witness] witness validation summary:
+    confirmed: 0
+    unconfirmed: 0
+    refuted: 0
+    error: 0
+    unchecked: 0
+    unsupported: 0
+    disabled: 0
+    total validation entries: 0
+  SV-COMP result: true
+
+If a correct progtam cannot be proven correct, return `unknown` for the violation witness:
+
+  $ goblint --set ana.activated[-] expRelation --enable ana.sv-comp.functions --enable ana.sv-comp.enabled --set witness.yaml.entry-types[+] violation_sequence --set ana.specification "CHECK( init(main()), LTL(G ! call(reach_error())) )" correct-hard.c --set witness.yaml.validate correct-hard.yml
+  [Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 7
+    dead: 0
+    total lines: 7
+  [Info][Witness] witness validation summary:
+    confirmed: 0
+    unconfirmed: 0
+    refuted: 0
+    error: 0
+    unchecked: 0
+    unsupported: 0
+    disabled: 0
+    total validation entries: 0
+  SV-COMP result: unknown
+
+Violation witness for an incorrect program cannot be proven correct, so return `unknown`:
+
+  $ goblint --enable ana.sv-comp.enabled --set witness.yaml.entry-types[+] violation_sequence --set ana.specification "CHECK( init(main()), LTL(G ! call(reach_error())) )" incorrect.c --set witness.yaml.validate incorrect.yml
+  [Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 4
+    dead: 0
+    total lines: 4
+  [Info][Witness] witness validation summary:
+    confirmed: 0
+    unconfirmed: 0
+    refuted: 0
+    error: 0
+    unchecked: 0
+    unsupported: 0
+    disabled: 0
+    total validation entries: 0
+  SV-COMP result: unknown
diff --git a/tests/util/yamlWitnessStrip.ml b/tests/util/yamlWitnessStrip.ml
index 8a5046d6ff..1c015b0f67 100644
--- a/tests/util/yamlWitnessStrip.ml
+++ b/tests/util/yamlWitnessStrip.ml
@@ -10,8 +10,13 @@ struct
 
   let strip_file_hashes {entry_type} =
     let stripped_file_hash = "$FILE_HASH" in
-    let location_strip_file_hash location: Location.t =
-      {location with file_hash = stripped_file_hash}
+    let location_strip_file_hash (location: Location.t): Location.t =
+      let file_hash =
+        match location.file_hash with
+        | Some _ -> Some stripped_file_hash (* TODO: or just map to None always? *)
+        | None -> None
+      in
+      {location with file_hash}
     in
     let target_strip_file_hash target: Target.t =
       {target with file_hash = stripped_file_hash}
@@ -26,6 +31,25 @@ struct
       in
       {invariant_type}
     in
+    let waypoint_strip_file_hash ({waypoint_type}: ViolationSequence.Waypoint.t): ViolationSequence.Waypoint.t =
+      let waypoint_type: ViolationSequence.WaypointType.t =
+        match waypoint_type with
+        | Assumption x ->
+          Assumption {x with location = location_strip_file_hash x.location}
+        | Target x ->
+          Target {x with location = location_strip_file_hash x.location}
+        | FunctionEnter x ->
+          FunctionEnter {x with location = location_strip_file_hash x.location}
+        | FunctionReturn x ->
+          FunctionReturn {x with location = location_strip_file_hash x.location}
+        | Branching x ->
+          Branching {x with location = location_strip_file_hash x.location}
+      in
+      {waypoint_type}
+    in
+    let segment_strip_file_hash ({segment}: ViolationSequence.Segment.t): ViolationSequence.Segment.t =
+      {segment = List.map waypoint_strip_file_hash segment}
+    in
     let entry_type: EntryType.t =
       match entry_type with
       | LocationInvariant x ->
@@ -42,6 +66,8 @@ struct
         PreconditionLoopInvariantCertificate {x with target = target_strip_file_hash x.target}
       | InvariantSet x ->
         InvariantSet {content = List.map invariant_strip_file_hash x.content}
+      | ViolationSequence x ->
+        ViolationSequence {content = List.map segment_strip_file_hash x.content}
     in
     {entry_type}