diff --git a/.git-blame-ignore-revs b/.git-blame-ignore-revs
index 53dd9114cc..95105e8616 100644
--- a/.git-blame-ignore-revs
+++ b/.git-blame-ignore-revs
@@ -31,3 +31,6 @@ ec8611a3a72ae0d95ec82ffee16c5c4785111aa1
 
 # fix indentation in baseInvariant
 f3ffd5e45c034574020f56519ccdb021da2a1479
+
+# Fix indentation in various non-legacy code
+c3e2cc848479ae86de5542b6ab0e75a74e9cf8c9
diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml
index 1d73e037f4..d1f7fb09e0 100644
--- a/.github/workflows/docs.yml
+++ b/.github/workflows/docs.yml
@@ -55,7 +55,7 @@ jobs:
         run: opam exec -- dune build @doc
 
       - name: Upload artifact
-        uses: actions/upload-pages-artifact@v2
+        uses: actions/upload-pages-artifact@v3
         with:
           path: _build/default/_doc/_html/
 
@@ -68,4 +68,4 @@ jobs:
     steps:
       - name: Deploy to GitHub Pages
         id: deployment
-        uses: actions/deploy-pages@v3
+        uses: actions/deploy-pages@v4
diff --git a/.github/workflows/locked.yml b/.github/workflows/locked.yml
index f28e21e147..505384f672 100644
--- a/.github/workflows/locked.yml
+++ b/.github/workflows/locked.yml
@@ -180,7 +180,7 @@ jobs:
         run: ./make.sh nat
 
       - name: Build Gobview
-        run: opam exec -- dune build gobview
+        run: ./make.sh view
 
       - name: Install selenium
         run: pip3 install selenium webdriver-manager
diff --git a/.github/workflows/unlocked.yml b/.github/workflows/unlocked.yml
index 956a03ea32..6ef35fb176 100644
--- a/.github/workflows/unlocked.yml
+++ b/.github/workflows/unlocked.yml
@@ -34,9 +34,6 @@ jobs:
           - os: ubuntu-latest
             ocaml-compiler: 4.14.x
             z3: true
-          - os: ubuntu-latest
-            ocaml-compiler: 5.0.0
-            apron: false
 
     # 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
@@ -65,7 +62,7 @@ jobs:
         if: ${{ matrix.apron }}
         run: |
           opam depext apron
-          opam install apron
+          opam install apron mlgmpidl.1.2.15
 
       - name: Install Z3 dependencies
         if: ${{ matrix.z3 }}
@@ -159,7 +156,7 @@ jobs:
       - name: Install Apron dependencies
         run: |
           opam depext apron
-          opam install apron
+          opam install apron mlgmpidl.1.2.15
 
       - name: Build
         if: ${{ false }}
@@ -280,7 +277,7 @@ jobs:
       - name: Install Apron dependencies
         run: |
           opam depext apron
-          opam install apron
+          opam install apron mlgmpidl.1.2.15
 
       - name: Symlink installed goblint to repository # because tests want to use locally built one
         run: ln -s $(opam exec -- which goblint) goblint
diff --git a/.gitignore b/.gitignore
index faf1513653..c3fe37f6ab 100644
--- a/.gitignore
+++ b/.gitignore
@@ -10,6 +10,7 @@ goblint
 goblint.byte
 goblint.json
 goblint.domaintest
+goblint_http.exe
 src/config*.ml
 tests/bench.txt
 .DS_Store
diff --git a/docs/user-guide/annotating.md b/docs/user-guide/annotating.md
index cdfb892ffe..8312869ef9 100644
--- a/docs/user-guide/annotating.md
+++ b/docs/user-guide/annotating.md
@@ -66,3 +66,4 @@ Include `goblint.h` when using these.
 * `__goblint_assume_join(id)` is like `pthread_join(id, NULL)`, but considers the given thread IDs must-joined even if Goblint cannot, e.g. due to non-uniqueness.
   Notably, this annotation can be used after a threads joining loop to make the assumption that the loop correctly joined all those threads.
   _Misuse of this annotation can cause unsoundness._
+* `__goblint_globalize(ptr)` forces all data potentially pointed to by `ptr` to be treated as global by simulating it escaping the thread.
diff --git a/docs/user-guide/inspecting.md b/docs/user-guide/inspecting.md
index 266a4866c6..6ea08db1f4 100644
--- a/docs/user-guide/inspecting.md
+++ b/docs/user-guide/inspecting.md
@@ -18,11 +18,10 @@ For the initial setup:
 
 To build GobView (also for development):
 
-1. Run `dune build gobview` in the analyzer directory to build the web UI
-2. The executable for the http-server can then be found in the directory `./_build/default/gobview/goblint-http-server`. It takes the analyzer directory and additional Goblint configurations such as the files to be analyzed as parameters. Run it e.g. with the following command:\
-`./_build/default/gobview/goblint-http-server/goblint_http.exe -with-goblint ../analyzer/goblint -goblint --set files[+] "../analyzer/tests/regression/00-sanity/01-assert.c"`
-
-4. Visit <http://localhost:8080>
+1. Run `make view` in the analyzer directory to build the web UI
+2. The executable `goblint_http.exe` takes the analyzer directory and additional Goblint configurations such as the files to be analyzed as parameters. Run it e.g. with the following command:\
+`./goblint_http.exe tests/regression/00-sanity/01-assert.c`
+3. Visit <http://localhost:8080>
 
 ## Witnesses
 
diff --git a/dune-project b/dune-project
index de6e955e60..d6ae4be7e7 100644
--- a/dune-project
+++ b/dune-project
@@ -59,6 +59,7 @@
   )
   (conflicts
     (result (< 1.5)) ; transitive dependency, overrides standard Result module and doesn't have map_error, bind
+    (ez-conf-lib (= 1)) ; https://github.com/nberth/ez-conf-lib/issues/3
   )
   (sites
     (share lib)
diff --git a/goblint.opam b/goblint.opam
index 8ccde7c6ba..d7724aad34 100644
--- a/goblint.opam
+++ b/goblint.opam
@@ -54,6 +54,7 @@ depends: [
 depopts: ["apron" "z3"]
 conflicts: [
   "result" {< "1.5"}
+  "ez-conf-lib" {= "1"}
 ]
 build: [
   ["dune" "subst"] {dev}
diff --git a/goblint.opam.locked b/goblint.opam.locked
index 5224d5aa18..2bb831d6ba 100644
--- a/goblint.opam.locked
+++ b/goblint.opam.locked
@@ -125,6 +125,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 available: os-distribution != "alpine" & arch != "arm64"
 conflicts: [
   "result" {< "1.5"}
+  "ez-conf-lib" {= "1"}
 ]
 post-messages: [
   "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}
diff --git a/gobview b/gobview
index 581a3e2e06..b5ab4dbd7b 160000
--- a/gobview
+++ b/gobview
@@ -1 +1 @@
-Subproject commit 581a3e2e06f7f076b05688e2e7085db36de3e260
+Subproject commit b5ab4dbd7b1b1dc4f0bf2a912012cb1879f54903
diff --git a/lib/goblint/runtime/include/goblint.h b/lib/goblint/runtime/include/goblint.h
index af87035d33..8b32bf6ccb 100644
--- a/lib/goblint/runtime/include/goblint.h
+++ b/lib/goblint/runtime/include/goblint.h
@@ -3,6 +3,7 @@ void __goblint_assume(int exp);
 void __goblint_assert(int exp);
 
 void __goblint_assume_join(/* pthread_t thread */); // undeclared argument to avoid pthread.h interfering with Linux kernel headers
+void __goblint_globalize(void *ptr);
 
 void __goblint_split_begin(int exp);
 void __goblint_split_end(int exp);
diff --git a/make.sh b/make.sh
index af1411a8d3..c4ff24c114 100755
--- a/make.sh
+++ b/make.sh
@@ -17,7 +17,6 @@ rule() {
     clean)
       git clean -X -f
       dune clean
-    ;; gen) gen
     ;; nat*)
       eval $(opam config env)
       dune build $TARGET.exe &&
@@ -33,10 +32,9 @@ rule() {
       dune build --profile=release $TARGET.exe &&
       rm -f goblint &&
       cp _build/default/$TARGET.exe goblint
-    # alternatives to .exe: .bc (bytecode), .bc.js (js_of_ocaml), see https://dune.readthedocs.io/en/stable/dune-files.html#executable
-    ;; js) # https://dune.readthedocs.io/en/stable/jsoo.html
-      dune build $TARGET.bc.js &&
-      node _build/default/$TARGET.bc.js
+    ;; view)
+      eval $(opam config env)
+      dune build gobview
     ;; watch)
       eval $(opam config env)
       # dune build -w $TARGET.exe
@@ -61,8 +59,6 @@ rule() {
       dune build goblint.byte &&
       rm -f goblint.byte &&
       cp _build/default/goblint.byte goblint.byte
-    # ;; tag*)
-    #   otags -vi `find src/ -iregex [^.]*\.mli?`
 
     # setup, dependencies
     ;; deps)
@@ -98,8 +94,6 @@ rule() {
       tar xf master.tar.gz && rm master.tar.gz
       rm -rf linux-headers && mv linux-headers-master linux-headers
       for n in $(compgen -c gcc- | sed 's/gcc-//'); do if [ $n != 5 ]; then cp -n linux-headers/include/linux/compiler-gcc{5,$n}.h; fi; done
-    ;; lock)
-      opam lock
     ;; npm)
       if test ! -e "webapp/package.json"; then
         git submodule update --init --recursive webapp
@@ -115,8 +109,6 @@ rule() {
     ;; setup_gobview )
       [[ -f gobview/gobview.opam ]] || git submodule update --init gobview
       opam install --deps-only --locked gobview/
-    # ;; watch)
-    #   fswatch --event Updated -e $TARGET.ml src/ | xargs -n1 -I{} make
     ;; install)
       eval $(opam config env)
       dune build @install
@@ -148,16 +140,6 @@ rule() {
       ./scripts/update_suite.rb # run regression tests
     ;; testci)
       ruby scripts/update_suite.rb -s -d # -s: run tests sequentially instead of in parallel such that output is not scrambled, -d shows some stats?
-    ;; travis) # run a travis docker container with the files tracked by git - intended to debug setup problems on travis-ci.com
-      echo "run ./scripts/travis-ci.sh to setup ocaml"
-      # echo "bind-mount cwd: beware that cwd of host can be modified and IO is very slow!"
-      # docker run -it -u travis -v $(pwd):$(pwd):delegated -w $(pwd) travisci/ci-garnet:packer-1515445631-7dfb2e1 bash
-      echo "copy cwd w/o git-ignored files: changes in container won't affect host's cwd."
-      # cp cwd (with .git, _opam, _build): 1m51s, cp ls-files: 0.5s
-      docker run -it -u travis -v `pwd`:/analyzer:ro,delegated -w /home/travis travisci/ci-garnet:packer-1515445631-7dfb2e1 bash -c 'cd /analyzer; mkdir ~/a; cp --parents $(git ls-files) ~/a; cd ~/a; bash'
-    ;; server)
-      rsync -avz --delete --exclude='/.git' --exclude='server.sh' --exclude-from="$(git ls-files --exclude-standard -oi --directory > /tmp/excludes; echo /tmp/excludes)" . serverseidl6.informatik.tu-muenchen.de:~/analyzer2
-      ssh serverseidl6.informatik.tu-muenchen.de 'cd ~/analyzer2; make nat && make test'
 
     ;; *)
       echo "Unknown action '$1'. Try clean, native, byte, profile or doc.";;
diff --git a/scripts/test-gobview.py b/scripts/test-gobview.py
index dcff1eac81..f5961108d7 100644
--- a/scripts/test-gobview.py
+++ b/scripts/test-gobview.py
@@ -24,10 +24,8 @@ def cleanup(browser, thread):
 # serve GobView in different thread so it does not block the testing
 def serve():
   global p
-  goblint_http_path = '_build/default/gobview/goblint-http-server/goblint_http.exe'
-  p = subprocess.Popen(['./' + goblint_http_path,
-                  '-with-goblint', '../analyzer/goblint',
-                  '-goblint', '--set', 'files[+]', '"../analyzer/tests/regression/00-sanity/01-assert.c"'])
+  goblint_http_path = './goblint_http.exe'
+  p = subprocess.Popen([goblint_http_path, 'tests/regression/00-sanity/01-assert.c'])
 
 print("serving at port", PORT)
 thread = Thread(target=serve, args=())
diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml
index b4e23b65cc..40f3e57065 100644
--- a/src/analyses/apron/relationPriv.apron.ml
+++ b/src/analyses/apron/relationPriv.apron.ml
@@ -451,7 +451,7 @@ struct
 end
 
 (** Per-mutex meet. *)
-module PerMutexMeetPriv : S = functor (RD: RelationDomain.RD) ->
+module PerMutexMeetPriv (Param: AtomicParam) : S = functor (RD: RelationDomain.RD) ->
 struct
   open CommonPerMutex(RD)
   include MutexGlobals
@@ -469,6 +469,8 @@ struct
 
   let startstate () = ()
 
+  let atomic_mutex = LockDomain.Addr.of_var LibraryFunctions.verifier_atomic_var
+
   let get_m_with_mutex_inits ask getg m =
     let get_m = getg (V.mutex m) in
     let get_mutex_inits = getg V.mutex_inits in
@@ -476,53 +478,96 @@ struct
     RD.join get_m get_mutex_inits'
 
   let get_mutex_global_g_with_mutex_inits ask getg g =
-    let get_mutex_global_g = getg (V.global g) in
-    let get_mutex_inits = getg V.mutex_inits in
     let g_var = AV.global g in
+    let get_mutex_global_g =
+      if Param.handle_atomic then (
+        (* Unprotected invariant is one big relation. *)
+        RD.keep_vars (getg (V.mutex atomic_mutex)) [g_var]
+      )
+      else
+        getg (V.global g)
+    in
+    let get_mutex_inits = getg V.mutex_inits in
     let get_mutex_inits' = RD.keep_vars get_mutex_inits [g_var] in
     RD.join get_mutex_global_g get_mutex_inits'
 
-  let read_global ask getg (st: relation_components_t) g x: RD.t =
+  let get_mutex_global_g_with_mutex_inits_atomic ask getg =
+    (* Unprotected invariant is one big relation. *)
+    let get_mutex_global_g = getg (V.mutex atomic_mutex) in
+    let get_mutex_inits = getg V.mutex_inits in
+    RD.join get_mutex_global_g get_mutex_inits
+
+  let read_global (ask: Q.ask) getg (st: relation_components_t) g x: RD.t =
+    let atomic = Param.handle_atomic && ask.f MustBeAtomic in
     let rel = st.rel in
     (* lock *)
-    let rel = RD.meet rel (get_mutex_global_g_with_mutex_inits ask getg g) in
+    let rel =
+      if atomic && RD.mem_var rel (AV.global g) then
+        rel (* Read previous unpublished unprotected write in current atomic section. *)
+      else if atomic then
+        RD.meet rel (get_mutex_global_g_with_mutex_inits_atomic ask getg) (* Read unprotected invariant as full relation. *)
+      else
+        RD.meet rel (get_mutex_global_g_with_mutex_inits ask getg g)
+    in
     (* read *)
     let g_var = AV.global g in
     let x_var = AV.local x in
     let rel_local = RD.add_vars rel [g_var] in
     let rel_local = RD.assign_var rel_local x_var g_var in
     (* unlock *)
-    let rel_local' =
-      if is_unprotected ask g then
-        RD.remove_vars rel_local [g_var]
-      else
-        rel_local
-    in
-    rel_local'
+    if not atomic then (
+      let rel_local' =
+        if is_unprotected ask g then
+          RD.remove_vars rel_local [g_var]
+        else
+          rel_local
+      in
+      rel_local'
+    )
+    else
+      rel_local (* Keep write local as if it were protected by the atomic section. *)
 
-  let write_global ?(invariant=false) ask getg sideg (st: relation_components_t) g x: relation_components_t =
+  let write_global ?(invariant=false) (ask: Q.ask) getg sideg (st: relation_components_t) g x: relation_components_t =
+    let atomic = Param.handle_atomic && ask.f MustBeAtomic in
     let rel = st.rel in
     (* lock *)
-    let rel = RD.meet rel (get_mutex_global_g_with_mutex_inits ask getg g) in
+    let rel =
+      if atomic && RD.mem_var rel (AV.global g) then
+        rel (* Read previous unpublished unprotected write in current atomic section. *)
+      else if atomic then
+        RD.meet rel (get_mutex_global_g_with_mutex_inits_atomic ask getg) (* Read unprotected invariant as full relation. *)
+      else
+        RD.meet rel (get_mutex_global_g_with_mutex_inits ask getg g)
+    in
     (* write *)
     let g_var = AV.global g in
     let x_var = AV.local x in
     let rel_local = RD.add_vars rel [g_var] in
     let rel_local = RD.assign_var rel_local g_var x_var in
     (* unlock *)
-    let rel_side = RD.keep_vars rel_local [g_var] in
-    sideg (V.global g) rel_side;
-    let rel_local' =
-      if is_unprotected ask g then
-        RD.remove_vars rel_local [g_var]
+    if not atomic then (
+      let rel_side = RD.keep_vars rel_local [g_var] in
+      if Param.handle_atomic then
+        sideg (V.mutex atomic_mutex) rel_side (* Unprotected invariant is one big relation. *)
       else
-        rel_local
-    in
-    {st with rel = rel_local'}
+        sideg (V.global g) rel_side;
+      let rel_local' =
+        if is_unprotected ask g then
+          RD.remove_vars rel_local [g_var]
+        else
+          rel_local
+      in
+      {st with rel = rel_local'}
+    )
+    else
+      (* Delay publishing unprotected write in the atomic section. *)
+      {st with rel = rel_local} (* 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
     (* TODO: somehow actually unneeded here? *)
-    if Locksets.(not (Lockset.mem m (current_lockset ask))) then (
+    if not atomic && Locksets.(not (Lockset.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. *)
@@ -531,14 +576,37 @@ struct
       {st with rel = rel'}
     )
     else
+      (* Atomic section locking is recursive. *)
       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 rel = st.rel in
-    let rel_side = keep_only_protected_globals ask m rel in
-    sideg (V.mutex m) rel_side;
-    let rel_local = remove_globals_unprotected_after_unlock ask m rel in
-    {st with rel = rel_local}
+    if not atomic then (
+      let rel_side = keep_only_protected_globals ask m rel in
+      sideg (V.mutex m) rel_side;
+      let rel_local = remove_globals_unprotected_after_unlock ask m rel in
+      {st with rel = rel_local}
+    )
+    else (
+      (* Publish delayed unprotected write as if it were protected by the atomic section. *)
+      let rel_side = RD.keep_filter rel (fun var ->
+          match AV.find_metadata var with
+          | Some (Global g) -> true
+          | _ -> false
+        )
+      in
+      (* Unprotected invariant is one big relation. *)
+      sideg (V.mutex atomic_mutex) rel_side;
+      let rel_local =
+        let newly_unprot var = match AV.find_metadata var with
+          | Some (Global g) -> is_unprotected_without ask g atomic_mutex
+          | _ -> false
+        in
+        RD.remove_filter rel newly_unprot
+      in
+      {st with rel = rel_local}
+    )
 
   let thread_join ?(force=false) ask getg exp st = st
   let thread_return ask getg sideg tid st = st
@@ -843,7 +911,7 @@ struct
 end
 
 (** Per-mutex meet with TIDs. *)
-module PerMutexMeetPrivTID (Digest: Digest) (Cluster: ClusterArg): S  = functor (RD: RelationDomain.RD) ->
+module PerMutexMeetPrivTID (Param: AtomicParam) (Digest: Digest) (Cluster: ClusterArg): S  = functor (RD: RelationDomain.RD) ->
 struct
   open CommonPerMutex(RD)
   include MutexGlobals
@@ -886,8 +954,18 @@ struct
     if M.tracing then M.traceu "relationpriv" "-> %a\n" LRD.pretty r;
     r
 
+  let atomic_mutex = LockDomain.Addr.of_var LibraryFunctions.verifier_atomic_var
+
   let get_mutex_global_g_with_mutex_inits inits ask getg g =
-    let get_mutex_global_g = get_relevant_writes_nofilter ask @@ G.mutex @@ getg (V.global g) in
+    let get_mutex_global_g =
+      if Param.handle_atomic then (
+        (* Unprotected invariant is one big relation. *)
+        get_relevant_writes_nofilter ask @@ G.mutex @@ getg (V.mutex atomic_mutex)
+        |> Cluster.keep_global g
+      )
+      else
+        get_relevant_writes_nofilter ask @@ G.mutex @@ getg (V.global g)
+    in
     if M.tracing then M.traceli "relationpriv" "get_mutex_global_g_with_mutex_inits %a\n  get=%a\n" CilType.Varinfo.pretty g LRD.pretty get_mutex_global_g;
     let r =
       if not inits then
@@ -901,60 +979,96 @@ struct
     if M.tracing then M.traceu "relationpriv" "-> %a\n" LRD.pretty r;
     r
 
-  let read_global ask getg (st: relation_components_t) g x: RD.t =
+  let get_mutex_global_g_with_mutex_inits_atomic inits ask getg =
+    (* Unprotected invariant is one big relation. *)
+    let get_mutex_global_g = get_relevant_writes_nofilter ask @@ G.mutex @@ getg (V.mutex atomic_mutex) in
+    if not inits then
+      get_mutex_global_g
+    else
+      let get_mutex_inits = merge_all @@ G.mutex @@ getg V.mutex_inits in
+      LRD.join get_mutex_global_g get_mutex_inits
+
+  let read_global (ask: Q.ask) getg (st: relation_components_t) g x: RD.t =
+    let atomic = Param.handle_atomic && ask.f MustBeAtomic in
     let _,lmust,l = st.priv in
     let rel = st.rel in
     let lm = LLock.global g in
     (* lock *)
-    let tmp = get_mutex_global_g_with_mutex_inits (not (LMust.mem lm lmust)) ask getg g in
     let local_m = BatOption.default (LRD.bot ()) (L.find_opt lm l) in
     (* Additionally filter get_m in case it contains variables it no longer protects. E.g. in 36/22. *)
-    let rel = Cluster.lock rel local_m tmp in
+    let rel =
+      if atomic && RD.mem_var rel (AV.global g) then
+        rel (* Read previous unpublished unprotected write in current atomic section. *)
+      else if atomic then
+        Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits_atomic (not (LMust.mem lm lmust)) ask getg) (* Read unprotected invariant as full relation. *)
+      else
+        Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits (not (LMust.mem lm lmust)) ask getg g)
+    in
     (* read *)
     let g_var = AV.global g in
     let x_var = AV.local x in
     let rel_local = RD.add_vars rel [g_var] in
     let rel_local = RD.assign_var rel_local x_var g_var in
     (* unlock *)
-    let rel_local' =
-      if is_unprotected ask g then
-        RD.remove_vars rel_local [g_var]
-      else
-        rel_local
-    in
-    rel_local'
+    if not atomic then (
+      let rel_local' =
+        if is_unprotected ask g then
+          RD.remove_vars rel_local [g_var]
+        else
+          rel_local
+      in
+      rel_local'
+    )
+    else
+      rel_local (* Keep write local as if it were protected by the atomic section. *)
 
   let write_global ?(invariant=false) (ask:Q.ask) getg sideg (st: relation_components_t) g x: relation_components_t =
+    let atomic = Param.handle_atomic && ask.f MustBeAtomic in
     let w,lmust,l = st.priv in
     let lm = LLock.global g in
     let rel = st.rel in
     (* lock *)
-    let tmp = get_mutex_global_g_with_mutex_inits (not (LMust.mem lm lmust)) ask getg g in
     let local_m = BatOption.default (LRD.bot ()) (L.find_opt lm l) in
     (* Additionally filter get_m in case it contains variables it no longer protects. E.g. in 36/22. *)
-    let rel = Cluster.lock rel local_m tmp in
+    let rel =
+      if atomic && RD.mem_var rel (AV.global g) then
+        rel (* Read previous unpublished unprotected write in current atomic section. *)
+      else if atomic then
+        Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits_atomic (not (LMust.mem lm lmust)) ask getg) (* Read unprotected invariant as full relation. *)
+      else
+        Cluster.lock rel local_m (get_mutex_global_g_with_mutex_inits (not (LMust.mem lm lmust)) ask getg g)
+    in
     (* write *)
     let g_var = AV.global g in
     let x_var = AV.local x in
     let rel_local = RD.add_vars rel [g_var] in
     let rel_local = RD.assign_var rel_local g_var x_var in
     (* unlock *)
-    let rel_side = RD.keep_vars rel_local [g_var] in
-    let rel_side = Cluster.unlock (W.singleton g) rel_side in
-    let digest = Digest.current ask in
-    let sidev = GMutex.singleton digest rel_side in
-    sideg (V.global g) (G.create_global sidev);
-    let l' = L.add lm rel_side l in
-    let rel_local' =
-      if is_unprotected ask g then
-        RD.remove_vars rel_local [g_var]
+    if not atomic then (
+      let rel_side = RD.keep_vars rel_local [g_var] in
+      let rel_side = Cluster.unlock (W.singleton g) rel_side in
+      let digest = Digest.current ask in
+      let sidev = GMutex.singleton digest rel_side in
+      if Param.handle_atomic then
+        sideg (V.mutex atomic_mutex) (G.create_global sidev) (* Unprotected invariant is one big relation. *)
       else
-        rel_local
-    in
-    {rel = rel_local'; priv = (W.add g w,LMust.add lm lmust,l')}
+        sideg (V.global g) (G.create_global sidev);
+      let l' = L.add lm rel_side l in
+      let rel_local' =
+        if is_unprotected ask g then
+          RD.remove_vars rel_local [g_var]
+        else
+          rel_local
+      in
+      {rel = rel_local'; priv = (W.add g w,LMust.add lm lmust,l')}
+    )
+    else
+      (* Delay publishing unprotected write in the atomic section. *)
+      {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 =
-    if Locksets.(not (Lockset.mem m (current_lockset ask))) then (
+    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 rel = st.rel in
       let _,lmust,l = st.priv in
       let lm = LLock.mutex m in
@@ -966,25 +1080,57 @@ struct
       {st with rel}
     )
     else
+      (* Atomic section locking is recursive. *)
       st (* sound w.r.t. recursive lock *)
 
+  let keep_only_globals ask m oct =
+    let protected var = match AV.find_metadata var with
+      | Some (Global g) -> true
+      | _ -> false
+    in
+    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 rel = st.rel in
     let w,lmust,l = st.priv in
-    let rel_local = remove_globals_unprotected_after_unlock ask m rel in
-    let w' = W.filter (fun v -> not (is_unprotected_without ask v m)) w in
-    let side_needed = W.exists (fun v -> is_protected_by ask m v) w in
-    if not side_needed then
-      {rel = rel_local; priv = (w',lmust,l)}
-    else
-      let rel_side = keep_only_protected_globals ask m rel in
-      let rel_side = Cluster.unlock w rel_side in
-      let digest = Digest.current ask in
-      let sidev = GMutex.singleton digest rel_side in
-      sideg (V.mutex m) (G.create_mutex sidev);
-      let lm = LLock.mutex m in
-      let l' = L.add lm rel_side l in
-      {rel = rel_local; priv = (w',LMust.add lm lmust,l')}
+    if not atomic then (
+      let rel_local = remove_globals_unprotected_after_unlock ask m rel in
+      let w' = W.filter (fun v -> not (is_unprotected_without ask v m)) w in
+      let side_needed = W.exists (fun v -> is_protected_by ask m v) w in
+      if not side_needed then
+        {rel = rel_local; priv = (w',lmust,l)}
+      else
+        let rel_side = keep_only_protected_globals ask m rel in
+        let rel_side = Cluster.unlock w rel_side in
+        let digest = Digest.current ask in
+        let sidev = GMutex.singleton digest rel_side in
+        sideg (V.mutex m) (G.create_mutex sidev);
+        let lm = LLock.mutex m in
+        let l' = L.add lm rel_side l in
+        {rel = rel_local; priv = (w',LMust.add lm lmust,l')}
+    )
+    else (
+      (* Publish delayed unprotected write as if it were protected by the atomic section. *)
+      let rel_local = remove_globals_unprotected_after_unlock ask m rel in
+      let w' = W.filter (fun v -> not (is_unprotected_without ask v m)) w in
+      let side_needed = not (W.is_empty w) in
+      if not side_needed then
+        {rel = rel_local; priv = (w',lmust,l)}
+      else
+        let rel_side = keep_only_globals ask m rel in
+        let rel_side = Cluster.unlock w rel_side in
+        let digest = Digest.current ask in
+        let sidev = GMutex.singleton digest rel_side in
+        (* Unprotected invariant is one big relation. *)
+        sideg (V.mutex atomic_mutex) (G.create_mutex sidev);
+        let (lmust', l') = W.fold (fun g (lmust, l) ->
+            let lm = LLock.global g in
+            (LMust.add lm lmust, L.add lm rel_side l)
+          ) w (lmust, l)
+        in
+        {rel = rel_local; priv = (w',lmust',l')}
+    )
 
   let thread_join ?(force=false) (ask:Q.ask) getg exp (st: relation_components_t) =
     let w,lmust,l = st.priv in
@@ -1192,6 +1338,50 @@ struct
     let r = sync ask getg sideg st reason in
     if M.tracing then M.traceu "relationpriv" "-> %a\n" RelComponents.pretty r;
     r
+
+  let escape node ask getg sideg st vs =
+    if M.tracing then M.traceli "relationpriv" "escape\n";
+    if M.tracing then M.trace "relationpriv" "st: %a\n" RelComponents.pretty st;
+    let getg x =
+      let r = getg x in
+      if M.tracing then M.trace "relationpriv" "getg %a -> %a\n" V.pretty x G.pretty r;
+      r
+    in
+    let sideg x v =
+      if M.tracing then M.trace "relationpriv" "sideg %a %a\n" V.pretty x G.pretty v;
+      sideg x v
+    in
+    let r = escape node ask getg sideg st vs in
+    if M.tracing then M.traceu "relationpriv" "-> %a\n" RelComponents.pretty r;
+    r
+
+  let thread_join ?force ask getg e st =
+    if M.tracing then M.traceli "relationpriv" "thread_join\n";
+    if M.tracing then M.trace "relationpriv" "st: %a\n" RelComponents.pretty st;
+    let getg x =
+      let r = getg x in
+      if M.tracing then M.trace "relationpriv" "getg %a -> %a\n" V.pretty x G.pretty r;
+      r
+    in
+    let r = thread_join ?force ask getg e st in
+    if M.tracing then M.traceu "relationpriv" "-> %a\n" RelComponents.pretty r;
+    r
+
+  let thread_return ask getg sideg tid st =
+    if M.tracing then M.traceli "relationpriv" "thread_return\n";
+    if M.tracing then M.trace "relationpriv" "st: %a\n" RelComponents.pretty st;
+    let getg x =
+      let r = getg x in
+      if M.tracing then M.trace "relationpriv" "getg %a -> %a\n" V.pretty x G.pretty r;
+      r
+    in
+    let sideg x v =
+      if M.tracing then M.trace "relationpriv" "sideg %a %a\n" V.pretty x G.pretty v;
+      sideg x v
+    in
+    let r = thread_return ask getg sideg tid st in
+    if M.tracing then M.traceu "relationpriv" "-> %a\n" RelComponents.pretty r;
+    r
 end
 
 
@@ -1202,12 +1392,14 @@ let priv_module: (module S) Lazy.t =
          | "top" -> (module Top : S)
          | "protection" -> (module ProtectionBasedPriv (struct let path_sensitive = false end))
          | "protection-path" -> (module ProtectionBasedPriv (struct let path_sensitive = true end))
-         | "mutex-meet" -> (module PerMutexMeetPriv)
-         | "mutex-meet-tid" -> (module PerMutexMeetPrivTID (ThreadDigest) (NoCluster))
-         | "mutex-meet-tid-cluster12" -> (module PerMutexMeetPrivTID (ThreadDigest) (DownwardClosedCluster (Clustering12)))
-         | "mutex-meet-tid-cluster2" -> (module PerMutexMeetPrivTID (ThreadDigest) (ArbitraryCluster (Clustering2)))
-         | "mutex-meet-tid-cluster-max" -> (module PerMutexMeetPrivTID (ThreadDigest) (ArbitraryCluster (ClusteringMax)))
-         | "mutex-meet-tid-cluster-power" -> (module PerMutexMeetPrivTID (ThreadDigest) (DownwardClosedCluster (ClusteringPower)))
+         | "mutex-meet" -> (module PerMutexMeetPriv (NoAtomic))
+         | "mutex-meet-atomic" -> (module PerMutexMeetPriv (struct let handle_atomic = true end)) (* experimental *)
+         | "mutex-meet-tid" -> (module PerMutexMeetPrivTID (NoAtomic) (ThreadDigest) (NoCluster))
+         | "mutex-meet-tid-atomic" -> (module PerMutexMeetPrivTID (struct let handle_atomic = true end) (ThreadDigest) (NoCluster)) (* experimental *)
+         | "mutex-meet-tid-cluster12" -> (module PerMutexMeetPrivTID (NoAtomic) (ThreadDigest) (DownwardClosedCluster (Clustering12)))
+         | "mutex-meet-tid-cluster2" -> (module PerMutexMeetPrivTID (NoAtomic) (ThreadDigest) (ArbitraryCluster (Clustering2)))
+         | "mutex-meet-tid-cluster-max" -> (module PerMutexMeetPrivTID (NoAtomic) (ThreadDigest) (ArbitraryCluster (ClusteringMax)))
+         | "mutex-meet-tid-cluster-power" -> (module PerMutexMeetPrivTID (NoAtomic) (ThreadDigest) (DownwardClosedCluster (ClusteringPower)))
          | _ -> failwith "ana.relation.privatization: illegal value"
       )
     in
diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml
index 043168ba57..125429231e 100644
--- a/src/analyses/basePriv.ml
+++ b/src/analyses/basePriv.ml
@@ -634,6 +634,8 @@ module type PerGlobalPrivParam =
 sig
   (** Whether to also check unprotectedness by reads for extra precision. *)
   val check_read_unprotected: bool
+
+  include AtomicParam
 end
 
 (** Protection-Based Reading. *)
@@ -671,22 +673,27 @@ struct
 
   let startstate () = P.empty ()
 
-  let read_global ask getg (st: BaseComponents (D).t) x =
+  let read_global (ask: Queries.ask) getg (st: BaseComponents (D).t) x =
     if P.mem x st.priv then
       CPA.find x st.cpa
+    else if Param.handle_atomic && ask.f MustBeAtomic then
+      VD.join (CPA.find x st.cpa) (getg (V.unprotected x)) (* Account for previous unpublished unprotected writes in current atomic section. *)
     else if is_unprotected ask x then
       getg (V.unprotected x) (* CPA unnecessary because all values in GUnprot anyway *)
     else
       VD.join (CPA.find x st.cpa) (getg (V.protected x))
 
-  let write_global ?(invariant=false) ask getg sideg (st: BaseComponents (D).t) x v =
+  let write_global ?(invariant=false) (ask: Queries.ask) getg sideg (st: BaseComponents (D).t) x v =
     if not invariant then (
-      sideg (V.unprotected x) v;
+      if not (Param.handle_atomic && ask.f MustBeAtomic) then
+        sideg (V.unprotected x) v; (* Delay publishing unprotected write in the atomic section. *)
       if !earlyglobs then (* earlyglobs workaround for 13/60 *)
         sideg (V.protected x) v
         (* Unlock after invariant will still side effect refined value (if protected) from CPA, because cannot distinguish from non-invariant write since W is implicit. *)
     );
-    if is_unprotected ask x then
+    if Param.handle_atomic && ask.f MustBeAtomic then
+      {st with cpa = CPA.add x v st.cpa; priv = P.add x st.priv} (* Keep write local as if it were protected by the atomic section. *)
+    else if is_unprotected ask x then
       st
     else
       {st with cpa = CPA.add x v st.cpa; priv = P.add x st.priv}
@@ -694,6 +701,7 @@ struct
   let lock ask getg st m = st
 
   let unlock ask getg sideg (st: BaseComponents (D).t) m =
+    let atomic = Param.handle_atomic && LockDomain.Addr.equal m (LockDomain.Addr.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 *)
@@ -702,6 +710,8 @@ struct
              then inner unlock shouldn't yet publish. *)
           if not Param.check_read_unprotected || is_unprotected_without ask ~write:false x m then
             sideg (V.protected x) v;
+          if atomic then
+            sideg (V.unprotected x) v; (* Publish delayed unprotected write as if it were protected by the atomic section. *)
 
           if is_unprotected_without ask x m then (* is_in_V' *)
             {st with cpa = CPA.remove x st.cpa; priv = P.remove x st.priv}
@@ -1779,8 +1789,10 @@ let priv_module: (module S) Lazy.t =
         | "mutex-oplus" -> (module PerMutexOplusPriv)
         | "mutex-meet" -> (module PerMutexMeetPriv)
         | "mutex-meet-tid" -> (module PerMutexMeetTIDPriv (ThreadDigest))
-        | "protection" -> (module ProtectionBasedPriv (struct let check_read_unprotected = false end))
-        | "protection-read" -> (module ProtectionBasedPriv (struct let check_read_unprotected = true end))
+        | "protection" -> (module ProtectionBasedPriv (struct let check_read_unprotected = false let handle_atomic = false end))
+        | "protection-atomic" -> (module ProtectionBasedPriv (struct let check_read_unprotected = false let handle_atomic = true end)) (* experimental *)
+        | "protection-read" -> (module ProtectionBasedPriv (struct let check_read_unprotected = true let handle_atomic = false end))
+        | "protection-read-atomic" -> (module ProtectionBasedPriv (struct let check_read_unprotected = true let handle_atomic = true end)) (* experimental *)
         | "mine" -> (module MinePriv)
         | "mine-nothread" -> (module MineNoThreadPriv)
         | "mine-W" -> (module MineWPriv (struct let side_effect_global_init = true end))
diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml
index 8c406df665..627b39166e 100644
--- a/src/analyses/commonPriv.ml
+++ b/src/analyses/commonPriv.ml
@@ -9,6 +9,17 @@ module Q = Queries
 module IdxDom = ValueDomain.IndexDomain
 module VD     = BaseDomain.VD
 
+module type AtomicParam =
+sig
+  val handle_atomic: bool
+  (** Whether to handle SV-COMP atomic blocks (experimental). *)
+end
+
+module NoAtomic: AtomicParam =
+struct
+  let handle_atomic = false
+end
+
 module ConfCheck =
 struct
   module RequireMutexActivatedInit =
@@ -110,7 +121,11 @@ end
 
 module Locksets =
 struct
-  module Lock = LockDomain.Addr
+  module Lock =
+  struct
+    include LockDomain.Addr
+    let name () = "lock"
+  end
 
   module Lockset = SetDomain.ToppedSet (Lock) (struct let topname = "All locks" end)
 
@@ -206,7 +221,7 @@ struct
 
   module LLock =
   struct
-    include Printable.Either (Locksets.Lock) (CilType.Varinfo)
+    include Printable.Either (Locksets.Lock) (struct include CilType.Varinfo let name () = "global" end)
     let mutex m = `Left m
     let global x = `Right x
   end
@@ -218,7 +233,11 @@ struct
   end
 
   (* Map from locks to last written values thread-locally *)
-  module L = MapDomain.MapBot_LiftTop (LLock) (LD)
+  module L =
+  struct
+    include MapDomain.MapBot_LiftTop (LLock) (LD)
+    let name () = "L"
+  end
   module GMutex = MapDomain.MapBot_LiftTop (Digest) (LD)
   module GThread = Lattice.Prod (LMust) (L)
 
diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml
index a13c8d6bfd..138f65ab47 100644
--- a/src/analyses/mutexAnalysis.ml
+++ b/src/analyses/mutexAnalysis.ml
@@ -229,7 +229,7 @@ struct
       let mutex_lockset = Lockset.export_locks @@ Lockset.singleton (mutex, true) in
       let protecting = protecting ~write protection v in
       (* TODO: unsound in 29/24, why did we do this before? *)
-      (* if LockDomain.Addr.equal mutex verifier_atomic then
+      (* if LockDomain.Addr.equal mutex (LockDomain.Addr.of_var LF.verifier_atomic_var) then
         true
       else *)
       Mutexes.leq mutex_lockset protecting
diff --git a/src/analyses/threadEscape.ml b/src/analyses/threadEscape.ml
index f5ff3dc50a..21fa3a8cfb 100644
--- a/src/analyses/threadEscape.ml
+++ b/src/analyses/threadEscape.ml
@@ -150,6 +150,9 @@ struct
   let special ctx (lval: lval option) (f:varinfo) (args:exp list) : D.t =
     let desc = LibraryFunctions.find f in
     match desc.special args, f.vname, args with
+    | Globalize ptr, _, _ ->
+      let escaped = escape_rval ctx (Analyses.ask_of_ctx ctx) ptr in
+      D.join ctx.local escaped
     | _, "pthread_setspecific" , [key; pt_value] ->
       let escaped = escape_rval ctx (Analyses.ask_of_ctx ctx) pt_value in
       D.join ctx.local escaped
diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index 4372df13fe..9752a774e5 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -1898,21 +1898,21 @@ struct
   let cast_to ?torg ?no_ov ik = function
     | `Excluded (s,r) ->
       let r' = size ik in
-        if R.leq r r' then (* upcast -> no change *)
-          `Excluded (s, r)
-        else if ik = IBool then (* downcast to bool *)
-          if S.mem Z.zero s then
-            `Definite Z.one
-          else
-            `Excluded (S.empty(), r')
+      if R.leq r r' then (* upcast -> no change *)
+        `Excluded (s, r)
+      else if ik = IBool then (* downcast to bool *)
+        if S.mem Z.zero s then
+          `Definite Z.one
         else
-          (* downcast: may overflow *)
-          (* let s' = S.map (Size.cast ik) s in *)
-          (* We want to filter out all i in s' where (t)x with x in r could be i. *)
-          (* Since this is hard to compute, we just keep all i in s' which overflowed, since those are safe - all i which did not overflow may now be possible due to overflow of r. *)
-          (* S.diff s' s, r' *)
-          (* The above is needed for test 21/03, but not sound! See example https://github.com/goblint/analyzer/pull/95#discussion_r483023140 *)
-          `Excluded (S.empty (), r')
+          `Excluded (S.empty(), r')
+      else
+        (* downcast: may overflow *)
+        (* let s' = S.map (Size.cast ik) s in *)
+        (* We want to filter out all i in s' where (t)x with x in r could be i. *)
+        (* Since this is hard to compute, we just keep all i in s' which overflowed, since those are safe - all i which did not overflow may now be possible due to overflow of r. *)
+        (* S.diff s' s, r' *)
+        (* The above is needed for test 21/03, but not sound! See example https://github.com/goblint/analyzer/pull/95#discussion_r483023140 *)
+        `Excluded (S.empty (), r')
     | `Definite x -> `Definite (Size.cast ik x)
     | `Bot -> `Bot
 
diff --git a/src/cdomain/value/cdomains/intDomain.mli b/src/cdomain/value/cdomains/intDomain.mli
index 632128ff72..63aa47d868 100644
--- a/src/cdomain/value/cdomains/intDomain.mli
+++ b/src/cdomain/value/cdomains/intDomain.mli
@@ -232,7 +232,7 @@ sig
   val invariant: Cil.exp -> t -> Invariant.t
 end
 (** Interface of IntDomain implementations that do not take ikinds for arithmetic operations yet.
-   TODO: Should be ported to S in the future. *)
+    TODO: Should be ported to S in the future. *)
 
 module type S =
 sig
diff --git a/src/cdomain/value/cdomains/valueDomain.ml b/src/cdomain/value/cdomains/valueDomain.ml
index de23a46620..61931bd891 100644
--- a/src/cdomain/value/cdomains/valueDomain.ml
+++ b/src/cdomain/value/cdomains/valueDomain.ml
@@ -413,10 +413,11 @@ struct
           Addr ({ v with vtype = t }, offs) (* HACK: equal varinfo with different type, causes inconsistencies down the line, when we again assume vtype being "right", but joining etc gives no consideration to which type version to keep *)
         | Addr (v, o) as a ->
           begin try Addr (v, (adjust_offs v o None)) (* cast of one address by adjusting the abstract offset *)
-            with CastError s -> (* don't know how to handle this cast :( *)
+            with
+            | CastError s -> (* don't know how to handle this cast :( *)
               M.tracel "caste" "%s\n" s;
               a (* probably garbage, but this is deref's problem *)
-              (*raise (CastError s)*)
+            (*raise (CastError s)*)
             | SizeOfError (s,t) ->
               M.warn "size of error: %s" s;
               a
@@ -471,7 +472,7 @@ struct
            | Int i -> Int(ID.cast_to ?torg (Cilfacade.ptr_ikind ()) i)
            | _ -> v (* TODO: Does it make sense to have things here that are neither Address nor Int? *)
           )
-          (* cast to voidPtr are ignored TODO what happens if our value does not fit? *)
+        (* cast to voidPtr are ignored TODO what happens if our value does not fit? *)
         | TPtr (t,_) ->
           Address (match v with
               | Int x when ID.to_int x = Some Z.zero -> AD.null_ptr
@@ -640,9 +641,9 @@ struct
     let leq_elem:(t ->t -> bool) = smart_leq x_eval_int y_eval_int in (* does not compile without type annotation *)
     match (x,y) with
     | (Struct x, Struct y) ->
-          Structs.leq_with_fct leq_elem x y
+      Structs.leq_with_fct leq_elem x y
     | (Union (f, x), Union (g, y)) ->
-        UnionDomain.Field.leq f g && leq_elem x y
+      UnionDomain.Field.leq f g && leq_elem x y
     | (Array x, Array y) -> CArrays.smart_leq x_eval_int y_eval_int x y
     | _ -> leq x y (* Others can not contain array -> normal leq *)
 
@@ -754,9 +755,9 @@ struct
         (* Remove the first part of an offset, returns (removedPart, remainingOffset) *)
         let removeFirstOffset offset =
           match offset with
-            | Field(f, o) -> Field(f, NoOffset), o
-            | Index(exp, o) -> Index(exp, NoOffset), o
-            | NoOffset -> offset, offset in
+          | Field(f, o) -> Field(f, NoOffset), o
+          | Index(exp, o) -> Index(exp, NoOffset), o
+          | NoOffset -> offset, offset in
         let removed, remaining = removeFirstOffset offset in
         Some (Cil.addOffsetLval removed left), Some(remaining)
       end
@@ -809,39 +810,39 @@ struct
       typeSigWithAttrs (List.filter attrFilter) t
     in
     match left, offset with
-      | Some(Var(_), _), Some(Index(exp, _)) -> (* The offset does not matter here, exp is used to index into this array *)
-        if not (contains_pointer exp) then
-          Some exp
-        else
-          None
-      | Some((Mem(ptr), NoOffset)), Some(NoOffset) ->
-        begin
-          match v with
-          | Some (v') ->
-            begin
-              try
-                (* This should mean the entire expression we have here is a pointer into the array *)
-                if Cil.isArrayType (Cilfacade.typeOfLval v') then
-                  let expr = ptr in
-                  let start_of_array = StartOf v' in
-                  let start_type = typeSigWithoutArraylen (Cilfacade.typeOf start_of_array) in
-                  let expr_type = typeSigWithoutArraylen (Cilfacade.typeOf ptr) in
-                  (* Comparing types for structural equality is incorrect here, use typeSig *)
-                  (* as explained at https://people.eecs.berkeley.edu/~necula/cil/api/Cil.html#TYPEtyp *)
-                  if start_type = expr_type then
-                    Some (equiv_expr expr v')
-                  else
-                    (* If types do not agree here, this means that we were looking at pointers that *)
-                    (* contain more than one array access. Those are not supported. *)
-                    None
+    | Some(Var(_), _), Some(Index(exp, _)) -> (* The offset does not matter here, exp is used to index into this array *)
+      if not (contains_pointer exp) then
+        Some exp
+      else
+        None
+    | Some((Mem(ptr), NoOffset)), Some(NoOffset) ->
+      begin
+        match v with
+        | Some (v') ->
+          begin
+            try
+              (* This should mean the entire expression we have here is a pointer into the array *)
+              if Cil.isArrayType (Cilfacade.typeOfLval v') then
+                let expr = ptr in
+                let start_of_array = StartOf v' in
+                let start_type = typeSigWithoutArraylen (Cilfacade.typeOf start_of_array) in
+                let expr_type = typeSigWithoutArraylen (Cilfacade.typeOf ptr) in
+                (* Comparing types for structural equality is incorrect here, use typeSig *)
+                (* as explained at https://people.eecs.berkeley.edu/~necula/cil/api/Cil.html#TYPEtyp *)
+                if start_type = expr_type then
+                  Some (equiv_expr expr v')
                 else
+                  (* If types do not agree here, this means that we were looking at pointers that *)
+                  (* contain more than one array access. Those are not supported. *)
                   None
-              with (Cilfacade.TypeOfError _) -> None
-            end
-          | _ ->
-            None
-        end
-      | _, _ ->  None
+              else
+                None
+            with (Cilfacade.TypeOfError _) -> None
+          end
+        | _ ->
+          None
+      end
+    | _, _ ->  None
 
   let zero_init_calloced_memory orig x t =
     if orig then
@@ -858,68 +859,68 @@ struct
     let rec do_eval_offset (ask:VDQ.t) f (x:t) (offs:offs) (exp:exp option) (l:lval option) (o:offset option) (v:lval option) (t:typ): t =
       if M.tracing then M.traceli "eval_offset" "do_eval_offset %a %a (%a)\n" pretty x Offs.pretty offs (Pretty.docOpt (CilType.Exp.pretty ())) exp;
       let r =
-      match x, offs with
-      | Blob((va, _, orig) as c), `Index (_, ox) ->
-        begin
-          let l', o' = shift_one_over l o in
-          let ev = do_eval_offset ask f (Blobs.value c) ox exp l' o' v t in
-          zero_init_calloced_memory orig ev t
-        end
-      | Blob((va, _, orig) as c), `Field _ ->
-        begin
-          let l', o' = shift_one_over l o in
-          let ev = do_eval_offset ask f (Blobs.value c) offs exp l' o' v t in
-          zero_init_calloced_memory orig ev t
-        end
-      | Blob((va, _, orig) as c), `NoOffset ->
-      begin
-        let l', o' = shift_one_over l o in
-        let ev = do_eval_offset ask f (Blobs.value c) offs exp l' o' v t in
-        zero_init_calloced_memory orig ev t
-      end
-      | Bot, _ -> Bot
-      | _ ->
-        match offs with
-        | `NoOffset -> x
-        | `Field (fld, offs) when fld.fcomp.cstruct -> begin
-            match x with
-            | Struct str ->
-              let x = Structs.get str fld in
-              let l', o' = shift_one_over l o in
-              do_eval_offset ask f x offs exp l' o' v t
-            | Top -> M.info ~category:Imprecise "Trying to read a field, but the struct is unknown"; top ()
-            | _ -> M.warn ~category:Imprecise ~tags:[Category Program] "Trying to read a field, but was not given a struct"; top ()
+        match x, offs with
+        | Blob((va, _, orig) as c), `Index (_, ox) ->
+          begin
+            let l', o' = shift_one_over l o in
+            let ev = do_eval_offset ask f (Blobs.value c) ox exp l' o' v t in
+            zero_init_calloced_memory orig ev t
           end
-        | `Field (fld, offs) -> begin
-            match x with
-            | Union (`Lifted l_fld, value) ->
-              (match value, fld.ftype with
-               (* only return an actual value if we have a type and return actually the exact same type *)
-               | Float f_value, TFloat(fkind, _) when FD.get_fkind f_value = fkind -> Float f_value
-               | Float _, t -> top_value t
-               | _, TFloat(fkind, _)  when not (Cilfacade.isComplexFKind fkind)-> Float (FD.top_of fkind)
-               | _ ->
-                 let x = cast ~torg:l_fld.ftype fld.ftype value in
-                 let l', o' = shift_one_over l o in
-                 do_eval_offset ask f x offs exp l' o' v t)
-            | Union _ -> top ()
-            | Top -> M.info ~category:Imprecise "Trying to read a field, but the union is unknown"; top ()
-            | _ -> M.warn ~category:Imprecise ~tags:[Category Program] "Trying to read a field, but was not given a union"; top ()
+        | Blob((va, _, orig) as c), `Field _ ->
+          begin
+            let l', o' = shift_one_over l o in
+            let ev = do_eval_offset ask f (Blobs.value c) offs exp l' o' v t in
+            zero_init_calloced_memory orig ev t
           end
-        | `Index (idx, offs) -> begin
+        | Blob((va, _, orig) as c), `NoOffset ->
+          begin
             let l', o' = shift_one_over l o in
-            match x with
-            | Array x ->
-              let e = determine_offset ask l o exp v in
-              do_eval_offset ask f (CArrays.get ask x (e, idx)) offs exp l' o' v t
-            | Address _ ->
-              begin
-                do_eval_offset ask f x offs exp l' o' v t (* this used to be `blob `address -> we ignore the index *)
-              end
-            | x when GobOption.exists (Z.equal Z.zero) (IndexDomain.to_int idx) -> eval_offset ask f x offs exp v t
-            | Top -> M.info ~category:Imprecise "Trying to read an index, but the array is unknown"; top ()
-            | _ -> M.warn ~category:Imprecise ~tags:[Category Program] "Trying to read an index, but was not given an array (%a)" pretty x; top ()
+            let ev = do_eval_offset ask f (Blobs.value c) offs exp l' o' v t in
+            zero_init_calloced_memory orig ev t
           end
+        | Bot, _ -> Bot
+        | _ ->
+          match offs with
+          | `NoOffset -> x
+          | `Field (fld, offs) when fld.fcomp.cstruct -> begin
+              match x with
+              | Struct str ->
+                let x = Structs.get str fld in
+                let l', o' = shift_one_over l o in
+                do_eval_offset ask f x offs exp l' o' v t
+              | Top -> M.info ~category:Imprecise "Trying to read a field, but the struct is unknown"; top ()
+              | _ -> M.warn ~category:Imprecise ~tags:[Category Program] "Trying to read a field, but was not given a struct"; top ()
+            end
+          | `Field (fld, offs) -> begin
+              match x with
+              | Union (`Lifted l_fld, value) ->
+                (match value, fld.ftype with
+                 (* only return an actual value if we have a type and return actually the exact same type *)
+                 | Float f_value, TFloat(fkind, _) when FD.get_fkind f_value = fkind -> Float f_value
+                 | Float _, t -> top_value t
+                 | _, TFloat(fkind, _)  when not (Cilfacade.isComplexFKind fkind)-> Float (FD.top_of fkind)
+                 | _ ->
+                   let x = cast ~torg:l_fld.ftype fld.ftype value in
+                   let l', o' = shift_one_over l o in
+                   do_eval_offset ask f x offs exp l' o' v t)
+              | Union _ -> top ()
+              | Top -> M.info ~category:Imprecise "Trying to read a field, but the union is unknown"; top ()
+              | _ -> M.warn ~category:Imprecise ~tags:[Category Program] "Trying to read a field, but was not given a union"; top ()
+            end
+          | `Index (idx, offs) -> begin
+              let l', o' = shift_one_over l o in
+              match x with
+              | Array x ->
+                let e = determine_offset ask l o exp v in
+                do_eval_offset ask f (CArrays.get ask x (e, idx)) offs exp l' o' v t
+              | Address _ ->
+                begin
+                  do_eval_offset ask f x offs exp l' o' v t (* this used to be `blob `address -> we ignore the index *)
+                end
+              | x when GobOption.exists (Z.equal Z.zero) (IndexDomain.to_int idx) -> eval_offset ask f x offs exp v t
+              | Top -> M.info ~category:Imprecise "Trying to read an index, but the array is unknown"; top ()
+              | _ -> M.warn ~category:Imprecise ~tags:[Category Program] "Trying to read an index, but was not given an array (%a)" pretty x; top ()
+            end
       in
       if M.tracing then M.traceu "eval_offset" "do_eval_offset -> %a\n" pretty r;
       r
@@ -935,72 +936,72 @@ struct
       if M.tracing then M.traceli "update_offset" "do_update_offset %a %a (%a) %a\n" pretty x Offs.pretty offs (Pretty.docOpt (CilType.Exp.pretty ())) exp pretty value;
       let mu = function Blob (Blob (y, s', orig), s, orig2) -> Blob (y, ID.join s s',orig) | x -> x in
       let r =
-      match x, offs with
+        match x, offs with
         | Mutex, _ -> (* hide mutex structure contents, not updated anyway *)
           Mutex
         | Blob (x,s,orig), `Index (_,ofs) ->
-        begin
-          let l', o' = shift_one_over l o in
-          let x = zero_init_calloced_memory orig x t in
-          mu (Blob (join x (do_update_offset ask x ofs value exp l' o' v t), s, orig))
-        end
+          begin
+            let l', o' = shift_one_over l o in
+            let x = zero_init_calloced_memory orig x t in
+            mu (Blob (join x (do_update_offset ask x ofs value exp l' o' v t), s, orig))
+          end
         | Blob (x,s,orig), `Field(f, _) ->
-        begin
-          (* We only have Blob for dynamically allocated memory. In these cases t is the type of the lval used to access it, i.e. for a struct s {int x; int y;} a; accessed via a->x     *)
-          (* will be int. Here, we need a zero_init of the entire contents of the blob though, which we get by taking the associated f.fcomp. Putting [] for attributes is ok, as we don't *)
-          (* consider them in VD *)
-          let l', o' = shift_one_over l o in
-          let x = zero_init_calloced_memory orig x (TComp (f.fcomp, [])) in
-          (* Strong update of scalar variable is possible if the variable is unique and size of written value matches size of blob being written to. *)
-          let do_strong_update =
-            match v with
-            | (Var var, Field (fld,_)) ->
-              let toptype = fld.fcomp in
-              let blob_size_opt = ID.to_int s in
-              not @@ ask.is_multiple var
-              && not @@ Cil.isVoidType t      (* Size of value is known *)
-              && Option.is_some blob_size_opt (* Size of blob is known *)
-              && Z.equal (Option.get blob_size_opt) (Z.of_int @@ Cil.bitsSizeOf (TComp (toptype, []))/8)
-            | _ -> false
-          in
-          if do_strong_update then
-            Blob ((do_update_offset ask x offs value exp l' o' v t), s, orig)
-          else
-            mu (Blob (join x (do_update_offset ask x offs value exp l' o' v t), s, orig))
-        end
-        | Blob (x,s,orig), _ ->
-        begin
-          let l', o' = shift_one_over l o in
-          let x = zero_init_calloced_memory orig x t in
-          (* Strong update of scalar variable is possible if the variable is unique and size of written value matches size of blob being written to. *)
-          let do_strong_update =
-            begin match v with
-              | (Var var, _) ->
+          begin
+            (* We only have Blob for dynamically allocated memory. In these cases t is the type of the lval used to access it, i.e. for a struct s {int x; int y;} a; accessed via a->x     *)
+            (* will be int. Here, we need a zero_init of the entire contents of the blob though, which we get by taking the associated f.fcomp. Putting [] for attributes is ok, as we don't *)
+            (* consider them in VD *)
+            let l', o' = shift_one_over l o in
+            let x = zero_init_calloced_memory orig x (TComp (f.fcomp, [])) in
+            (* Strong update of scalar variable is possible if the variable is unique and size of written value matches size of blob being written to. *)
+            let do_strong_update =
+              match v with
+              | (Var var, Field (fld,_)) ->
+                let toptype = fld.fcomp in
                 let blob_size_opt = ID.to_int s in
                 not @@ ask.is_multiple var
+                && not @@ Cil.isVoidType t      (* Size of value is known *)
                 && Option.is_some blob_size_opt (* Size of blob is known *)
-                && ((
-                    not @@ Cil.isVoidType t     (* Size of value is known *)
-                    && Z.equal (Option.get blob_size_opt) (Z.of_int @@ Cil.alignOf_int t)
-                  ) || blob_destructive)
+                && Z.equal (Option.get blob_size_opt) (Z.of_int @@ Cil.bitsSizeOf (TComp (toptype, []))/8)
               | _ -> false
-            end
-          in
-          if do_strong_update then
-            Blob ((do_update_offset ask x offs value exp l' o' v t), s, orig)
-          else
-            mu (Blob (join x (do_update_offset ask x offs value exp l' o' v t), s, orig))
-        end
-        | Thread _, _ ->
-        (* hack for pthread_t variables *)
-        begin match value with
-          | Thread t -> value (* if actually assigning thread, use value *)
-          | _ ->
-            if !AnalysisState.global_initialization then
-              Thread (ConcDomain.ThreadSet.empty ()) (* if assigning global init (int on linux, ptr to struct on mac), use empty set instead *)
+            in
+            if do_strong_update then
+              Blob ((do_update_offset ask x offs value exp l' o' v t), s, orig)
             else
-              Top
-        end
+              mu (Blob (join x (do_update_offset ask x offs value exp l' o' v t), s, orig))
+          end
+        | Blob (x,s,orig), _ ->
+          begin
+            let l', o' = shift_one_over l o in
+            let x = zero_init_calloced_memory orig x t in
+            (* Strong update of scalar variable is possible if the variable is unique and size of written value matches size of blob being written to. *)
+            let do_strong_update =
+              begin match v with
+                | (Var var, _) ->
+                  let blob_size_opt = ID.to_int s in
+                  not @@ ask.is_multiple var
+                  && Option.is_some blob_size_opt (* Size of blob is known *)
+                  && ((
+                      not @@ Cil.isVoidType t     (* Size of value is known *)
+                      && Z.equal (Option.get blob_size_opt) (Z.of_int @@ Cil.alignOf_int t)
+                    ) || blob_destructive)
+                | _ -> false
+              end
+            in
+            if do_strong_update then
+              Blob ((do_update_offset ask x offs value exp l' o' v t), s, orig)
+            else
+              mu (Blob (join x (do_update_offset ask x offs value exp l' o' v t), s, orig))
+          end
+        | Thread _, _ ->
+          (* hack for pthread_t variables *)
+          begin match value with
+            | Thread t -> value (* if actually assigning thread, use value *)
+            | _ ->
+              if !AnalysisState.global_initialization then
+                Thread (ConcDomain.ThreadSet.empty ()) (* if assigning global init (int on linux, ptr to struct on mac), use empty set instead *)
+              else
+                Top
+          end
         | JmpBuf _, _ ->
           (* hack for jmp_buf variables *)
           begin match value with
@@ -1012,100 +1013,100 @@ struct
               else
                 Top
           end
-      | _ ->
-      let result =
-        match offs with
-        | `NoOffset -> begin
-            match value with
-            | Blob (y, s, orig) -> mu (Blob (join x y, s, orig))
-            | Int _ -> cast t value
-            | _ -> value
-          end
-        | `Field (fld, offs) when fld.fcomp.cstruct -> begin
-            let t = fld.ftype in
-            match x with
-            | Struct str ->
-              begin
-                let l', o' = shift_one_over l o in
-                let value' = do_update_offset ask (Structs.get str fld) offs value exp l' o' v t in
-                Struct (Structs.replace str fld value')
+        | _ ->
+          let result =
+            match offs with
+            | `NoOffset -> begin
+                match value with
+                | Blob (y, s, orig) -> mu (Blob (join x y, s, orig))
+                | Int _ -> cast t value
+                | _ -> value
               end
-            | Bot ->
-              let init_comp compinfo =
-                let nstruct = Structs.create (fun fd -> Bot) compinfo in
-                let init_field nstruct fd = Structs.replace nstruct fd Bot in
-                List.fold_left init_field nstruct compinfo.cfields
-              in
-              let strc = init_comp fld.fcomp in
-              let l', o' = shift_one_over l o in
-              Struct (Structs.replace strc fld (do_update_offset ask Bot offs value exp l' o' v t))
-            | Top -> M.warn ~category:Imprecise "Trying to update a field, but the struct is unknown"; top ()
-            | _ -> M.warn ~category:Imprecise "Trying to update a field, but was not given a struct"; top ()
-          end
-        | `Field (fld, offs) -> begin
-            let t = fld.ftype in
-            let l', o' = shift_one_over l o in
-            match x with
-            | Union (last_fld, prev_val) ->
-              let tempval, tempoffs =
-                if UnionDomain.Field.equal last_fld (`Lifted fld) then
-                  prev_val, offs
-                else begin
-                  match offs with
-                  | `Field (fldi, _) when fldi.fcomp.cstruct ->
-                    (top_value ~varAttr:fld.fattr fld.ftype), offs
-                  | `Field (fldi, _) -> Union (Unions.top ()), offs
-                  | `NoOffset -> top (), offs
-                  | `Index (idx, _) when Cil.isArrayType fld.ftype ->
-                    begin
-                      match fld.ftype with
-                      | TArray(_, l, _) ->
-                        let len = try Cil.lenOfArray l
-                          with Cil.LenOfArray -> 42 (* will not happen, VLA not allowed in union and struct *) in
-                        Array(CArrays.make (IndexDomain.of_int (Cilfacade.ptrdiff_ikind ()) (Z.of_int len)) Top), offs
-                      | _ -> top (), offs (* will not happen*)
+            | `Field (fld, offs) when fld.fcomp.cstruct -> begin
+                let t = fld.ftype in
+                match x with
+                | Struct str ->
+                  begin
+                    let l', o' = shift_one_over l o in
+                    let value' = do_update_offset ask (Structs.get str fld) offs value exp l' o' v t in
+                    Struct (Structs.replace str fld value')
+                  end
+                | Bot ->
+                  let init_comp compinfo =
+                    let nstruct = Structs.create (fun fd -> Bot) compinfo in
+                    let init_field nstruct fd = Structs.replace nstruct fd Bot in
+                    List.fold_left init_field nstruct compinfo.cfields
+                  in
+                  let strc = init_comp fld.fcomp in
+                  let l', o' = shift_one_over l o in
+                  Struct (Structs.replace strc fld (do_update_offset ask Bot offs value exp l' o' v t))
+                | Top -> M.warn ~category:Imprecise "Trying to update a field, but the struct is unknown"; top ()
+                | _ -> M.warn ~category:Imprecise "Trying to update a field, but was not given a struct"; top ()
+              end
+            | `Field (fld, offs) -> begin
+                let t = fld.ftype in
+                let l', o' = shift_one_over l o in
+                match x with
+                | Union (last_fld, prev_val) ->
+                  let tempval, tempoffs =
+                    if UnionDomain.Field.equal last_fld (`Lifted fld) then
+                      prev_val, offs
+                    else begin
+                      match offs with
+                      | `Field (fldi, _) when fldi.fcomp.cstruct ->
+                        (top_value ~varAttr:fld.fattr fld.ftype), offs
+                      | `Field (fldi, _) -> Union (Unions.top ()), offs
+                      | `NoOffset -> top (), offs
+                      | `Index (idx, _) when Cil.isArrayType fld.ftype ->
+                        begin
+                          match fld.ftype with
+                          | TArray(_, l, _) ->
+                            let len = try Cil.lenOfArray l
+                              with Cil.LenOfArray -> 42 (* will not happen, VLA not allowed in union and struct *) in
+                            Array(CArrays.make (IndexDomain.of_int (Cilfacade.ptrdiff_ikind ()) (Z.of_int len)) Top), offs
+                          | _ -> top (), offs (* will not happen*)
+                        end
+                      | `Index (idx, _) when IndexDomain.equal idx (IndexDomain.of_int (Cilfacade.ptrdiff_ikind ()) Z.zero) ->
+                        (* Why does cil index unions? We'll just pick the first field. *)
+                        top (), `Field (List.nth fld.fcomp.cfields 0,`NoOffset)
+                      | _ -> M.warn ~category:Analyzer ~tags:[Category Unsound] "Indexing on a union is unusual, and unsupported by the analyzer";
+                        top (), offs
                     end
-                  | `Index (idx, _) when IndexDomain.equal idx (IndexDomain.of_int (Cilfacade.ptrdiff_ikind ()) Z.zero) ->
-                    (* Why does cil index unions? We'll just pick the first field. *)
-                    top (), `Field (List.nth fld.fcomp.cfields 0,`NoOffset)
-                  | _ -> M.warn ~category:Analyzer ~tags:[Category Unsound] "Indexing on a union is unusual, and unsupported by the analyzer";
-                    top (), offs
-                end
-              in
-              Union (`Lifted fld, do_update_offset ask tempval tempoffs value exp l' o' v t)
-            | Bot -> Union (`Lifted fld, do_update_offset ask Bot offs value exp l' o' v t)
-            | Top -> M.warn ~category:Imprecise "Trying to update a field, but the union is unknown"; top ()
-            | _ -> M.warn ~category:Imprecise "Trying to update a field, but was not given a union"; top ()
-          end
-        | `Index (idx, offs) -> begin
-            let l', o' = shift_one_over l o in
-            match x with
-            | Array x' ->
-              let t = (match t with
-              | TArray(t1 ,_,_) -> t1
-              | _ -> t) in (* This is necessary because t is not a TArray in case of calloc *)
-              let e = determine_offset ask l o exp (Some v) in
-              let new_value_at_index = do_update_offset ask (CArrays.get ask x' (e,idx)) offs value exp l' o' v t in
-              let new_array_value = CArrays.set ask x' (e, idx) new_value_at_index in
-              Array new_array_value
-            | Bot ->
-              let t,len = (match t with
-                  | TArray(t1 ,len,_) -> t1, len
-                  | _ -> t, None) in (* This is necessary because t is not a TArray in case of calloc *)
-              let x' = CArrays.bot () in
-              let e = determine_offset ask l o exp (Some v) in
-              let new_value_at_index = do_update_offset ask Bot offs value exp l' o' v t in
-              let new_array_value =  CArrays.set ask x' (e, idx) new_value_at_index in
-              let len_ci = BatOption.bind len (fun e -> Cil.getInteger @@ Cil.constFold true e) in
-              let len_id = BatOption.map (IndexDomain.of_int (Cilfacade.ptrdiff_ikind ())) len_ci in
-              let newl = BatOption.default (ID.starting (Cilfacade.ptrdiff_ikind ()) Z.zero) len_id in
-              let new_array_value = CArrays.update_length newl new_array_value in
-              Array new_array_value
-            | Top -> M.warn ~category:Imprecise "Trying to update an index, but the array is unknown"; top ()
-            | x when GobOption.exists (Z.equal Z.zero) (IndexDomain.to_int idx) -> do_update_offset ask x offs value exp l' o' v t
-            | _ -> M.warn ~category:Imprecise "Trying to update an index, but was not given an array(%a)" pretty x; top ()
-          end
-      in mu result
+                  in
+                  Union (`Lifted fld, do_update_offset ask tempval tempoffs value exp l' o' v t)
+                | Bot -> Union (`Lifted fld, do_update_offset ask Bot offs value exp l' o' v t)
+                | Top -> M.warn ~category:Imprecise "Trying to update a field, but the union is unknown"; top ()
+                | _ -> M.warn ~category:Imprecise "Trying to update a field, but was not given a union"; top ()
+              end
+            | `Index (idx, offs) -> begin
+                let l', o' = shift_one_over l o in
+                match x with
+                | Array x' ->
+                  let t = (match t with
+                      | TArray(t1 ,_,_) -> t1
+                      | _ -> t) in (* This is necessary because t is not a TArray in case of calloc *)
+                  let e = determine_offset ask l o exp (Some v) in
+                  let new_value_at_index = do_update_offset ask (CArrays.get ask x' (e,idx)) offs value exp l' o' v t in
+                  let new_array_value = CArrays.set ask x' (e, idx) new_value_at_index in
+                  Array new_array_value
+                | Bot ->
+                  let t,len = (match t with
+                      | TArray(t1 ,len,_) -> t1, len
+                      | _ -> t, None) in (* This is necessary because t is not a TArray in case of calloc *)
+                  let x' = CArrays.bot () in
+                  let e = determine_offset ask l o exp (Some v) in
+                  let new_value_at_index = do_update_offset ask Bot offs value exp l' o' v t in
+                  let new_array_value =  CArrays.set ask x' (e, idx) new_value_at_index in
+                  let len_ci = BatOption.bind len (fun e -> Cil.getInteger @@ Cil.constFold true e) in
+                  let len_id = BatOption.map (IndexDomain.of_int (Cilfacade.ptrdiff_ikind ())) len_ci in
+                  let newl = BatOption.default (ID.starting (Cilfacade.ptrdiff_ikind ()) Z.zero) len_id in
+                  let new_array_value = CArrays.update_length newl new_array_value in
+                  Array new_array_value
+                | Top -> M.warn ~category:Imprecise "Trying to update an index, but the array is unknown"; top ()
+                | x when GobOption.exists (Z.equal Z.zero) (IndexDomain.to_int idx) -> do_update_offset ask x offs value exp l' o' v t
+                | _ -> M.warn ~category:Imprecise "Trying to update an index, but was not given an array(%a)" pretty x; top ()
+              end
+          in mu result
       in
       if M.tracing then M.traceu "update_offset" "do_update_offset -> %a\n" pretty r;
       r
@@ -1143,9 +1144,9 @@ struct
         CArrays.fold_left add_affecting_one_level immediately_affecting a
       end
     | Struct s ->
-        Structs.fold (fun x value acc -> add_affecting_one_level acc value) s []
+      Structs.fold (fun x value acc -> add_affecting_one_level acc value) s []
     | Union (f, v) ->
-        affecting_vars v
+      affecting_vars v
     (* Blob can not contain Array *)
     | _ -> []
 
diff --git a/src/cdomain/value/domains/invariantCil.ml b/src/cdomain/value/domains/invariantCil.ml
index 8a1d8f0745..ef0687d6eb 100644
--- a/src/cdomain/value/domains/invariantCil.ml
+++ b/src/cdomain/value/domains/invariantCil.ml
@@ -21,7 +21,11 @@ let exp_replace_original_name e =
 let var_is_in_scope scope vi =
   match Cilfacade.find_scope_fundec vi with
   | None -> vi.vstorage <> Static (* CIL pulls static locals into globals, but they aren't syntactically in global scope *)
-  | Some fd -> CilType.Fundec.equal fd scope
+  | Some fd -> 
+    if CilType.Fundec.equal fd scope then
+      GobConfig.get_bool "witness.invariant.all-locals" || (not @@ hasAttribute "goblint_cil_nested" vi.vattr)
+    else
+      false
 
 class exp_is_in_scope_visitor (scope: fundec) (acc: bool ref) = object
   inherit nopCilVisitor
diff --git a/src/common/util/messages.ml b/src/common/util/messages.ml
index fe090379a1..0bc9449dcb 100644
--- a/src/common/util/messages.ml
+++ b/src/common/util/messages.ml
@@ -61,15 +61,17 @@ end
 
 module Piece =
 struct
+  let context_to_yojson context = `Assoc [("tag", `Int (ControlSpecC.tag context))]
+
   type t = {
     loc: Location.t option; (* only *_each warnings have this, used for deduplication *)
     text: string;
-    context: (ControlSpecC.t [@of_yojson fun x -> Result.Error "ControlSpecC"]) option;
+    context: (ControlSpecC.t [@to_yojson context_to_yojson] [@of_yojson fun x -> Result.Error "ControlSpecC"]) option;
   } [@@deriving eq, ord, hash, yojson]
 
   let text_with_context {text; context; _} =
     match context with
-    | Some context when GobConfig.get_bool "dbg.warn_with_context" -> text ^ " in context " ^ string_of_int (ControlSpecC.hash context) (* TODO: this is kind of useless *)
+    | Some context when GobConfig.get_bool "dbg.warn_with_context" -> text ^ " in context " ^ string_of_int (ControlSpecC.tag context) (* TODO: this is kind of useless *)
     | _ -> text
 end
 
diff --git a/src/config/options.schema.json b/src/config/options.schema.json
index df4b1365db..5d69990499 100644
--- a/src/config/options.schema.json
+++ b/src/config/options.schema.json
@@ -747,7 +747,7 @@
               "description":
                 "Which privatization to use? none/mutex-oplus/mutex-meet/mutex-meet-tid/protection/protection-read/mine/mine-nothread/mine-W/mine-W-noinit/lock/write/write+lock",
               "type": "string",
-              "enum": ["none", "mutex-oplus", "mutex-meet", "protection", "protection-read", "mine", "mine-nothread", "mine-W", "mine-W-noinit", "lock", "write", "write+lock","mutex-meet-tid"],
+              "enum": ["none", "mutex-oplus", "mutex-meet", "protection", "protection-atomic", "protection-read", "protection-read-atomic", "mine", "mine-nothread", "mine-W", "mine-W-noinit", "lock", "write", "write+lock","mutex-meet-tid"],
               "default": "protection-read"
             },
             "priv": {
@@ -901,7 +901,7 @@
               "description":
                 "Which relation privatization to use? top/protection/protection-path/mutex-meet/mutex-meet-tid/mutex-meet-tid-cluster12/mutex-meet-tid-cluster2/mutex-meet-tid-cluster-max/mutex-meet-tid-cluster-power",
               "type": "string",
-              "enum": ["top", "protection", "protection-path", "mutex-meet", "mutex-meet-tid", "mutex-meet-tid-cluster12", "mutex-meet-tid-cluster2", "mutex-meet-tid-cluster-max", "mutex-meet-tid-cluster-power"],
+              "enum": ["top", "protection", "protection-path", "mutex-meet", "mutex-meet-atomic", "mutex-meet-tid", "mutex-meet-tid-atomic", "mutex-meet-tid-cluster12", "mutex-meet-tid-cluster2", "mutex-meet-tid-cluster-max", "mutex-meet-tid-cluster-power"],
               "default": "mutex-meet"
             },
             "priv": {
@@ -2450,6 +2450,12 @@
                 "RETURN"
               ]
             },
+            "all-locals": {
+              "title": "witness.invariant.all-locals",
+              "description": "Emit invariants for local variables under the assumption they are always in scope within their function.",
+              "type": "boolean",
+              "default": true
+            },
             "goblint": {
               "title": "witness.invariant.goblint",
               "description": "Emit non-standard Goblint-specific invariants. Currently array invariants with all_index offsets.",
diff --git a/src/constraint/constrSys.ml b/src/constraint/constrSys.ml
index 1698d5f214..60859f1ccb 100644
--- a/src/constraint/constrSys.ml
+++ b/src/constraint/constrSys.ml
@@ -219,7 +219,7 @@ struct
           | `Lifted2 d -> LH.replace l' x d
           (* | `Bot -> () *)
           (* Since Verify2 is broken and only checks existing keys, add it with local bottom value.
-            This works around some cases, where Verify2 would not detect a problem due to completely missing variable. *)
+             This works around some cases, where Verify2 would not detect a problem due to completely missing variable. *)
           | `Bot -> LH.replace l' x (S.D.bot ())
           | `Top -> failwith "GlobConstrSolFromEqConstrSolBase.split_vars: local variable has top value"
           | `Lifted1 _ -> failwith "GlobConstrSolFromEqConstrSolBase.split_vars: local variable has global value"
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index 030b86446c..52022b8aee 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -1757,10 +1757,10 @@ struct
     in
     PP.iter f h1;
     (* let k1 = Set.of_enum @@ PP.keys h1 in
-    let k2 = Set.of_enum @@ PP.keys h2 in
-    let o1 = Set.cardinal @@ Set.diff k1 k2 in
-    let o2 = Set.cardinal @@ Set.diff k2 k1 in
-    Logs.info "locals: \tequal = %d\tleft = %d[%d]\tright = %d[%d]\tincomparable = %d" !eq !le o1 !gr o2 !uk *)
+       let k2 = Set.of_enum @@ PP.keys h2 in
+       let o1 = Set.cardinal @@ Set.diff k1 k2 in
+       let o2 = Set.cardinal @@ Set.diff k2 k1 in
+       Logs.info "locals: \tequal = %d\tleft = %d[%d]\tright = %d[%d]\tincomparable = %d" !eq !le o1 !gr o2 !uk *)
     Logs.info "locals: \tequal = %d\tleft = %d\tright = %d\tincomparable = %d" !eq !le !gr !uk
 
   let compare_locals_ctx h1 h2 =
diff --git a/src/maingoblint.ml b/src/maingoblint.ml
index 40a997edee..7fdb7a4a13 100644
--- a/src/maingoblint.ml
+++ b/src/maingoblint.ml
@@ -144,6 +144,7 @@ let check_arguments () =
   if get_bool "incremental.restart.sided.enabled" && get_string_list "incremental.restart.list" <> [] then warn "Passing a non-empty list to incremental.restart.list (manual restarting) while incremental.restart.sided.enabled (automatic restarting) is activated.";
   if get_bool "ana.autotune.enabled" && get_bool "incremental.load" then (set_bool "ana.autotune.enabled" false; warn "ana.autotune.enabled implicitly disabled by incremental.load");
   if get_bool "exp.basic-blocks" && not (get_bool "justcil") && List.mem "assert" @@ get_string_list "trans.activated" then (set_bool "exp.basic-blocks" false; warn "The option exp.basic-blocks implicitely disabled by activating the \"assert\" tranformation.");
+  if (not @@ get_bool "witness.invariant.all-locals") && (not @@ get_bool "cil.addNestedScopeAttr") then (set_bool "cil.addNestedScopeAttr" true; warn "Disabling witness.invariant.all-locals implicitly enables cil.addNestedScopeAttr.");
   if List.mem "remove_dead_code" @@ get_string_list "trans.activated" then (
     (* 'assert' transform happens before 'remove_dead_code' transform *)
     ignore @@ List.fold_left
@@ -546,8 +547,7 @@ let do_analyze change_info merged_AST =
     Logs.debug "And now...  the Goblin!";
     let (stf,exf,otf as funs) = Cilfacade.getFuns merged_AST in
     if stf@exf@otf = [] then raise (FrontendError "no suitable function to start from");
-    Logs.debug "Startfuns: %a\nExitfuns: %a\nOtherfuns: %a"
-                                             L.pretty stf L.pretty exf L.pretty otf;
+    Logs.debug "Startfuns: %a\nExitfuns: %a\nOtherfuns: %a" L.pretty stf L.pretty exf L.pretty otf;
     (* and here we run the analysis! *)
 
     let control_analyze ast funs =
@@ -598,11 +598,7 @@ let do_html_output () =
 
 let do_gobview cilfile =
   let gobview = GobConfig.get_bool "gobview" in
-  let goblint_root = GobFpath.cwd_append (fst (Fpath.split_base (Fpath.v Sys.argv.(0)))) in
-  let dist_dir = Fpath.(goblint_root // (Fpath.v "_build/default/gobview/dist")) in
-  let js_file = Fpath.(dist_dir / "main.js") in
   if gobview then (
-    if Sys.file_exists (Fpath.to_string js_file) then (
       let save_run = GobConfig.get_string "save_run" in
       let run_dir = Fpath.v(if save_run <> "" then save_run else "run") in
       (* copy relevant c files to gobview directory *)
@@ -626,20 +622,7 @@ let do_gobview cilfile =
       (* marshal timing statistics *)
       let stats = Fpath.(run_dir / "stats.marshalled") in
       Serialize.marshal (Timing.Default.root, Gc.quick_stat ()) stats;
-      let dist_files =
-        Sys.files_of (Fpath.to_string dist_dir)
-        |> Enum.filter (fun n -> n <> "dune")
-        |> List.of_enum
-      in
-      List.iter (fun n ->
-          FileUtil.cp
-            [Fpath.to_string (Fpath.(dist_dir / n))]
-            (Fpath.to_string (Fpath.(run_dir / n)))
-        ) dist_files
     )
-    else
-      Logs.error "Warning: Cannot locate GobView."
-  )
 
 let handle_extraspecials () =
   let funs = get_string_list "exp.extraspecials" in
diff --git a/src/solver/sLRterm.ml b/src/solver/sLRterm.ml
index ab5e985392..b2678d3a68 100644
--- a/src/solver/sLRterm.ml
+++ b/src/solver/sLRterm.ml
@@ -50,11 +50,11 @@ module SLR3term =
       let count_side  = ref (max_int - 1) in
 
       let () = print_solver_stats := fun () ->
-        Logs.info "wpoint: %d, rho: %d, rho': %d, q: %d, count: %d, count_side: %d" (HM.length wpoint) (HM.length rho) (HPM.length rho') (H.size !q) (Int.neg !count) (max_int - !count_side);
-        let histo = Hashtbl.create 13 in (* histogram: node id -> number of contexts *)
-        HM.iter (fun k _ -> Hashtbl.modify_def 1 (S.Var.var_id k) ((+)1) histo) rho;
-        let vid,n = Hashtbl.fold (fun k v (k',v') -> if v > v' then k,v else k',v') histo (Obj.magic (), 0) in
-        Logs.info "max #contexts: %d for var_id %s" n vid
+          Logs.info "wpoint: %d, rho: %d, rho': %d, q: %d, count: %d, count_side: %d" (HM.length wpoint) (HM.length rho) (HPM.length rho') (H.size !q) (Int.neg !count) (max_int - !count_side);
+          let histo = Hashtbl.create 13 in (* histogram: node id -> number of contexts *)
+          HM.iter (fun k _ -> Hashtbl.modify_def 1 (S.Var.var_id k) ((+)1) histo) rho;
+          let vid,n = Hashtbl.fold (fun k v (k',v') -> if v > v' then k,v else k',v') histo (Obj.magic (), 0) in
+          Logs.info "max #contexts: %d for var_id %s" n vid
       in
 
       let init ?(side=false) x =
diff --git a/src/solver/td3.ml b/src/solver/td3.ml
index ae899b7337..fe7940a828 100644
--- a/src/solver/td3.ml
+++ b/src/solver/td3.ml
@@ -11,8 +11,7 @@
  * - space (false) ? only keep values at widening points (TDspace + side) in rho : keep all values in rho
  * - space_cache (true) ? local cache l for eval calls in each solve (TDcombined) : no cache
  * - space_restore (true) ? eval each rhs and store all in rho : do not restore missing values
- * For simpler (but unmaintained) versions without the incremental parts see the paper or topDown{,_space_cache_term}.ml.
- *)
+ * For simpler (but unmaintained) versions without the incremental parts see the paper or topDown{,_space_cache_term}.ml. *)
 
 open Batteries
 open ConstrSys
@@ -318,16 +317,15 @@ module Base =
           let old = HM.find rho x in (* d from older solve *) (* find old value after eq since wpoint restarting in eq/eval might have changed it meanwhile *)
           let wpd = (* d after widen/narrow (if wp) *)
             if not wp then eqd
+            else if term then
+              match phase with
+              | Widen -> S.Dom.widen old (S.Dom.join old eqd)
+              | Narrow when GobConfig.get_bool "exp.no-narrow" -> old (* no narrow *)
+              | Narrow ->
+                (* assert S.Dom.(leq eqd old || not (leq old eqd)); (* https://github.com/goblint/analyzer/pull/490#discussion_r875554284 *) *)
+                S.Dom.narrow old eqd
             else
-              if term then
-                match phase with
-                | Widen -> S.Dom.widen old (S.Dom.join old eqd)
-                | Narrow when GobConfig.get_bool "exp.no-narrow" -> old (* no narrow *)
-                | Narrow ->
-                  (* assert S.Dom.(leq eqd old || not (leq old eqd)); (* https://github.com/goblint/analyzer/pull/490#discussion_r875554284 *) *)
-                  S.Dom.narrow old eqd
-              else
-                box old eqd
+              box old eqd
           in
           if tracing then trace "sol" "Var: %a (wp: %b)\nOld value: %a\nEqd: %a\nNew value: %a\n" S.Var.pretty_trace x wp S.Dom.pretty old S.Dom.pretty eqd S.Dom.pretty wpd;
           if cache then (
@@ -464,12 +462,13 @@ module Base =
             (* x caused more than one update to y. >=3 partial context calls will be precise since sides come from different x. TODO this has 8 instead of 5 phases of `solver` for side_cycle.c *)
             wpoint_if sided
           | "sides-pp" ->
-            (match x with
-            | Some x ->
-              let n = S.Var.node x in
-              let sided = VS.exists (fun v -> Node.equal (S.Var.node v) n) old_sides in
-              wpoint_if sided
-            | None -> ())
+            begin match x with
+              | Some x ->
+                let n = S.Var.node x in
+                let sided = VS.exists (fun v -> Node.equal (S.Var.node v) n) old_sides in
+                wpoint_if sided
+              | None -> ()
+            end
           | "cycle" -> (* destabilized a called or start var. Problem: two partial context calls will be precise, but third call will widen the state. *)
             (* if this side destabilized some of the initial unknowns vs, there may be a side-cycle between vs and we should make y a wpoint *)
             let destabilized_vs = destabilize_vs y in
diff --git a/src/util/library/libraryDesc.ml b/src/util/library/libraryDesc.ml
index e2dbedb516..ef22dc0df0 100644
--- a/src/util/library/libraryDesc.ml
+++ b/src/util/library/libraryDesc.ml
@@ -56,6 +56,7 @@ type special =
   | ThreadCreate of { thread: Cil.exp; start_routine: Cil.exp; arg: Cil.exp; multiple: bool }
   | ThreadJoin of { thread: Cil.exp; ret_var: Cil.exp; }
   | ThreadExit of { ret_val: Cil.exp; }
+  | Globalize of Cil.exp
   | Signal of Cil.exp
   | Broadcast of Cil.exp
   | MutexAttrSetType of { attr:Cil.exp; typ: Cil.exp; }
diff --git a/src/util/library/libraryFunctions.ml b/src/util/library/libraryFunctions.ml
index 54b244f9e0..eef9563d94 100644
--- a/src/util/library/libraryFunctions.ml
+++ b/src/util/library/libraryFunctions.ml
@@ -759,6 +759,7 @@ let goblint_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("__goblint_check", special [__ "exp" []] @@ fun exp -> Assert { exp; check = true; refine = false });
     ("__goblint_assume", special [__ "exp" []] @@ fun exp -> Assert { exp; check = false; refine = true });
     ("__goblint_assert", special [__ "exp" []] @@ fun exp -> Assert { exp; check = true; refine = get_bool "sem.assert.refine" });
+    ("__goblint_globalize", special [__ "ptr" []] @@ fun ptr -> Globalize ptr);
     ("__goblint_split_begin", unknown [drop "exp" []]);
     ("__goblint_split_end", unknown [drop "exp" []]);
     ("__goblint_bounded", special [__ "exp"[]] @@ fun exp -> Bounded { exp });
diff --git a/tests/regression/13-privatized/74-mutex.c b/tests/regression/13-privatized/74-mutex.c
new file mode 100644
index 0000000000..8ed9448b7b
--- /dev/null
+++ b/tests/regression/13-privatized/74-mutex.c
@@ -0,0 +1,42 @@
+// PARAM: --enable ana.sv-comp.functions
+/*-----------------------------------------------------------------------------
+ * mutex.c - Concurrent program using locking to access a shared variable
+ *-----------------------------------------------------------------------------
+ * Author: Frank Schüssele
+ *   Date: 2023-07-11
+ *---------------------------------------------------------------------------*/
+#include <pthread.h>
+#include <goblint.h>
+
+extern void __VERIFIER_atomic_begin();
+extern void __VERIFIER_atomic_end();
+
+int used;
+pthread_mutex_t m;
+
+void* producer()
+{
+  while (1) {
+    pthread_mutex_lock(&m);
+    used++;
+    used--;
+    pthread_mutex_unlock(&m);
+  }
+
+  return 0;
+}
+
+int main()
+{
+  pthread_t tid;
+
+  pthread_mutex_init(&m, 0);
+  pthread_create(&tid, 0, producer, 0);
+
+  pthread_mutex_lock(&m);
+  __goblint_check(used == 0);
+  pthread_mutex_unlock(&m);
+
+  pthread_mutex_destroy(&m);
+  return 0;
+}
diff --git a/tests/regression/29-svcomp/16-atomic_priv.c b/tests/regression/29-svcomp/16-atomic_priv.c
index 92e1896f58..2f39c0ee3a 100644
--- a/tests/regression/29-svcomp/16-atomic_priv.c
+++ b/tests/regression/29-svcomp/16-atomic_priv.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.sv-comp.functions
+// PARAM: --enable ana.sv-comp.functions --set ana.base.privatization protection-atomic
 #include <pthread.h>
 #include <goblint.h>
 
@@ -21,7 +21,7 @@ void *t_fun(void *arg) {
 int main(void) {
   pthread_t id;
   pthread_create(&id, NULL, t_fun, NULL);
-  __goblint_check(myglobal == 5); // TODO
+  __goblint_check(myglobal == 5);
   __VERIFIER_atomic_begin();
   __goblint_check(myglobal == 5);
   __VERIFIER_atomic_end();
diff --git a/tests/regression/29-svcomp/18-atomic_fun_priv.c b/tests/regression/29-svcomp/18-atomic_fun_priv.c
index 0449f9af0d..13c03ffb48 100644
--- a/tests/regression/29-svcomp/18-atomic_fun_priv.c
+++ b/tests/regression/29-svcomp/18-atomic_fun_priv.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.sv-comp.functions
+// PARAM: --enable ana.sv-comp.functions --set ana.base.privatization protection-atomic
 #include <pthread.h>
 #include <goblint.h>
 
@@ -21,7 +21,7 @@ void *t_fun(void *arg) {
 int main(void) {
   pthread_t id;
   pthread_create(&id, NULL, t_fun, NULL);
-  __goblint_check(myglobal == 5); // TODO
+  __goblint_check(myglobal == 5);
   __VERIFIER_atomic_begin();
   __goblint_check(myglobal == 5);
   __VERIFIER_atomic_end();
diff --git a/tests/regression/46-apron2/61-atomic_priv.c b/tests/regression/46-apron2/61-atomic_priv.c
new file mode 100644
index 0000000000..5c65457c5f
--- /dev/null
+++ b/tests/regression/46-apron2/61-atomic_priv.c
@@ -0,0 +1,30 @@
+// SKIP PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set ana.base.privatization none
+#include <pthread.h>
+#include <goblint.h>
+
+extern void __VERIFIER_atomic_begin();
+extern void __VERIFIER_atomic_end();
+
+int myglobal = 5;
+
+void *t_fun(void *arg) {
+  __VERIFIER_atomic_begin();
+  __goblint_check(myglobal == 5);
+  myglobal++;
+  __goblint_check(myglobal == 6);
+  myglobal--;
+  __goblint_check(myglobal == 5);
+  __VERIFIER_atomic_end();
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  __goblint_check(myglobal == 5);
+  __VERIFIER_atomic_begin();
+  __goblint_check(myglobal == 5);
+  __VERIFIER_atomic_end();
+  pthread_join (id, NULL);
+  return 0;
+}
diff --git a/tests/regression/46-apron2/62-atomic_fun_priv.c b/tests/regression/46-apron2/62-atomic_fun_priv.c
new file mode 100644
index 0000000000..7fa601fb75
--- /dev/null
+++ b/tests/regression/46-apron2/62-atomic_fun_priv.c
@@ -0,0 +1,30 @@
+// SKIP PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set ana.base.privatization none
+#include <pthread.h>
+#include <goblint.h>
+
+int myglobal = 5;
+
+// atomic by function name prefix
+void __VERIFIER_atomic_fun() {
+  __goblint_check(myglobal == 5);
+  myglobal++;
+  __goblint_check(myglobal == 6);
+  myglobal--;
+  __goblint_check(myglobal == 5);
+}
+
+void *t_fun(void *arg) {
+  __VERIFIER_atomic_fun();
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  __goblint_check(myglobal == 5);
+  __VERIFIER_atomic_begin();
+  __goblint_check(myglobal == 5);
+  __VERIFIER_atomic_end();
+  pthread_join (id, NULL);
+  return 0;
+}
diff --git a/tests/regression/46-apron2/63-atomic_priv_sound.c b/tests/regression/46-apron2/63-atomic_priv_sound.c
new file mode 100644
index 0000000000..6e597263b5
--- /dev/null
+++ b/tests/regression/46-apron2/63-atomic_priv_sound.c
@@ -0,0 +1,28 @@
+// SKIP PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set ana.base.privatization none
+#include <pthread.h>
+#include <goblint.h>
+
+extern void __VERIFIER_atomic_begin();
+extern void __VERIFIER_atomic_end();
+
+int myglobal = 5;
+
+void *t_fun(void *arg) {
+  __VERIFIER_atomic_begin();
+  __goblint_check(myglobal == 5); // TODO
+  myglobal++;
+  __goblint_check(myglobal == 6); // TODO
+  __VERIFIER_atomic_end();
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  __goblint_check(myglobal == 5); // UNKNOWN!
+  __VERIFIER_atomic_begin();
+  __goblint_check(myglobal == 5); // UNKNOWN!
+  __VERIFIER_atomic_end();
+  pthread_join (id, NULL);
+  return 0;
+}
diff --git a/tests/regression/46-apron2/64-atomic_priv_sound2.c b/tests/regression/46-apron2/64-atomic_priv_sound2.c
new file mode 100644
index 0000000000..352dc16e93
--- /dev/null
+++ b/tests/regression/46-apron2/64-atomic_priv_sound2.c
@@ -0,0 +1,43 @@
+// SKIP PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set ana.base.privatization none
+#include <pthread.h>
+#include <goblint.h>
+
+extern void __VERIFIER_atomic_begin();
+extern void __VERIFIER_atomic_end();
+
+int myglobal = 0;
+int myglobal2 = 0;
+int myglobal3 = 0;
+
+void *t_fun(void *arg) {
+  __VERIFIER_atomic_begin();
+  myglobal2++;
+  __VERIFIER_atomic_end();
+  __VERIFIER_atomic_begin();
+  myglobal++;
+  __VERIFIER_atomic_end();
+  return NULL;
+}
+
+void *t2_fun(void *arg) {
+  __VERIFIER_atomic_begin();
+  myglobal3++;
+  __VERIFIER_atomic_end();
+  __VERIFIER_atomic_begin();
+  myglobal++;
+  __VERIFIER_atomic_end();
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id, id2;
+  pthread_create(&id, NULL, t_fun, NULL);
+  pthread_create(&id2, NULL, t2_fun, NULL);
+  __goblint_check(myglobal == 2); // UNKNOWN!
+  __VERIFIER_atomic_begin();
+  __goblint_check(myglobal == 2); // UNKNOWN!
+  __VERIFIER_atomic_end();
+  pthread_join (id, NULL);
+  pthread_join (id2, NULL);
+  return 0;
+}
diff --git a/tests/regression/46-apron2/65-atomic_priv_sound3.c b/tests/regression/46-apron2/65-atomic_priv_sound3.c
new file mode 100644
index 0000000000..0dd88319b9
--- /dev/null
+++ b/tests/regression/46-apron2/65-atomic_priv_sound3.c
@@ -0,0 +1,23 @@
+// SKIP PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set ana.base.privatization none
+#include <pthread.h>
+#include <goblint.h>
+
+extern void __VERIFIER_atomic_begin();
+extern void __VERIFIER_atomic_end();
+
+int myglobal = 5;
+
+void *t_fun(void *arg) {
+  myglobal++;
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  __VERIFIER_atomic_begin();
+  __goblint_check(myglobal == 5); // UNKNOWN!
+  __VERIFIER_atomic_end();
+  pthread_join (id, NULL);
+  return 0;
+}
diff --git a/tests/regression/46-apron2/66-atomic_relation.c b/tests/regression/46-apron2/66-atomic_relation.c
new file mode 100644
index 0000000000..fd1ac0781e
--- /dev/null
+++ b/tests/regression/46-apron2/66-atomic_relation.c
@@ -0,0 +1,33 @@
+// SKIP PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set sem.int.signed_overflow assume_none
+#include <pthread.h>
+#include <goblint.h>
+
+extern void __VERIFIER_atomic_begin();
+extern void __VERIFIER_atomic_end();
+
+int g = 0;
+int h = 0;
+
+pthread_mutex_t m = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  __VERIFIER_atomic_begin();
+  // pthread_mutex_lock(&m);
+  g++;
+  h++;
+  __VERIFIER_atomic_end();
+  // pthread_mutex_unlock(&m);
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  __VERIFIER_atomic_begin();
+  // pthread_mutex_lock(&m);
+  __goblint_check(g == h);
+  __VERIFIER_atomic_end();
+  // pthread_mutex_unlock(&m);
+  pthread_join (id, NULL);
+  return 0;
+}
diff --git a/tests/regression/46-apron2/67-case_distinction_with_ghosts.c b/tests/regression/46-apron2/67-case_distinction_with_ghosts.c
new file mode 100644
index 0000000000..8b65701fec
--- /dev/null
+++ b/tests/regression/46-apron2/67-case_distinction_with_ghosts.c
@@ -0,0 +1,39 @@
+// SKIP PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set sem.int.signed_overflow assume_none
+#include <pthread.h>
+#include <assert.h>
+
+extern int  __VERIFIER_nondet_int();
+extern void __VERIFIER_atomic_begin();
+extern void __VERIFIER_atomic_end();
+
+int x = 0;
+int g = 0;
+
+void* inc()
+{
+  int n = __VERIFIER_nondet_int();
+
+  while (x < n) {
+    __VERIFIER_atomic_begin();
+    x++;
+    __VERIFIER_atomic_end();
+
+    __VERIFIER_atomic_begin();
+    assert(g != 1 || x >= 42); // TODO
+    __VERIFIER_atomic_end();
+  }
+
+  return 0;
+}
+
+int main()
+{
+  pthread_t tid;
+  pthread_create(&tid, 0, inc, 0);
+  __VERIFIER_atomic_begin();
+  g = 1; x = 42;
+  __VERIFIER_atomic_end();
+
+  assert(x >= 42); // TODO
+  return 0;
+}
diff --git a/tests/regression/46-apron2/68-case_distinction_with_ghosts-2.c b/tests/regression/46-apron2/68-case_distinction_with_ghosts-2.c
new file mode 100644
index 0000000000..9f3938a6a9
--- /dev/null
+++ b/tests/regression/46-apron2/68-case_distinction_with_ghosts-2.c
@@ -0,0 +1,30 @@
+// SKIP PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set sem.int.signed_overflow assume_none
+#include <pthread.h>
+#include <assert.h>
+
+extern int  __VERIFIER_nondet_int();
+extern void __VERIFIER_atomic_begin();
+extern void __VERIFIER_atomic_end();
+
+int x = 0;
+int g = 0;
+
+void* inc()
+{
+  __VERIFIER_atomic_begin();
+  assert(g != 1 || x >= 42); // TODO
+  __VERIFIER_atomic_end();
+  return 0;
+}
+
+int main()
+{
+  pthread_t tid;
+  pthread_create(&tid, 0, inc, 0);
+  __VERIFIER_atomic_begin();
+  g = 1; x = 42;
+  __VERIFIER_atomic_end();
+
+  assert(x >= 42); // TODO
+  return 0;
+}
diff --git a/tests/regression/46-apron2/70-nondet_inc_with_ghosts.c b/tests/regression/46-apron2/70-nondet_inc_with_ghosts.c
new file mode 100644
index 0000000000..aa8b0a607d
--- /dev/null
+++ b/tests/regression/46-apron2/70-nondet_inc_with_ghosts.c
@@ -0,0 +1,43 @@
+// SKIP PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set sem.int.signed_overflow assume_none --enable ana.apron.threshold_widening
+#include <pthread.h>
+#include <assert.h>
+
+extern int  __VERIFIER_nondet_int();
+extern void __VERIFIER_atomic_begin();
+extern void __VERIFIER_atomic_end();
+
+int x = 0;
+int g = 0;
+
+void* inc()
+{
+  int n = __VERIFIER_nondet_int();
+
+  while (x < n) {
+    __VERIFIER_atomic_begin();
+    x++;
+    __VERIFIER_atomic_end();
+
+    __VERIFIER_atomic_begin();
+    assert(x >= g);
+    __VERIFIER_atomic_end();
+  }
+
+  return 0;
+}
+
+int main()
+{
+  pthread_t tid;
+  pthread_create(&tid, 0, inc, 0);
+
+  int val = __VERIFIER_nondet_int();
+  __VERIFIER_atomic_begin();
+  g = val; x = val;
+  __VERIFIER_atomic_end();
+
+  __VERIFIER_atomic_begin(); // TODO: atomic needed?
+  assert(x >= val); // TODO
+  __VERIFIER_atomic_end();
+  return 0;
+}
diff --git a/tests/regression/46-apron2/71-nondet_inc_with_ghosts-2.c b/tests/regression/46-apron2/71-nondet_inc_with_ghosts-2.c
new file mode 100644
index 0000000000..01e8bf7b4b
--- /dev/null
+++ b/tests/regression/46-apron2/71-nondet_inc_with_ghosts-2.c
@@ -0,0 +1,38 @@
+// SKIP PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set sem.int.signed_overflow assume_none --enable ana.apron.threshold_widening
+#include <pthread.h>
+#include <assert.h>
+
+extern int  __VERIFIER_nondet_int();
+extern void __VERIFIER_atomic_begin();
+extern void __VERIFIER_atomic_end();
+
+int x = 0;
+int g = 0;
+
+void* inc()
+{
+  __VERIFIER_atomic_begin();
+  x++;
+  __VERIFIER_atomic_end();
+
+  __VERIFIER_atomic_begin();
+  assert(x >= g);
+  __VERIFIER_atomic_end();
+  return 0;
+}
+
+int main()
+{
+  pthread_t tid;
+  pthread_create(&tid, 0, inc, 0);
+
+  int val = __VERIFIER_nondet_int();
+  __VERIFIER_atomic_begin();
+  g = val; x = val;
+  __VERIFIER_atomic_end();
+
+  __VERIFIER_atomic_begin(); // TODO: atomic needed?
+  assert(x >= val); // TODO
+  __VERIFIER_atomic_end();
+  return 0;
+}
diff --git a/tests/regression/46-apron2/72-nondet_inc_with_ghosts-3.c b/tests/regression/46-apron2/72-nondet_inc_with_ghosts-3.c
new file mode 100644
index 0000000000..1c42834e72
--- /dev/null
+++ b/tests/regression/46-apron2/72-nondet_inc_with_ghosts-3.c
@@ -0,0 +1,34 @@
+// SKIP PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set sem.int.signed_overflow assume_none
+#include <pthread.h>
+#include <assert.h>
+
+extern int  __VERIFIER_nondet_int();
+extern void __VERIFIER_atomic_begin();
+extern void __VERIFIER_atomic_end();
+
+int x = 0;
+int g = 0;
+
+void* inc()
+{
+  __VERIFIER_atomic_begin();
+  assert(x >= g);
+  __VERIFIER_atomic_end();
+  return 0;
+}
+
+int main()
+{
+  pthread_t tid;
+  pthread_create(&tid, 0, inc, 0);
+
+  int val = __VERIFIER_nondet_int();
+  __VERIFIER_atomic_begin();
+  g = val; x = val;
+  __VERIFIER_atomic_end();
+
+  __VERIFIER_atomic_begin(); // TODO: atomic needed?
+  assert(x >= val); // TODO
+  __VERIFIER_atomic_end();
+  return 0;
+}
diff --git a/tests/regression/46-apron2/73-nondet_inc_with_ghosts-globalize.c b/tests/regression/46-apron2/73-nondet_inc_with_ghosts-globalize.c
new file mode 100644
index 0000000000..d30d4ef68a
--- /dev/null
+++ b/tests/regression/46-apron2/73-nondet_inc_with_ghosts-globalize.c
@@ -0,0 +1,46 @@
+// SKIP PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-tid-atomic --set sem.int.signed_overflow assume_none --enable ana.apron.threshold_widening --set ana.path_sens[+] threadflag --enable ana.apron.strengthening
+// TODO: -atomic unneeded?
+#include <pthread.h>
+#include <assert.h>
+#include <goblint.h>
+
+extern int  __VERIFIER_nondet_int();
+extern void __VERIFIER_atomic_begin();
+extern void __VERIFIER_atomic_end();
+
+int x = 0;
+int g = 0;
+
+void* inc()
+{
+  int n = __VERIFIER_nondet_int();
+
+  while (x < n) {
+    __VERIFIER_atomic_begin();
+    x++;
+    __VERIFIER_atomic_end();
+
+    __VERIFIER_atomic_begin();
+    assert(x >= g);
+    __VERIFIER_atomic_end();
+  }
+
+  return 0;
+}
+
+int main()
+{
+  pthread_t tid;
+  pthread_create(&tid, 0, inc, 0);
+
+  int val = __VERIFIER_nondet_int();
+  __VERIFIER_atomic_begin();
+  __goblint_globalize(&val);
+  g = val; x = val;
+  __VERIFIER_atomic_end();
+
+  __VERIFIER_atomic_begin(); // TODO: atomic needed?
+  assert(x >= val);
+  __VERIFIER_atomic_end();
+  return 0;
+}
diff --git a/tests/regression/46-apron2/74-mutex.c b/tests/regression/46-apron2/74-mutex.c
new file mode 100644
index 0000000000..72e83f1eda
--- /dev/null
+++ b/tests/regression/46-apron2/74-mutex.c
@@ -0,0 +1,42 @@
+// SKIP PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set ana.base.privatization none
+/*-----------------------------------------------------------------------------
+ * mutex.c - Concurrent program using locking to access a shared variable
+ *-----------------------------------------------------------------------------
+ * Author: Frank Schüssele
+ *   Date: 2023-07-11
+ *---------------------------------------------------------------------------*/
+#include <pthread.h>
+#include <goblint.h>
+
+extern void __VERIFIER_atomic_begin();
+extern void __VERIFIER_atomic_end();
+
+int used;
+pthread_mutex_t m;
+
+void* producer()
+{
+  while (1) {
+    pthread_mutex_lock(&m);
+    used++;
+    used--;
+    pthread_mutex_unlock(&m);
+  }
+
+  return 0;
+}
+
+int main()
+{
+  pthread_t tid;
+
+  pthread_mutex_init(&m, 0);
+  pthread_create(&tid, 0, producer, 0);
+
+  pthread_mutex_lock(&m);
+  __goblint_check(used == 0);
+  pthread_mutex_unlock(&m);
+
+  pthread_mutex_destroy(&m);
+  return 0;
+}
diff --git a/tests/regression/46-apron2/75-mutex_with_ghosts.c b/tests/regression/46-apron2/75-mutex_with_ghosts.c
new file mode 100644
index 0000000000..c784720aee
--- /dev/null
+++ b/tests/regression/46-apron2/75-mutex_with_ghosts.c
@@ -0,0 +1,65 @@
+// SKIP PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set sem.int.signed_overflow assume_none
+/*-----------------------------------------------------------------------------
+ * mutex_with_ghosts.c - Annotated concurrent program with ghost variables for
+ *                       witness validation using locking to access a shared
+ *                       variable
+ *-----------------------------------------------------------------------------
+ * Author: Frank Schüssele
+ *   Date: 2023-07-11
+ *---------------------------------------------------------------------------*/
+#include <pthread.h>
+#include <goblint.h>
+
+extern void __VERIFIER_atomic_begin();
+extern void __VERIFIER_atomic_end();
+
+int used;
+int g = 0;
+pthread_mutex_t m;
+
+void* producer()
+{
+  while (1) {
+    __VERIFIER_atomic_begin();
+    g = 1;
+    pthread_mutex_lock(&m);
+    __VERIFIER_atomic_end();
+
+    used++;
+    used--;
+
+    __VERIFIER_atomic_begin();
+    g = 0;
+    pthread_mutex_unlock(&m);
+    __VERIFIER_atomic_end();
+  }
+
+  return 0;
+}
+
+int main()
+{
+  pthread_t tid;
+
+  pthread_mutex_init(&m, 0);
+  pthread_create(&tid, 0, producer, 0);
+
+  __VERIFIER_atomic_begin();
+  __goblint_check(g == 1 || used == 0); // TODO (unprotected invariant precision loss?)
+  __VERIFIER_atomic_end();
+
+  __VERIFIER_atomic_begin();
+  g = 1;
+  pthread_mutex_lock(&m);
+  __VERIFIER_atomic_end();
+
+  __goblint_check(used == 0); // TODO (read/refine? of used above makes used write-unprotected)
+
+  __VERIFIER_atomic_begin();
+  g = 0;
+  pthread_mutex_unlock(&m);
+  __VERIFIER_atomic_end();
+
+  pthread_mutex_destroy(&m);
+  return 0;
+}
diff --git a/tests/regression/46-apron2/76-mutex_with_ghosts-2.c b/tests/regression/46-apron2/76-mutex_with_ghosts-2.c
new file mode 100644
index 0000000000..4e2fcf962f
--- /dev/null
+++ b/tests/regression/46-apron2/76-mutex_with_ghosts-2.c
@@ -0,0 +1,67 @@
+// SKIP PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set sem.int.signed_overflow assume_none
+/*-----------------------------------------------------------------------------
+ * mutex_with_ghosts.c - Annotated concurrent program with ghost variables for
+ *                       witness validation using locking to access a shared
+ *                       variable
+ *-----------------------------------------------------------------------------
+ * Author: Frank Schüssele
+ *   Date: 2023-07-11
+ *---------------------------------------------------------------------------*/
+#include <pthread.h>
+#include <goblint.h>
+
+extern void __VERIFIER_atomic_begin();
+extern void __VERIFIER_atomic_end();
+
+int used;
+int g = 0;
+pthread_mutex_t m;
+
+void* producer()
+{
+  while (1) {
+    __VERIFIER_atomic_begin();
+    g = 1;
+    pthread_mutex_lock(&m);
+    __VERIFIER_atomic_end();
+
+    used++;
+    used--;
+
+    __VERIFIER_atomic_begin();
+    g = 0;
+    pthread_mutex_unlock(&m);
+    __VERIFIER_atomic_end();
+  }
+
+  return 0;
+}
+
+int main()
+{
+  pthread_t tid;
+
+  pthread_mutex_init(&m, 0);
+  pthread_create(&tid, 0, producer, 0);
+
+  __VERIFIER_atomic_begin();
+  int g2 = g;
+  int used2 = used;
+  __goblint_check(g2 == 1 || used2 == 0); // TODO (unprotected invariant precision loss?)
+  __VERIFIER_atomic_end();
+
+  __VERIFIER_atomic_begin();
+  g = 1;
+  pthread_mutex_lock(&m);
+  __VERIFIER_atomic_end();
+
+  __goblint_check(used == 0);
+
+  __VERIFIER_atomic_begin();
+  g = 0;
+  pthread_mutex_unlock(&m);
+  __VERIFIER_atomic_end();
+
+  pthread_mutex_destroy(&m);
+  return 0;
+}
diff --git a/tests/regression/46-apron2/77-mutex_with_ghosts-3.c b/tests/regression/46-apron2/77-mutex_with_ghosts-3.c
new file mode 100644
index 0000000000..1f1c70c068
--- /dev/null
+++ b/tests/regression/46-apron2/77-mutex_with_ghosts-3.c
@@ -0,0 +1,69 @@
+// SKIP PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-tid-atomic --set ana.path_sens[+] threadflag --set sem.int.signed_overflow assume_none --enable ana.apron.strengthening
+// TODO: unsound with cluster12
+/*-----------------------------------------------------------------------------
+ * mutex_with_ghosts.c - Annotated concurrent program with ghost variables for
+ *                       witness validation using locking to access a shared
+ *                       variable
+ *-----------------------------------------------------------------------------
+ * Author: Frank Schüssele
+ *   Date: 2023-07-11
+ *---------------------------------------------------------------------------*/
+#include <pthread.h>
+#include <goblint.h>
+
+extern void __VERIFIER_atomic_begin();
+extern void __VERIFIER_atomic_end();
+
+int used;
+int g = 0;
+pthread_mutex_t m;
+
+void* producer()
+{
+  while (1) {
+    __VERIFIER_atomic_begin();
+    g = 1;
+    pthread_mutex_lock(&m);
+    __VERIFIER_atomic_end();
+
+    used++;
+    used--;
+
+    __VERIFIER_atomic_begin();
+    g = 0;
+    pthread_mutex_unlock(&m);
+    __VERIFIER_atomic_end();
+  }
+
+  return 0;
+}
+
+int main()
+{
+  pthread_t tid;
+
+  pthread_mutex_init(&m, 0);
+  pthread_create(&tid, 0, producer, 0);
+
+  __VERIFIER_atomic_begin();
+  int g2 = g;
+  int used2 = used;
+  __goblint_check(used2 == 0); // UNKNOWN!
+  __goblint_check(g2 == 1 || used2 == 0); // TODO (unprotected invariant precision loss?)
+  __VERIFIER_atomic_end();
+
+  __VERIFIER_atomic_begin();
+  g = 1;
+  pthread_mutex_lock(&m);
+  __VERIFIER_atomic_end();
+
+  __goblint_check(used == 0);
+
+  __VERIFIER_atomic_begin();
+  g = 0;
+  pthread_mutex_unlock(&m);
+  __VERIFIER_atomic_end();
+
+  pthread_mutex_destroy(&m);
+  return 0;
+}
diff --git a/tests/regression/46-apron2/78-case_distinction_with_ghosts-3.c b/tests/regression/46-apron2/78-case_distinction_with_ghosts-3.c
new file mode 100644
index 0000000000..1d250870cc
--- /dev/null
+++ b/tests/regression/46-apron2/78-case_distinction_with_ghosts-3.c
@@ -0,0 +1,31 @@
+// SKIP PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-tid-atomic --set sem.int.signed_overflow assume_none --set ana.path_sens[+] threadflag
+#include <pthread.h>
+#include <assert.h>
+
+extern int  __VERIFIER_nondet_int();
+extern void __VERIFIER_atomic_begin();
+extern void __VERIFIER_atomic_end();
+
+int x = 0;
+int g = 0;
+
+void* inc()
+{
+  __VERIFIER_atomic_begin();
+  int x2 = x;
+  int g2 = g;
+  __VERIFIER_atomic_end();
+  return 0;
+}
+
+int main()
+{
+  pthread_t tid;
+  pthread_create(&tid, 0, inc, 0);
+  __VERIFIER_atomic_begin();
+  g = 1; x = 42;
+  __VERIFIER_atomic_end();
+
+  assert(x >= 42);
+  return 0;
+}
diff --git a/tests/regression/56-witness/08-witness-all-locals.c b/tests/regression/56-witness/08-witness-all-locals.c
new file mode 100644
index 0000000000..982296829a
--- /dev/null
+++ b/tests/regression/56-witness/08-witness-all-locals.c
@@ -0,0 +1,10 @@
+// CRAM PARAM: --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --disable witness.invariant.all-locals
+int main() {
+  int x;
+  x = 5;
+  {
+    int y;
+    y = 10;
+  }
+  return 0;
+}
diff --git a/tests/regression/56-witness/08-witness-all-locals.t b/tests/regression/56-witness/08-witness-all-locals.t
new file mode 100644
index 0000000000..64ab054549
--- /dev/null
+++ b/tests/regression/56-witness/08-witness-all-locals.t
@@ -0,0 +1,22 @@
+  $ goblint --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --enable witness.invariant.all-locals 08-witness-all-locals.c
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 4
+    dead: 0
+    total lines: 4
+  [Info][Witness] witness generation summary:
+    total generation entries: 3
+
+TODO: check witness.yml content with yamlWitnessStrip
+
+Fewer entries are emitted if locals from nested block scopes are excluded:
+
+  $ goblint --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --disable witness.invariant.all-locals 08-witness-all-locals.c
+  [Warning] Disabling witness.invariant.all-locals implicitly enables cil.addNestedScopeAttr.
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 4
+    dead: 0
+    total lines: 4
+  [Info][Witness] witness generation summary:
+    total generation entries: 2
+
+TODO: check witness.yml content with yamlWitnessStrip
diff --git a/tests/regression/56-witness/dune b/tests/regression/56-witness/dune
new file mode 100644
index 0000000000..aff6f94276
--- /dev/null
+++ b/tests/regression/56-witness/dune
@@ -0,0 +1,2 @@
+(cram
+ (deps (glob_files *.c) (glob_files ??-*.yml)))