diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml
index 8ca986f52f..cd0414d6fe 100644
--- a/.github/workflows/docs.yml
+++ b/.github/workflows/docs.yml
@@ -52,7 +52,7 @@ jobs:
         run: opam exec -- dune build @doc
 
       - name: Upload artifact
-        uses: actions/upload-pages-artifact@v1
+        uses: actions/upload-pages-artifact@v2
         with:
           path: _build/default/_doc/_html/
 
diff --git a/.github/workflows/locked.yml b/.github/workflows/locked.yml
index 751ade6880..358682a2f3 100644
--- a/.github/workflows/locked.yml
+++ b/.github/workflows/locked.yml
@@ -174,5 +174,4 @@ jobs:
 
       - name: Test Gobview
         run: |
-          ./goblint --enable gobview tests/regression/00-sanity/01-assert.c
           python3 scripts/test-gobview.py
diff --git a/docs/user-guide/inspecting.md b/docs/user-guide/inspecting.md
index 67aa86aa97..f4f6036f1b 100644
--- a/docs/user-guide/inspecting.md
+++ b/docs/user-guide/inspecting.md
@@ -22,4 +22,4 @@ To build GobView (also for development):
 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:8000>
+4. Visit <http://localhost:8080>
diff --git a/scripts/test-gobview.py b/scripts/test-gobview.py
index 0dc2cacaa4..1ac8f6a76c 100644
--- a/scripts/test-gobview.py
+++ b/scripts/test-gobview.py
@@ -7,32 +7,30 @@
 from selenium.webdriver.common.by import By
 from selenium.webdriver.chrome.options import Options
 from threading import Thread
-import http.server
-import socketserver
+import subprocess
 
-PORT = 9000
+PORT = 8080 # has to match port defined in goblint_http.ml
 DIRECTORY = "run"
 IP = "localhost"
 url = 'http://' + IP + ':' + str(PORT) + '/'
 
 # cleanup
-def cleanup(browser, httpd, thread):
+def cleanup(browser, thread):
   print("cleanup")
   browser.close()
-  httpd.shutdown()
-  httpd.server_close()
+  p.kill()
   thread.join()
 
 # serve GobView in different thread so it does not block the testing
-class Handler(http.server.SimpleHTTPRequestHandler):
-    def __init__(self, *args, **kwargs):
-        super().__init__(*args, directory=DIRECTORY, **kwargs)
-class Server(socketserver.TCPServer):
-    allow_reuse_address = True # avoids that during a consecutive run the server cannot connect due to an 'Adress already in use' os error
+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"'])
 
-httpd = Server((IP, PORT), Handler)
 print("serving at port", PORT)
-thread = Thread(target=httpd.serve_forever, args=())
+thread = Thread(target=serve, args=())
 thread.start()
 
 # installation of browser
@@ -42,6 +40,7 @@ class Server(socketserver.TCPServer):
 browser = webdriver.Chrome(service=Service(ChromeDriverManager().install()),options=options)
 print("finished webdriver installation \n")
 browser.maximize_window()
+browser.implicitly_wait(10);
 
 try:
     # retrieve and wait until page is fully loaded and rendered
@@ -62,8 +61,8 @@ class Server(socketserver.TCPServer):
     panel = browser.find_element(By.CLASS_NAME, "panel")
     print("found DOM elements main, sidebar-left, sidebar-right, content and panel")
 
-    cleanup(browser, httpd, thread)
+    cleanup(browser, thread)
 
 except Exception as e:
-    cleanup(browser, httpd, thread)
+    cleanup(browser, thread)
     raise e
diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml
index 8988a83c76..c5ad08ec76 100644
--- a/src/analyses/apron/relationAnalysis.apron.ml
+++ b/src/analyses/apron/relationAnalysis.apron.ml
@@ -507,6 +507,12 @@ struct
     | Unknown, "__goblint_assume_join" ->
       let id = List.hd args in
       Priv.thread_join ~force:true ask ctx.global id st
+    | Rand, _ ->
+      (match r with
+       | Some lv ->
+         let st = invalidate_one ask ctx st lv in
+         assert_fn {ctx with local = st} (BinOp (Ge, Lval lv, zero, intType)) true
+       | None -> st)
     | _, _ ->
       let lvallist e =
         let s = ask.f (Queries.MayPointTo e) in
diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml
index 5302478dd9..b386af162b 100644
--- a/src/analyses/apron/relationPriv.apron.ml
+++ b/src/analyses/apron/relationPriv.apron.ml
@@ -713,11 +713,7 @@ module DownwardClosedCluster (ClusteringArg: ClusteringArg) =  functor (RD: Rela
 struct
   open CommonPerMutex(RD)
 
-  module VS =
-  struct
-    include Printable.Std
-    include SetDomain.Make (CilType.Varinfo)
-  end
+  module VS = SetDomain.Make (CilType.Varinfo)
   module LRD = MapDomain.MapBot (VS) (RD)
 
   let keep_only_protected_globals ask m octs =
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index fca27d96da..01fc47e472 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -1336,7 +1336,8 @@ struct
           (* ignore @@ printf "EvalStr Unknown: %a -> %s\n" d_plainexp e (VD.short 80 x); *)
           Queries.Result.top q
       end
-    | Q.IsMultiple v -> WeakUpdates.mem v ctx.local.weak
+    | Q.IsMultiple v -> WeakUpdates.mem v ctx.local.weak ||
+                        (hasAttribute "thread" v.vattr && v.vaddrof) (* thread-local variables if they have their address taken, as one could then compare several such variables *)
     | Q.IterSysVars (vq, vf) ->
       let vf' x = vf (Obj.repr (V.priv x)) in
       Priv.iter_sys_vars (priv_getg ctx.global) vq vf'
@@ -2362,6 +2363,13 @@ struct
       let rv = ensure_not_zero @@ eval_rv ask ctx.global ctx.local value in
       let t = Cilfacade.typeOf value in
       set ~ctx ~t_override:t ask ctx.global ctx.local (AD.of_var !longjmp_return) t rv (* Not raising Deadcode here, deadcode is raised at a higher level! *)
+    | Rand, _ ->
+      begin match lv with
+      | Some x -> 
+        let result:value = (Int (ID.starting IInt Z.zero)) in
+        set ~ctx (Analyses.ask_of_ctx ctx) gs st (eval_lv (Analyses.ask_of_ctx ctx) ctx.global st x) (Cilfacade.typeOfLval x) result
+      | None -> st
+      end
     | _, _ ->
       let st =
         special_unknown_invalidate ctx (Analyses.ask_of_ctx ctx) gs st f args
diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml
index 8878dc49f9..aaef8076df 100644
--- a/src/analyses/baseInvariant.ml
+++ b/src/analyses/baseInvariant.ml
@@ -57,33 +57,30 @@ struct
     | Bot -> false (* HACK: bot is here due to typing conflict (we do not cast appropriately) *)
     | _ -> VD.is_bot_value x
 
-  let apply_invariant oldv newv =
-    match oldv, newv with
-    (* | Address o, Address n when AD.mem (Addr.unknown_ptr ()) o && AD.mem (Addr.unknown_ptr ()) n -> *)
-    (*   Address (AD.join o n) *)
-    (* | Address o, Address n when AD.mem (Addr.unknown_ptr ()) o -> Address n *)
-    (* | Address o, Address n when AD.mem (Addr.unknown_ptr ()) n -> Address o *)
-    | _ -> VD.meet oldv newv
+  let apply_invariant ~old_val ~new_val =
+    try
+      VD.meet old_val new_val
+    with Lattice.Uncomparable -> old_val
 
   let refine_lv_fallback ctx a gs st lval value tv =
     if M.tracing then M.tracec "invariant" "Restricting %a with %a\n" d_lval lval VD.pretty value;
     let addr = eval_lv a gs st lval in
     if (AD.is_top addr) then st
     else
-      let oldval = get a gs st addr None in (* None is ok here, we could try to get more precise, but this is ok (reading at unknown position in array) *)
+      let old_val = get a gs st addr None in (* None is ok here, we could try to get more precise, but this is ok (reading at unknown position in array) *)
       let t_lval = Cilfacade.typeOfLval lval in
-      let oldval = map_oldval oldval t_lval in
-      let oldval =
-        if is_some_bot oldval then (
+      let old_val = map_oldval old_val t_lval in
+      let old_val =
+        if is_some_bot old_val then (
           if M.tracing then M.tracec "invariant" "%a is bot! This should not happen. Will continue with top!" d_lval lval;
           VD.top ()
         )
         else
-          oldval
+          old_val
       in
       let state_with_excluded = set a gs st addr t_lval value ~ctx in
       let value =  get a gs state_with_excluded addr None in
-      let new_val = apply_invariant oldval value in
+      let new_val = apply_invariant ~old_val ~new_val:value in
       if M.tracing then M.traceu "invariant" "New value is %a\n" VD.pretty new_val;
       (* make that address meet the invariant, i.e exclusion sets will be joined *)
       if is_some_bot new_val then (
@@ -99,14 +96,14 @@ struct
     match x with
     | Var var, o when refine_entire_var ->
       (* For variables, this is done at to the level of entire variables to benefit e.g. from disjunctive struct domains *)
-      let oldv = get_var a gs st var in
-      let oldv = map_oldval oldv var.vtype in
+      let old_val = get_var a gs st var in
+      let old_val = map_oldval old_val var.vtype in
       let offs = convert_offset a gs st o in
-      let newv = VD.update_offset (Queries.to_value_domain_ask a) oldv offs c' (Some exp) x (var.vtype) in
-      let v = VD.meet oldv newv in
+      let new_val = VD.update_offset (Queries.to_value_domain_ask a) old_val offs c' (Some exp) x (var.vtype) in
+      let v = apply_invariant ~old_val ~new_val in
       if is_some_bot v then contra st
       else (
-        if M.tracing then M.tracel "inv" "improve variable %a from %a to %a (c = %a, c' = %a)\n" CilType.Varinfo.pretty var VD.pretty oldv VD.pretty v pretty c VD.pretty c';
+        if M.tracing then M.tracel "inv" "improve variable %a from %a to %a (c = %a, c' = %a)\n" CilType.Varinfo.pretty var VD.pretty old_val VD.pretty v pretty c VD.pretty c';
         let r = set' (Var var,NoOffset) v st in
         if M.tracing then M.tracel "inv" "st from %a to %a\n" D.pretty st D.pretty r;
         r
@@ -114,12 +111,12 @@ struct
     | Var _, _
     | Mem _, _ ->
       (* For accesses via pointers, not yet *)
-      let oldv = eval_rv_lval_refine a gs st exp x in
-      let oldv = map_oldval oldv (Cilfacade.typeOfLval x) in
-      let v = VD.meet oldv c' in
+      let old_val = eval_rv_lval_refine a gs st exp x in
+      let old_val = map_oldval old_val (Cilfacade.typeOfLval x) in
+      let v = apply_invariant ~old_val ~new_val:c' in
       if is_some_bot v then contra st
       else (
-        if M.tracing then M.tracel "inv" "improve lval %a from %a to %a (c = %a, c' = %a)\n" d_lval x VD.pretty oldv VD.pretty v pretty c VD.pretty c';
+        if M.tracing then M.tracel "inv" "improve lval %a from %a to %a (c = %a, c' = %a)\n" d_lval x VD.pretty old_val VD.pretty v pretty c VD.pretty c';
         set' x v st
       )
 
diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml
index 151bc94a91..1b92cb320d 100644
--- a/src/analyses/commonPriv.ml
+++ b/src/analyses/commonPriv.ml
@@ -117,11 +117,7 @@ module Locksets =
 struct
   module Lock = LockDomain.Addr
 
-  module Lockset =
-  struct
-    include Printable.Std (* To make it Groupable *)
-    include SetDomain.ToppedSet (Lock) (struct let topname = "All locks" end)
-  end
+  module Lockset = SetDomain.ToppedSet (Lock) (struct let topname = "All locks" end)
 
   module MustLockset = SetDomain.Reverse (Lockset)
 
diff --git a/src/analyses/libraryDesc.ml b/src/analyses/libraryDesc.ml
index 8b90553e95..2df292772a 100644
--- a/src/analyses/libraryDesc.ml
+++ b/src/analyses/libraryDesc.ml
@@ -72,6 +72,7 @@ type special =
   | Identity of Cil.exp (** Identity function. Some compiler optimization annotation functions map to this. *)
   | Setjmp of { env: Cil.exp; }
   | Longjmp of { env: Cil.exp; value: Cil.exp; }
+  | Rand
   | Unknown (** Anything not belonging to other types. *) (* TODO: rename to Other? *)
 
 
diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml
index 56230529e6..1c4e84eab4 100644
--- a/src/analyses/libraryFunctions.ml
+++ b/src/analyses/libraryFunctions.ml
@@ -70,6 +70,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("_setjmp", special [__ "env" [w]] @@ fun env -> Setjmp { env }); (* only has one underscore *)
     ("setjmp", special [__ "env" [w]] @@ fun env -> Setjmp { env });
     ("longjmp", special [__ "env" [r]; __ "value" []] @@ fun env value -> Longjmp { env; value });
+    ("rand", special [] Rand);
   ]
 
 (** C POSIX library functions.
@@ -872,7 +873,6 @@ let invalidate_actions = [
     "sendto", writes [2;4]; (*keep [2;4]*)
     "recvfrom", writes [4;5]; (*keep [4;5]*)
     "srand", readsAll; (*safe*)
-    "rand", readsAll; (*safe*)
     "gethostname", writesAll; (*unsafe*)
     "fork", readsAll; (*safe*)
     "setrlimit", readsAll; (*safe*)
diff --git a/src/analyses/spec.ml b/src/analyses/spec.ml
index b594214518..d7328310dd 100644
--- a/src/analyses/spec.ml
+++ b/src/analyses/spec.ml
@@ -253,7 +253,7 @@ struct
     | Some k1, Some k2 when D.mem k2 m -> (* only k2 in D *)
       M.debug ~category:Analyzer "assign (only k2 in D): %s = %s" (D.string_of_key k1) (D.string_of_key k2);
       let m = D.alias k1 k2 m in (* point k1 to k2 *)
-      if Basetype.Variables.to_group (fst k2) = Some Temp (* check if k2 is a temporary Lval introduced by CIL *)
+      if Basetype.Variables.to_group (fst k2) = Temp (* check if k2 is a temporary Lval introduced by CIL *)
       then D.remove' k2 m (* if yes we need to remove it from our map *)
       else m (* otherwise no change *)
     | Some k1, _ when D.mem k1 m -> (* k1 in D and assign something unknown *)
diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml
index bcfd9979fc..c3aebc985e 100644
--- a/src/analyses/useAfterFree.ml
+++ b/src/analyses/useAfterFree.ml
@@ -1,10 +1,11 @@
-(** An analysis for the detection of use-after-free vulnerabilities. *)
+(** An analysis for the detection of use-after-free vulnerabilities ([useAfterFree]). *)
 
 open GoblintCil
 open Analyses
 open MessageCategory
 
 module ToppedVarInfoSet = SetDomain.ToppedSet(CilType.Varinfo)(struct let topname = "All Heap Variables" end)
+module ThreadIdSet = SetDomain.Make(ThreadIdDomain.ThreadLifted)
 
 module Spec : Analyses.MCPSpec =
 struct
@@ -14,6 +15,8 @@ struct
 
   module D = ToppedVarInfoSet
   module C = Lattice.Unit
+  module G = ThreadIdSet
+  module V = VarinfoV
 
   (** TODO: Try out later in benchmarks to see how we perform with and without context-sensititivty *)
   let context _ _ = ()
@@ -21,15 +24,52 @@ struct
 
   (* HELPER FUNCTIONS *)
 
-  let warn_for_multi_threaded ctx behavior cwe_number =
-    if not (ctx.ask (Queries.MustBeSingleThreaded { since_start = true })) then
-      M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Program isn't running in single-threaded mode. Use-After-Free might occur due to multi-threading"
+  let get_current_threadid ctx =
+    ctx.ask Queries.CurrentThreadId
+
+  let warn_for_multi_threaded_access ctx (heap_var:varinfo) behavior cwe_number =
+    let freeing_threads = ctx.global heap_var in
+    (* If we're single-threaded or there are no threads freeing the memory, we have nothing to WARN about *)
+    if ctx.ask (Queries.MustBeSingleThreaded { since_start = true }) || ThreadIdSet.is_empty freeing_threads then ()
+    else begin
+      let possibly_started current = function
+        | `Lifted tid ->
+          let threads = ctx.ask Queries.CreatedThreads in
+          let not_started = MHP.definitely_not_started (current, threads) tid in
+          let possibly_started = not not_started in
+          possibly_started
+        | `Top -> true
+        | `Bot -> false
+      in
+      let equal_current current = function
+        | `Lifted tid ->
+          ThreadId.Thread.equal current tid
+        | `Top -> true
+        | `Bot -> false
+      in
+      match get_current_threadid ctx with
+      | `Lifted current ->
+        let possibly_started = ThreadIdSet.exists (possibly_started current) freeing_threads in
+        if possibly_started then
+          M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "There's a thread that's been started in parallel with the memory-freeing threads for heap variable %a. Use-After-Free might occur" CilType.Varinfo.pretty heap_var
+        else begin
+          let current_is_unique = ThreadId.Thread.is_unique current in
+          let any_equal_current threads = ThreadIdSet.exists (equal_current current) threads in
+          if not current_is_unique && any_equal_current freeing_threads then
+            M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Current thread is not unique and a Use-After-Free might occur for heap variable %a" CilType.Varinfo.pretty heap_var
+          else if D.mem heap_var ctx.local then
+            M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Use-After-Free might occur in current unique thread %a for heap variable %a" ThreadIdDomain.FlagConfiguredTID.pretty current CilType.Varinfo.pretty heap_var
+        end
+      | `Top ->
+        M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "CurrentThreadId is top. A Use-After-Free might occur for heap variable %a" CilType.Varinfo.pretty heap_var
+      | `Bot ->
+        M.warn ~category:MessageCategory.Analyzer "CurrentThreadId is bottom"
+    end
 
   let rec warn_lval_might_contain_freed ?(is_double_free = false) (transfer_fn_name:string) ctx (lval:lval) =
     let state = ctx.local in
     let undefined_behavior = if is_double_free then Undefined DoubleFree else Undefined UseAfterFree in
     let cwe_number = if is_double_free then 415 else 416 in
-    warn_for_multi_threaded ctx undefined_behavior cwe_number; (* Simple solution to warn when multi-threaded *)
     let rec offset_might_contain_freed offset =
       match offset with
       | NoOffset -> ()
@@ -53,7 +93,9 @@ struct
         |> List.map fst
         |> List.filter (fun var -> ctx.ask (Queries.IsHeapVar var))
       in
-      List.iter warn_for_heap_var pointed_to_heap_vars (* Warn for all heap vars that the lval possibly points to *)
+      List.iter warn_for_heap_var pointed_to_heap_vars; (* Warn for all heap vars that the lval possibly points to *)
+      (* Warn for a potential multi-threaded UAF for all heap vars that the lval possibly points to *)
+      List.iter (fun heap_var -> warn_for_multi_threaded_access ctx heap_var undefined_behavior cwe_number) pointed_to_heap_vars
     | _ -> ()
 
   and warn_exp_might_contain_freed ?(is_double_free = false) (transfer_fn_name:string) ctx (exp:exp) =
@@ -83,6 +125,10 @@ struct
     | StartOf lval
     | AddrOf lval -> warn_lval_might_contain_freed ~is_double_free transfer_fn_name ctx lval
 
+  let side_effect_mem_free ctx freed_heap_vars threadid =
+    let threadid = G.singleton threadid in
+    D.iter (fun var -> ctx.sideg var threadid) freed_heap_vars
+
 
   (* TRANSFER FUNCTIONS *)
 
@@ -138,8 +184,11 @@ struct
             Queries.LS.elements a
             |> List.map fst
             |> List.filter (fun var -> ctx.ask (Queries.IsHeapVar var))
+            |> D.of_list
           in
-          D.join state (D.of_list pointed_to_heap_vars) (* Add all heap vars, which ptr points to, to the state *)
+          (* Side-effect the tid that's freeing all the heap vars collected here *)
+          side_effect_mem_free ctx pointed_to_heap_vars (get_current_threadid ctx);
+          D.join state (pointed_to_heap_vars) (* Add all heap vars, which ptr points to, to the state *)
         | _ -> state
       end
     | _ -> state
diff --git a/src/cdomains/addressDomain.ml b/src/cdomains/addressDomain.ml
index d6b4ed577b..9f6ee56cbf 100644
--- a/src/cdomains/addressDomain.ml
+++ b/src/cdomains/addressDomain.ml
@@ -76,12 +76,6 @@ module AddressPrintable (Mval: Mval.Printable) =
 struct
   include AddressBase (Mval)
 
-  type group = Basetype.Variables.group
-  let show_group = Basetype.Variables.show_group
-  let to_group = function
-    | Addr (x,_) -> Basetype.Variables.to_group x
-    | _ -> Some Basetype.Variables.Local
-
   let of_var x = Addr (x, `NoOffset)
   let of_mval (x, o) = Addr (x, o)
 
diff --git a/src/cdomains/addressDomain_intf.ml b/src/cdomains/addressDomain_intf.ml
index e80922d7f9..0ef3d6dd8d 100644
--- a/src/cdomains/addressDomain_intf.ml
+++ b/src/cdomains/addressDomain_intf.ml
@@ -9,7 +9,6 @@ sig
       | UnknownPtr (** Unknown pointer. Could point to globals, heap and escaped variables. *)
       | StrPtr of string option (** String literal pointer. [StrPtr None] abstracts any string pointer *)
     include Printable.S with type t := t (** @closed *)
-    include MapDomain.Groupable with type t := t (** @closed *)
 
     val of_string: string -> t
     (** Convert string to {!StrPtr}. *)
@@ -32,7 +31,6 @@ sig
   module AddressPrintable (Mval: Mval.Printable):
   sig
     include module type of AddressBase (Mval)
-    include MapDomain.Groupable with type t := t and type group = Basetype.Variables.group (** @closed *)
 
     val is_definite: t -> bool
     (** Whether address is a [NULL] pointer or an mvalue that has only definite integer indexing (and fields). *)
diff --git a/src/cdomains/baseDomain.ml b/src/cdomains/baseDomain.ml
index 6950c16889..ce6cc171fa 100644
--- a/src/cdomains/baseDomain.ml
+++ b/src/cdomains/baseDomain.ml
@@ -6,20 +6,14 @@ module BI = IntOps.BigIntOps
 
 module CPA =
 struct
+  module M0 = MapDomain.MapBot (Basetype.Variables) (VD)
   module M =
   struct
-    include MapDomain.LiftTop (VD) (MapDomain.HashCached (MapDomain.MapBot (Basetype.Variables) (VD)))
-    let name () = "value domain"
+    include M0
+    include MapDomain.PrintGroupable (Basetype.Variables) (VD) (M0)
   end
-
-  include M
-end
-
-
-module Glob =
-struct
-  module Var = Basetype.Variables
-  module Val = VD
+  include MapDomain.LiftTop (VD) (MapDomain.HashCached (M))
+  let name () = "value domain"
 end
 
 (* Keeps track of which arrays are potentially partitioned according to an expression containing a specific variable *)
diff --git a/src/cdomains/basetype.ml b/src/cdomains/basetype.ml
index d576b803b6..55b5dbde07 100644
--- a/src/cdomains/basetype.ml
+++ b/src/cdomains/basetype.ml
@@ -6,16 +6,14 @@ open GoblintCil
 module Variables =
 struct
   include CilType.Varinfo
-  let trace_enabled = true
   let show x =
     if RichVarinfo.BiVarinfoMap.Collection.mem_varinfo x then
       let description = RichVarinfo.BiVarinfoMap.Collection.describe_varinfo x in
       "(" ^ x.vname ^ ", " ^ description ^ ")"
     else x.vname
   let pretty () x = Pretty.text (show x)
-  type group = Global | Local | Parameter | Temp [@@deriving show { with_path = false }]
-  let (%) = Batteries.(%)
-  let to_group = Option.some % function
+  type group = Global | Local | Parameter | Temp [@@deriving ord, show { with_path = false }]
+  let to_group = function
     | x when x.vglob -> Global
     | x when x.vdecl.line = -1 -> Temp
     | x when Cilfacade.is_varinfo_formal x -> Parameter
@@ -62,7 +60,6 @@ module Bools: Lattice.S with type t = [`Bot | `Lifted of bool | `Top] =
 
 module CilExp =
 struct
-  include Printable.Std (* for Groupable *)
   include CilType.Exp
 
   let name () = "expressions"
@@ -159,8 +156,4 @@ struct
   let printXml f x = BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" (XmlUtil.escape (show x))
 end
 
-module CilField =
-struct
-  include Printable.Std (* for default MapDomain.Groupable *)
-  include CilType.Fieldinfo
-end
+module CilField = CilType.Fieldinfo
diff --git a/src/cdomains/intDomain.ml b/src/cdomains/intDomain.ml
index 589239810f..b1db3796a8 100644
--- a/src/cdomains/intDomain.ml
+++ b/src/cdomains/intDomain.ml
@@ -513,16 +513,19 @@ module Size = struct (* size in bits as int, range as int64 *)
     BI.compare to_min from_min <= 0 && BI.compare from_max to_max <= 0
 
   let cast t x = (* TODO: overflow is implementation-dependent! *)
-    let a,b = range t in
-    let c = card t in
-    (* let z = add (rem (sub x a) c) a in (* might lead to overflows itself... *)*)
-    let y = Z.erem x c in
-    let y = if Z.gt y b then Z.sub y c
-      else if Z.lt y a then Z.add y c
-      else y
-    in
-    if M.tracing then M.tracel "cast_int" "Cast %s to range [%s, %s] (%s) = %s (%s in int64)\n" (Z.to_string x) (Z.to_string a) (Z.to_string b) (Z.to_string c) (Z.to_string y) (if is_int64_big_int y then "fits" else "does not fit");
-    y
+    if t = IBool then
+      (* C11 6.3.1.2 Boolean type *) 
+      if Z.equal x Z.zero then Z.zero else Z.one
+    else
+      let a,b = range t in
+      let c = card t in
+      let y = Z.erem x c in
+      let y = if Z.gt y b then Z.sub y c
+        else if Z.lt y a then Z.add y c
+        else y
+      in
+      if M.tracing then M.tracel "cast" "Cast %s to range [%s, %s] (%s) = %s (%s in int64)\n" (Z.to_string x) (Z.to_string a) (Z.to_string b) (Z.to_string c) (Z.to_string y) (if is_int64_big_int y then "fits" else "does not fit");
+      y
 
   let min_range_sign_agnostic x =
     let size ik =
@@ -1975,18 +1978,22 @@ struct
   let top_of ik = `Excluded (S.empty (), size ik)
   let cast_to ?torg ?no_ov ik = function
     | `Excluded (s,r) ->
-      let r' = size ik in
-      `Excluded (
+      let r' = size ik in 
         if R.leq r r' then (* upcast -> no change *)
-          s, r
-        else (* downcast: may overflow *)
+          `Excluded (s, r)
+        else if ik = IBool then (* downcast to bool *)
+          if S.mem BI.zero s then
+            `Definite (BI.one)
+          else
+            `Excluded (S.empty(), r')
+        else 
+          (* downcast: may overflow *)
           (* let s' = S.map (BigInt.cast_to ik) s in *)
           (* We want to filter out all i in s' where (t)x with x in r could be i. *)
           (* 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 *)
-          S.empty (), r'
-      )
+          `Excluded (S.empty (), r')
     | `Definite x -> `Definite (BigInt.cast_to ik x)
     | `Bot -> `Bot
 
@@ -2518,6 +2525,11 @@ module Enums : S with type int_t = BigInt.t = struct
       let r' = size ik in
       if R.leq r r' then (* upcast -> no change *)
         Exc (s, r)
+      else if ik = IBool then (* downcast to bool *)
+        if BISet.mem BI.zero s then
+          Inc (BISet.singleton BI.one)
+        else
+          Exc (BISet.empty(), r')
       else (* downcast: may overflow *)
         Exc ((BISet.empty ()), r')
     | Inc xs ->
diff --git a/src/cdomains/lockDomain.ml b/src/cdomains/lockDomain.ml
index 3a6ea3b52d..0de5afc32c 100644
--- a/src/cdomains/lockDomain.ml
+++ b/src/cdomains/lockDomain.ml
@@ -11,12 +11,6 @@ module Mutexes = SetDomain.ToppedSet (Addr) (struct let topname = "All mutexes"
 module Simple = Lattice.Reverse (Mutexes)
 module Priorities = IntDomain.Lifted
 
-module Glob =
-struct
-  module Var = Basetype.Variables
-  module Val = Simple
-end
-
 module Lockset =
 struct
 
diff --git a/src/cdomains/mval_intf.ml b/src/cdomains/mval_intf.ml
index ac0e6c4666..7b956bf8b8 100644
--- a/src/cdomains/mval_intf.ml
+++ b/src/cdomains/mval_intf.ml
@@ -5,7 +5,6 @@ sig
 
   type t = GoblintCil.varinfo * idx Offset.t
   include Printable.S with type t := t (** @closed *)
-  include MapDomain.Groupable with type t := t (** @closed *)
 
   val is_definite: t -> bool
   (** Whether offset of mvalue has only definite integer indexing (and fields). *)
diff --git a/src/cdomains/threadIdDomain.ml b/src/cdomains/threadIdDomain.ml
index a081835b34..7193552048 100644
--- a/src/cdomains/threadIdDomain.ml
+++ b/src/cdomains/threadIdDomain.ml
@@ -7,7 +7,6 @@ open BatPervasives
 module type S =
 sig
   include Printable.S
-  include MapDomain.Groupable with type t := t
 
   val threadinit: varinfo -> multiple:bool -> t
   val is_main: t -> bool
@@ -212,7 +211,7 @@ struct
   (* Plain thread IDs *)
   module P = Unit(FunNode)
 
-  include GroupableFlagHelper(H)(P)(struct
+  include FlagHelper(H)(P)(struct
       let msg = "FlagConfiguredTID received a value where not exactly one component is set"
       let name = "FlagConfiguredTID"
     end)
diff --git a/src/cdomains/unionDomain.ml b/src/cdomains/unionDomain.ml
index 08efecf421..ac25450c6a 100644
--- a/src/cdomains/unionDomain.ml
+++ b/src/cdomains/unionDomain.ml
@@ -15,16 +15,29 @@ sig
   val invariant: value_invariant:(offset:Cil.offset -> lval:Cil.lval -> value -> Invariant.t) -> offset:Cil.offset -> lval:Cil.lval -> t -> Invariant.t
 end
 
-module Field =  Lattice.Flat (CilType.Fieldinfo) (struct
-    let top_name = "Unknown field"
-    let bot_name = "If you see this, you are special!"
-  end)
+module Field = struct
+  include Lattice.Flat (CilType.Fieldinfo) (struct
+      let top_name = "Unknown field"
+      let bot_name = "If you see this, you are special!"
+    end)
+
+  let meet f g =
+    if equal f g then
+      f
+    else
+      raise Lattice.Uncomparable
+end
 
 module Simple (Values: Arg) =
 struct
   include Lattice.Prod (Field) (Values)
   type value = Values.t
 
+  let meet (f, x) (g, y) =
+    let field = Field.meet f g in
+    let value = Values.meet x y in
+    (field, value)
+
   let invariant ~value_invariant ~offset ~lval (lift_f, v) =
     match offset with
     (* invariants for all fields *)
diff --git a/src/cdomains/valueDomain.ml b/src/cdomains/valueDomain.ml
index ccc7e0b2c8..4e40f3a287 100644
--- a/src/cdomains/valueDomain.ml
+++ b/src/cdomains/valueDomain.ml
@@ -545,9 +545,7 @@ struct
         | None -> AD.join y AD.top_ptr)
     | (Address x, Address y) -> Address (AD.join x y)
     | (Struct x, Struct y) -> Struct (Structs.join x y)
-    | (Union (f,x), Union (g,y)) -> Union (match UnionDomain.Field.join f g with
-        | `Lifted f -> (`Lifted f, join x y) (* f = g *)
-        | x -> (x, Top)) (* f <> g *)
+    | (Union x, Union y) -> Union (Unions.join x y)
     | (Array x, Array y) -> Array (CArrays.join x y)
     | (Blob x, Blob y) -> Blob (Blobs.join x y)
     | Blob (x,s,o), y
@@ -582,9 +580,7 @@ struct
         | None -> AD.widen y (AD.join y AD.top_ptr))
     | (Address x, Address y) -> Address (AD.widen x y)
     | (Struct x, Struct y) -> Struct (Structs.widen x y)
-    | (Union (f,x), Union (g,y)) -> Union (match UnionDomain.Field.widen f g with
-        | `Lifted f -> (`Lifted f, widen x y) (* f = g *)
-        | x -> (x, Top))
+    | (Union x, Union y) -> Union (Unions.widen x y)
     | (Array x, Array y) -> Array (CArrays.widen x y)
     | (Blob x, Blob y) -> Blob (Blobs.widen x y)
     | (Thread x, Thread y) -> Thread (Threads.widen x y)
@@ -605,9 +601,10 @@ struct
     let join_elem: (t -> t -> t) = smart_join x_eval_int y_eval_int in  (* does not compile without type annotation *)
     match (x,y) with
     | (Struct x, Struct y) -> Struct (Structs.join_with_fct join_elem x y)
-    | (Union (f,x), Union (g,y)) -> Union (match UnionDomain.Field.join f g with
-        | `Lifted f -> (`Lifted f, join_elem x y) (* f = g *)
-        | x -> (x, Top)) (* f <> g *)
+    | (Union (f,x), Union (g,y)) ->
+      let field = UnionDomain.Field.join f g in
+      let value = join_elem x y in
+      Union (field, value)
     | (Array x, Array y) -> Array (CArrays.smart_join x_eval_int y_eval_int x y)
     | _ -> join x y  (* Others can not contain array -> normal join  *)
 
@@ -615,9 +612,10 @@ struct
     let widen_elem: (t -> t -> t) = smart_widen x_eval_int y_eval_int in (* does not compile without type annotation *)
     match (x,y) with
     | (Struct x, Struct y) -> Struct (Structs.widen_with_fct widen_elem x y)
-    | (Union (f,x), Union (g,y)) -> Union (match UnionDomain.Field.widen f g with
-        | `Lifted f -> `Lifted f, widen_elem x y  (* f = g *)
-        | x -> x, Top) (* f <> g *)
+    | (Union (f,x), Union (g,y)) ->
+      let field = UnionDomain.Field.widen f g in
+      let value = widen_elem x y in
+      Union (field, value)
     | (Array x, Array y) -> Array (CArrays.smart_widen x_eval_int y_eval_int x y)
     | _ -> widen x y  (* Others can not contain array -> normal widen  *)
 
diff --git a/src/domains/access.ml b/src/domains/access.ml
index 8c2321233f..a183a32633 100644
--- a/src/domains/access.ml
+++ b/src/domains/access.ml
@@ -92,7 +92,7 @@ struct
   let pretty () vt =
     (* Imitate old printing for now *)
     match vt with
-    | `Var v -> Pretty.dprintf "%a@@%a" CilType.Varinfo.pretty v CilType.Location.pretty v.vdecl
+    | `Var v -> CilType.Varinfo.pretty () v
     | `Type (TComp (c, _)) -> Pretty.dprintf "(struct %s)" c.cname
     | `Type t -> Pretty.dprintf "(%a)" CilType.Typ.pretty t
 
@@ -116,7 +116,7 @@ struct
   let pretty () (vt, o) =
     (* Imitate old printing for now *)
     match vt with
-    | `Var v -> Pretty.dprintf "%a%a@@%a" CilType.Varinfo.pretty v Offset.Unit.pretty o CilType.Location.pretty v.vdecl
+    | `Var v -> Pretty.dprintf "%a%a" CilType.Varinfo.pretty v Offset.Unit.pretty o
     | `Type (TComp (c, _)) -> Pretty.dprintf "(struct %s)%a" c.cname Offset.Unit.pretty o
     | `Type t -> Pretty.dprintf "(%a)%a" CilType.Typ.pretty t Offset.Unit.pretty o
 
@@ -459,6 +459,10 @@ let print_accesses memo grouped_accs =
     AS.elements race_accs
     |> List.map h
   in
+  let group_loc = match memo with
+    | (`Var v, _) -> Some (M.Location.CilLocation v.vdecl) (* TODO: offset location *)
+    | (`Type _, _) -> None (* TODO: type location *)
+  in
   grouped_accs
   |> List.fold_left (fun safe_accs accs ->
       match race_conf accs with
@@ -471,12 +475,12 @@ let print_accesses memo grouped_accs =
           else
             Info
         in
-        M.msg_group severity ~category:Race "Memory location %a (race with conf. %d)" Memo.pretty memo conf (msgs accs);
+        M.msg_group severity ?loc:group_loc ~category:Race "Memory location %a (race with conf. %d)" Memo.pretty memo conf (msgs accs);
         safe_accs
     ) (AS.empty ())
   |> (fun safe_accs ->
       if allglobs && not (AS.is_empty safe_accs) then
-        M.msg_group Success ~category:Race "Memory location %a (safe)" Memo.pretty memo (msgs safe_accs)
+        M.msg_group Success ?loc:group_loc ~category:Race "Memory location %a (safe)" Memo.pretty memo (msgs safe_accs)
     )
 
 let warn_global ~safe ~vulnerable ~unsafe ~ancestor_accs memo accs =
diff --git a/src/domains/disjointDomain.ml b/src/domains/disjointDomain.ml
index 170046214b..d8e59c4ba7 100644
--- a/src/domains/disjointDomain.ml
+++ b/src/domains/disjointDomain.ml
@@ -36,11 +36,6 @@ end
 struct
   type elt = E.t
 
-  module R =
-  struct
-    include Printable.Std (* for Groupable *)
-    include R
-  end
   module M = MapDomain.MapBot (R) (B)
 
   (** Invariant: no explicit bot buckets.
@@ -475,11 +470,6 @@ struct
   type key = E.t
   type value = B.value
 
-  module R =
-  struct
-    include Printable.Std (* for Groupable *)
-    include R
-  end
   module M = MapDomain.MapBot (R) (B)
 
   (** Invariant: no explicit bot buckets.
@@ -610,17 +600,12 @@ struct
         | _, _ -> None
       ) m1 m2
 
-  module GroupableE =
-  struct
-    include Printable.Std (* for Groupable *)
-    include E
-  end
-  include MapDomain.Print (GroupableE) (V) (
+  include MapDomain.Print (E) (V) (
     struct
       type nonrec t = t
       type nonrec key = key
       type nonrec value = value
-      let bindings = bindings
+      let fold = fold
       let iter = iter
     end
     )
@@ -873,17 +858,12 @@ struct
     in
     snd (S.fold f s2 (s1, S.empty ()))
 
-  module GroupableE =
-  struct
-    include Printable.Std (* for Groupable *)
-    include E
-  end
-  include MapDomain.Print (GroupableE) (R) (
+  include MapDomain.Print (E) (R) (
     struct
       type nonrec t = t
       type nonrec key = key
       type nonrec value = value
-      let bindings = bindings
+      let fold = fold
       let iter = iter
     end
     )
diff --git a/src/domains/flagHelper.ml b/src/domains/flagHelper.ml
index 933d371f48..c3bcb584b2 100644
--- a/src/domains/flagHelper.ml
+++ b/src/domains/flagHelper.ml
@@ -40,28 +40,6 @@ struct
   let arbitrary () = failwith (Msg.name ^ ": no arbitrary")
 end
 
-module GroupableFlagHelper (L:MapDomain.Groupable) (R:MapDomain.Groupable) (Msg: FlagError) =
-struct
-  include FlagHelper (L) (R) (Msg)
-  type group = L.group option * R.group option
-
-  let trace_enabled = false
-
-  let show_group = unop L.show_group R.show_group
-  let to_group (h,p) = match (h, p) with
-    | (Some h, None) ->
-      (let r = L.to_group h in
-       match r with
-       | Some r -> Some (Some r, None)
-       | _ -> None)
-    | (None, Some p) ->
-      (let r = R.to_group p in
-       match r with
-       | Some r -> Some (None, Some r)
-       | _ -> None)
-    | _ -> failwith Msg.msg
-end
-
 module type LatticeFlagHelperArg = sig
   include Lattice.PO
   val is_top: t -> bool
diff --git a/src/domains/hoareDomain.ml b/src/domains/hoareDomain.ml
index f14cabf6dc..23b1a92240 100644
--- a/src/domains/hoareDomain.ml
+++ b/src/domains/hoareDomain.ml
@@ -255,12 +255,7 @@ end
 (* TODO: weaken R to Lattice.S ? *)
 module MapBot (SpecD:Lattice.S) (R:SetDomain.S) =
 struct
-  module SpecDGroupable =
-  struct
-    include Printable.Std
-    include SpecD
-  end
-  include MapDomain.MapBot (SpecDGroupable) (R)
+  include MapDomain.MapBot (SpecD) (R)
 
   (* TODO: get rid of these value-ignoring set-mimicing hacks *)
   let choose' = choose
diff --git a/src/domains/mapDomain.ml b/src/domains/mapDomain.ml
index 3dcb4f8d17..6c40ab9792 100644
--- a/src/domains/mapDomain.ml
+++ b/src/domains/mapDomain.ml
@@ -2,7 +2,6 @@
 
 module Pretty = GoblintCil.Pretty
 open Pretty
-module ME = Messages
 
 module type PS =
 sig
@@ -55,69 +54,86 @@ sig
   (* Leq test using a custom leq function for value rather than the default one provided for value *)
 end
 
-module type Groupable =
-sig
-  include Printable.S
-  type group (* use [@@deriving show { with_path = false }] *)
-  val show_group: group -> string
-  val to_group: t -> group option
-  val trace_enabled: bool (* Just a global hack for tracing individual variables. *)
-end
-
 (** Subsignature of {!S}, which is sufficient for {!Print}. *)
 module type Bindings =
 sig
   type t
   type key
   type value
-  val bindings: t -> (key * value) list
+  val fold: (key -> value -> 'a -> 'a) -> t -> 'a -> 'a
   val iter: (key -> value -> unit) -> t -> unit
 end
 
 (** Reusable output definitions for maps. *)
-module Print (D: Groupable) (R: Printable.S) (M: Bindings with type key = D.t and type value = R.t) =
+module Print (D: Printable.S) (R: Printable.S) (M: Bindings with type key = D.t and type value = R.t) =
 struct
-  let show x = "mapping" (* TODO: WTF? *)
+  let pretty () map =
+    let pretty_bindings () = M.fold (fun k v acc ->
+        acc ++ dprintf "%a ->@?  @[%a@]\n" D.pretty k R.pretty v
+      ) map nil
+    in
+    dprintf "@[{\n  @[%t@]}@]" pretty_bindings
+
+  let show map = GobPretty.sprint pretty map
+
+  let printXml f map =
+    BatPrintf.fprintf f "<value>\n<map>\n";
+    M.iter (fun k v ->
+        BatPrintf.fprintf f "<key>\n%s</key>\n%a" (XmlUtil.escape (D.show k)) R.printXml v
+      ) map;
+    BatPrintf.fprintf f "</map>\n</value>\n"
+
+  let to_yojson map =
+    let l = M.fold (fun k v acc ->
+        (D.show k, R.to_yojson v) :: acc
+      ) map []
+    in
+    `Assoc l
+end
+
+module type Groupable =
+sig
+  include Printable.S
+  type group (* use [@@deriving show { with_path = false }] *)
+  val compare_group: group -> group -> int
+  val show_group: group -> string
+  val to_group: t -> group
+end
+
+(** Reusable output definitions for maps with key grouping. *)
+module PrintGroupable (D: Groupable) (R: Printable.S) (M: Bindings with type key = D.t and type value = R.t) =
+struct
+  include Print (D) (R) (M)
+
+  module Group =
+  struct
+    type t = D.group
+    let compare = D.compare_group
+  end
+
+  module GroupMap = Map.Make (Group)
 
   let pretty () mapping =
-    let module MM = Map.Make (D) in
     let groups =
-      let h = Hashtbl.create 13 in
-      M.iter (fun k v -> BatHashtbl.modify_def MM.empty (D.to_group k) (MM.add k v) h) mapping;
-      let cmpBy f a b = Stdlib.compare (f a) (f b) in
-      (* sort groups (order of constructors in type group)  *)
-      BatHashtbl.to_list h |> List.sort (cmpBy fst)
-    in
-    let f key st dok =
-      if ME.tracing && D.trace_enabled && !ME.tracevars <> [] &&
-         not (List.mem (D.show key) !ME.tracevars) then
-        dok
-      else
-        dok ++ dprintf "%a ->@?  @[%a@]\n" D.pretty key R.pretty st
+      M.fold (fun k v acc ->
+          GroupMap.update (D.to_group k) (fun doc ->
+              let doc = Option.value doc ~default:Pretty.nil in
+              let doc' = doc ++ dprintf "%a ->@?  @[%a@]\n" D.pretty k R.pretty v in
+              Some doc'
+            ) acc
+        ) mapping GroupMap.empty
     in
-    let group_name a () = text (D.show_group a) in
-    let pretty_group map () = MM.fold f map nil in
-    let pretty_groups rest (group, map) =
-      match group with
-      | None ->  rest ++ pretty_group map ()
-      | Some g -> rest ++ dprintf "@[%t {\n  @[%t@]}@]\n" (group_name g) (pretty_group map) in
-    let content () = List.fold_left pretty_groups nil groups in
-    dprintf "@[%s {\n  @[%t@]}@]" (show mapping) content
-
-  let printXml f xs =
-    let print_one k v =
-      BatPrintf.fprintf f "<key>\n%s</key>\n%a" (XmlUtil.escape (D.show k)) R.printXml v
-    in
-    BatPrintf.fprintf f "<value>\n<map>\n";
-    M.iter print_one xs;
-    BatPrintf.fprintf f "</map>\n</value>\n"
+    let pretty_groups () = GroupMap.fold (fun group doc acc ->
+        acc ++ dprintf "@[%s {\n  @[%a@]}@]\n" (D.show_group group) Pretty.insert doc
+      ) groups nil in
+    dprintf "@[{\n  @[%t@]}@]" pretty_groups
+
+  let show map = GobPretty.sprint pretty map
 
-  let to_yojson xs =
-    let f (k, v) = (D.show k, R.to_yojson v) in
-    `Assoc (xs |> M.bindings |> List.map f)
+  (* TODO: groups in XML, JSON? *)
 end
 
-module PMap (Domain: Groupable) (Range: Lattice.S) : PS with
+module PMap (Domain: Printable.S) (Range: Lattice.S) : PS with
   type key = Domain.t and
   type value = Range.t =
 struct
@@ -174,7 +190,7 @@ struct
       type nonrec t = t
       type nonrec key = key
       type nonrec value = value
-      let bindings = bindings
+      let fold = fold
       let iter = iter
     end
     )
@@ -363,7 +379,7 @@ struct
   let relift x = M.relift x
 end
 
-module MapBot (Domain: Groupable) (Range: Lattice.S) : S with
+module MapBot (Domain: Printable.S) (Range: Lattice.S) : S with
   type key = Domain.t and
   type value = Range.t =
 struct
@@ -412,7 +428,7 @@ struct
   let narrow = map2 Range.narrow
 end
 
-module MapTop (Domain: Groupable) (Range: Lattice.S) : S with
+module MapTop (Domain: Printable.S) (Range: Lattice.S) : S with
   type key = Domain.t and
   type value = Range.t =
 struct
@@ -583,7 +599,7 @@ struct
     | `Lifted x -> `Lifted (M.mapi f x)
 end
 
-module MapBot_LiftTop (Domain: Groupable) (Range: Lattice.S) : S with
+module MapBot_LiftTop (Domain: Printable.S) (Range: Lattice.S) : S with
   type key = Domain.t and
   type value = Range.t =
 struct
@@ -711,7 +727,7 @@ struct
     | `Lifted x -> `Lifted (M.mapi f x)
 end
 
-module MapTop_LiftBot (Domain: Groupable) (Range: Lattice.S): S with
+module MapTop_LiftBot (Domain: Printable.S) (Range: Lattice.S): S with
   type key = Domain.t and
   type value = Range.t =
 struct
diff --git a/src/domains/printable.ml b/src/domains/printable.ml
index 59d22957b4..1207d35db2 100644
--- a/src/domains/printable.ml
+++ b/src/domains/printable.ml
@@ -48,13 +48,6 @@ end
     Include as the first thing to avoid these overriding actual definitions. *)
 module Std =
 struct
-  (* start MapDomain.Groupable *)
-  type group = |
-  let show_group (x: group) = match x with _ -> .
-  let to_group _ = None
-  let trace_enabled = false
-  (* end MapDomain.Groupable *)
-
   let tag _ = failwith "Std: no tag"
   let arbitrary () = failwith "no arbitrary"
 end
diff --git a/src/domains/queries.ml b/src/domains/queries.ml
index cc61a58101..ada8979b79 100644
--- a/src/domains/queries.ml
+++ b/src/domains/queries.ml
@@ -99,7 +99,10 @@ type _ t =
   | DYojson: FlatYojson.t t (** Get local state Yojson of one path under [PathQuery]. *)
   | HeapVar: VI.t t
   | IsHeapVar: varinfo -> MayBool.t t (* TODO: is may or must? *)
-  | IsMultiple: varinfo -> MustBool.t t (* Is no other copy of this local variable reachable via pointers? *)
+  | IsMultiple: varinfo -> MustBool.t t
+  (* For locals: Is another copy of this local variable reachable via pointers? *)
+  (* For dynamically allocated memory: Does this abstract variable corrrespond to a unique heap location? *)
+  (* For globals: Is it declared as thread-local? (https://github.com/goblint/analyzer/issues/1072) *)
   | MutexType: Mval.Unit.t -> MutexAttrDomain.t t
   | EvalThread: exp -> ConcDomain.ThreadSet.t t
   | EvalMutexAttr: exp -> MutexAttrDomain.t t
diff --git a/src/domains/trieDomain.ml b/src/domains/trieDomain.ml
index 52f53df6ab..0bab7d8628 100644
--- a/src/domains/trieDomain.ml
+++ b/src/domains/trieDomain.ml
@@ -1,6 +1,6 @@
 (** Trie domains. *)
 
-module Make (Key: MapDomain.Groupable) (Value: Lattice.S) =
+module Make (Key: Printable.S) (Value: Lattice.S) =
 struct
   module rec Trie:
   sig
diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
index 1a3a4ebeb1..dd57f40c70 100644
--- a/src/framework/analyses.ml
+++ b/src/framework/analyses.ml
@@ -217,8 +217,12 @@ struct
     in
     let one_w f (m: Messages.Message.t) = match m.multipiece with
       | Single piece  -> one_text f piece
-      | Group {group_text = n; pieces = e} ->
-        BatPrintf.fprintf f "<group name=\"%s\">%a</group>\n" n (BatList.print ~first:"" ~last:"" ~sep:"" one_text) e
+      | Group {group_text = n; pieces = e; group_loc} ->
+        let group_loc_text = match group_loc with
+          | None -> ""
+          | Some group_loc -> GobPretty.sprintf " (%a)" CilType.Location.pretty (Messages.Location.to_cil group_loc)
+        in
+        BatPrintf.fprintf f "<group name=\"%s%s\">%a</group>\n" n group_loc_text (BatList.print ~first:"" ~last:"" ~sep:"" one_text) e
     in
     let one_w f x = BatPrintf.fprintf f "\n<warning>%a</warning>" one_w x in
     List.iter (one_w f) !Messages.Table.messages_list
diff --git a/src/framework/control.ml b/src/framework/control.ml
index fb8a5a8ea1..5ceddf2870 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -165,7 +165,7 @@ struct
           ) xs []
       in
       let msgs = List.rev msgs in (* lines in ascending order *)
-      M.msg_group Warning ~category:Deadcode "Function '%s' has dead code" f msgs
+      M.msg_group Warning ~category:Deadcode "Function '%s' has dead code" f msgs (* TODO: function location for group *)
     in
     let warn_file f = StringMap.iter (warn_func f) in
     if get_bool "ana.dead-code.lines" then (
diff --git a/src/util/cilType.ml b/src/util/cilType.ml
index 87b78e60e9..fe4f257da1 100644
--- a/src/util/cilType.ml
+++ b/src/util/cilType.ml
@@ -6,7 +6,6 @@ open Pretty
 module type S =
 sig
   include Printable.S
-  (* include MapDomain.Groupable *) (* FIXME: dependency cycle *)
 end
 
 module Std =
diff --git a/src/util/gobFormat.ml b/src/util/gobFormat.ml
index a489e92a88..11beec524c 100644
--- a/src/util/gobFormat.ml
+++ b/src/util/gobFormat.ml
@@ -18,4 +18,4 @@ let pp_set_ansi_color_tags ppf =
   Format.pp_set_formatter_stag_functions ppf stag_functions';
   Format.pp_set_mark_tags ppf true
 
-let pp_print_nothing ppf () = ()
+let pp_print_nothing (ppf: Format.formatter) () = ()
diff --git a/src/util/messages.ml b/src/util/messages.ml
index ddbcb12cd1..a06a183eee 100644
--- a/src/util/messages.ml
+++ b/src/util/messages.ml
@@ -75,7 +75,11 @@ end
 
 module MultiPiece =
 struct
-  type group = {group_text: string; pieces: Piece.t list} [@@deriving eq, ord, hash, yojson]
+  type group = {
+    group_text: string;
+    group_loc: Location.t option;
+    pieces: Piece.t list;
+  } [@@deriving eq, ord, hash, yojson]
   type t =
     | Single of Piece.t
     | Group of group
@@ -190,9 +194,12 @@ let print ?(ppf= !formatter) (m: Message.t) =
     | Success -> "green"
   in
   let pp_prefix = Format.dprintf "@{<%s>[%a]%a@}" severity_stag Severity.pp m.severity Tags.pp m.tags in
+  let pp_loc ppf = Format.fprintf ppf " @{<violet>(%a)@}" CilType.Location.pp in
+  let pp_loc ppf loc =
+    Format.fprintf ppf "%a" (Format.pp_print_option pp_loc) (Option.map Location.to_cil loc)
+  in
   let pp_piece ppf piece =
-    let pp_loc ppf = Format.fprintf ppf " @{<violet>(%a)@}" CilType.Location.pp in
-    Format.fprintf ppf "@{<%s>%s@}%a" severity_stag (Piece.text_with_context piece) (Format.pp_print_option pp_loc) (Option.map Location.to_cil piece.loc)
+    Format.fprintf ppf "@{<%s>%s@}%a" severity_stag (Piece.text_with_context piece) pp_loc piece.loc
   in
   let pp_quote ppf (loc: GoblintCil.location) =
     let lines = BatFile.lines_of loc.file in
@@ -217,20 +224,19 @@ let print ?(ppf= !formatter) (m: Message.t) =
         | _ -> assert false
       end
   in
-  let pp_piece ppf piece =
+  let pp_quote ppf loc =
     if get_bool "warn.quote-code" then (
       let pp_cut_quote ppf = Format.fprintf ppf "@,@[<v 0>%a@,@]" pp_quote in
-      Format.fprintf ppf "%a%a" pp_piece piece (Format.pp_print_option pp_cut_quote) (Option.map Location.to_cil piece.loc)
+      (Format.pp_print_option pp_cut_quote) ppf (Option.map Location.to_cil loc)
     )
-    else
-      pp_piece ppf piece
   in
+  let pp_piece ppf piece = Format.fprintf ppf "%a%a" pp_piece piece pp_quote piece.loc in
   let pp_multipiece ppf = match m.multipiece with
     | Single piece ->
       pp_piece ppf piece
-    | Group {group_text; pieces} ->
+    | Group {group_text; group_loc; pieces} ->
       let pp_piece2 ppf = Format.fprintf ppf "@[<v 2>%a@]" pp_piece in (* indented box for quote *)
-      Format.fprintf ppf "@{<%s>%s:@}@,@[<v>%a@]" severity_stag group_text (Format.pp_print_list pp_piece2) pieces
+      Format.fprintf ppf "@{<%s>%s:@}%a%a@,@[<v>%a@]" severity_stag group_text pp_loc group_loc pp_quote group_loc (Format.pp_print_list pp_piece2) pieces
   in
   Format.fprintf ppf "@[<v 2>%t %t@]\n%!" pp_prefix pp_multipiece
 
@@ -283,7 +289,7 @@ let msg_noloc severity ?(tags=[]) ?(category=Category.Unknown) fmt =
   else
     GobPretty.igprintf () fmt
 
-let msg_group severity ?(tags=[]) ?(category=Category.Unknown) fmt =
+let msg_group severity ?loc ?(tags=[]) ?(category=Category.Unknown) fmt =
   if !AnalysisState.should_warn && Severity.should_warn severity && (Category.should_warn category || Tags.should_warn tags) then (
     let finish doc msgs =
       let group_text = GobPretty.show doc in
@@ -291,7 +297,7 @@ let msg_group severity ?(tags=[]) ?(category=Category.Unknown) fmt =
         let text = GobPretty.show doc in
         Piece.{loc; text; context = None}
       in
-      add {tags = Category category :: tags; severity; multipiece = Group {group_text; pieces = List.map piece_of_msg msgs}}
+      add {tags = Category category :: tags; severity; multipiece = Group {group_text; group_loc = loc; pieces = List.map piece_of_msg msgs}}
     in
     Pretty.gprintf finish fmt
   )
diff --git a/src/util/sarif.ml b/src/util/sarif.ml
index 9fa428ff46..4374da46d7 100644
--- a/src/util/sarif.ml
+++ b/src/util/sarif.ml
@@ -88,11 +88,16 @@ let result_of_message (message: Messages.Message.t): Result.t list =
     }
     in
     [result]
-  | Group {group_text; pieces} ->
+  | Group {group_text; group_loc; pieces} ->
     (* each grouped piece becomes a separate result with the other locations as related *)
+    (* TODO: use group_loc instead of distributing? *)
+    let group_loc_text = match group_loc with
+      | None -> ""
+      | Some group_loc -> GobPretty.sprintf " (%a)" CilType.Location.pretty (Messages.Location.to_cil group_loc)
+    in
     let piece_locations = List.map piece_location pieces in
     List.map2i (fun i piece locations ->
-        let text = prefix ^ group_text ^ "\n" ^ piece.Messages.Piece.text in
+        let text = prefix ^ group_text ^ group_loc_text ^ "\n" ^ piece.Messages.Piece.text in
         let relatedLocations = List.unique ~eq:Location.equal (List.flatten (List.remove_at i piece_locations)) in
         let result: Result.t = {
           ruleId;
diff --git a/tests/regression/01-cpa/74-rand.c b/tests/regression/01-cpa/74-rand.c
new file mode 100644
index 0000000000..dc5e5b3bba
--- /dev/null
+++ b/tests/regression/01-cpa/74-rand.c
@@ -0,0 +1,12 @@
+//PARAM: --enable ana.int.interval
+#include <stdio.h>
+#include <stdlib.h>
+#include <goblint.h>
+
+int main () {
+  int r = rand();
+
+  __goblint_check(r >= 0);
+
+  return 0;
+}
diff --git a/tests/regression/03-practical/28-bool.c b/tests/regression/03-practical/28-bool.c
new file mode 100644
index 0000000000..abcf63da01
--- /dev/null
+++ b/tests/regression/03-practical/28-bool.c
@@ -0,0 +1,20 @@
+#include <stdbool.h>
+#include <goblint.h>
+
+int main() {
+  int a;
+  int *p = &a;
+
+  bool x = p;
+  __goblint_check(x);
+  bool y = !!p;
+  __goblint_check(y);
+  bool z = p != 0;
+  __goblint_check(z);
+
+  int b = 10;
+  bool bb = b;
+  __goblint_check(bb);
+
+  return 0;
+}
\ No newline at end of file
diff --git a/tests/regression/03-practical/29-bool-interval.c b/tests/regression/03-practical/29-bool-interval.c
new file mode 100644
index 0000000000..ad55e37701
--- /dev/null
+++ b/tests/regression/03-practical/29-bool-interval.c
@@ -0,0 +1,21 @@
+//PARAM: --enable ana.int.interval --disable ana.int.def_exc
+#include <stdbool.h>
+#include <goblint.h>
+
+int main() {
+  int a;
+  int *p = &a;
+
+  bool x = p;
+  __goblint_check(x); //UNKNOWN (not null cannot be expressed in interval domain)
+  bool y = !!p;
+  __goblint_check(y);
+  bool z = p != 0;
+  __goblint_check(z);
+
+  int b = 10;
+  bool bb = b;
+  __goblint_check(bb);
+
+  return 0;
+}
\ No newline at end of file
diff --git a/tests/regression/03-practical/30-bool-congr.c b/tests/regression/03-practical/30-bool-congr.c
new file mode 100644
index 0000000000..86249848c1
--- /dev/null
+++ b/tests/regression/03-practical/30-bool-congr.c
@@ -0,0 +1,13 @@
+//PARAM:  --enable ana.int.congruence
+#include <stdbool.h>
+#include <goblint.h>
+
+int main() {
+
+  bool x = 1;
+  bool y = 1;
+  bool z = x + y;
+  __goblint_check(z);
+
+  return 0;
+}
diff --git a/tests/regression/04-mutex/01-simple_rc.t b/tests/regression/04-mutex/01-simple_rc.t
index 78c79eb0d1..b61650c6d3 100644
--- a/tests/regression/04-mutex/01-simple_rc.t
+++ b/tests/regression/04-mutex/01-simple_rc.t
@@ -1,5 +1,5 @@
   $ goblint --enable warn.deterministic 01-simple_rc.c
-  [Warning][Race] Memory location myglobal@01-simple_rc.c:4:5-4:13 (race with conf. 110):
+  [Warning][Race] Memory location myglobal (race with conf. 110): (01-simple_rc.c:4:5-4:13)
     write with [mhp:{tid=[main, t_fun@01-simple_rc.c:17:3-17:40#top]}, lock:{mutex1}, thread:[main, t_fun@01-simple_rc.c:17:3-17:40#top]] (conf. 110)  (exp: & myglobal) (01-simple_rc.c:10:3-10:22)
     write with [mhp:{tid=[main]; created={[main, t_fun@01-simple_rc.c:17:3-17:40#top]}}, lock:{mutex2}, thread:[main]] (conf. 110)  (exp: & myglobal) (01-simple_rc.c:19:3-19:22)
     read with [mhp:{tid=[main, t_fun@01-simple_rc.c:17:3-17:40#top]}, lock:{mutex1}, thread:[main, t_fun@01-simple_rc.c:17:3-17:40#top]] (conf. 110)  (exp: & myglobal) (01-simple_rc.c:10:3-10:22)
diff --git a/tests/regression/04-mutex/49-type-invariants.t b/tests/regression/04-mutex/49-type-invariants.t
index 30f79e9e56..3d3f7442ef 100644
--- a/tests/regression/04-mutex/49-type-invariants.t
+++ b/tests/regression/04-mutex/49-type-invariants.t
@@ -1,6 +1,6 @@
   $ goblint --enable warn.deterministic --enable ana.race.direct-arithmetic --enable allglobs 49-type-invariants.c
   [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (49-type-invariants.c:22:3-22:21)
-  [Warning][Race] Memory location s.field@49-type-invariants.c:9:10-9:11 (race with conf. 110):
+  [Warning][Race] Memory location s.field (race with conf. 110): (49-type-invariants.c:9:10-9:11)
     write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:21:3-21:40#top]}}, thread:[main]] (conf. 100)  (exp: & tmp->field) (49-type-invariants.c:22:3-22:21)
     read with [mhp:{tid=[main, t_fun@49-type-invariants.c:21:3-21:40#top]}, thread:[main, t_fun@49-type-invariants.c:21:3-21:40#top]] (conf. 110)  (exp: & s.field) (49-type-invariants.c:12:3-12:23)
   [Info][Race] Memory locations race summary:
@@ -24,7 +24,7 @@
 
   $ goblint --enable warn.deterministic --disable ana.race.direct-arithmetic --enable allglobs 49-type-invariants.c
   [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (49-type-invariants.c:22:3-22:21)
-  [Warning][Race] Memory location s.field@49-type-invariants.c:9:10-9:11 (race with conf. 110):
+  [Warning][Race] Memory location s.field (race with conf. 110): (49-type-invariants.c:9:10-9:11)
     write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:21:3-21:40#top]}}, thread:[main]] (conf. 100)  (exp: & tmp->field) (49-type-invariants.c:22:3-22:21)
     read with [mhp:{tid=[main, t_fun@49-type-invariants.c:21:3-21:40#top]}, thread:[main, t_fun@49-type-invariants.c:21:3-21:40#top]] (conf. 110)  (exp: & s.field) (49-type-invariants.c:12:3-12:23)
   [Info][Race] Memory locations race summary:
diff --git a/tests/regression/04-mutex/84-distribute-fields-1.t b/tests/regression/04-mutex/84-distribute-fields-1.t
index af4b0bb284..7c79572d88 100644
--- a/tests/regression/04-mutex/84-distribute-fields-1.t
+++ b/tests/regression/04-mutex/84-distribute-fields-1.t
@@ -1,5 +1,5 @@
   $ goblint --enable warn.deterministic --enable allglobs 84-distribute-fields-1.c
-  [Warning][Race] Memory location s.data@84-distribute-fields-1.c:9:10-9:11 (race with conf. 110):
+  [Warning][Race] Memory location s.data (race with conf. 110): (84-distribute-fields-1.c:9:10-9:11)
     write with [mhp:{tid=[main, t_fun@84-distribute-fields-1.c:18:3-18:40#top]}, thread:[main, t_fun@84-distribute-fields-1.c:18:3-18:40#top]] (conf. 110)  (exp: & s.data) (84-distribute-fields-1.c:12:3-12:13)
     write with [mhp:{tid=[main]; created={[main, t_fun@84-distribute-fields-1.c:18:3-18:40#top]}}, thread:[main]] (conf. 110)  (exp: & s) (84-distribute-fields-1.c:20:3-20:9)
   [Info][Race] Memory locations race summary:
@@ -7,7 +7,7 @@
     vulnerable: 0
     unsafe: 1
     total memory locations: 2
-  [Success][Race] Memory location s@84-distribute-fields-1.c:9:10-9:11 (safe):
+  [Success][Race] Memory location s (safe): (84-distribute-fields-1.c:9:10-9:11)
     write with [mhp:{tid=[main]; created={[main, t_fun@84-distribute-fields-1.c:18:3-18:40#top]}}, thread:[main]] (conf. 110)  (exp: & s) (84-distribute-fields-1.c:20:3-20:9)
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 8
diff --git a/tests/regression/04-mutex/85-distribute-fields-2.t b/tests/regression/04-mutex/85-distribute-fields-2.t
index 077e5739c4..303c10dccd 100644
--- a/tests/regression/04-mutex/85-distribute-fields-2.t
+++ b/tests/regression/04-mutex/85-distribute-fields-2.t
@@ -1,5 +1,5 @@
   $ goblint --enable warn.deterministic --enable allglobs 85-distribute-fields-2.c
-  [Warning][Race] Memory location t.s.data@85-distribute-fields-2.c:15:10-15:11 (race with conf. 110):
+  [Warning][Race] Memory location t.s.data (race with conf. 110): (85-distribute-fields-2.c:15:10-15:11)
     write with [mhp:{tid=[main, t_fun@85-distribute-fields-2.c:24:3-24:40#top]}, thread:[main, t_fun@85-distribute-fields-2.c:24:3-24:40#top]] (conf. 110)  (exp: & t.s.data) (85-distribute-fields-2.c:18:3-18:15)
     write with [mhp:{tid=[main]; created={[main, t_fun@85-distribute-fields-2.c:24:3-24:40#top]}}, thread:[main]] (conf. 110)  (exp: & t.s) (85-distribute-fields-2.c:26:3-26:11)
   [Info][Race] Memory locations race summary:
@@ -7,7 +7,7 @@
     vulnerable: 0
     unsafe: 1
     total memory locations: 2
-  [Success][Race] Memory location t.s@85-distribute-fields-2.c:15:10-15:11 (safe):
+  [Success][Race] Memory location t.s (safe): (85-distribute-fields-2.c:15:10-15:11)
     write with [mhp:{tid=[main]; created={[main, t_fun@85-distribute-fields-2.c:24:3-24:40#top]}}, thread:[main]] (conf. 110)  (exp: & t.s) (85-distribute-fields-2.c:26:3-26:11)
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 8
diff --git a/tests/regression/04-mutex/86-distribute-fields-3.t b/tests/regression/04-mutex/86-distribute-fields-3.t
index e46d226bc5..084148392c 100644
--- a/tests/regression/04-mutex/86-distribute-fields-3.t
+++ b/tests/regression/04-mutex/86-distribute-fields-3.t
@@ -1,5 +1,5 @@
   $ goblint --enable warn.deterministic --enable allglobs 86-distribute-fields-3.c
-  [Warning][Race] Memory location t.s.data@86-distribute-fields-3.c:15:10-15:11 (race with conf. 110):
+  [Warning][Race] Memory location t.s.data (race with conf. 110): (86-distribute-fields-3.c:15:10-15:11)
     write with [mhp:{tid=[main, t_fun@86-distribute-fields-3.c:24:3-24:40#top]}, thread:[main, t_fun@86-distribute-fields-3.c:24:3-24:40#top]] (conf. 110)  (exp: & t.s.data) (86-distribute-fields-3.c:18:3-18:15)
     write with [mhp:{tid=[main]; created={[main, t_fun@86-distribute-fields-3.c:24:3-24:40#top]}}, thread:[main]] (conf. 110)  (exp: & t) (86-distribute-fields-3.c:26:3-26:9)
   [Info][Race] Memory locations race summary:
@@ -7,7 +7,7 @@
     vulnerable: 0
     unsafe: 1
     total memory locations: 2
-  [Success][Race] Memory location t@86-distribute-fields-3.c:15:10-15:11 (safe):
+  [Success][Race] Memory location t (safe): (86-distribute-fields-3.c:15:10-15:11)
     write with [mhp:{tid=[main]; created={[main, t_fun@86-distribute-fields-3.c:24:3-24:40#top]}}, thread:[main]] (conf. 110)  (exp: & t) (86-distribute-fields-3.c:26:3-26:9)
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 8
diff --git a/tests/regression/04-mutex/87-distribute-fields-4.t b/tests/regression/04-mutex/87-distribute-fields-4.t
index 734f3e4efd..5c26e80592 100644
--- a/tests/regression/04-mutex/87-distribute-fields-4.t
+++ b/tests/regression/04-mutex/87-distribute-fields-4.t
@@ -1,5 +1,5 @@
   $ goblint --enable warn.deterministic --enable allglobs 87-distribute-fields-4.c
-  [Warning][Race] Memory location s@87-distribute-fields-4.c:9:10-9:11 (race with conf. 110):
+  [Warning][Race] Memory location s (race with conf. 110): (87-distribute-fields-4.c:9:10-9:11)
     write with [mhp:{tid=[main, t_fun@87-distribute-fields-4.c:19:3-19:40#top]}, thread:[main, t_fun@87-distribute-fields-4.c:19:3-19:40#top]] (conf. 110)  (exp: & s) (87-distribute-fields-4.c:13:3-13:9)
     write with [mhp:{tid=[main]; created={[main, t_fun@87-distribute-fields-4.c:19:3-19:40#top]}}, thread:[main]] (conf. 110)  (exp: & s) (87-distribute-fields-4.c:21:3-21:9)
   [Info][Race] Memory locations race summary:
diff --git a/tests/regression/04-mutex/88-distribute-fields-5.t b/tests/regression/04-mutex/88-distribute-fields-5.t
index b8a2eb67c9..8f0014e34c 100644
--- a/tests/regression/04-mutex/88-distribute-fields-5.t
+++ b/tests/regression/04-mutex/88-distribute-fields-5.t
@@ -1,5 +1,5 @@
   $ goblint --enable warn.deterministic --enable allglobs 88-distribute-fields-5.c
-  [Warning][Race] Memory location t.s@88-distribute-fields-5.c:15:10-15:11 (race with conf. 110):
+  [Warning][Race] Memory location t.s (race with conf. 110): (88-distribute-fields-5.c:15:10-15:11)
     write with [mhp:{tid=[main, t_fun@88-distribute-fields-5.c:25:3-25:40#top]}, thread:[main, t_fun@88-distribute-fields-5.c:25:3-25:40#top]] (conf. 110)  (exp: & t.s) (88-distribute-fields-5.c:19:3-19:11)
     write with [mhp:{tid=[main]; created={[main, t_fun@88-distribute-fields-5.c:25:3-25:40#top]}}, thread:[main]] (conf. 110)  (exp: & t.s) (88-distribute-fields-5.c:27:3-27:11)
   [Info][Race] Memory locations race summary:
diff --git a/tests/regression/04-mutex/89-distribute-fields-6.t b/tests/regression/04-mutex/89-distribute-fields-6.t
index b999a61239..aeb5050395 100644
--- a/tests/regression/04-mutex/89-distribute-fields-6.t
+++ b/tests/regression/04-mutex/89-distribute-fields-6.t
@@ -1,5 +1,5 @@
   $ goblint --enable warn.deterministic --enable allglobs 89-distribute-fields-6.c
-  [Warning][Race] Memory location t@89-distribute-fields-6.c:15:10-15:11 (race with conf. 110):
+  [Warning][Race] Memory location t (race with conf. 110): (89-distribute-fields-6.c:15:10-15:11)
     write with [mhp:{tid=[main, t_fun@89-distribute-fields-6.c:25:3-25:40#top]}, thread:[main, t_fun@89-distribute-fields-6.c:25:3-25:40#top]] (conf. 110)  (exp: & t) (89-distribute-fields-6.c:19:3-19:9)
     write with [mhp:{tid=[main]; created={[main, t_fun@89-distribute-fields-6.c:25:3-25:40#top]}}, thread:[main]] (conf. 110)  (exp: & t) (89-distribute-fields-6.c:27:3-27:9)
   [Info][Race] Memory locations race summary:
diff --git a/tests/regression/04-mutex/98-thread-local-eq.c b/tests/regression/04-mutex/98-thread-local-eq.c
new file mode 100644
index 0000000000..801494de21
--- /dev/null
+++ b/tests/regression/04-mutex/98-thread-local-eq.c
@@ -0,0 +1,26 @@
+#include <pthread.h>
+#include <stdio.h>
+#include <assert.h>
+
+__thread int myglobal;
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  int top;
+  int* ptr = (int*) arg;
+
+  if(top) { 
+    ptr = &myglobal;
+  }
+
+  __goblint_check(&myglobal == ptr); //UNKNOWN!
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, (void*) &myglobal);
+  pthread_join (id, NULL);
+  return 0;
+}
\ No newline at end of file
diff --git a/tests/regression/27-inv_invariants/18-union-float-int.c b/tests/regression/27-inv_invariants/18-union-float-int.c
new file mode 100644
index 0000000000..d56f7d6c56
--- /dev/null
+++ b/tests/regression/27-inv_invariants/18-union-float-int.c
@@ -0,0 +1,28 @@
+// PARAM: --enable ana.float.interval
+#include <goblint.h>
+union u {
+	int x;
+	float f;
+};
+
+int main(){
+	union u a;
+	union u b;
+
+	a.x = 12;
+	b.f = 129.0;
+
+	int i = 0;
+	if(a.x == b.x){
+		i++;
+	}
+	// Should not be dead after if
+	__goblint_check(1);
+
+	if(a.f == b.f){
+		i++;
+	}
+	// Should not be dead after if
+	__goblint_check(1);
+	return 0;
+}
diff --git a/tests/regression/27-inv_invariants/19-union-char-int.c b/tests/regression/27-inv_invariants/19-union-char-int.c
new file mode 100644
index 0000000000..1cfbc1f0b1
--- /dev/null
+++ b/tests/regression/27-inv_invariants/19-union-char-int.c
@@ -0,0 +1,38 @@
+// PARAM: --enable ana.float.interval
+#include <goblint.h>
+union u {
+	int x;
+	char c;
+};
+
+int main(){
+	union u a;
+	union u b;
+
+	a.x = 12;
+	b.c = 12;
+
+	int i = 0;
+	if(a.x == b.x){
+		i++;
+	}
+	// Should not be dead after if
+	__goblint_check(1);
+
+	a.x = 257;
+	b.c = 1;
+
+	if(a.x == b.x){
+		i++;
+	}
+	// Should not be dead after if
+	__goblint_check(1);
+
+	if(a.c == b.c){
+		i++;
+	}
+	// Should not be dead after if
+	__goblint_check(1);
+
+	return 0;
+}
diff --git a/tests/regression/46-apron2/57-rand.c b/tests/regression/46-apron2/57-rand.c
new file mode 100644
index 0000000000..40a699433e
--- /dev/null
+++ b/tests/regression/46-apron2/57-rand.c
@@ -0,0 +1,11 @@
+// SKIP PARAM: --disable ana.int.def_exc --enable ana.int.congruence --set ana.activated[+] apron --set ana.base.privatization none --set ana.relation.privatization top
+// Strange int domains, I know: The ranges of def_exc are already able to prove this assertion, meaning it is no longer about apron also knowing this.
+// Disabling all int domains leads to all queries returning top though, meaning the assertion is not proven.
+// Congruence offers support for constants, but does not contain any poor man's intervals. => That's why we use it here.
+#include <goblint.h>
+#include <stdlib.h>
+
+int main() {
+    int i = rand();
+    __goblint_check(i >= 0);
+}
diff --git a/unittest/domains/mapDomainTest.ml b/unittest/domains/mapDomainTest.ml
index 7f9b262238..ff64a75f92 100644
--- a/unittest/domains/mapDomainTest.ml
+++ b/unittest/domains/mapDomainTest.ml
@@ -3,12 +3,12 @@ open OUnit2
 
 module Pretty = GoblintCil.Pretty
 
-module GroupableDriver : MapDomain.Groupable with type t = string  =
+module PrintableDriver : Printable.S with type t = string  =
 struct
   include Printable.Strings
 end
 
-module LatticeDriver = Lattice.Fake (GroupableDriver)
+module LatticeDriver = Lattice.Fake (PrintableDriver)
 
 
 module TestMap (M:MapDomain.S with type key = string and type value = string) =
@@ -162,8 +162,8 @@ struct
 end
 
 
-module Mbot = MapDomain.MapBot (GroupableDriver) (LatticeDriver)
-module Mtop = MapDomain.MapTop (GroupableDriver) (LatticeDriver)
+module Mbot = MapDomain.MapBot (PrintableDriver) (LatticeDriver)
+module Mtop = MapDomain.MapTop (PrintableDriver) (LatticeDriver)
 
 module Tbot = TestMap (Mbot)
 module Ttop = TestMap (Mtop)
diff --git a/unittest/maindomaintest.ml b/unittest/maindomaintest.ml
index a37e8de8a7..8e6a7f5a3a 100644
--- a/unittest/maindomaintest.ml
+++ b/unittest/maindomaintest.ml
@@ -67,7 +67,7 @@ let ikinds: Cil.ikind list = [
   IChar;
   ISChar;
   IUChar;
-  IBool;
+  (* IBool; *) (* see https://github.com/goblint/analyzer/pull/1111 *)
   IInt;
   IUInt;
   IShort;