diff --git a/.github/workflows/coverage.yml b/.github/workflows/coverage.yml
index fd2c55b84e..3f924869fc 100644
--- a/.github/workflows/coverage.yml
+++ b/.github/workflows/coverage.yml
@@ -46,6 +46,9 @@ jobs:
       - name: Install dependencies
         run: opam install . --deps-only --locked --with-test
 
+      - name: Install os gem for operating system detection
+        run: sudo gem install os
+        
       - name: Install coverage dependencies
         run: opam install bisect_ppx
 
diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml
index 0ada04e369..1a6d17fab4 100644
--- a/.github/workflows/docs.yml
+++ b/.github/workflows/docs.yml
@@ -46,6 +46,9 @@ jobs:
       - name: Install dependencies
         run: opam install . --deps-only --locked --with-doc
 
+      - name: Install os gem for operating system detection
+        run: sudo gem install os
+
       - name: Build API docs
         run: opam exec -- dune build @doc
 
diff --git a/.github/workflows/locked.yml b/.github/workflows/locked.yml
index 16655bfdc7..8205d4ef34 100644
--- a/.github/workflows/locked.yml
+++ b/.github/workflows/locked.yml
@@ -48,6 +48,9 @@ jobs:
       - name: Install dependencies
         run: opam install . --deps-only --locked --with-test
 
+      - name: Install os gem for operating system detection
+        run: sudo gem install os
+
       - name: Build
         run: ./make.sh nat
 
@@ -100,6 +103,9 @@ jobs:
       - name: Install dependencies
         run: opam install . --deps-only --locked --with-test
 
+      - name: Install os gem for operating system detection
+        run: sudo gem install os
+
       - name: Build
         run: ./make.sh nat
 
@@ -142,6 +148,9 @@ jobs:
       - name: Install dependencies
         run: opam install . --deps-only --locked
 
+      - name: Install os gem for operating system detection
+        run: sudo gem install os
+
       - name: Setup Gobview
         run: ./make.sh setup_gobview
 
diff --git a/.github/workflows/unlocked.yml b/.github/workflows/unlocked.yml
index f3fe6cc558..81d1d3dc1c 100644
--- a/.github/workflows/unlocked.yml
+++ b/.github/workflows/unlocked.yml
@@ -57,6 +57,9 @@ jobs:
 
       - name: Install dependencies
         run: opam install . --deps-only --with-test
+      
+      - name: Install os gem for operating system detection
+        run: sudo gem install os
 
       - name: Install Apron dependencies
         if: ${{ matrix.apron }}
@@ -118,6 +121,9 @@ jobs:
       - name: Install dependencies
         run: opam install . --deps-only --with-test
 
+      - name: Install os gem for operating system detection
+        run: sudo gem install os
+
       - name: Install Apron dependencies
         run: |
           opam depext apron
diff --git a/conf/bench-yaml-validate.json b/conf/bench-yaml-validate.json
index 7b18371bd1..2fcdb418da 100644
--- a/conf/bench-yaml-validate.json
+++ b/conf/bench-yaml-validate.json
@@ -71,7 +71,6 @@
   },
   "pre": {
     "cppflags": [
-      "-DGOBLINT_NO_PTHREAD_ONCE",
       "-DGOBLINT_NO_QSORT",
       "-DGOBLINT_NO_BSEARCH"
     ]
diff --git a/conf/bench-yaml.json b/conf/bench-yaml.json
index fd97b2c08c..52f0b33347 100644
--- a/conf/bench-yaml.json
+++ b/conf/bench-yaml.json
@@ -67,7 +67,6 @@
   },
   "pre": {
     "cppflags": [
-      "-DGOBLINT_NO_PTHREAD_ONCE",
       "-DGOBLINT_NO_QSORT",
       "-DGOBLINT_NO_BSEARCH"
     ]
diff --git a/conf/ldv-races.json b/conf/ldv-races.json
index a06a6da610..da8355c7e8 100644
--- a/conf/ldv-races.json
+++ b/conf/ldv-races.json
@@ -1,7 +1,6 @@
 {
   "pre": {
     "cppflags": [
-      "-DGOBLINT_NO_PTHREAD_ONCE",
       "-DGOBLINT_NO_QSORT",
       "-DGOBLINT_NO_BSEARCH"
     ]
diff --git a/conf/race-digests/fresh-only.json b/conf/race-digests/fresh-only.json
new file mode 100644
index 0000000000..9f2cafd408
--- /dev/null
+++ b/conf/race-digests/fresh-only.json
@@ -0,0 +1,127 @@
+{
+  "ana": {
+    "sv-comp": {
+      "enabled": true,
+      "functions": true
+    },
+    "int": {
+      "def_exc": true,
+      "enums": false,
+      "interval": true
+    },
+    "float": {
+      "interval": true,
+      "evaluate_math_functions": true
+    },
+    "activated": [
+      "base",
+      "threadid",
+      "threadflag",
+      "threadreturn",
+      "mallocWrapper",
+      "mutexEvents",
+      "mutex",
+      "access",
+      "race",
+      "escape",
+      "expRelation",
+      "mhp",
+      "assert",
+      "var_eq",
+      "symb_locks",
+      "region",
+      "thread",
+      "threadJoins",
+      "abortUnless"
+    ],
+    "path_sens": [
+      "mutex",
+      "malloc_null",
+      "uninit",
+      "expsplit",
+      "activeSetjmp",
+      "memLeak",
+      "threadflag"
+    ],
+    "context": {
+      "widen": false
+    },
+    "base": {
+      "arrays": {
+        "domain": "partitioned"
+      }
+    },
+    "race": {
+      "free": false,
+      "call": false,
+      "digests": {
+        "lockset": false,
+        "fresh": true,
+        "region": false,
+        "symb_locks": false,
+        "threadflag": false,
+        "tid": false,
+        "join" : false
+      }
+    },
+    "autotune": {
+      "enabled": true,
+      "activated": [
+        "singleThreaded",
+        "mallocWrappers",
+        "noRecursiveIntervals",
+        "enums",
+        "congruence",
+        "octagon",
+        "wideningThresholds",
+        "loopUnrollHeuristic",
+        "memsafetySpecification",
+        "noOverflows",
+        "termination",
+        "tmpSpecialAnalysis"
+      ]
+    }
+  },
+  "exp": {
+    "region-offsets": true
+  },
+  "solver": "td3",
+  "sem": {
+    "unknown_function": {
+      "spawn": false
+    },
+    "int": {
+      "signed_overflow": "assume_none"
+    },
+    "null-pointer": {
+      "dereference": "assume_none"
+    }
+  },
+  "witness": {
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    },
+    "yaml": {
+      "enabled": true,
+      "format-version": "2.0",
+      "entry-types": [
+        "invariant_set"
+      ],
+      "invariant-types": [
+        "loop_invariant"
+      ]
+    },
+    "invariant": {
+      "loop-head": true,
+      "after-lock": false,
+      "other": false,
+      "accessed": false,
+      "exact": true
+    }
+  },
+  "pre": {
+    "enabled": false
+  }
+}
diff --git a/conf/race-digests/full+once+barrier.json b/conf/race-digests/full+once+barrier.json
new file mode 100644
index 0000000000..70ca39b92b
--- /dev/null
+++ b/conf/race-digests/full+once+barrier.json
@@ -0,0 +1,120 @@
+{
+  "ana": {
+    "sv-comp": {
+      "enabled": true,
+      "functions": true
+    },
+    "int": {
+      "def_exc": true,
+      "enums": false,
+      "interval": true
+    },
+    "float": {
+      "interval": true,
+      "evaluate_math_functions": true
+    },
+    "activated": [
+      "base",
+      "threadid",
+      "threadflag",
+      "threadreturn",
+      "mallocWrapper",
+      "mutexEvents",
+      "mutex",
+      "access",
+      "race",
+      "escape",
+      "expRelation",
+      "mhp",
+      "assert",
+      "var_eq",
+      "symb_locks",
+      "region",
+      "thread",
+      "threadJoins",
+      "abortUnless",
+      "pthreadBarriers",
+      "pthreadOnce"
+    ],
+    "path_sens": [
+      "mutex",
+      "malloc_null",
+      "uninit",
+      "expsplit",
+      "activeSetjmp",
+      "memLeak",
+      "threadflag"
+    ],
+    "context": {
+      "widen": false
+    },
+    "base": {
+      "arrays": {
+        "domain": "partitioned"
+      }
+    },
+    "race": {
+      "free": false,
+      "call": false
+    },
+    "autotune": {
+      "enabled": true,
+      "activated": [
+        "singleThreaded",
+        "mallocWrappers",
+        "noRecursiveIntervals",
+        "enums",
+        "congruence",
+        "octagon",
+        "wideningThresholds",
+        "loopUnrollHeuristic",
+        "memsafetySpecification",
+        "noOverflows",
+        "termination",
+        "tmpSpecialAnalysis"
+      ]
+    }
+  },
+  "exp": {
+    "region-offsets": true
+  },
+  "solver": "td3",
+  "sem": {
+    "unknown_function": {
+      "spawn": false
+    },
+    "int": {
+      "signed_overflow": "assume_none"
+    },
+    "null-pointer": {
+      "dereference": "assume_none"
+    }
+  },
+  "witness": {
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    },
+    "yaml": {
+      "enabled": true,
+      "format-version": "2.0",
+      "entry-types": [
+        "invariant_set"
+      ],
+      "invariant-types": [
+        "loop_invariant"
+      ]
+    },
+    "invariant": {
+      "loop-head": true,
+      "after-lock": false,
+      "other": false,
+      "accessed": false,
+      "exact": true
+    }
+  },
+  "pre": {
+    "enabled": false
+  }
+}
diff --git a/conf/race-digests/full-minus-region+symblocks.json b/conf/race-digests/full-minus-region+symblocks.json
new file mode 100644
index 0000000000..0f7093a867
--- /dev/null
+++ b/conf/race-digests/full-minus-region+symblocks.json
@@ -0,0 +1,127 @@
+{
+  "ana": {
+    "sv-comp": {
+      "enabled": true,
+      "functions": true
+    },
+    "int": {
+      "def_exc": true,
+      "enums": false,
+      "interval": true
+    },
+    "float": {
+      "interval": true,
+      "evaluate_math_functions": true
+    },
+    "activated": [
+      "base",
+      "threadid",
+      "threadflag",
+      "threadreturn",
+      "mallocWrapper",
+      "mutexEvents",
+      "mutex",
+      "access",
+      "race",
+      "escape",
+      "expRelation",
+      "mhp",
+      "assert",
+      "var_eq",
+      "symb_locks",
+      "region",
+      "thread",
+      "threadJoins",
+      "abortUnless"
+    ],
+    "path_sens": [
+      "mutex",
+      "malloc_null",
+      "uninit",
+      "expsplit",
+      "activeSetjmp",
+      "memLeak",
+      "threadflag"
+    ],
+    "context": {
+      "widen": false
+    },
+    "base": {
+      "arrays": {
+        "domain": "partitioned"
+      }
+    },
+    "race": {
+      "free": false,
+      "call": false,
+      "digests": {
+        "lockset": true,
+        "fresh": true,
+        "region": false,
+        "symb_locks": false,
+        "threadflag": true,
+        "tid": true,
+        "join" : true
+      }
+    },
+    "autotune": {
+      "enabled": true,
+      "activated": [
+        "singleThreaded",
+        "mallocWrappers",
+        "noRecursiveIntervals",
+        "enums",
+        "congruence",
+        "octagon",
+        "wideningThresholds",
+        "loopUnrollHeuristic",
+        "memsafetySpecification",
+        "noOverflows",
+        "termination",
+        "tmpSpecialAnalysis"
+      ]
+    }
+  },
+  "exp": {
+    "region-offsets": true
+  },
+  "solver": "td3",
+  "sem": {
+    "unknown_function": {
+      "spawn": false
+    },
+    "int": {
+      "signed_overflow": "assume_none"
+    },
+    "null-pointer": {
+      "dereference": "assume_none"
+    }
+  },
+  "witness": {
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    },
+    "yaml": {
+      "enabled": true,
+      "format-version": "2.0",
+      "entry-types": [
+        "invariant_set"
+      ],
+      "invariant-types": [
+        "loop_invariant"
+      ]
+    },
+    "invariant": {
+      "loop-head": true,
+      "after-lock": false,
+      "other": false,
+      "accessed": false,
+      "exact": true
+    }
+  },
+  "pre": {
+    "enabled": false
+  }
+}
diff --git a/conf/race-digests/full-minus-region.json b/conf/race-digests/full-minus-region.json
new file mode 100644
index 0000000000..afb1b4048c
--- /dev/null
+++ b/conf/race-digests/full-minus-region.json
@@ -0,0 +1,127 @@
+{
+  "ana": {
+    "sv-comp": {
+      "enabled": true,
+      "functions": true
+    },
+    "int": {
+      "def_exc": true,
+      "enums": false,
+      "interval": true
+    },
+    "float": {
+      "interval": true,
+      "evaluate_math_functions": true
+    },
+    "activated": [
+      "base",
+      "threadid",
+      "threadflag",
+      "threadreturn",
+      "mallocWrapper",
+      "mutexEvents",
+      "mutex",
+      "access",
+      "race",
+      "escape",
+      "expRelation",
+      "mhp",
+      "assert",
+      "var_eq",
+      "symb_locks",
+      "region",
+      "thread",
+      "threadJoins",
+      "abortUnless"
+    ],
+    "path_sens": [
+      "mutex",
+      "malloc_null",
+      "uninit",
+      "expsplit",
+      "activeSetjmp",
+      "memLeak",
+      "threadflag"
+    ],
+    "context": {
+      "widen": false
+    },
+    "base": {
+      "arrays": {
+        "domain": "partitioned"
+      }
+    },
+    "race": {
+      "free": false,
+      "call": false,
+      "digests": {
+        "lockset": true,
+        "fresh": true,
+        "region": false,
+        "symb_locks": true,
+        "threadflag": true,
+        "tid": true,
+        "join" : true
+      }
+    },
+    "autotune": {
+      "enabled": true,
+      "activated": [
+        "singleThreaded",
+        "mallocWrappers",
+        "noRecursiveIntervals",
+        "enums",
+        "congruence",
+        "octagon",
+        "wideningThresholds",
+        "loopUnrollHeuristic",
+        "memsafetySpecification",
+        "noOverflows",
+        "termination",
+        "tmpSpecialAnalysis"
+      ]
+    }
+  },
+  "exp": {
+    "region-offsets": true
+  },
+  "solver": "td3",
+  "sem": {
+    "unknown_function": {
+      "spawn": false
+    },
+    "int": {
+      "signed_overflow": "assume_none"
+    },
+    "null-pointer": {
+      "dereference": "assume_none"
+    }
+  },
+  "witness": {
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    },
+    "yaml": {
+      "enabled": true,
+      "format-version": "2.0",
+      "entry-types": [
+        "invariant_set"
+      ],
+      "invariant-types": [
+        "loop_invariant"
+      ]
+    },
+    "invariant": {
+      "loop-head": true,
+      "after-lock": false,
+      "other": false,
+      "accessed": false,
+      "exact": true
+    }
+  },
+  "pre": {
+    "enabled": false
+  }
+}
diff --git a/conf/race-digests/full.json b/conf/race-digests/full.json
new file mode 100644
index 0000000000..dedc393ba1
--- /dev/null
+++ b/conf/race-digests/full.json
@@ -0,0 +1,118 @@
+{
+  "ana": {
+    "sv-comp": {
+      "enabled": true,
+      "functions": true
+    },
+    "int": {
+      "def_exc": true,
+      "enums": false,
+      "interval": true
+    },
+    "float": {
+      "interval": true,
+      "evaluate_math_functions": true
+    },
+    "activated": [
+      "base",
+      "threadid",
+      "threadflag",
+      "threadreturn",
+      "mallocWrapper",
+      "mutexEvents",
+      "mutex",
+      "access",
+      "race",
+      "escape",
+      "expRelation",
+      "mhp",
+      "assert",
+      "var_eq",
+      "symb_locks",
+      "region",
+      "thread",
+      "threadJoins",
+      "abortUnless"
+    ],
+    "path_sens": [
+      "mutex",
+      "malloc_null",
+      "uninit",
+      "expsplit",
+      "activeSetjmp",
+      "memLeak",
+      "threadflag"
+    ],
+    "context": {
+      "widen": false
+    },
+    "base": {
+      "arrays": {
+        "domain": "partitioned"
+      }
+    },
+    "race": {
+      "free": false,
+      "call": false
+    },
+    "autotune": {
+      "enabled": true,
+      "activated": [
+        "singleThreaded",
+        "mallocWrappers",
+        "noRecursiveIntervals",
+        "enums",
+        "congruence",
+        "octagon",
+        "wideningThresholds",
+        "loopUnrollHeuristic",
+        "memsafetySpecification",
+        "noOverflows",
+        "termination",
+        "tmpSpecialAnalysis"
+      ]
+    }
+  },
+  "exp": {
+    "region-offsets": true
+  },
+  "solver": "td3",
+  "sem": {
+    "unknown_function": {
+      "spawn": false
+    },
+    "int": {
+      "signed_overflow": "assume_none"
+    },
+    "null-pointer": {
+      "dereference": "assume_none"
+    }
+  },
+  "witness": {
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    },
+    "yaml": {
+      "enabled": true,
+      "format-version": "2.0",
+      "entry-types": [
+        "invariant_set"
+      ],
+      "invariant-types": [
+        "loop_invariant"
+      ]
+    },
+    "invariant": {
+      "loop-head": true,
+      "after-lock": false,
+      "other": false,
+      "accessed": false,
+      "exact": true
+    }
+  },
+  "pre": {
+    "enabled": false
+  }
+}
diff --git a/conf/race-digests/mutex+threadflag.json b/conf/race-digests/mutex+threadflag.json
new file mode 100644
index 0000000000..9bed592781
--- /dev/null
+++ b/conf/race-digests/mutex+threadflag.json
@@ -0,0 +1,127 @@
+{
+  "ana": {
+    "sv-comp": {
+      "enabled": true,
+      "functions": true
+    },
+    "int": {
+      "def_exc": true,
+      "enums": false,
+      "interval": true
+    },
+    "float": {
+      "interval": true,
+      "evaluate_math_functions": true
+    },
+    "activated": [
+      "base",
+      "threadid",
+      "threadflag",
+      "threadreturn",
+      "mallocWrapper",
+      "mutexEvents",
+      "mutex",
+      "access",
+      "race",
+      "escape",
+      "expRelation",
+      "mhp",
+      "assert",
+      "var_eq",
+      "symb_locks",
+      "region",
+      "thread",
+      "threadJoins",
+      "abortUnless"
+    ],
+    "path_sens": [
+      "mutex",
+      "malloc_null",
+      "uninit",
+      "expsplit",
+      "activeSetjmp",
+      "memLeak",
+      "threadflag"
+    ],
+    "context": {
+      "widen": false
+    },
+    "base": {
+      "arrays": {
+        "domain": "partitioned"
+      }
+    },
+    "race": {
+      "free": false,
+      "call": false,
+      "digests": {
+        "lockset": true,
+
+        "region": false,
+        "symb_locks": false,
+        "threadflag": true,
+        "tid": false,
+        "join" : false
+      }
+    },
+    "autotune": {
+      "enabled": true,
+      "activated": [
+        "singleThreaded",
+        "mallocWrappers",
+        "noRecursiveIntervals",
+        "enums",
+        "congruence",
+        "octagon",
+        "wideningThresholds",
+        "loopUnrollHeuristic",
+        "memsafetySpecification",
+        "noOverflows",
+        "termination",
+        "tmpSpecialAnalysis"
+      ]
+    }
+  },
+  "exp": {
+    "region-offsets": true
+  },
+  "solver": "td3",
+  "sem": {
+    "unknown_function": {
+      "spawn": false
+    },
+    "int": {
+      "signed_overflow": "assume_none"
+    },
+    "null-pointer": {
+      "dereference": "assume_none"
+    }
+  },
+  "witness": {
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    },
+    "yaml": {
+      "enabled": true,
+      "format-version": "2.0",
+      "entry-types": [
+        "invariant_set"
+      ],
+      "invariant-types": [
+        "loop_invariant"
+      ]
+    },
+    "invariant": {
+      "loop-head": true,
+      "after-lock": false,
+      "other": false,
+      "accessed": false,
+      "exact": true
+    }
+  },
+  "pre": {
+    "enabled": false
+  }
+}
diff --git a/conf/race-digests/mutex-only.json b/conf/race-digests/mutex-only.json
new file mode 100644
index 0000000000..a23e3bf546
--- /dev/null
+++ b/conf/race-digests/mutex-only.json
@@ -0,0 +1,127 @@
+{
+  "ana": {
+    "sv-comp": {
+      "enabled": true,
+      "functions": true
+    },
+    "int": {
+      "def_exc": true,
+      "enums": false,
+      "interval": true
+    },
+    "float": {
+      "interval": true,
+      "evaluate_math_functions": true
+    },
+    "activated": [
+      "base",
+      "threadid",
+      "threadflag",
+      "threadreturn",
+      "mallocWrapper",
+      "mutexEvents",
+      "mutex",
+      "access",
+      "race",
+      "escape",
+      "expRelation",
+      "mhp",
+      "assert",
+      "var_eq",
+      "symb_locks",
+      "region",
+      "thread",
+      "threadJoins",
+      "abortUnless"
+    ],
+    "path_sens": [
+      "mutex",
+      "malloc_null",
+      "uninit",
+      "expsplit",
+      "activeSetjmp",
+      "memLeak",
+      "threadflag"
+    ],
+    "context": {
+      "widen": false
+    },
+    "base": {
+      "arrays": {
+        "domain": "partitioned"
+      }
+    },
+    "race": {
+      "free": false,
+      "call": false,
+      "digests": {
+        "lockset": true,
+        "fresh": false,
+        "region": false,
+        "symb_locks": false,
+        "threadflag": false,
+        "tid": false,
+        "join" : false
+      }
+    },
+    "autotune": {
+      "enabled": true,
+      "activated": [
+        "singleThreaded",
+        "mallocWrappers",
+        "noRecursiveIntervals",
+        "enums",
+        "congruence",
+        "octagon",
+        "wideningThresholds",
+        "loopUnrollHeuristic",
+        "memsafetySpecification",
+        "noOverflows",
+        "termination",
+        "tmpSpecialAnalysis"
+      ]
+    }
+  },
+  "exp": {
+    "region-offsets": true
+  },
+  "solver": "td3",
+  "sem": {
+    "unknown_function": {
+      "spawn": false
+    },
+    "int": {
+      "signed_overflow": "assume_none"
+    },
+    "null-pointer": {
+      "dereference": "assume_none"
+    }
+  },
+  "witness": {
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    },
+    "yaml": {
+      "enabled": true,
+      "format-version": "2.0",
+      "entry-types": [
+        "invariant_set"
+      ],
+      "invariant-types": [
+        "loop_invariant"
+      ]
+    },
+    "invariant": {
+      "loop-head": true,
+      "after-lock": false,
+      "other": false,
+      "accessed": false,
+      "exact": true
+    }
+  },
+  "pre": {
+    "enabled": false
+  }
+}
diff --git a/conf/race-digests/none.json b/conf/race-digests/none.json
new file mode 100644
index 0000000000..93b82cc39a
--- /dev/null
+++ b/conf/race-digests/none.json
@@ -0,0 +1,127 @@
+{
+  "ana": {
+    "sv-comp": {
+      "enabled": true,
+      "functions": true
+    },
+    "int": {
+      "def_exc": true,
+      "enums": false,
+      "interval": true
+    },
+    "float": {
+      "interval": true,
+      "evaluate_math_functions": true
+    },
+    "activated": [
+      "base",
+      "threadid",
+      "threadflag",
+      "threadreturn",
+      "mallocWrapper",
+      "mutexEvents",
+      "mutex",
+      "access",
+      "race",
+      "escape",
+      "expRelation",
+      "mhp",
+      "assert",
+      "var_eq",
+      "symb_locks",
+      "region",
+      "thread",
+      "threadJoins",
+      "abortUnless"
+    ],
+    "path_sens": [
+      "mutex",
+      "malloc_null",
+      "uninit",
+      "expsplit",
+      "activeSetjmp",
+      "memLeak",
+      "threadflag"
+    ],
+    "context": {
+      "widen": false
+    },
+    "base": {
+      "arrays": {
+        "domain": "partitioned"
+      }
+    },
+    "race": {
+      "free": false,
+      "call": false,
+      "digests": {
+        "lockset": false,
+        "fresh": false,
+        "region": false,
+        "symb_locks": false,
+        "threadflag": false,
+        "tid": false,
+        "join" : false
+      }
+    },
+    "autotune": {
+      "enabled": true,
+      "activated": [
+        "singleThreaded",
+        "mallocWrappers",
+        "noRecursiveIntervals",
+        "enums",
+        "congruence",
+        "octagon",
+        "wideningThresholds",
+        "loopUnrollHeuristic",
+        "memsafetySpecification",
+        "noOverflows",
+        "termination",
+        "tmpSpecialAnalysis"
+      ]
+    }
+  },
+  "exp": {
+    "region-offsets": true
+  },
+  "solver": "td3",
+  "sem": {
+    "unknown_function": {
+      "spawn": false
+    },
+    "int": {
+      "signed_overflow": "assume_none"
+    },
+    "null-pointer": {
+      "dereference": "assume_none"
+    }
+  },
+  "witness": {
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    },
+    "yaml": {
+      "enabled": true,
+      "format-version": "2.0",
+      "entry-types": [
+        "invariant_set"
+      ],
+      "invariant-types": [
+        "loop_invariant"
+      ]
+    },
+    "invariant": {
+      "loop-head": true,
+      "after-lock": false,
+      "other": false,
+      "accessed": false,
+      "exact": true
+    }
+  },
+  "pre": {
+    "enabled": false
+  }
+}
diff --git a/conf/race-digests/region-only.json b/conf/race-digests/region-only.json
new file mode 100644
index 0000000000..e202197269
--- /dev/null
+++ b/conf/race-digests/region-only.json
@@ -0,0 +1,128 @@
+{
+  "ana": {
+    "sv-comp": {
+      "enabled": true,
+      "functions": true
+    },
+    "int": {
+      "def_exc": true,
+      "enums": false,
+      "interval": true
+    },
+    "float": {
+      "interval": true,
+      "evaluate_math_functions": true
+    },
+    "activated": [
+      "base",
+      "threadid",
+      "threadflag",
+      "threadreturn",
+      "mallocWrapper",
+      "mutexEvents",
+      "mutex",
+      "access",
+      "race",
+      "escape",
+      "expRelation",
+      "mhp",
+      "assert",
+      "var_eq",
+      "symb_locks",
+      "region",
+      "thread",
+      "threadJoins",
+      "abortUnless"
+    ],
+    "path_sens": [
+      "mutex",
+      "malloc_null",
+      "uninit",
+      "expsplit",
+      "activeSetjmp",
+      "memLeak",
+      "threadflag"
+    ],
+    "context": {
+      "widen": false
+    },
+    "base": {
+      "arrays": {
+        "domain": "partitioned"
+      }
+    },
+    "race": {
+      "free": false,
+      "call": false,
+      "digests": {
+        "lockset": false,
+
+        "fresh": false,
+        "region": true,
+        "symb_locks": false,
+        "threadflag": false,
+        "tid": false,
+        "join" : false
+      }
+    },
+    "autotune": {
+      "enabled": true,
+      "activated": [
+        "singleThreaded",
+        "mallocWrappers",
+        "noRecursiveIntervals",
+        "enums",
+        "congruence",
+        "octagon",
+        "wideningThresholds",
+        "loopUnrollHeuristic",
+        "memsafetySpecification",
+        "noOverflows",
+        "termination",
+        "tmpSpecialAnalysis"
+      ]
+    }
+  },
+  "exp": {
+    "region-offsets": true
+  },
+  "solver": "td3",
+  "sem": {
+    "unknown_function": {
+      "spawn": false
+    },
+    "int": {
+      "signed_overflow": "assume_none"
+    },
+    "null-pointer": {
+      "dereference": "assume_none"
+    }
+  },
+  "witness": {
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    },
+    "yaml": {
+      "enabled": true,
+      "format-version": "2.0",
+      "entry-types": [
+        "invariant_set"
+      ],
+      "invariant-types": [
+        "loop_invariant"
+      ]
+    },
+    "invariant": {
+      "loop-head": true,
+      "after-lock": false,
+      "other": false,
+      "accessed": false,
+      "exact": true
+    }
+  },
+  "pre": {
+    "enabled": false
+  }
+}
diff --git a/conf/race-digests/symblocks-only.json b/conf/race-digests/symblocks-only.json
new file mode 100644
index 0000000000..e3a3ce6a06
--- /dev/null
+++ b/conf/race-digests/symblocks-only.json
@@ -0,0 +1,128 @@
+{
+  "ana": {
+    "sv-comp": {
+      "enabled": true,
+      "functions": true
+    },
+    "int": {
+      "def_exc": true,
+      "enums": false,
+      "interval": true
+    },
+    "float": {
+      "interval": true,
+      "evaluate_math_functions": true
+    },
+    "activated": [
+      "base",
+      "threadid",
+      "threadflag",
+      "threadreturn",
+      "mallocWrapper",
+      "mutexEvents",
+      "mutex",
+      "access",
+      "race",
+      "escape",
+      "expRelation",
+      "mhp",
+      "assert",
+      "var_eq",
+      "symb_locks",
+      "region",
+      "thread",
+      "threadJoins",
+      "abortUnless"
+    ],
+    "path_sens": [
+      "mutex",
+      "malloc_null",
+      "uninit",
+      "expsplit",
+      "activeSetjmp",
+      "memLeak",
+      "threadflag"
+    ],
+    "context": {
+      "widen": false
+    },
+    "base": {
+      "arrays": {
+        "domain": "partitioned"
+      }
+    },
+    "race": {
+      "free": false,
+      "call": false,
+      "digests": {
+        "lockset": false,
+
+        "fresh": false,
+        "region": false,
+        "symb_locks": true,
+        "threadflag": false,
+        "tid": false,
+        "join" : false
+      }
+    },
+    "autotune": {
+      "enabled": true,
+      "activated": [
+        "singleThreaded",
+        "mallocWrappers",
+        "noRecursiveIntervals",
+        "enums",
+        "congruence",
+        "octagon",
+        "wideningThresholds",
+        "loopUnrollHeuristic",
+        "memsafetySpecification",
+        "noOverflows",
+        "termination",
+        "tmpSpecialAnalysis"
+      ]
+    }
+  },
+  "exp": {
+    "region-offsets": true
+  },
+  "solver": "td3",
+  "sem": {
+    "unknown_function": {
+      "spawn": false
+    },
+    "int": {
+      "signed_overflow": "assume_none"
+    },
+    "null-pointer": {
+      "dereference": "assume_none"
+    }
+  },
+  "witness": {
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    },
+    "yaml": {
+      "enabled": true,
+      "format-version": "2.0",
+      "entry-types": [
+        "invariant_set"
+      ],
+      "invariant-types": [
+        "loop_invariant"
+      ]
+    },
+    "invariant": {
+      "loop-head": true,
+      "after-lock": false,
+      "other": false,
+      "accessed": false,
+      "exact": true
+    }
+  },
+  "pre": {
+    "enabled": false
+  }
+}
diff --git a/conf/race-digests/tf-only.json b/conf/race-digests/tf-only.json
new file mode 100644
index 0000000000..f87f076c03
--- /dev/null
+++ b/conf/race-digests/tf-only.json
@@ -0,0 +1,128 @@
+{
+  "ana": {
+    "sv-comp": {
+      "enabled": true,
+      "functions": true
+    },
+    "int": {
+      "def_exc": true,
+      "enums": false,
+      "interval": true
+    },
+    "float": {
+      "interval": true,
+      "evaluate_math_functions": true
+    },
+    "activated": [
+      "base",
+      "threadid",
+      "threadflag",
+      "threadreturn",
+      "mallocWrapper",
+      "mutexEvents",
+      "mutex",
+      "access",
+      "race",
+      "escape",
+      "expRelation",
+      "mhp",
+      "assert",
+      "var_eq",
+      "symb_locks",
+      "region",
+      "thread",
+      "threadJoins",
+      "abortUnless"
+    ],
+    "path_sens": [
+      "mutex",
+      "malloc_null",
+      "uninit",
+      "expsplit",
+      "activeSetjmp",
+      "memLeak",
+      "threadflag"
+    ],
+    "context": {
+      "widen": false
+    },
+    "base": {
+      "arrays": {
+        "domain": "partitioned"
+      }
+    },
+    "race": {
+      "free": false,
+      "call": false,
+      "digests": {
+        "lockset": false,
+
+        "fresh": false,
+        "region": false,
+        "symb_locks": false,
+        "threadflag": true,
+        "tid": false,
+        "join" : false
+      }
+    },
+    "autotune": {
+      "enabled": true,
+      "activated": [
+        "singleThreaded",
+        "mallocWrappers",
+        "noRecursiveIntervals",
+        "enums",
+        "congruence",
+        "octagon",
+        "wideningThresholds",
+        "loopUnrollHeuristic",
+        "memsafetySpecification",
+        "noOverflows",
+        "termination",
+        "tmpSpecialAnalysis"
+      ]
+    }
+  },
+  "exp": {
+    "region-offsets": true
+  },
+  "solver": "td3",
+  "sem": {
+    "unknown_function": {
+      "spawn": false
+    },
+    "int": {
+      "signed_overflow": "assume_none"
+    },
+    "null-pointer": {
+      "dereference": "assume_none"
+    }
+  },
+  "witness": {
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    },
+    "yaml": {
+      "enabled": true,
+      "format-version": "2.0",
+      "entry-types": [
+        "invariant_set"
+      ],
+      "invariant-types": [
+        "loop_invariant"
+      ]
+    },
+    "invariant": {
+      "loop-head": true,
+      "after-lock": false,
+      "other": false,
+      "accessed": false,
+      "exact": true
+    }
+  },
+  "pre": {
+    "enabled": false
+  }
+}
diff --git a/conf/race-digests/tid+join.json b/conf/race-digests/tid+join.json
new file mode 100644
index 0000000000..55382576e0
--- /dev/null
+++ b/conf/race-digests/tid+join.json
@@ -0,0 +1,128 @@
+{
+  "ana": {
+    "sv-comp": {
+      "enabled": true,
+      "functions": true
+    },
+    "int": {
+      "def_exc": true,
+      "enums": false,
+      "interval": true
+    },
+    "float": {
+      "interval": true,
+      "evaluate_math_functions": true
+    },
+    "activated": [
+      "base",
+      "threadid",
+      "threadflag",
+      "threadreturn",
+      "mallocWrapper",
+      "mutexEvents",
+      "mutex",
+      "access",
+      "race",
+      "escape",
+      "expRelation",
+      "mhp",
+      "assert",
+      "var_eq",
+      "symb_locks",
+      "region",
+      "thread",
+      "threadJoins",
+      "abortUnless"
+    ],
+    "path_sens": [
+      "mutex",
+      "malloc_null",
+      "uninit",
+      "expsplit",
+      "activeSetjmp",
+      "memLeak",
+      "threadflag"
+    ],
+    "context": {
+      "widen": false
+    },
+    "base": {
+      "arrays": {
+        "domain": "partitioned"
+      }
+    },
+    "race": {
+      "free": false,
+      "call": false,
+      "digests": {
+        "lockset": false,
+
+        "fresh": false,
+        "region": false,
+        "symb_locks": false,
+        "threadflag": false,
+        "tid": true,
+        "join" : true
+      }
+    },
+    "autotune": {
+      "enabled": true,
+      "activated": [
+        "singleThreaded",
+        "mallocWrappers",
+        "noRecursiveIntervals",
+        "enums",
+        "congruence",
+        "octagon",
+        "wideningThresholds",
+        "loopUnrollHeuristic",
+        "memsafetySpecification",
+        "noOverflows",
+        "termination",
+        "tmpSpecialAnalysis"
+      ]
+    }
+  },
+  "exp": {
+    "region-offsets": true
+  },
+  "solver": "td3",
+  "sem": {
+    "unknown_function": {
+      "spawn": false
+    },
+    "int": {
+      "signed_overflow": "assume_none"
+    },
+    "null-pointer": {
+      "dereference": "assume_none"
+    }
+  },
+  "witness": {
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    },
+    "yaml": {
+      "enabled": true,
+      "format-version": "2.0",
+      "entry-types": [
+        "invariant_set"
+      ],
+      "invariant-types": [
+        "loop_invariant"
+      ]
+    },
+    "invariant": {
+      "loop-head": true,
+      "after-lock": false,
+      "other": false,
+      "accessed": false,
+      "exact": true
+    }
+  },
+  "pre": {
+    "enabled": false
+  }
+}
diff --git a/conf/race-digests/tid+mutex+join.json b/conf/race-digests/tid+mutex+join.json
new file mode 100644
index 0000000000..e32d35f73c
--- /dev/null
+++ b/conf/race-digests/tid+mutex+join.json
@@ -0,0 +1,128 @@
+{
+  "ana": {
+    "sv-comp": {
+      "enabled": true,
+      "functions": true
+    },
+    "int": {
+      "def_exc": true,
+      "enums": false,
+      "interval": true
+    },
+    "float": {
+      "interval": true,
+      "evaluate_math_functions": true
+    },
+    "activated": [
+      "base",
+      "threadid",
+      "threadflag",
+      "threadreturn",
+      "mallocWrapper",
+      "mutexEvents",
+      "mutex",
+      "access",
+      "race",
+      "escape",
+      "expRelation",
+      "mhp",
+      "assert",
+      "var_eq",
+      "symb_locks",
+      "region",
+      "thread",
+      "threadJoins",
+      "abortUnless"
+    ],
+    "path_sens": [
+      "mutex",
+      "malloc_null",
+      "uninit",
+      "expsplit",
+      "activeSetjmp",
+      "memLeak",
+      "threadflag"
+    ],
+    "context": {
+      "widen": false
+    },
+    "base": {
+      "arrays": {
+        "domain": "partitioned"
+      }
+    },
+    "race": {
+      "free": false,
+      "call": false,
+      "digests": {
+        "lockset": true,
+
+        "fresh": false,
+        "region": false,
+        "symb_locks": false,
+        "threadflag": false,
+        "tid": true,
+        "join" : true
+      }
+    },
+    "autotune": {
+      "enabled": true,
+      "activated": [
+        "singleThreaded",
+        "mallocWrappers",
+        "noRecursiveIntervals",
+        "enums",
+        "congruence",
+        "octagon",
+        "wideningThresholds",
+        "loopUnrollHeuristic",
+        "memsafetySpecification",
+        "noOverflows",
+        "termination",
+        "tmpSpecialAnalysis"
+      ]
+    }
+  },
+  "exp": {
+    "region-offsets": true
+  },
+  "solver": "td3",
+  "sem": {
+    "unknown_function": {
+      "spawn": false
+    },
+    "int": {
+      "signed_overflow": "assume_none"
+    },
+    "null-pointer": {
+      "dereference": "assume_none"
+    }
+  },
+  "witness": {
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    },
+    "yaml": {
+      "enabled": true,
+      "format-version": "2.0",
+      "entry-types": [
+        "invariant_set"
+      ],
+      "invariant-types": [
+        "loop_invariant"
+      ]
+    },
+    "invariant": {
+      "loop-head": true,
+      "after-lock": false,
+      "other": false,
+      "accessed": false,
+      "exact": true
+    }
+  },
+  "pre": {
+    "enabled": false
+  }
+}
diff --git a/conf/race-digests/tid+mutex.json b/conf/race-digests/tid+mutex.json
new file mode 100644
index 0000000000..f5baca160c
--- /dev/null
+++ b/conf/race-digests/tid+mutex.json
@@ -0,0 +1,128 @@
+{
+  "ana": {
+    "sv-comp": {
+      "enabled": true,
+      "functions": true
+    },
+    "int": {
+      "def_exc": true,
+      "enums": false,
+      "interval": true
+    },
+    "float": {
+      "interval": true,
+      "evaluate_math_functions": true
+    },
+    "activated": [
+      "base",
+      "threadid",
+      "threadflag",
+      "threadreturn",
+      "mallocWrapper",
+      "mutexEvents",
+      "mutex",
+      "access",
+      "race",
+      "escape",
+      "expRelation",
+      "mhp",
+      "assert",
+      "var_eq",
+      "symb_locks",
+      "region",
+      "thread",
+      "threadJoins",
+      "abortUnless"
+    ],
+    "path_sens": [
+      "mutex",
+      "malloc_null",
+      "uninit",
+      "expsplit",
+      "activeSetjmp",
+      "memLeak",
+      "threadflag"
+    ],
+    "context": {
+      "widen": false
+    },
+    "base": {
+      "arrays": {
+        "domain": "partitioned"
+      }
+    },
+    "race": {
+      "free": false,
+      "call": false,
+      "digests": {
+        "lockset": true,
+
+        "fresh": false,
+        "region": false,
+        "symb_locks": false,
+        "threadflag": false,
+        "tid": true,
+        "join" : false
+      }
+    },
+    "autotune": {
+      "enabled": true,
+      "activated": [
+        "singleThreaded",
+        "mallocWrappers",
+        "noRecursiveIntervals",
+        "enums",
+        "congruence",
+        "octagon",
+        "wideningThresholds",
+        "loopUnrollHeuristic",
+        "memsafetySpecification",
+        "noOverflows",
+        "termination",
+        "tmpSpecialAnalysis"
+      ]
+    }
+  },
+  "exp": {
+    "region-offsets": true
+  },
+  "solver": "td3",
+  "sem": {
+    "unknown_function": {
+      "spawn": false
+    },
+    "int": {
+      "signed_overflow": "assume_none"
+    },
+    "null-pointer": {
+      "dereference": "assume_none"
+    }
+  },
+  "witness": {
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    },
+    "yaml": {
+      "enabled": true,
+      "format-version": "2.0",
+      "entry-types": [
+        "invariant_set"
+      ],
+      "invariant-types": [
+        "loop_invariant"
+      ]
+    },
+    "invariant": {
+      "loop-head": true,
+      "after-lock": false,
+      "other": false,
+      "accessed": false,
+      "exact": true
+    }
+  },
+  "pre": {
+    "enabled": false
+  }
+}
diff --git a/conf/race-digests/tid-only.json b/conf/race-digests/tid-only.json
new file mode 100644
index 0000000000..c97b857073
--- /dev/null
+++ b/conf/race-digests/tid-only.json
@@ -0,0 +1,128 @@
+{
+  "ana": {
+    "sv-comp": {
+      "enabled": true,
+      "functions": true
+    },
+    "int": {
+      "def_exc": true,
+      "enums": false,
+      "interval": true
+    },
+    "float": {
+      "interval": true,
+      "evaluate_math_functions": true
+    },
+    "activated": [
+      "base",
+      "threadid",
+      "threadflag",
+      "threadreturn",
+      "mallocWrapper",
+      "mutexEvents",
+      "mutex",
+      "access",
+      "race",
+      "escape",
+      "expRelation",
+      "mhp",
+      "assert",
+      "var_eq",
+      "symb_locks",
+      "region",
+      "thread",
+      "threadJoins",
+      "abortUnless"
+    ],
+    "path_sens": [
+      "mutex",
+      "malloc_null",
+      "uninit",
+      "expsplit",
+      "activeSetjmp",
+      "memLeak",
+      "threadflag"
+    ],
+    "context": {
+      "widen": false
+    },
+    "base": {
+      "arrays": {
+        "domain": "partitioned"
+      }
+    },
+    "race": {
+      "free": false,
+      "call": false,
+      "digests": {
+        "lockset": false,
+
+        "fresh": false,
+        "region": false,
+        "symb_locks": false,
+        "threadflag": false,
+        "tid": true,
+        "join" : false
+      }
+    },
+    "autotune": {
+      "enabled": true,
+      "activated": [
+        "singleThreaded",
+        "mallocWrappers",
+        "noRecursiveIntervals",
+        "enums",
+        "congruence",
+        "octagon",
+        "wideningThresholds",
+        "loopUnrollHeuristic",
+        "memsafetySpecification",
+        "noOverflows",
+        "termination",
+        "tmpSpecialAnalysis"
+      ]
+    }
+  },
+  "exp": {
+    "region-offsets": true
+  },
+  "solver": "td3",
+  "sem": {
+    "unknown_function": {
+      "spawn": false
+    },
+    "int": {
+      "signed_overflow": "assume_none"
+    },
+    "null-pointer": {
+      "dereference": "assume_none"
+    }
+  },
+  "witness": {
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    },
+    "yaml": {
+      "enabled": true,
+      "format-version": "2.0",
+      "entry-types": [
+        "invariant_set"
+      ],
+      "invariant-types": [
+        "loop_invariant"
+      ]
+    },
+    "invariant": {
+      "loop-head": true,
+      "after-lock": false,
+      "other": false,
+      "accessed": false,
+      "exact": true
+    }
+  },
+  "pre": {
+    "enabled": false
+  }
+}
diff --git a/conf/traces-rel.json b/conf/traces-rel.json
index 2b82a57554..fafb397a7f 100644
--- a/conf/traces-rel.json
+++ b/conf/traces-rel.json
@@ -83,7 +83,6 @@
   },
   "pre": {
     "cppflags": [
-      "-DGOBLINT_NO_PTHREAD_ONCE",
       "-DGOBLINT_NO_QSORT",
       "-DGOBLINT_NO_BSEARCH"
     ]
diff --git a/lib/libc/stub/src/pthread.c b/lib/libc/stub/src/pthread.c
deleted file mode 100644
index 1de6202b4b..0000000000
--- a/lib/libc/stub/src/pthread.c
+++ /dev/null
@@ -1,11 +0,0 @@
-#ifndef GOBLINT_NO_PTHREAD_ONCE
-#include <pthread.h>
-
-int pthread_once(pthread_once_t *once_control,void (*init_routine)(void)) __attribute__((goblint_stub));
-int pthread_once(pthread_once_t *once_control,void (*init_routine)(void)) {
-  // Not actually once, just call it
-  int top;
-  init_routine();
-  return top;
-}
-#endif
diff --git a/make.sh b/make.sh
index 0f76759065..fddbf73ae0 100755
--- a/make.sh
+++ b/make.sh
@@ -75,7 +75,7 @@ rule() {
     ;; setup)
       echo "Make sure you have the following installed: opam >= 2.0.0, git, patch, m4, autoconf, libgmp-dev, libmpfr-dev, pkg-config"
       echo "For the --html output you also need: javac, ant, dot (graphviz)"
-      echo "For running the regression tests you also need: ruby, gem, curl"
+      echo "For running the regression tests you also need: ruby, gem, curl, and the `os` gem"
       echo "For reference see ./Dockerfile or ./scripts/travis-ci.sh"
       opam_setup
     ;; dev)
@@ -90,6 +90,7 @@ rule() {
       # Use `git commit -n` to temporarily bypass the hook if necessary.
       echo "Installing gem parallel (not needed for ./scripts/update_suite.rb -s)"
       sudo gem install parallel
+      sudo gem install os
     ;; headers)
       curl -L -O https://github.com/goblint/linux-headers/archive/master.tar.gz
       tar xf master.tar.gz && rm master.tar.gz
diff --git a/scripts/sv-comp/archive.sh b/scripts/sv-comp/archive.sh
index aefac8f769..33ea1b4368 100755
--- a/scripts/sv-comp/archive.sh
+++ b/scripts/sv-comp/archive.sh
@@ -37,7 +37,6 @@ zip goblint/scripts/sv-comp/goblint.zip \
     goblint/lib/libc/stub/include/assert.h \
     goblint/lib/goblint/runtime/include/goblint.h \
     goblint/lib/libc/stub/src/stdlib.c \
-    goblint/lib/libc/stub/src/pthread.c \
     goblint/lib/sv-comp/stub/src/sv-comp.c \
     goblint/README.md \
     goblint/LICENSE
diff --git a/scripts/update_suite.rb b/scripts/update_suite.rb
index b21fb4b532..74fddc7b04 100755
--- a/scripts/update_suite.rb
+++ b/scripts/update_suite.rb
@@ -2,6 +2,7 @@
 
 # gobopt environment variable can be used to override goblint defaults and PARAMs
 
+require 'os'
 require 'find'
 require 'fileutils'
 require 'timeout'
@@ -575,6 +576,8 @@ def run ()
     end
 end
 
+mac = OS.mac?
+
 #processing the file information
 projects = []
 project_ids = Set.new
@@ -603,6 +606,7 @@ def run ()
     lines = IO.readlines(path, :encoding => "UTF-8")
 
     next if not future and only.nil? and lines[0] =~ /SKIP/
+    next if mac and lines[0] =~ /NOMAC/
     next if marshal and lines[0] =~ /NOMARSHAL/
     next if not has_linux_headers and lines[0] =~ /kernel/
     if incremental then
diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml
index 55d79a1131..4c2741ac4a 100644
--- a/src/analyses/accessAnalysis.ml
+++ b/src/analyses/accessAnalysis.ml
@@ -28,8 +28,7 @@ struct
 
   let init _ =
     collect_local := get_bool "witness.yaml.enabled" && get_bool "witness.invariant.accessed";
-    let activated = get_string_list "ana.activated" in
-    emit_single_threaded := List.mem (ModifiedSinceSetjmp.Spec.name ()) activated || List.mem (PoisonVariables.Spec.name ()) activated
+    emit_single_threaded := true
 
   let do_access (man: (D.t, G.t, C.t, V.t) man) (kind:AccessKind.t) (reach:bool) (e:exp) =
     if M.tracing then M.trace "access" "do_access %a %a %B" d_exp e AccessKind.pretty kind reach;
diff --git a/src/analyses/mallocFresh.ml b/src/analyses/mallocFresh.ml
index c226d7e6ce..4e7bd84571 100644
--- a/src/analyses/mallocFresh.ml
+++ b/src/analyses/mallocFresh.ml
@@ -64,7 +64,9 @@ struct
   struct
     include BoolDomain.Bool
     let name () = "fresh"
-    let may_race f1 f2 = not (f1 || f2)
+    let may_race f1 f2 =
+      let use_fresh = GobConfig.get_bool "ana.race.digests.fresh" in
+      (not use_fresh) || not (f1 || f2)
     let should_print f = f
   end
   let access man (a: Queries.access) =
diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml
index c712ca9644..996eca9954 100644
--- a/src/analyses/mutexAnalysis.ml
+++ b/src/analyses/mutexAnalysis.ml
@@ -267,6 +267,8 @@ struct
     include MustLocksetRW
     let name () = "lock"
     let may_race ls1 ls2 =
+      let use_lockset = GobConfig.get_bool "ana.race.digests.lockset" in
+      (not use_lockset) ||
       (* not mutually exclusive *)
       not @@ exists (fun ((m1, w1) as l1) ->
           if w1 then
diff --git a/src/analyses/pthreadBarriers.ml b/src/analyses/pthreadBarriers.ml
new file mode 100644
index 0000000000..cc51c163c6
--- /dev/null
+++ b/src/analyses/pthreadBarriers.ml
@@ -0,0 +1,167 @@
+(** Must have waited barriers for Pthread barriers ([pthreadBarriers]). *)
+
+open GoblintCil
+open Analyses
+module LF = LibraryFunctions
+
+module Spec =
+struct
+  module Barriers = struct
+    include SetDomain.ToppedSet (ValueDomain.Addr) (struct let topname = "All barriers" end)
+    let name () = "mayBarriers"
+  end
+
+  module MustBarriers = struct
+    include Lattice.Reverse (Barriers)
+    let name () = "mustBarriers"
+  end
+
+  module Capacity = Queries.ID
+
+  include Analyses.IdentitySpec
+  module V = VarinfoV
+
+  module TID = ThreadIdDomain.ThreadLifted
+
+  module MHPplusLock = struct
+    module Locks = LockDomain.MustLockset
+
+    include Printable.Prod (MHP) (Locks)
+    let name () = "MHPplusLock"
+
+    let mhp (mhp1, l1) (mhp2, l2) =
+      MHP.may_happen_in_parallel mhp1 mhp2 && Locks.is_empty (Locks.inter l1 l2)
+
+    let tid ((mhp:MHP.t), _) = mhp.tid
+
+    let may_be_non_unique_thread (mhp, _) = MHP.may_be_non_unique_thread mhp
+  end
+
+  module Waiters = SetDomain.ToppedSet (MHPplusLock) (struct let topname = "All MHP" end)
+  module Multiprocess = BoolDomain.MayBool
+  module G = Lattice.Prod3 (Multiprocess) (Capacity) (Waiters)
+
+  let name () = "pthreadBarriers"
+
+  module MustObserved = MapDomain.MapTop_LiftBot (TID) (MustBarriers)
+  module D = Lattice.Prod (Barriers) (MustObserved)
+
+  include Analyses.ValueContexts(D)
+
+  let possible_vinfos (a: Queries.ask) barrier =
+    Queries.AD.to_var_may (a.f (Queries.MayPointTo barrier))
+
+  let special man (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
+    let exists_k pred k waiters =
+      let k_product elems =
+        let rec doit k =
+          if k = 1 then
+            Seq.map (Seq.return) elems
+          else
+            let arg = doit (k-1) in
+            Seq.map_product (Seq.cons) elems arg
+        in
+        doit k
+      in
+      Seq.exists pred (k_product (Waiters.to_seq waiters))
+    in
+    let desc = LF.find f in
+    match desc.special arglist with
+    | BarrierWait barrier ->
+      let ask = Analyses.ask_of_man man in
+      let may, must = man.local in
+      let barriers = possible_vinfos ask barrier in
+      let mhp = MHP.current ask in
+      let handle_one b =
+        try
+          let locks = man.ask (Queries.MustLockset) in
+          man.sideg b (Multiprocess.bot (), Capacity.bot (), Waiters.singleton (mhp, locks));
+          let addr = ValueDomain.Addr.of_var b in
+          let (multiprocess, capacity, waiters) = man.global b in
+          let may = Barriers.add addr may in
+          if multiprocess then
+            (may, must)
+          else
+            let relevant_waiters = Waiters.filter (fun other -> MHPplusLock.mhp (mhp, locks) other) waiters in
+            if Waiters.exists MHPplusLock.may_be_non_unique_thread relevant_waiters then
+              (may, must)
+            else
+              match capacity with
+              | `Top | `Bot -> (may, must)
+              | `Lifted c ->
+                let count = Waiters.cardinal relevant_waiters in
+                (* Add 1 as the thread calling wait at the moment will not be MHP with itself *)
+                let min_cap = (BatOption.default Z.zero (Capacity.I.minimal c)) in
+                if Z.leq min_cap Z.one then
+                  (may, must)
+                else if Z.geq (Z.of_int (count + 1)) min_cap then
+                  (* This is quite a cute problem: Do (min_cap-1) elements exist in the set such that
+                      MHP is pairwise true? This solution is a sledgehammer, there should be something much
+                      better algorithmically (beyond just laziness) *)
+                  let must =
+                    let waiters = Waiters.elements relevant_waiters in
+                    let min_cap = Z.to_int min_cap in
+                    let can_proceed_pred seq =
+                      let rec doit seq = match Seq.uncons seq with
+                        | None -> true
+                        | Some (h, t) -> Seq.for_all (MHPplusLock.mhp h) t && doit t
+                      in
+                      doit seq
+                    in
+                    let can_proceed = exists_k can_proceed_pred (min_cap - 1) relevant_waiters in
+                    if not can_proceed then raise Analyses.Deadcode;
+                    (* limit to this case to avoid having to construct all permutations above *)
+                    if BatList.compare_length_with waiters (min_cap - 1) = 0 then
+                      List.fold_left (fun acc elem ->
+                          let tid = MHPplusLock.tid elem in
+                          let curr = MustObserved.find tid acc in
+                          let must' = MustObserved.add tid (Barriers.add addr curr) acc in
+                          must'
+                        ) must waiters
+                    else
+                      must
+                  in
+                  (may, must)
+                else
+                  raise Analyses.Deadcode;
+        with Analyses.Deadcode -> D.bot ()
+      in
+      let (may, must) = List.fold_left (fun acc b-> D.join acc (handle_one b)) (D.bot ()) barriers in
+      if Barriers.is_empty may then raise Analyses.Deadcode;
+      (may, must)
+    | BarrierInit { barrier; attr; count } ->
+      let multitprocess = not @@ Queries.AD.is_null @@ man.ask (Queries.MayPointTo attr) in
+      if multitprocess then M.warn "Barrier initialized with a non-NULL attr argument. Handled as if PTHREAD_PROCESS_SHARED potentially set.";
+      let count = man.ask (Queries.EvalInt count) in
+      let publish_one b = man.sideg b (multitprocess, count, Waiters.bot ()) in
+      let barriers = possible_vinfos (Analyses.ask_of_man man) barrier in
+      List.iter publish_one barriers;
+      man.local
+    | _ -> man.local
+
+  let startstate v = (Barriers.empty (), MustObserved.empty ())
+  let threadenter man ~multiple lval f args = [man.local]
+  let exitstate  v = (Barriers.empty (), MustObserved.empty ())
+
+  module A =
+  struct
+    include Lattice.Prod3 (Barriers) (MustObserved) (TID)
+    let name () = "barriers"
+    let may_race (may_await_t1, must_observed_by_t1, t1) (may_await_t2, must_observed_by_t2, t2) =
+      let observed_from_t2 = MustObserved.find t2 must_observed_by_t1 in
+      if not (Barriers.subset observed_from_t2 may_await_t2) then
+        false
+      else
+        let observed_from_t1 = MustObserved.find t1 must_observed_by_t2 in
+        Barriers.subset observed_from_t1 may_await_t1
+    let should_print f = true
+  end
+
+  let access man (a: Queries.access) =
+    let (may,must) = man.local in
+    let mhp = MHP.current (Analyses.ask_of_man man) in
+    (may, must, mhp.tid)
+end
+
+let _ =
+  MCP.register_analysis (module Spec : MCPSpec)
diff --git a/src/analyses/pthreadOnce.ml b/src/analyses/pthreadOnce.ml
new file mode 100644
index 0000000000..cc7dc3e611
--- /dev/null
+++ b/src/analyses/pthreadOnce.ml
@@ -0,0 +1,109 @@
+(** Must active and have passed pthreadOnce calls ([pthreadOnce]). *)
+
+open GoblintCil
+open Analyses
+module LF = LibraryFunctions
+
+module Spec =
+struct
+  module Onces = struct
+    include SetDomain.ToppedSet (CilType.Varinfo) (struct let topname = "All onces" end)
+    let name () = "mayOnces"
+  end
+
+  module ActiveOnces = struct
+    include Lattice.Reverse (Onces)
+    let name () = "active"
+  end
+
+  module SeenOnces = struct
+    include Lattice.Reverse (Onces)
+    let name () = "seen"
+  end
+
+  include Analyses.DefaultSpec
+
+  let name () = "pthreadOnce"
+  module D = Lattice.Prod (ActiveOnces) (SeenOnces)
+  include Analyses.ValueContexts(D)
+
+  (* transfer functions *)
+  let assign man (lval:lval) (rval:exp) : D.t =
+    man.local
+
+  let branch man (exp:exp) (tv:bool) : D.t =
+    man.local
+
+  let body man (f:fundec) : D.t =
+    man.local
+
+  let return man (exp:exp option) (f:fundec) : D.t =
+    man.local
+
+  let enter man (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
+    [man.local, man.local]
+
+  let combine_env man lval fexp f args fc au f_ask =
+    au
+
+  let combine_assign man (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask: Queries.ask) : D.t =
+    man.local
+
+  let special man (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
+    man.local
+
+  let startstate v = (Onces.empty (), Onces.empty ())
+
+  let possible_vinfos (a: Queries.ask) barrier =
+    Queries.AD.to_var_may (a.f (Queries.MayPointTo barrier))
+
+  let event man (e: Events.t) oman : D.t =
+    match e with
+    | Events.EnterOnce { once_control; tf } when tf ->
+      (let (active, seen) = man.local in
+       let ask = Analyses.ask_of_man man in
+       let possible_vinfos = possible_vinfos ask once_control in
+       let unseen = List.filter (fun v -> not (Onces.mem v seen) && not (Onces.mem v active)) possible_vinfos in
+       match unseen with
+       | [] -> raise Deadcode
+       | [v] -> (Onces.add v active, seen)
+       | _ :: _ -> man.local)
+    | Events.EnterOnce { once_control; tf } ->
+      (let (active, seen) = man.local in
+       let ask = Analyses.ask_of_man man in
+       match possible_vinfos ask once_control with
+       | [v] -> (Onces.add v active, seen)
+       | _ -> man.local)
+    | Events.LeaveOnce { once_control } ->
+      (let (active, seen) = man.local in
+       let ask = Analyses.ask_of_man man in
+       let active' = Onces.diff active (Onces.of_list (possible_vinfos ask once_control)) in
+       let seen' = match possible_vinfos ask once_control with
+         | [v] -> Onces.add v seen
+         | _ -> seen
+       in
+       (active', seen'))
+    | _ -> man.local
+
+  let access man _ = man.local
+
+  module A =
+  struct
+    include D
+    let name () = "onces"
+    let may_race (a1, s1) (a2, s2) =
+      (Onces.is_empty (Onces.inter a1 (Onces.union a2 s2))) && (Onces.is_empty (Onces.inter a2 (Onces.union a1 s1)))
+    let should_print (a1, s1) = not (Onces.is_empty a1) || not (Onces.is_empty s1)
+  end
+
+
+  let threadenter man ~multiple lval f args =
+    let (_, seen) = man.local in
+    [Onces.empty (), seen]
+
+  let threadspawn man ~multiple lval f args fman = man.local
+  let exitstate  v = D.top ()
+end
+
+let _ =
+  MCP.register_analysis (module Spec : MCPSpec)
diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml
index 263506b4fb..c1ca2e97b9 100644
--- a/src/analyses/raceAnalysis.ml
+++ b/src/analyses/raceAnalysis.ml
@@ -304,7 +304,7 @@ struct
 
   let event man e oman =
     match e with
-    | Events.Access {exp; ad; kind; reach} when ThreadFlag.is_currently_multi (Analyses.ask_of_man man) -> (* threadflag query in post-threadspawn man *)
+    | Events.Access {exp; ad; kind; reach} when true (* ThreadFlag.is_currently_multi (Analyses.ask_of_man man) *) -> (* threadflag query in post-threadspawn man *)
       (* must use original (pre-assign, etc) man queries *)
       let conf = 110 in
       let module AD = Queries.AD in
diff --git a/src/analyses/region.ml b/src/analyses/region.ml
index 0fb61059e2..d02df20d0d 100644
--- a/src/analyses/region.ml
+++ b/src/analyses/region.ml
@@ -64,7 +64,10 @@ struct
   struct
     include Printable.Option (Lvals) (struct let name = "no region" end)
     let name () = "region"
-    let may_race r1 r2 = match r1, r2 with
+    let may_race r1 r2 =
+      let use_region = GobConfig.get_bool "ana.race.digests.region" in
+      (not use_region) ||
+      match r1, r2 with
       | None, _
       | _, None -> false
       (* TODO: Should it happen in the first place that RegMap has empty value? Happens in 09-regions/34-escape_rc *)
diff --git a/src/analyses/symbLocks.ml b/src/analyses/symbLocks.ml
index 0850fac317..9cf212b6b9 100644
--- a/src/analyses/symbLocks.ml
+++ b/src/analyses/symbLocks.ml
@@ -121,7 +121,9 @@ struct
     include SetDomain.Make (E)
 
     let name () = "symblock"
-    let may_race lp lp2 = disjoint lp lp2
+    let may_race lp lp2 =
+      let use_symblocks = GobConfig.get_bool "ana.race.digests.symb_locks" in
+      (not use_symblocks) || disjoint lp lp2
     let should_print lp = not (is_empty lp)
   end
 
diff --git a/src/analyses/threadFlag.ml b/src/analyses/threadFlag.ml
index 1e0ff7db9f..1e362fa104 100644
--- a/src/analyses/threadFlag.ml
+++ b/src/analyses/threadFlag.ml
@@ -54,13 +54,30 @@ struct
 
   module A =
   struct
-    include BoolDomain.Bool
-    let name () = "multi"
-    let may_race m1 m2 = m1 && m2 (* kill access when single threaded *)
-    let should_print m = not m
+    include Lattice.Prod(Flag)(BoolDomain.MayBool)
+    let name () = "threadflag"
+
+    let may_race (m1,b1) (m2,b2) =
+      let use_threadflag = GobConfig.get_bool "ana.race.digests.threadflag" in
+      let both_mt = Flag.is_multi m1 && Flag.is_multi m2 in
+      let one_not_main = Flag.is_not_main m1 || Flag.is_not_main m2 in
+      ((not use_threadflag) || (both_mt && one_not_main)) && b1 && b2
+
+    (* kill access when single threaded *)
+
+    let should_print m = true
   end
+
   let access man _ =
-    is_currently_multi (Analyses.ask_of_man man)
+    let st =
+      if GobConfig.get_bool "ana.race.digests.join" then
+        is_currently_multi (Analyses.ask_of_man man)
+      else if GobConfig.get_bool "ana.race.digests.tid" then
+        has_ever_been_multi (Analyses.ask_of_man man)
+      else
+        true
+    in
+    ((man.local,st):A.t)
 
   let threadenter man ~multiple lval f args =
     if not (has_ever_been_multi (Analyses.ask_of_man man)) then
diff --git a/src/analyses/threadId.ml b/src/analyses/threadId.ml
index 53d070a056..c6e521b1d5 100644
--- a/src/analyses/threadId.ml
+++ b/src/analyses/threadId.ml
@@ -132,7 +132,10 @@ struct
   struct
     include Printable.Option (ThreadLifted) (struct let name = "nonunique" end)
     let name () = "thread"
-    let may_race (t1: t) (t2: t) = match t1, t2 with
+    let may_race (t1: t) (t2: t) =
+      let use_tid = GobConfig.get_bool "ana.race.digests.tid" in
+      (not use_tid) ||
+      match t1, t2 with
       | Some t1, Some t2 when ThreadLifted.equal t1 t2 -> false (* only unique threads *)
       | _, _ -> true
     let should_print = Option.is_some
diff --git a/src/cdomains/mHP.ml b/src/cdomains/mHP.ml
index afaf6d67e3..dc6d49a529 100644
--- a/src/cdomains/mHP.ml
+++ b/src/cdomains/mHP.ml
@@ -77,18 +77,25 @@ let must_be_joined other joined =
 
 (** May two program points with respective MHP information happen in parallel *)
 let may_happen_in_parallel one two =
-  let {tid=tid; created=created; must_joined=must_joined} = one in
+  let use_tid = GobConfig.get_bool "ana.race.digests.tid" in
+  let use_join = GobConfig.get_bool "ana.race.digests.join" in
+  let {tid; created; must_joined} = one in
   let {tid=tid2; created=created2; must_joined=must_joined2} = two in
   match tid,tid2 with
   | `Lifted tid, `Lifted tid2 ->
-    if (TID.is_unique tid) && (TID.equal tid tid2) then
+    if use_tid && (TID.is_unique tid) && (TID.equal tid tid2) then
       false
-    else if definitely_not_started (tid,created) tid2 || definitely_not_started (tid2,created2) tid then
+    else if use_tid && (definitely_not_started (tid,created) tid2 || definitely_not_started (tid2,created2) tid) then
       false
-    else if must_be_joined tid2 must_joined || must_be_joined tid must_joined2 then
+    else if use_tid && use_join && (must_be_joined tid2 must_joined || must_be_joined tid must_joined2) then
       false
-    else if exists_definitely_not_started_in_joined (tid,created) must_joined2 || exists_definitely_not_started_in_joined (tid2,created2) must_joined then
+    else if use_tid && use_join && (exists_definitely_not_started_in_joined (tid,created) must_joined2 || exists_definitely_not_started_in_joined (tid2,created2) must_joined) then
       false
     else
       true
   | _ -> true
+
+let may_be_non_unique_thread mhp =
+  match mhp.tid with
+  | `Lifted tid -> not (TID.is_unique tid)
+  | _ -> true
\ No newline at end of file
diff --git a/src/config/options.schema.json b/src/config/options.schema.json
index 39c863ad49..8a11ed88de 100644
--- a/src/config/options.schema.json
+++ b/src/config/options.schema.json
@@ -1105,6 +1105,55 @@
               "description": "Report races for volatile variables.",
               "type": "boolean",
               "default": true
+            },
+            "digests": {
+              "title": "ana.race.digests",
+              "type" : "object",
+              "properties" : {
+                "lockset" : {
+                  "title": "ana.race.digests.lockset",
+                  "description": "Use lockset digest for excluding data races.",
+                  "type" : "boolean",
+                  "default" : true
+                },
+                "fresh" : {
+                  "title": "ana.race.digests.fresh",
+                  "description": "Use freshness analysis for excluding data races.",
+                  "type" : "boolean",
+                  "default" : true
+                },
+                "region" : {
+                  "title": "ana.race.digests.region",
+                  "description": "Use region analysis for excluding data races.",
+                  "type" : "boolean",
+                  "default" : true
+                },
+                "symb_locks" : {
+                  "title": "ana.race.digests.symb_locks",
+                  "description": "Use symb_locks analysis for excluding data races.",
+                  "type" : "boolean",
+                  "default" : true
+                },
+                "threadflag" : {
+                  "title": "ana.race.digests.threadflag",
+                  "description": "Use threadflag analysis for excluding data races.",
+                  "type" : "boolean",
+                  "default" : true
+                },
+                "tid" : {
+                  "title": "ana.race.digests.tid",
+                  "description": "Use tid analysis for excluding data races.",
+                  "type" : "boolean",
+                  "default" : true
+                },
+                "join" : {
+                  "title": "ana.race.digests.join",
+                  "description": "Use join analysis for excluding data races.",
+                  "type" : "boolean",
+                  "default" : true
+                }
+              },
+              "additionalProperties": false
             }
           },
           "additionalProperties": false
diff --git a/src/domain/disjointDomain.ml b/src/domain/disjointDomain.ml
index 3e02c1d3a0..35a730a4d5 100644
--- a/src/domain/disjointDomain.ml
+++ b/src/domain/disjointDomain.ml
@@ -117,6 +117,7 @@ struct
       add e acc
     ) (empty ()) es
   let elements m = fold List.cons m [] (* no intermediate per-bucket lists *)
+  let to_seq m = fold Seq.cons m Seq.empty
   let map f m = fold (fun e acc ->
       add (f e) acc
     ) m (empty ()) (* no intermediate lists *)
@@ -323,6 +324,7 @@ struct
       add e acc
     ) (empty ()) es
   let elements m = fold List.cons m [] (* no intermediate per-bucket lists *)
+  let to_seq m = fold Seq.cons m Seq.empty
   let map f s = fold (fun e acc ->
       add (f e) acc
     ) s (empty ()) (* no intermediate lists *)
diff --git a/src/domain/setDomain.ml b/src/domain/setDomain.ml
index c552363f3d..e11c8182de 100644
--- a/src/domain/setDomain.ml
+++ b/src/domain/setDomain.ml
@@ -95,6 +95,12 @@ sig
       On set abstractions this lists only canonical elements,
       not all subsumed elements. *)
 
+  val to_seq: t -> elt Seq.t
+  (** See {!Set.S.to_seq}.
+
+      On set abstractions this lists only canonical elements,
+      not all subsumed elements. *)
+
   val of_list: elt list -> t
 
   val min_elt: t -> elt
@@ -332,6 +338,7 @@ struct
   let exists f = schema_default true (S.exists f)
   let filter f = schema (fun t -> `Lifted (S.filter f t)) "filter on `Top"
   let elements = schema S.elements "elements on `Top"
+  let to_seq = schema S.to_seq "to_seq on `Top"
   let of_list xs = `Lifted (S.of_list xs)
   let cardinal = schema S.cardinal "cardinal on `Top"
   let min_elt = schema S.min_elt "min_elt on `Top"
@@ -471,6 +478,7 @@ struct
   let mem e e' = E.leq e e'
   let choose e = e
   let elements e = [e]
+  let to_seq e = Seq.return e
   let remove e e' =
     if E.leq e' e then
       E.bot () (* NB! strong removal *)
diff --git a/src/domains/events.ml b/src/domains/events.ml
index cc4af83819..205b81e443 100644
--- a/src/domains/events.ml
+++ b/src/domains/events.ml
@@ -16,6 +16,8 @@ type t =
   | Assert of exp
   | Unassume of {exp: CilType.Exp.t; tokens: WideningToken.t list}
   | Longjmped of {lval: CilType.Lval.t option}
+  | EnterOnce of {once_control: CilType.Exp.t; tf:bool}
+  | LeaveOnce of {once_control: CilType.Exp.t}
 
 (** Should event be emitted after transfer function raises [Deadcode]? *)
 let emit_on_deadcode = function
@@ -31,7 +33,9 @@ let emit_on_deadcode = function
   | UpdateExpSplit _ (* Pointless to split on dead. *)
   | Unassume _ (* Avoid spurious writes. *)
   | Assert _ (* Pointless to refine dead. *)
-  | Longjmped _ ->
+  | Longjmped _
+  | EnterOnce _
+  | LeaveOnce _ ->
     false
 
 let pretty () = function
@@ -47,3 +51,5 @@ let pretty () = function
   | Assert exp -> dprintf "Assert %a" d_exp exp
   | Unassume {exp; tokens} -> dprintf "Unassume {exp=%a; tokens=%a}" d_exp exp (d_list ", " WideningToken.pretty) tokens
   | Longjmped {lval} -> dprintf "Longjmped {lval=%a}" (docOpt (CilType.Lval.pretty ())) lval
+  | EnterOnce {once_control; tf} -> dprintf "todo"
+  | LeaveOnce {once_control} -> dprintf "todo"
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index c7cfce95d2..93755e668c 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -245,7 +245,7 @@ struct
 
   let tf_special_call man lv f args = S.special man lv f args
 
-  let tf_proc var edge prev_node lv e args getl sidel getg sideg d =
+  let rec tf_proc var edge prev_node lv e args getl sidel getg sideg d =
     let man, r, spawns = common_man var edge prev_node d getl sidel getg sideg in
     let functions =
       match e with
@@ -258,6 +258,34 @@ struct
         let ad = man.ask (Queries.EvalFunvar e) in
         Queries.AD.to_var_may ad (* TODO: don't convert, handle UnknownPtr below *)
     in
+    let once once_control init_routine =
+      let enter =
+        let d' = S.event man (Events.EnterOnce { once_control;  tf = true }) man in
+        let proc = tf_proc var edge prev_node None init_routine [] getl sidel getg sideg d' in
+        if not (S.D.is_bot proc) then
+          let rec proc_man =
+            { man with
+              ask = (fun (type a) (q: a Queries.t) -> S.query proc_man q);
+              local = proc;
+            }
+          in
+          S.event proc_man (Events.LeaveOnce { once_control }) proc_man
+        else
+          S.D.bot ()
+      in
+      let not_enter =
+        (* Always possible, will never yield `Bot *)
+        let d' = S.event man (Events.EnterOnce { once_control;  tf = false }) man in
+        let rec d'_man =
+          { man with
+            ask = (fun (type a) (q: a Queries.t) -> S.query d'_man q);
+            local = d';
+          }
+        in
+        S.event d'_man (Events.LeaveOnce { once_control }) d'_man
+      in
+      D.join enter not_enter
+    in
     let one_function f =
       match f.vtype with
       | TFun (_, params, var_arg, _)  ->
@@ -266,14 +294,21 @@ struct
         (* Check whether number of arguments fits. *)
         (* If params is None, the function or its parameters are not declared, so we still analyze the unknown function call. *)
         if Option.is_none params || p_length = arg_length || (var_arg && arg_length >= p_length) then
-          begin Some (match Cilfacade.find_varinfo_fundec f with
-              | fd when LibraryFunctions.use_special f.vname ->
-                M.info ~category:Analyzer "Using special for defined function %s" f.vname;
-                tf_special_call man lv f args
-              | fd ->
-                tf_normal_call man lv e fd args getl sidel getg sideg
-              | exception Not_found ->
-                tf_special_call man lv f args)
+          begin
+            let is_once = LibraryFunctions.find ~nowarn:true f in
+            match is_once.special args with
+            | Once { once_control; init_routine } ->
+              Some (once once_control init_routine)
+            | _
+            | exception LibraryDsl.Expected _-> (* propagate weirdness inside *)
+              Some (match Cilfacade.find_varinfo_fundec f with
+                  | fd when LibraryFunctions.use_special f.vname ->
+                    M.info ~category:Analyzer "Using special for defined function %s" f.vname;
+                    tf_special_call man lv f args
+                  | fd ->
+                    tf_normal_call man lv e fd args getl sidel getg sideg
+                  | exception Not_found ->
+                    tf_special_call man lv f args)
           end
         else begin
           let geq = if var_arg then ">=" else "" in
diff --git a/src/goblint_lib.ml b/src/goblint_lib.ml
index 415fb21605..96e816b32c 100644
--- a/src/goblint_lib.ml
+++ b/src/goblint_lib.ml
@@ -129,7 +129,9 @@ module BasePriv = BasePriv
 module RelationPriv = RelationPriv
 module ThreadEscape = ThreadEscape
 module PthreadSignals = PthreadSignals
+module PthreadBarriers = PthreadBarriers
 module ExtractPthread = ExtractPthread
+module PthreadOnce = PthreadOnce
 
 (** {2 Longjmp}
 
diff --git a/src/maingoblint.ml b/src/maingoblint.ml
index cb81ea0b86..c3f1d0f9ea 100644
--- a/src/maingoblint.ml
+++ b/src/maingoblint.ml
@@ -418,9 +418,6 @@ let preprocess_files () =
   if List.mem "c" (get_string_list "lib.activated") then
     extra_files := find_custom_include (Fpath.v "stdlib.c") :: !extra_files;
 
-  if List.mem "pthread" (get_string_list "lib.activated") then
-    extra_files := find_custom_include (Fpath.v "pthread.c") :: !extra_files;
-
   if List.mem "sv-comp" (get_string_list "lib.activated") then
     extra_files := find_custom_include (Fpath.v "sv-comp.c") :: !extra_files;
 
diff --git a/src/util/library/libraryDesc.ml b/src/util/library/libraryDesc.ml
index 6f34de1864..862205aad1 100644
--- a/src/util/library/libraryDesc.ml
+++ b/src/util/library/libraryDesc.ml
@@ -69,6 +69,8 @@ type special =
   | SemDestroy of Cil.exp
   | Wait of { cond: Cil.exp; mutex: Cil.exp; }
   | TimedWait of { cond: Cil.exp; mutex: Cil.exp; abstime: Cil.exp; (** Unused *) }
+  | BarrierWait of Cil.exp
+  | BarrierInit of { barrier: Cil.exp; attr:Cil.exp; count: Cil.exp; }
   | Math of { fun_args: math; }
   | Memset of { dest: Cil.exp; ch: Cil.exp; count: Cil.exp; }
   | Bzero of { dest: Cil.exp; count: Cil.exp; }
@@ -84,6 +86,7 @@ type special =
   | Longjmp of { env: Cil.exp; value: Cil.exp; }
   | Bounded of { exp: Cil.exp}  (** Used to check for bounds for termination analysis. *)
   | Rand
+  | Once of { once_control: Cil.exp; init_routine: Cil.exp; }
   | Unknown (** Anything not belonging to other types. *) (* TODO: rename to Other? *)
 
 
diff --git a/src/util/library/libraryDsl.ml b/src/util/library/libraryDsl.ml
index a380714dc0..240c318579 100644
--- a/src/util/library/libraryDsl.ml
+++ b/src/util/library/libraryDsl.ml
@@ -30,6 +30,8 @@ struct
     | [] -> fail "^::"
 end
 
+exception Expected = Pattern.Expected
+
 type access =
   | Access of LibraryDesc.Access.t
   | If of (unit -> bool) * access
diff --git a/src/util/library/libraryDsl.mli b/src/util/library/libraryDsl.mli
index 42c300af8e..2eed55666d 100644
--- a/src/util/library/libraryDsl.mli
+++ b/src/util/library/libraryDsl.mli
@@ -82,3 +82,5 @@ val c_deep: access
 
 (** Conditional access, e.g. on an option. *)
 val if_: (unit -> bool) -> access -> access
+
+exception Expected of string
diff --git a/src/util/library/libraryFunctions.ml b/src/util/library/libraryFunctions.ml
index 6643b58eef..326637654e 100644
--- a/src/util/library/libraryFunctions.ml
+++ b/src/util/library/libraryFunctions.ml
@@ -464,6 +464,7 @@ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("pthread_create", special [__ "thread" [w]; drop "attr" [r]; __ "start_routine" [s]; __ "arg" []] @@ fun thread start_routine arg -> ThreadCreate { thread; start_routine; arg; multiple = false }); (* For precision purposes arg is not considered accessed here. Instead all accesses (if any) come from actually analyzing start_routine. *)
     ("pthread_exit", special [__ "retval" []] @@ fun retval -> ThreadExit { ret_val = retval }); (* Doesn't dereference the void* itself, but just passes to pthread_join. *)
     ("pthread_join", special [__ "thread" []; __ "retval" [w]] @@ fun thread retval -> ThreadJoin {thread; ret_var = retval});
+    ("pthread_once", special [__ "once_control" []; __ "init_routine" []] @@ fun once_control init_routine -> Once {once_control; init_routine});
     ("pthread_kill", unknown [drop "thread" []; drop "sig" []]);
     ("pthread_equal", unknown [drop "t1" []; drop "t2" []]);
     ("pthread_cond_init", unknown [drop "cond" [w]; drop "attr" [r]]);
@@ -520,6 +521,8 @@ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("pthread_getspecific", unknown ~attrs:[InvalidateGlobals] [drop "key" []]);
     ("pthread_key_create", unknown [drop "key" [w]; drop "destructor" [s]]);
     ("pthread_key_delete", unknown [drop "key" [f]]);
+    ("pthread_barrier_init", special [__ "barrier" []; __ "attr" []; __ "count" []] @@ fun barrier attr count -> BarrierInit {barrier; attr; count});
+    ("pthread_barrier_wait", special [__ "barrier" []] @@ fun barrier -> BarrierWait barrier);
     ("pthread_cancel", unknown [drop "thread" []]);
     ("pthread_testcancel", unknown []);
     ("pthread_setcancelstate", unknown [drop "state" []; drop "oldstate" [w]]);
@@ -1298,7 +1301,7 @@ let is_safe_uncalled fn_name =
   List.exists (fun r -> Str.string_match r fn_name 0) kernel_safe_uncalled_regex
 
 
-let unknown_desc f : LibraryDesc.t =
+let unknown_desc f ~nowarn : LibraryDesc.t =
   let accs args : (LibraryDesc.Access.t * 'a list) list = [
     ({ kind = Read; deep = true; }, if GobConfig.get_bool "sem.unknown_function.read.args" then args else []);
     ({ kind = Write; deep = true; }, if GobConfig.get_bool "sem.unknown_function.invalidate.args" then args else []);
@@ -1314,7 +1317,7 @@ let unknown_desc f : LibraryDesc.t =
       []
   in
   (* TODO: remove hack when all classify are migrated *)
-  if not (CilType.Varinfo.equal f dummyFunDec.svar) && not (use_special f.vname) then (
+  if not nowarn && not (CilType.Varinfo.equal f dummyFunDec.svar) && not (use_special f.vname) then (
     M.msg_final Error ~category:Imprecise ~tags:[Category Unsound] "Function definition missing";
     M.error ~category:Imprecise ~tags:[Category Unsound] "Function definition missing for %s" f.vname
   );
@@ -1324,12 +1327,11 @@ let unknown_desc f : LibraryDesc.t =
     special = fun _ -> Unknown;
   }
 
-let find f =
+let find ?(nowarn=false) f =
   let name = f.vname in
   match Hashtbl.find_option (ResettableLazy.force activated_library_descs) name with
   | Some desc -> desc
-  | None -> unknown_desc f
-
+  | None -> unknown_desc ~nowarn f
 
 let is_special fv =
   if use_special fv.vname then
diff --git a/src/util/library/libraryFunctions.mli b/src/util/library/libraryFunctions.mli
index 9a8e55a48a..7eb9c531fe 100644
--- a/src/util/library/libraryFunctions.mli
+++ b/src/util/library/libraryFunctions.mli
@@ -11,7 +11,7 @@ val use_special : string -> bool
 val is_safe_uncalled : string -> bool
 
 (** Find library function descriptor for {e special} function (as per {!is_special}). *)
-val find: Cil.varinfo -> LibraryDesc.t
+val find: ?nowarn:bool -> Cil.varinfo -> LibraryDesc.t
 
 val is_special: Cil.varinfo -> bool
 (** Check if function is treated specially. *)
diff --git a/tests/regression/03-practical/35-base-mutex-macos.t b/tests/regression/03-practical/35-base-mutex-macos.t
index 1d8a184d4c..929d03eb5b 100644
--- a/tests/regression/03-practical/35-base-mutex-macos.t
+++ b/tests/regression/03-practical/35-base-mutex-macos.t
@@ -1,4 +1,4 @@
-  $ goblint --enable witness.yaml.enabled --disable witness.invariant.accessed --set pre.cppflags[+] -DGOBLINT_NO_PTHREAD_ONCE 35-base-mutex-macos.c
+  $ goblint --enable witness.yaml.enabled --disable witness.invariant.accessed 35-base-mutex-macos.c
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 2
     dead: 0
diff --git a/tests/regression/04-mutex/01-simple_rc.t b/tests/regression/04-mutex/01-simple_rc.t
index bd0bc0e161..f7b1131840 100644
--- a/tests/regression/04-mutex/01-simple_rc.t
+++ b/tests/regression/04-mutex/01-simple_rc.t
@@ -1,9 +1,9 @@
   $ goblint --enable warn.deterministic 01-simple_rc.c 2>&1 | tee default-output.txt
   [Warning][Race] Memory location myglobal (race with conf. 110): (01-simple_rc.c:4:5-4:13)
-    write with [lock:{mutex1}, thread:[main, t_fun@01-simple_rc.c:17:3-17:40]] (conf. 110)  (exp: & myglobal) (01-simple_rc.c:10:3-10:22)
-    write with [mhp:{created={[main, t_fun@01-simple_rc.c:17:3-17:40]}}, lock:{mutex2}, thread:[main]] (conf. 110)  (exp: & myglobal) (01-simple_rc.c:19:3-19:22)
-    read with [lock:{mutex1}, thread:[main, t_fun@01-simple_rc.c:17:3-17:40]] (conf. 110)  (exp: & myglobal) (01-simple_rc.c:10:3-10:22)
-    read with [mhp:{created={[main, t_fun@01-simple_rc.c:17:3-17:40]}}, lock:{mutex2}, thread:[main]] (conf. 110)  (exp: & myglobal) (01-simple_rc.c:19:3-19:22)
+    write with [lock:{mutex1}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@01-simple_rc.c:17:3-17:40]] (conf. 110)  (exp: & myglobal) (01-simple_rc.c:10:3-10:22)
+    write with [mhp:{created={[main, t_fun@01-simple_rc.c:17:3-17:40]}}, lock:{mutex2}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & myglobal) (01-simple_rc.c:19:3-19:22)
+    read with [lock:{mutex1}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@01-simple_rc.c:17:3-17:40]] (conf. 110)  (exp: & myglobal) (01-simple_rc.c:10:3-10:22)
+    read with [mhp:{created={[main, t_fun@01-simple_rc.c:17:3-17:40]}}, lock:{mutex2}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & myglobal) (01-simple_rc.c:19:3-19:22)
   [Info][Race] Memory locations race summary:
     safe: 0
     vulnerable: 0
@@ -18,13 +18,13 @@
 
   $ diff default-output.txt full-output.txt
   2,5c2,5
-  <   write with [lock:{mutex1}, thread:[main, t_fun@01-simple_rc.c:17:3-17:40]] (conf. 110)  (exp: & myglobal) (01-simple_rc.c:10:3-10:22)
-  <   write with [mhp:{created={[main, t_fun@01-simple_rc.c:17:3-17:40]}}, lock:{mutex2}, thread:[main]] (conf. 110)  (exp: & myglobal) (01-simple_rc.c:19:3-19:22)
-  <   read with [lock:{mutex1}, thread:[main, t_fun@01-simple_rc.c:17:3-17:40]] (conf. 110)  (exp: & myglobal) (01-simple_rc.c:10:3-10:22)
-  <   read with [mhp:{created={[main, t_fun@01-simple_rc.c:17:3-17:40]}}, lock:{mutex2}, thread:[main]] (conf. 110)  (exp: & myglobal) (01-simple_rc.c:19:3-19:22)
+  <   write with [lock:{mutex1}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@01-simple_rc.c:17:3-17:40]] (conf. 110)  (exp: & myglobal) (01-simple_rc.c:10:3-10:22)
+  <   write with [mhp:{created={[main, t_fun@01-simple_rc.c:17:3-17:40]}}, lock:{mutex2}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & myglobal) (01-simple_rc.c:19:3-19:22)
+  <   read with [lock:{mutex1}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@01-simple_rc.c:17:3-17:40]] (conf. 110)  (exp: & myglobal) (01-simple_rc.c:10:3-10:22)
+  <   read with [mhp:{created={[main, t_fun@01-simple_rc.c:17:3-17:40]}}, lock:{mutex2}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & myglobal) (01-simple_rc.c:19:3-19:22)
   ---
-  >   write with [mhp:{tid=[main, t_fun@01-simple_rc.c:17:3-17:40#⊤]}, lock:{mutex1}, thread:[main, t_fun@01-simple_rc.c:17:3-17:40#⊤]] (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#⊤]}}, 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#⊤]}, lock:{mutex1}, thread:[main, t_fun@01-simple_rc.c:17:3-17:40#⊤]] (conf. 110)  (exp: & myglobal) (01-simple_rc.c:10:3-10:22)
-  >   read with [mhp:{tid=[main]; created={[main, t_fun@01-simple_rc.c:17:3-17:40#⊤]}}, lock:{mutex2}, thread:[main]] (conf. 110)  (exp: & myglobal) (01-simple_rc.c:19:3-19:22)
+  >   write with [mhp:{tid=[main, t_fun@01-simple_rc.c:17:3-17:40#⊤]}, lock:{mutex1}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@01-simple_rc.c:17:3-17:40#⊤]] (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#⊤]}}, lock:{mutex2}, threadflag:(MT mode:Multithreaded (main), bool:true), 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#⊤]}, lock:{mutex1}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@01-simple_rc.c:17:3-17:40#⊤]] (conf. 110)  (exp: & myglobal) (01-simple_rc.c:10:3-10:22)
+  >   read with [mhp:{tid=[main]; created={[main, t_fun@01-simple_rc.c:17:3-17:40#⊤]}}, lock:{mutex2}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & myglobal) (01-simple_rc.c:19:3-19:22)
   [1]
diff --git a/tests/regression/04-mutex/49-type-invariants.t b/tests/regression/04-mutex/49-type-invariants.t
index d757519b29..cd12bbd170 100644
--- a/tests/regression/04-mutex/49-type-invariants.t
+++ b/tests/regression/04-mutex/49-type-invariants.t
@@ -1,15 +1,15 @@
   $ goblint --enable warn.deterministic --enable ana.race.direct-arithmetic --enable allglobs 49-type-invariants.c 2>&1 | tee default-output-1.txt
   [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (49-type-invariants.c:21:3-21:21)
   [Warning][Race] Memory location s.field (race with conf. 110): (49-type-invariants.c:8:10-8:11)
-    write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40]}}, thread:[main]] (conf. 100)  (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
-    read with thread:[main, t_fun@49-type-invariants.c:20:3-20:40] (conf. 110)  (exp: & s.field) (49-type-invariants.c:11:3-11:23)
+    write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100)  (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
+    read with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@49-type-invariants.c:20:3-20:40]] (conf. 110)  (exp: & s.field) (49-type-invariants.c:11:3-11:23)
   [Info][Race] Memory locations race summary:
     safe: 1
     vulnerable: 0
     unsafe: 1
     total memory locations: 2
   [Success][Race] Memory location (struct S).field (safe):
-    write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40]}}, thread:[main]] (conf. 100)  (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
+    write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100)  (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 7
     dead: 0
@@ -24,15 +24,15 @@
   $ goblint --enable warn.deterministic --disable ana.race.direct-arithmetic --enable allglobs 49-type-invariants.c 2>&1 | tee default-output-2.txt
   [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (49-type-invariants.c:21:3-21:21)
   [Warning][Race] Memory location s.field (race with conf. 110): (49-type-invariants.c:8:10-8:11)
-    write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40]}}, thread:[main]] (conf. 100)  (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
-    read with thread:[main, t_fun@49-type-invariants.c:20:3-20:40] (conf. 110)  (exp: & s.field) (49-type-invariants.c:11:3-11:23)
+    write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100)  (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
+    read with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@49-type-invariants.c:20:3-20:40]] (conf. 110)  (exp: & s.field) (49-type-invariants.c:11:3-11:23)
   [Info][Race] Memory locations race summary:
     safe: 1
     vulnerable: 0
     unsafe: 1
     total memory locations: 2
   [Success][Race] Memory location (struct S).field (safe):
-    write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40]}}, thread:[main]] (conf. 100)  (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
+    write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100)  (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 7
     dead: 0
@@ -48,28 +48,28 @@
 
   $ diff default-output-1.txt full-output-1.txt
   3,4c3,4
-  <   write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40]}}, thread:[main]] (conf. 100)  (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
-  <   read with thread:[main, t_fun@49-type-invariants.c:20:3-20:40] (conf. 110)  (exp: & s.field) (49-type-invariants.c:11:3-11:23)
+  <   write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100)  (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
+  <   read with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@49-type-invariants.c:20:3-20:40]] (conf. 110)  (exp: & s.field) (49-type-invariants.c:11:3-11:23)
   ---
-  >   write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:20:3-20:40#⊤]}}, thread:[main]] (conf. 100)  (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
-  >   read with [mhp:{tid=[main, t_fun@49-type-invariants.c:20:3-20:40#⊤]}, thread:[main, t_fun@49-type-invariants.c:20:3-20:40#⊤]] (conf. 110)  (exp: & s.field) (49-type-invariants.c:11:3-11:23)
+  >   write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:20:3-20:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100)  (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
+  >   read with [mhp:{tid=[main, t_fun@49-type-invariants.c:20:3-20:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@49-type-invariants.c:20:3-20:40#⊤]] (conf. 110)  (exp: & s.field) (49-type-invariants.c:11:3-11:23)
   11c11
-  <   write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40]}}, thread:[main]] (conf. 100)  (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
+  <   write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100)  (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
   ---
-  >   write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:20:3-20:40#⊤]}}, thread:[main]] (conf. 100)  (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
+  >   write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:20:3-20:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100)  (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
   [1]
 
   $ goblint --enable warn.deterministic --disable ana.race.direct-arithmetic --enable allglobs --enable dbg.full-output 49-type-invariants.c > full-output-2.txt 2>&1
 
   $ diff default-output-2.txt full-output-2.txt
   3,4c3,4
-  <   write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40]}}, thread:[main]] (conf. 100)  (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
-  <   read with thread:[main, t_fun@49-type-invariants.c:20:3-20:40] (conf. 110)  (exp: & s.field) (49-type-invariants.c:11:3-11:23)
+  <   write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100)  (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
+  <   read with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@49-type-invariants.c:20:3-20:40]] (conf. 110)  (exp: & s.field) (49-type-invariants.c:11:3-11:23)
   ---
-  >   write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:20:3-20:40#⊤]}}, thread:[main]] (conf. 100)  (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
-  >   read with [mhp:{tid=[main, t_fun@49-type-invariants.c:20:3-20:40#⊤]}, thread:[main, t_fun@49-type-invariants.c:20:3-20:40#⊤]] (conf. 110)  (exp: & s.field) (49-type-invariants.c:11:3-11:23)
+  >   write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:20:3-20:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100)  (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
+  >   read with [mhp:{tid=[main, t_fun@49-type-invariants.c:20:3-20:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@49-type-invariants.c:20:3-20:40#⊤]] (conf. 110)  (exp: & s.field) (49-type-invariants.c:11:3-11:23)
   11c11
-  <   write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40]}}, thread:[main]] (conf. 100)  (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
+  <   write with [mhp:{created={[main, t_fun@49-type-invariants.c:20:3-20:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100)  (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
   ---
-  >   write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:20:3-20:40#⊤]}}, thread:[main]] (conf. 100)  (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
+  >   write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:20:3-20:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100)  (exp: & tmp->field) (49-type-invariants.c:21:3-21:21)
   [1]
diff --git a/tests/regression/04-mutex/77-type-nested-fields.t b/tests/regression/04-mutex/77-type-nested-fields.t
index 15559cefec..7041b8e19c 100644
--- a/tests/regression/04-mutex/77-type-nested-fields.t
+++ b/tests/regression/04-mutex/77-type-nested-fields.t
@@ -2,15 +2,15 @@
   [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (77-type-nested-fields.c:31:3-31:20)
   [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (77-type-nested-fields.c:38:3-38:22)
   [Warning][Race] Memory location (struct T).s.field (race with conf. 100):
-    write with thread:[main, t_fun@77-type-nested-fields.c:37:3-37:40] (conf. 100)  (exp: & tmp->field) (77-type-nested-fields.c:31:3-31:20)
-    write with [mhp:{created={[main, t_fun@77-type-nested-fields.c:37:3-37:40]}}, thread:[main]] (conf. 100)  (exp: & tmp->s.field) (77-type-nested-fields.c:38:3-38:22)
+    write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@77-type-nested-fields.c:37:3-37:40]] (conf. 100)  (exp: & tmp->field) (77-type-nested-fields.c:31:3-31:20)
+    write with [mhp:{created={[main, t_fun@77-type-nested-fields.c:37:3-37:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100)  (exp: & tmp->s.field) (77-type-nested-fields.c:38:3-38:22)
   [Info][Race] Memory locations race summary:
     safe: 1
     vulnerable: 0
     unsafe: 1
     total memory locations: 2
   [Success][Race] Memory location (struct S).field (safe):
-    write with thread:[main, t_fun@77-type-nested-fields.c:37:3-37:40] (conf. 100)  (exp: & tmp->field) (77-type-nested-fields.c:31:3-31:20)
+    write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@77-type-nested-fields.c:37:3-37:40]] (conf. 100)  (exp: & tmp->field) (77-type-nested-fields.c:31:3-31:20)
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 7
     dead: 0
@@ -29,13 +29,13 @@
 
   $ diff default-output.txt full-output.txt
   4,5c4,5
-  <   write with thread:[main, t_fun@77-type-nested-fields.c:37:3-37:40] (conf. 100)  (exp: & tmp->field) (77-type-nested-fields.c:31:3-31:20)
-  <   write with [mhp:{created={[main, t_fun@77-type-nested-fields.c:37:3-37:40]}}, thread:[main]] (conf. 100)  (exp: & tmp->s.field) (77-type-nested-fields.c:38:3-38:22)
+  <   write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@77-type-nested-fields.c:37:3-37:40]] (conf. 100)  (exp: & tmp->field) (77-type-nested-fields.c:31:3-31:20)
+  <   write with [mhp:{created={[main, t_fun@77-type-nested-fields.c:37:3-37:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100)  (exp: & tmp->s.field) (77-type-nested-fields.c:38:3-38:22)
   ---
-  >   write with [mhp:{tid=[main, t_fun@77-type-nested-fields.c:37:3-37:40#⊤]}, thread:[main, t_fun@77-type-nested-fields.c:37:3-37:40#⊤]] (conf. 100)  (exp: & tmp->field) (77-type-nested-fields.c:31:3-31:20)
-  >   write with [mhp:{tid=[main]; created={[main, t_fun@77-type-nested-fields.c:37:3-37:40#⊤]}}, thread:[main]] (conf. 100)  (exp: & tmp->s.field) (77-type-nested-fields.c:38:3-38:22)
+  >   write with [mhp:{tid=[main, t_fun@77-type-nested-fields.c:37:3-37:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@77-type-nested-fields.c:37:3-37:40#⊤]] (conf. 100)  (exp: & tmp->field) (77-type-nested-fields.c:31:3-31:20)
+  >   write with [mhp:{tid=[main]; created={[main, t_fun@77-type-nested-fields.c:37:3-37:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100)  (exp: & tmp->s.field) (77-type-nested-fields.c:38:3-38:22)
   12c12
-  <   write with thread:[main, t_fun@77-type-nested-fields.c:37:3-37:40] (conf. 100)  (exp: & tmp->field) (77-type-nested-fields.c:31:3-31:20)
+  <   write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@77-type-nested-fields.c:37:3-37:40]] (conf. 100)  (exp: & tmp->field) (77-type-nested-fields.c:31:3-31:20)
   ---
-  >   write with [mhp:{tid=[main, t_fun@77-type-nested-fields.c:37:3-37:40#⊤]}, thread:[main, t_fun@77-type-nested-fields.c:37:3-37:40#⊤]] (conf. 100)  (exp: & tmp->field) (77-type-nested-fields.c:31:3-31:20)
+  >   write with [mhp:{tid=[main, t_fun@77-type-nested-fields.c:37:3-37:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@77-type-nested-fields.c:37:3-37:40#⊤]] (conf. 100)  (exp: & tmp->field) (77-type-nested-fields.c:31:3-31:20)
   [1]
diff --git a/tests/regression/04-mutex/79-type-nested-fields-deep1.t b/tests/regression/04-mutex/79-type-nested-fields-deep1.t
index 680200aecd..857fa3aaf1 100644
--- a/tests/regression/04-mutex/79-type-nested-fields-deep1.t
+++ b/tests/regression/04-mutex/79-type-nested-fields-deep1.t
@@ -2,15 +2,15 @@
   [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (79-type-nested-fields-deep1.c:36:3-36:20)
   [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (79-type-nested-fields-deep1.c:43:3-43:24)
   [Warning][Race] Memory location (struct U).t.s.field (race with conf. 100):
-    write with thread:[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40] (conf. 100)  (exp: & tmp->field) (79-type-nested-fields-deep1.c:36:3-36:20)
-    write with [mhp:{created={[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40]}}, thread:[main]] (conf. 100)  (exp: & tmp->t.s.field) (79-type-nested-fields-deep1.c:43:3-43:24)
+    write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40]] (conf. 100)  (exp: & tmp->field) (79-type-nested-fields-deep1.c:36:3-36:20)
+    write with [mhp:{created={[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100)  (exp: & tmp->t.s.field) (79-type-nested-fields-deep1.c:43:3-43:24)
   [Info][Race] Memory locations race summary:
     safe: 1
     vulnerable: 0
     unsafe: 1
     total memory locations: 2
   [Success][Race] Memory location (struct S).field (safe):
-    write with thread:[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40] (conf. 100)  (exp: & tmp->field) (79-type-nested-fields-deep1.c:36:3-36:20)
+    write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40]] (conf. 100)  (exp: & tmp->field) (79-type-nested-fields-deep1.c:36:3-36:20)
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 7
     dead: 0
@@ -29,13 +29,13 @@
 
   $ diff default-output.txt full-output.txt
   4,5c4,5
-  <   write with thread:[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40] (conf. 100)  (exp: & tmp->field) (79-type-nested-fields-deep1.c:36:3-36:20)
-  <   write with [mhp:{created={[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40]}}, thread:[main]] (conf. 100)  (exp: & tmp->t.s.field) (79-type-nested-fields-deep1.c:43:3-43:24)
+  <   write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40]] (conf. 100)  (exp: & tmp->field) (79-type-nested-fields-deep1.c:36:3-36:20)
+  <   write with [mhp:{created={[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100)  (exp: & tmp->t.s.field) (79-type-nested-fields-deep1.c:43:3-43:24)
   ---
-  >   write with [mhp:{tid=[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40#⊤]}, thread:[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40#⊤]] (conf. 100)  (exp: & tmp->field) (79-type-nested-fields-deep1.c:36:3-36:20)
-  >   write with [mhp:{tid=[main]; created={[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40#⊤]}}, thread:[main]] (conf. 100)  (exp: & tmp->t.s.field) (79-type-nested-fields-deep1.c:43:3-43:24)
+  >   write with [mhp:{tid=[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40#⊤]] (conf. 100)  (exp: & tmp->field) (79-type-nested-fields-deep1.c:36:3-36:20)
+  >   write with [mhp:{tid=[main]; created={[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100)  (exp: & tmp->t.s.field) (79-type-nested-fields-deep1.c:43:3-43:24)
   12c12
-  <   write with thread:[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40] (conf. 100)  (exp: & tmp->field) (79-type-nested-fields-deep1.c:36:3-36:20)
+  <   write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40]] (conf. 100)  (exp: & tmp->field) (79-type-nested-fields-deep1.c:36:3-36:20)
   ---
-  >   write with [mhp:{tid=[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40#⊤]}, thread:[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40#⊤]] (conf. 100)  (exp: & tmp->field) (79-type-nested-fields-deep1.c:36:3-36:20)
+  >   write with [mhp:{tid=[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40#⊤]] (conf. 100)  (exp: & tmp->field) (79-type-nested-fields-deep1.c:36:3-36:20)
   [1]
diff --git a/tests/regression/04-mutex/80-type-nested-fields-deep2.t b/tests/regression/04-mutex/80-type-nested-fields-deep2.t
index 4a2811ccbd..dd4d6e90a8 100644
--- a/tests/regression/04-mutex/80-type-nested-fields-deep2.t
+++ b/tests/regression/04-mutex/80-type-nested-fields-deep2.t
@@ -2,15 +2,15 @@
   [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (80-type-nested-fields-deep2.c:36:3-36:22)
   [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (80-type-nested-fields-deep2.c:43:3-43:24)
   [Warning][Race] Memory location (struct U).t.s.field (race with conf. 100):
-    write with thread:[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40] (conf. 100)  (exp: & tmp->s.field) (80-type-nested-fields-deep2.c:36:3-36:22)
-    write with [mhp:{created={[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40]}}, thread:[main]] (conf. 100)  (exp: & tmp->t.s.field) (80-type-nested-fields-deep2.c:43:3-43:24)
+    write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40]] (conf. 100)  (exp: & tmp->s.field) (80-type-nested-fields-deep2.c:36:3-36:22)
+    write with [mhp:{created={[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100)  (exp: & tmp->t.s.field) (80-type-nested-fields-deep2.c:43:3-43:24)
   [Info][Race] Memory locations race summary:
     safe: 1
     vulnerable: 0
     unsafe: 1
     total memory locations: 2
   [Success][Race] Memory location (struct T).s.field (safe):
-    write with thread:[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40] (conf. 100)  (exp: & tmp->s.field) (80-type-nested-fields-deep2.c:36:3-36:22)
+    write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40]] (conf. 100)  (exp: & tmp->s.field) (80-type-nested-fields-deep2.c:36:3-36:22)
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 7
     dead: 0
@@ -29,13 +29,13 @@
 
   $ diff default-output.txt full-output.txt
   4,5c4,5
-  <   write with thread:[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40] (conf. 100)  (exp: & tmp->s.field) (80-type-nested-fields-deep2.c:36:3-36:22)
-  <   write with [mhp:{created={[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40]}}, thread:[main]] (conf. 100)  (exp: & tmp->t.s.field) (80-type-nested-fields-deep2.c:43:3-43:24)
+  <   write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40]] (conf. 100)  (exp: & tmp->s.field) (80-type-nested-fields-deep2.c:36:3-36:22)
+  <   write with [mhp:{created={[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100)  (exp: & tmp->t.s.field) (80-type-nested-fields-deep2.c:43:3-43:24)
   ---
-  >   write with [mhp:{tid=[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40#⊤]}, thread:[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40#⊤]] (conf. 100)  (exp: & tmp->s.field) (80-type-nested-fields-deep2.c:36:3-36:22)
-  >   write with [mhp:{tid=[main]; created={[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40#⊤]}}, thread:[main]] (conf. 100)  (exp: & tmp->t.s.field) (80-type-nested-fields-deep2.c:43:3-43:24)
+  >   write with [mhp:{tid=[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40#⊤]] (conf. 100)  (exp: & tmp->s.field) (80-type-nested-fields-deep2.c:36:3-36:22)
+  >   write with [mhp:{tid=[main]; created={[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100)  (exp: & tmp->t.s.field) (80-type-nested-fields-deep2.c:43:3-43:24)
   12c12
-  <   write with thread:[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40] (conf. 100)  (exp: & tmp->s.field) (80-type-nested-fields-deep2.c:36:3-36:22)
+  <   write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40]] (conf. 100)  (exp: & tmp->s.field) (80-type-nested-fields-deep2.c:36:3-36:22)
   ---
-  >   write with [mhp:{tid=[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40#⊤]}, thread:[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40#⊤]] (conf. 100)  (exp: & tmp->s.field) (80-type-nested-fields-deep2.c:36:3-36:22)
+  >   write with [mhp:{tid=[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40#⊤]] (conf. 100)  (exp: & tmp->s.field) (80-type-nested-fields-deep2.c:36:3-36:22)
   [1]
diff --git a/tests/regression/04-mutex/84-distribute-fields-1.t b/tests/regression/04-mutex/84-distribute-fields-1.t
index 0fd55dcb53..cf30127d7d 100644
--- a/tests/regression/04-mutex/84-distribute-fields-1.t
+++ b/tests/regression/04-mutex/84-distribute-fields-1.t
@@ -1,14 +1,14 @@
   $ goblint --enable warn.deterministic --enable allglobs 84-distribute-fields-1.c 2>&1 | tee default-output.txt
   [Warning][Race] Memory location s.data (race with conf. 110): (84-distribute-fields-1.c:9:10-9:11)
-    write with thread:[main, t_fun@84-distribute-fields-1.c:18:3-18:40] (conf. 110)  (exp: & s.data) (84-distribute-fields-1.c:12:3-12:13)
-    write with [mhp:{created={[main, t_fun@84-distribute-fields-1.c:18:3-18:40]}}, thread:[main]] (conf. 110)  (exp: & s) (84-distribute-fields-1.c:20:3-20:9)
+    write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@84-distribute-fields-1.c:18:3-18:40]] (conf. 110)  (exp: & s.data) (84-distribute-fields-1.c:12:3-12:13)
+    write with [mhp:{created={[main, t_fun@84-distribute-fields-1.c:18:3-18:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & s) (84-distribute-fields-1.c:20:3-20:9)
   [Info][Race] Memory locations race summary:
     safe: 1
     vulnerable: 0
     unsafe: 1
     total memory locations: 2
   [Success][Race] Memory location s (safe): (84-distribute-fields-1.c:9:10-9:11)
-    write with [mhp:{created={[main, t_fun@84-distribute-fields-1.c:18:3-18:40]}}, thread:[main]] (conf. 110)  (exp: & s) (84-distribute-fields-1.c:20:3-20:9)
+    write with [mhp:{created={[main, t_fun@84-distribute-fields-1.c:18:3-18:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), 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
     dead: 0
@@ -18,13 +18,13 @@
 
   $ diff default-output.txt full-output.txt
   2,3c2,3
-  <   write with thread:[main, t_fun@84-distribute-fields-1.c:18:3-18:40] (conf. 110)  (exp: & s.data) (84-distribute-fields-1.c:12:3-12:13)
-  <   write with [mhp:{created={[main, t_fun@84-distribute-fields-1.c:18:3-18:40]}}, thread:[main]] (conf. 110)  (exp: & s) (84-distribute-fields-1.c:20:3-20:9)
+  <   write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@84-distribute-fields-1.c:18:3-18:40]] (conf. 110)  (exp: & s.data) (84-distribute-fields-1.c:12:3-12:13)
+  <   write with [mhp:{created={[main, t_fun@84-distribute-fields-1.c:18:3-18:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & s) (84-distribute-fields-1.c:20:3-20:9)
   ---
-  >   write with [mhp:{tid=[main, t_fun@84-distribute-fields-1.c:18:3-18:40#⊤]}, thread:[main, t_fun@84-distribute-fields-1.c:18:3-18:40#⊤]] (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#⊤]}}, thread:[main]] (conf. 110)  (exp: & s) (84-distribute-fields-1.c:20:3-20:9)
+  >   write with [mhp:{tid=[main, t_fun@84-distribute-fields-1.c:18:3-18:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@84-distribute-fields-1.c:18:3-18:40#⊤]] (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#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & s) (84-distribute-fields-1.c:20:3-20:9)
   10c10
-  <   write with [mhp:{created={[main, t_fun@84-distribute-fields-1.c:18:3-18:40]}}, thread:[main]] (conf. 110)  (exp: & s) (84-distribute-fields-1.c:20:3-20:9)
+  <   write with [mhp:{created={[main, t_fun@84-distribute-fields-1.c:18:3-18:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & s) (84-distribute-fields-1.c:20:3-20:9)
   ---
-  >   write with [mhp:{tid=[main]; created={[main, t_fun@84-distribute-fields-1.c:18:3-18:40#⊤]}}, thread:[main]] (conf. 110)  (exp: & s) (84-distribute-fields-1.c:20:3-20:9)
+  >   write with [mhp:{tid=[main]; created={[main, t_fun@84-distribute-fields-1.c:18:3-18:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & s) (84-distribute-fields-1.c:20:3-20:9)
   [1]
diff --git a/tests/regression/04-mutex/85-distribute-fields-2.t b/tests/regression/04-mutex/85-distribute-fields-2.t
index 7f8fb7c942..76ba6c759c 100644
--- a/tests/regression/04-mutex/85-distribute-fields-2.t
+++ b/tests/regression/04-mutex/85-distribute-fields-2.t
@@ -1,14 +1,14 @@
   $ goblint --enable warn.deterministic --enable allglobs 85-distribute-fields-2.c 2>&1 | tee default-output.txt
   [Warning][Race] Memory location t.s.data (race with conf. 110): (85-distribute-fields-2.c:15:10-15:11)
-    write with thread:[main, t_fun@85-distribute-fields-2.c:24:3-24:40] (conf. 110)  (exp: & t.s.data) (85-distribute-fields-2.c:18:3-18:15)
-    write with [mhp:{created={[main, t_fun@85-distribute-fields-2.c:24:3-24:40]}}, thread:[main]] (conf. 110)  (exp: & t.s) (85-distribute-fields-2.c:26:3-26:11)
+    write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@85-distribute-fields-2.c:24:3-24:40]] (conf. 110)  (exp: & t.s.data) (85-distribute-fields-2.c:18:3-18:15)
+    write with [mhp:{created={[main, t_fun@85-distribute-fields-2.c:24:3-24:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & t.s) (85-distribute-fields-2.c:26:3-26:11)
   [Info][Race] Memory locations race summary:
     safe: 1
     vulnerable: 0
     unsafe: 1
     total memory locations: 2
   [Success][Race] Memory location t.s (safe): (85-distribute-fields-2.c:15:10-15:11)
-    write with [mhp:{created={[main, t_fun@85-distribute-fields-2.c:24:3-24:40]}}, thread:[main]] (conf. 110)  (exp: & t.s) (85-distribute-fields-2.c:26:3-26:11)
+    write with [mhp:{created={[main, t_fun@85-distribute-fields-2.c:24:3-24:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), 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
     dead: 0
@@ -18,13 +18,13 @@
 
   $ diff default-output.txt full-output.txt
   2,3c2,3
-  <   write with thread:[main, t_fun@85-distribute-fields-2.c:24:3-24:40] (conf. 110)  (exp: & t.s.data) (85-distribute-fields-2.c:18:3-18:15)
-  <   write with [mhp:{created={[main, t_fun@85-distribute-fields-2.c:24:3-24:40]}}, thread:[main]] (conf. 110)  (exp: & t.s) (85-distribute-fields-2.c:26:3-26:11)
+  <   write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@85-distribute-fields-2.c:24:3-24:40]] (conf. 110)  (exp: & t.s.data) (85-distribute-fields-2.c:18:3-18:15)
+  <   write with [mhp:{created={[main, t_fun@85-distribute-fields-2.c:24:3-24:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & t.s) (85-distribute-fields-2.c:26:3-26:11)
   ---
-  >   write with [mhp:{tid=[main, t_fun@85-distribute-fields-2.c:24:3-24:40#⊤]}, thread:[main, t_fun@85-distribute-fields-2.c:24:3-24:40#⊤]] (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#⊤]}}, thread:[main]] (conf. 110)  (exp: & t.s) (85-distribute-fields-2.c:26:3-26:11)
+  >   write with [mhp:{tid=[main, t_fun@85-distribute-fields-2.c:24:3-24:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@85-distribute-fields-2.c:24:3-24:40#⊤]] (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#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & t.s) (85-distribute-fields-2.c:26:3-26:11)
   10c10
-  <   write with [mhp:{created={[main, t_fun@85-distribute-fields-2.c:24:3-24:40]}}, thread:[main]] (conf. 110)  (exp: & t.s) (85-distribute-fields-2.c:26:3-26:11)
+  <   write with [mhp:{created={[main, t_fun@85-distribute-fields-2.c:24:3-24:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & t.s) (85-distribute-fields-2.c:26:3-26:11)
   ---
-  >   write with [mhp:{tid=[main]; created={[main, t_fun@85-distribute-fields-2.c:24:3-24:40#⊤]}}, thread:[main]] (conf. 110)  (exp: & t.s) (85-distribute-fields-2.c:26:3-26:11)
+  >   write with [mhp:{tid=[main]; created={[main, t_fun@85-distribute-fields-2.c:24:3-24:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & t.s) (85-distribute-fields-2.c:26:3-26:11)
   [1]
diff --git a/tests/regression/04-mutex/86-distribute-fields-3.t b/tests/regression/04-mutex/86-distribute-fields-3.t
index c5ebd6d28a..6819a98396 100644
--- a/tests/regression/04-mutex/86-distribute-fields-3.t
+++ b/tests/regression/04-mutex/86-distribute-fields-3.t
@@ -1,14 +1,14 @@
   $ goblint --enable warn.deterministic --enable allglobs 86-distribute-fields-3.c 2>&1 | tee default-output.txt
   [Warning][Race] Memory location t.s.data (race with conf. 110): (86-distribute-fields-3.c:15:10-15:11)
-    write with thread:[main, t_fun@86-distribute-fields-3.c:24:3-24:40] (conf. 110)  (exp: & t.s.data) (86-distribute-fields-3.c:18:3-18:15)
-    write with [mhp:{created={[main, t_fun@86-distribute-fields-3.c:24:3-24:40]}}, thread:[main]] (conf. 110)  (exp: & t) (86-distribute-fields-3.c:26:3-26:9)
+    write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@86-distribute-fields-3.c:24:3-24:40]] (conf. 110)  (exp: & t.s.data) (86-distribute-fields-3.c:18:3-18:15)
+    write with [mhp:{created={[main, t_fun@86-distribute-fields-3.c:24:3-24:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & t) (86-distribute-fields-3.c:26:3-26:9)
   [Info][Race] Memory locations race summary:
     safe: 1
     vulnerable: 0
     unsafe: 1
     total memory locations: 2
   [Success][Race] Memory location t (safe): (86-distribute-fields-3.c:15:10-15:11)
-    write with [mhp:{created={[main, t_fun@86-distribute-fields-3.c:24:3-24:40]}}, thread:[main]] (conf. 110)  (exp: & t) (86-distribute-fields-3.c:26:3-26:9)
+    write with [mhp:{created={[main, t_fun@86-distribute-fields-3.c:24:3-24:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), 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
     dead: 0
@@ -18,13 +18,13 @@
 
   $ diff default-output.txt full-output.txt
   2,3c2,3
-  <   write with thread:[main, t_fun@86-distribute-fields-3.c:24:3-24:40] (conf. 110)  (exp: & t.s.data) (86-distribute-fields-3.c:18:3-18:15)
-  <   write with [mhp:{created={[main, t_fun@86-distribute-fields-3.c:24:3-24:40]}}, thread:[main]] (conf. 110)  (exp: & t) (86-distribute-fields-3.c:26:3-26:9)
+  <   write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@86-distribute-fields-3.c:24:3-24:40]] (conf. 110)  (exp: & t.s.data) (86-distribute-fields-3.c:18:3-18:15)
+  <   write with [mhp:{created={[main, t_fun@86-distribute-fields-3.c:24:3-24:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & t) (86-distribute-fields-3.c:26:3-26:9)
   ---
-  >   write with [mhp:{tid=[main, t_fun@86-distribute-fields-3.c:24:3-24:40#⊤]}, thread:[main, t_fun@86-distribute-fields-3.c:24:3-24:40#⊤]] (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#⊤]}}, thread:[main]] (conf. 110)  (exp: & t) (86-distribute-fields-3.c:26:3-26:9)
+  >   write with [mhp:{tid=[main, t_fun@86-distribute-fields-3.c:24:3-24:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@86-distribute-fields-3.c:24:3-24:40#⊤]] (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#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & t) (86-distribute-fields-3.c:26:3-26:9)
   10c10
-  <   write with [mhp:{created={[main, t_fun@86-distribute-fields-3.c:24:3-24:40]}}, thread:[main]] (conf. 110)  (exp: & t) (86-distribute-fields-3.c:26:3-26:9)
+  <   write with [mhp:{created={[main, t_fun@86-distribute-fields-3.c:24:3-24:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & t) (86-distribute-fields-3.c:26:3-26:9)
   ---
-  >   write with [mhp:{tid=[main]; created={[main, t_fun@86-distribute-fields-3.c:24:3-24:40#⊤]}}, thread:[main]] (conf. 110)  (exp: & t) (86-distribute-fields-3.c:26:3-26:9)
+  >   write with [mhp:{tid=[main]; created={[main, t_fun@86-distribute-fields-3.c:24:3-24:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & t) (86-distribute-fields-3.c:26:3-26:9)
   [1]
diff --git a/tests/regression/04-mutex/87-distribute-fields-4.t b/tests/regression/04-mutex/87-distribute-fields-4.t
index 2d3dfb6b7c..713bc79679 100644
--- a/tests/regression/04-mutex/87-distribute-fields-4.t
+++ b/tests/regression/04-mutex/87-distribute-fields-4.t
@@ -1,7 +1,7 @@
   $ goblint --enable warn.deterministic --enable allglobs 87-distribute-fields-4.c 2>&1 | tee default-output.txt
   [Warning][Race] Memory location s (race with conf. 110): (87-distribute-fields-4.c:9:10-9:11)
-    write with thread:[main, t_fun@87-distribute-fields-4.c:19:3-19:40] (conf. 110)  (exp: & s) (87-distribute-fields-4.c:13:3-13:9)
-    write with [mhp:{created={[main, t_fun@87-distribute-fields-4.c:19:3-19:40]}}, thread:[main]] (conf. 110)  (exp: & s) (87-distribute-fields-4.c:21:3-21:9)
+    write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@87-distribute-fields-4.c:19:3-19:40]] (conf. 110)  (exp: & s) (87-distribute-fields-4.c:13:3-13:9)
+    write with [mhp:{created={[main, t_fun@87-distribute-fields-4.c:19:3-19:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & s) (87-distribute-fields-4.c:21:3-21:9)
   [Info][Race] Memory locations race summary:
     safe: 0
     vulnerable: 0
@@ -16,9 +16,9 @@
 
   $ diff default-output.txt full-output.txt
   2,3c2,3
-  <   write with thread:[main, t_fun@87-distribute-fields-4.c:19:3-19:40] (conf. 110)  (exp: & s) (87-distribute-fields-4.c:13:3-13:9)
-  <   write with [mhp:{created={[main, t_fun@87-distribute-fields-4.c:19:3-19:40]}}, thread:[main]] (conf. 110)  (exp: & s) (87-distribute-fields-4.c:21:3-21:9)
+  <   write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@87-distribute-fields-4.c:19:3-19:40]] (conf. 110)  (exp: & s) (87-distribute-fields-4.c:13:3-13:9)
+  <   write with [mhp:{created={[main, t_fun@87-distribute-fields-4.c:19:3-19:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & s) (87-distribute-fields-4.c:21:3-21:9)
   ---
-  >   write with [mhp:{tid=[main, t_fun@87-distribute-fields-4.c:19:3-19:40#⊤]}, thread:[main, t_fun@87-distribute-fields-4.c:19:3-19:40#⊤]] (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#⊤]}}, thread:[main]] (conf. 110)  (exp: & s) (87-distribute-fields-4.c:21:3-21:9)
+  >   write with [mhp:{tid=[main, t_fun@87-distribute-fields-4.c:19:3-19:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@87-distribute-fields-4.c:19:3-19:40#⊤]] (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#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & s) (87-distribute-fields-4.c:21:3-21:9)
   [1]
diff --git a/tests/regression/04-mutex/88-distribute-fields-5.t b/tests/regression/04-mutex/88-distribute-fields-5.t
index 0afdc729ef..eba8db4d5a 100644
--- a/tests/regression/04-mutex/88-distribute-fields-5.t
+++ b/tests/regression/04-mutex/88-distribute-fields-5.t
@@ -1,7 +1,7 @@
   $ goblint --enable warn.deterministic --enable allglobs 88-distribute-fields-5.c 2>&1 | tee default-output.txt
   [Warning][Race] Memory location t.s (race with conf. 110): (88-distribute-fields-5.c:15:10-15:11)
-    write with thread:[main, t_fun@88-distribute-fields-5.c:25:3-25:40] (conf. 110)  (exp: & t.s) (88-distribute-fields-5.c:19:3-19:11)
-    write with [mhp:{created={[main, t_fun@88-distribute-fields-5.c:25:3-25:40]}}, thread:[main]] (conf. 110)  (exp: & t.s) (88-distribute-fields-5.c:27:3-27:11)
+    write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@88-distribute-fields-5.c:25:3-25:40]] (conf. 110)  (exp: & t.s) (88-distribute-fields-5.c:19:3-19:11)
+    write with [mhp:{created={[main, t_fun@88-distribute-fields-5.c:25:3-25:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & t.s) (88-distribute-fields-5.c:27:3-27:11)
   [Info][Race] Memory locations race summary:
     safe: 0
     vulnerable: 0
@@ -16,9 +16,9 @@
 
   $ diff default-output.txt full-output.txt
   2,3c2,3
-  <   write with thread:[main, t_fun@88-distribute-fields-5.c:25:3-25:40] (conf. 110)  (exp: & t.s) (88-distribute-fields-5.c:19:3-19:11)
-  <   write with [mhp:{created={[main, t_fun@88-distribute-fields-5.c:25:3-25:40]}}, thread:[main]] (conf. 110)  (exp: & t.s) (88-distribute-fields-5.c:27:3-27:11)
+  <   write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@88-distribute-fields-5.c:25:3-25:40]] (conf. 110)  (exp: & t.s) (88-distribute-fields-5.c:19:3-19:11)
+  <   write with [mhp:{created={[main, t_fun@88-distribute-fields-5.c:25:3-25:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & t.s) (88-distribute-fields-5.c:27:3-27:11)
   ---
-  >   write with [mhp:{tid=[main, t_fun@88-distribute-fields-5.c:25:3-25:40#⊤]}, thread:[main, t_fun@88-distribute-fields-5.c:25:3-25:40#⊤]] (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#⊤]}}, thread:[main]] (conf. 110)  (exp: & t.s) (88-distribute-fields-5.c:27:3-27:11)
+  >   write with [mhp:{tid=[main, t_fun@88-distribute-fields-5.c:25:3-25:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@88-distribute-fields-5.c:25:3-25:40#⊤]] (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#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & t.s) (88-distribute-fields-5.c:27:3-27:11)
   [1]
diff --git a/tests/regression/04-mutex/89-distribute-fields-6.t b/tests/regression/04-mutex/89-distribute-fields-6.t
index 20533099de..0bad7aba3f 100644
--- a/tests/regression/04-mutex/89-distribute-fields-6.t
+++ b/tests/regression/04-mutex/89-distribute-fields-6.t
@@ -1,7 +1,7 @@
   $ goblint --enable warn.deterministic --enable allglobs 89-distribute-fields-6.c 2>&1 | tee default-output.txt
   [Warning][Race] Memory location t (race with conf. 110): (89-distribute-fields-6.c:15:10-15:11)
-    write with thread:[main, t_fun@89-distribute-fields-6.c:25:3-25:40] (conf. 110)  (exp: & t) (89-distribute-fields-6.c:19:3-19:9)
-    write with [mhp:{created={[main, t_fun@89-distribute-fields-6.c:25:3-25:40]}}, thread:[main]] (conf. 110)  (exp: & t) (89-distribute-fields-6.c:27:3-27:9)
+    write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@89-distribute-fields-6.c:25:3-25:40]] (conf. 110)  (exp: & t) (89-distribute-fields-6.c:19:3-19:9)
+    write with [mhp:{created={[main, t_fun@89-distribute-fields-6.c:25:3-25:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & t) (89-distribute-fields-6.c:27:3-27:9)
   [Info][Race] Memory locations race summary:
     safe: 0
     vulnerable: 0
@@ -16,9 +16,9 @@
 
   $ diff default-output.txt full-output.txt
   2,3c2,3
-  <   write with thread:[main, t_fun@89-distribute-fields-6.c:25:3-25:40] (conf. 110)  (exp: & t) (89-distribute-fields-6.c:19:3-19:9)
-  <   write with [mhp:{created={[main, t_fun@89-distribute-fields-6.c:25:3-25:40]}}, thread:[main]] (conf. 110)  (exp: & t) (89-distribute-fields-6.c:27:3-27:9)
+  <   write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@89-distribute-fields-6.c:25:3-25:40]] (conf. 110)  (exp: & t) (89-distribute-fields-6.c:19:3-19:9)
+  <   write with [mhp:{created={[main, t_fun@89-distribute-fields-6.c:25:3-25:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & t) (89-distribute-fields-6.c:27:3-27:9)
   ---
-  >   write with [mhp:{tid=[main, t_fun@89-distribute-fields-6.c:25:3-25:40#⊤]}, thread:[main, t_fun@89-distribute-fields-6.c:25:3-25:40#⊤]] (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#⊤]}}, thread:[main]] (conf. 110)  (exp: & t) (89-distribute-fields-6.c:27:3-27:9)
+  >   write with [mhp:{tid=[main, t_fun@89-distribute-fields-6.c:25:3-25:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@89-distribute-fields-6.c:25:3-25:40#⊤]] (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#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & t) (89-distribute-fields-6.c:27:3-27:9)
   [1]
diff --git a/tests/regression/04-mutex/90-distribute-fields-type-1.t b/tests/regression/04-mutex/90-distribute-fields-type-1.t
index 1a5c739e9c..cc40a3cf4c 100644
--- a/tests/regression/04-mutex/90-distribute-fields-type-1.t
+++ b/tests/regression/04-mutex/90-distribute-fields-type-1.t
@@ -2,17 +2,17 @@
   [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (90-distribute-fields-type-1.c:31:3-31:20)
   [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (90-distribute-fields-type-1.c:39:3-39:17)
   [Warning][Race] Memory location (struct T).s.field (race with conf. 100):
-    write with thread:[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40] (conf. 100)  (exp: & tmp->field) (90-distribute-fields-type-1.c:31:3-31:20)
-    write with [mhp:{created={[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40]}}, thread:[main]] (conf. 100)  (exp: & tmp->s) (90-distribute-fields-type-1.c:39:3-39:17)
+    write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40]] (conf. 100)  (exp: & tmp->field) (90-distribute-fields-type-1.c:31:3-31:20)
+    write with [mhp:{created={[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100)  (exp: & tmp->s) (90-distribute-fields-type-1.c:39:3-39:17)
   [Info][Race] Memory locations race summary:
     safe: 2
     vulnerable: 0
     unsafe: 1
     total memory locations: 3
   [Success][Race] Memory location (struct S).field (safe):
-    write with thread:[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40] (conf. 100)  (exp: & tmp->field) (90-distribute-fields-type-1.c:31:3-31:20)
+    write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40]] (conf. 100)  (exp: & tmp->field) (90-distribute-fields-type-1.c:31:3-31:20)
   [Success][Race] Memory location (struct T).s (safe):
-    write with [mhp:{created={[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40]}}, thread:[main]] (conf. 100)  (exp: & tmp->s) (90-distribute-fields-type-1.c:39:3-39:17)
+    write with [mhp:{created={[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100)  (exp: & tmp->s) (90-distribute-fields-type-1.c:39:3-39:17)
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 7
     dead: 0
@@ -31,17 +31,17 @@
 
   $ diff default-output.txt full-output.txt
   4,5c4,5
-  <   write with thread:[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40] (conf. 100)  (exp: & tmp->field) (90-distribute-fields-type-1.c:31:3-31:20)
-  <   write with [mhp:{created={[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40]}}, thread:[main]] (conf. 100)  (exp: & tmp->s) (90-distribute-fields-type-1.c:39:3-39:17)
+  <   write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40]] (conf. 100)  (exp: & tmp->field) (90-distribute-fields-type-1.c:31:3-31:20)
+  <   write with [mhp:{created={[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100)  (exp: & tmp->s) (90-distribute-fields-type-1.c:39:3-39:17)
   ---
-  >   write with [mhp:{tid=[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#⊤]}, thread:[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#⊤]] (conf. 100)  (exp: & tmp->field) (90-distribute-fields-type-1.c:31:3-31:20)
-  >   write with [mhp:{tid=[main]; created={[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#⊤]}}, thread:[main]] (conf. 100)  (exp: & tmp->s) (90-distribute-fields-type-1.c:39:3-39:17)
+  >   write with [mhp:{tid=[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#⊤]] (conf. 100)  (exp: & tmp->field) (90-distribute-fields-type-1.c:31:3-31:20)
+  >   write with [mhp:{tid=[main]; created={[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100)  (exp: & tmp->s) (90-distribute-fields-type-1.c:39:3-39:17)
   12c12
-  <   write with thread:[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40] (conf. 100)  (exp: & tmp->field) (90-distribute-fields-type-1.c:31:3-31:20)
+  <   write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40]] (conf. 100)  (exp: & tmp->field) (90-distribute-fields-type-1.c:31:3-31:20)
   ---
-  >   write with [mhp:{tid=[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#⊤]}, thread:[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#⊤]] (conf. 100)  (exp: & tmp->field) (90-distribute-fields-type-1.c:31:3-31:20)
+  >   write with [mhp:{tid=[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#⊤]] (conf. 100)  (exp: & tmp->field) (90-distribute-fields-type-1.c:31:3-31:20)
   14c14
-  <   write with [mhp:{created={[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40]}}, thread:[main]] (conf. 100)  (exp: & tmp->s) (90-distribute-fields-type-1.c:39:3-39:17)
+  <   write with [mhp:{created={[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100)  (exp: & tmp->s) (90-distribute-fields-type-1.c:39:3-39:17)
   ---
-  >   write with [mhp:{tid=[main]; created={[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#⊤]}}, thread:[main]] (conf. 100)  (exp: & tmp->s) (90-distribute-fields-type-1.c:39:3-39:17)
+  >   write with [mhp:{tid=[main]; created={[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100)  (exp: & tmp->s) (90-distribute-fields-type-1.c:39:3-39:17)
   [1]
diff --git a/tests/regression/04-mutex/91-distribute-fields-type-2.t b/tests/regression/04-mutex/91-distribute-fields-type-2.t
index e22b21d2bd..e3a861adc0 100644
--- a/tests/regression/04-mutex/91-distribute-fields-type-2.t
+++ b/tests/regression/04-mutex/91-distribute-fields-type-2.t
@@ -2,17 +2,17 @@
   [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (91-distribute-fields-type-2.c:32:3-32:17)
   [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (91-distribute-fields-type-2.c:40:3-40:17)
   [Warning][Race] Memory location (struct T).s (race with conf. 100):
-    write with thread:[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40] (conf. 100)  (exp: & *tmp) (91-distribute-fields-type-2.c:32:3-32:17)
-    write with [mhp:{created={[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40]}}, thread:[main]] (conf. 100)  (exp: & *tmp) (91-distribute-fields-type-2.c:40:3-40:17)
+    write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40]] (conf. 100)  (exp: & *tmp) (91-distribute-fields-type-2.c:32:3-32:17)
+    write with [mhp:{created={[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100)  (exp: & *tmp) (91-distribute-fields-type-2.c:40:3-40:17)
   [Info][Race] Memory locations race summary:
     safe: 2
     vulnerable: 0
     unsafe: 1
     total memory locations: 3
   [Success][Race] Memory location (struct S) (safe):
-    write with thread:[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40] (conf. 100)  (exp: & *tmp) (91-distribute-fields-type-2.c:32:3-32:17)
+    write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40]] (conf. 100)  (exp: & *tmp) (91-distribute-fields-type-2.c:32:3-32:17)
   [Success][Race] Memory location (struct T) (safe):
-    write with [mhp:{created={[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40]}}, thread:[main]] (conf. 100)  (exp: & *tmp) (91-distribute-fields-type-2.c:40:3-40:17)
+    write with [mhp:{created={[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100)  (exp: & *tmp) (91-distribute-fields-type-2.c:40:3-40:17)
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 7
     dead: 0
@@ -31,17 +31,17 @@
 
   $ diff default-output.txt full-output.txt
   4,5c4,5
-  <   write with thread:[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40] (conf. 100)  (exp: & *tmp) (91-distribute-fields-type-2.c:32:3-32:17)
-  <   write with [mhp:{created={[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40]}}, thread:[main]] (conf. 100)  (exp: & *tmp) (91-distribute-fields-type-2.c:40:3-40:17)
+  <   write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40]] (conf. 100)  (exp: & *tmp) (91-distribute-fields-type-2.c:32:3-32:17)
+  <   write with [mhp:{created={[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100)  (exp: & *tmp) (91-distribute-fields-type-2.c:40:3-40:17)
   ---
-  >   write with [mhp:{tid=[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#⊤]}, thread:[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#⊤]] (conf. 100)  (exp: & *tmp) (91-distribute-fields-type-2.c:32:3-32:17)
-  >   write with [mhp:{tid=[main]; created={[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#⊤]}}, thread:[main]] (conf. 100)  (exp: & *tmp) (91-distribute-fields-type-2.c:40:3-40:17)
+  >   write with [mhp:{tid=[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#⊤]] (conf. 100)  (exp: & *tmp) (91-distribute-fields-type-2.c:32:3-32:17)
+  >   write with [mhp:{tid=[main]; created={[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100)  (exp: & *tmp) (91-distribute-fields-type-2.c:40:3-40:17)
   12c12
-  <   write with thread:[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40] (conf. 100)  (exp: & *tmp) (91-distribute-fields-type-2.c:32:3-32:17)
+  <   write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40]] (conf. 100)  (exp: & *tmp) (91-distribute-fields-type-2.c:32:3-32:17)
   ---
-  >   write with [mhp:{tid=[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#⊤]}, thread:[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#⊤]] (conf. 100)  (exp: & *tmp) (91-distribute-fields-type-2.c:32:3-32:17)
+  >   write with [mhp:{tid=[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#⊤]] (conf. 100)  (exp: & *tmp) (91-distribute-fields-type-2.c:32:3-32:17)
   14c14
-  <   write with [mhp:{created={[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40]}}, thread:[main]] (conf. 100)  (exp: & *tmp) (91-distribute-fields-type-2.c:40:3-40:17)
+  <   write with [mhp:{created={[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100)  (exp: & *tmp) (91-distribute-fields-type-2.c:40:3-40:17)
   ---
-  >   write with [mhp:{tid=[main]; created={[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#⊤]}}, thread:[main]] (conf. 100)  (exp: & *tmp) (91-distribute-fields-type-2.c:40:3-40:17)
+  >   write with [mhp:{tid=[main]; created={[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100)  (exp: & *tmp) (91-distribute-fields-type-2.c:40:3-40:17)
   [1]
diff --git a/tests/regression/04-mutex/92-distribute-fields-type-deep.t b/tests/regression/04-mutex/92-distribute-fields-type-deep.t
index d754ded21b..a0663678dd 100644
--- a/tests/regression/04-mutex/92-distribute-fields-type-deep.t
+++ b/tests/regression/04-mutex/92-distribute-fields-type-deep.t
@@ -2,17 +2,17 @@
   [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (92-distribute-fields-type-deep.c:36:3-36:20)
   [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (92-distribute-fields-type-deep.c:44:3-44:17)
   [Warning][Race] Memory location (struct U).t.s.field (race with conf. 100):
-    write with thread:[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40] (conf. 100)  (exp: & tmp->field) (92-distribute-fields-type-deep.c:36:3-36:20)
-    write with [mhp:{created={[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40]}}, thread:[main]] (conf. 100)  (exp: & tmp->t) (92-distribute-fields-type-deep.c:44:3-44:17)
+    write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40]] (conf. 100)  (exp: & tmp->field) (92-distribute-fields-type-deep.c:36:3-36:20)
+    write with [mhp:{created={[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100)  (exp: & tmp->t) (92-distribute-fields-type-deep.c:44:3-44:17)
   [Info][Race] Memory locations race summary:
     safe: 2
     vulnerable: 0
     unsafe: 1
     total memory locations: 3
   [Success][Race] Memory location (struct S).field (safe):
-    write with thread:[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40] (conf. 100)  (exp: & tmp->field) (92-distribute-fields-type-deep.c:36:3-36:20)
+    write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40]] (conf. 100)  (exp: & tmp->field) (92-distribute-fields-type-deep.c:36:3-36:20)
   [Success][Race] Memory location (struct U).t (safe):
-    write with [mhp:{created={[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40]}}, thread:[main]] (conf. 100)  (exp: & tmp->t) (92-distribute-fields-type-deep.c:44:3-44:17)
+    write with [mhp:{created={[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100)  (exp: & tmp->t) (92-distribute-fields-type-deep.c:44:3-44:17)
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 7
     dead: 0
@@ -31,17 +31,17 @@
 
   $ diff default-output.txt full-output.txt
   4,5c4,5
-  <   write with thread:[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40] (conf. 100)  (exp: & tmp->field) (92-distribute-fields-type-deep.c:36:3-36:20)
-  <   write with [mhp:{created={[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40]}}, thread:[main]] (conf. 100)  (exp: & tmp->t) (92-distribute-fields-type-deep.c:44:3-44:17)
+  <   write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40]] (conf. 100)  (exp: & tmp->field) (92-distribute-fields-type-deep.c:36:3-36:20)
+  <   write with [mhp:{created={[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100)  (exp: & tmp->t) (92-distribute-fields-type-deep.c:44:3-44:17)
   ---
-  >   write with [mhp:{tid=[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#⊤]}, thread:[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#⊤]] (conf. 100)  (exp: & tmp->field) (92-distribute-fields-type-deep.c:36:3-36:20)
-  >   write with [mhp:{tid=[main]; created={[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#⊤]}}, thread:[main]] (conf. 100)  (exp: & tmp->t) (92-distribute-fields-type-deep.c:44:3-44:17)
+  >   write with [mhp:{tid=[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#⊤]] (conf. 100)  (exp: & tmp->field) (92-distribute-fields-type-deep.c:36:3-36:20)
+  >   write with [mhp:{tid=[main]; created={[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100)  (exp: & tmp->t) (92-distribute-fields-type-deep.c:44:3-44:17)
   12c12
-  <   write with thread:[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40] (conf. 100)  (exp: & tmp->field) (92-distribute-fields-type-deep.c:36:3-36:20)
+  <   write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40]] (conf. 100)  (exp: & tmp->field) (92-distribute-fields-type-deep.c:36:3-36:20)
   ---
-  >   write with [mhp:{tid=[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#⊤]}, thread:[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#⊤]] (conf. 100)  (exp: & tmp->field) (92-distribute-fields-type-deep.c:36:3-36:20)
+  >   write with [mhp:{tid=[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#⊤]] (conf. 100)  (exp: & tmp->field) (92-distribute-fields-type-deep.c:36:3-36:20)
   14c14
-  <   write with [mhp:{created={[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40]}}, thread:[main]] (conf. 100)  (exp: & tmp->t) (92-distribute-fields-type-deep.c:44:3-44:17)
+  <   write with [mhp:{created={[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100)  (exp: & tmp->t) (92-distribute-fields-type-deep.c:44:3-44:17)
   ---
-  >   write with [mhp:{tid=[main]; created={[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#⊤]}}, thread:[main]] (conf. 100)  (exp: & tmp->t) (92-distribute-fields-type-deep.c:44:3-44:17)
+  >   write with [mhp:{tid=[main]; created={[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100)  (exp: & tmp->t) (92-distribute-fields-type-deep.c:44:3-44:17)
   [1]
diff --git a/tests/regression/04-mutex/93-distribute-fields-type-global.t b/tests/regression/04-mutex/93-distribute-fields-type-global.t
index 7e0dc61a3c..c5ca112278 100644
--- a/tests/regression/04-mutex/93-distribute-fields-type-global.t
+++ b/tests/regression/04-mutex/93-distribute-fields-type-global.t
@@ -1,17 +1,17 @@
   $ goblint --enable warn.deterministic --enable allglobs 93-distribute-fields-type-global.c 2>&1 | tee default-output.txt
   [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (93-distribute-fields-type-global.c:13:3-13:29)
   [Warning][Race] Memory location s.field (race with conf. 110): (93-distribute-fields-type-global.c:8:10-8:11)
-    read with thread:[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40] (conf. 100)  (exp: & tmp->field) (93-distribute-fields-type-global.c:13:3-13:29)
-    write with [mhp:{created={[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40]}}, thread:[main]] (conf. 110)  (exp: & s) (93-distribute-fields-type-global.c:22:3-22:9)
+    read with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40]] (conf. 100)  (exp: & tmp->field) (93-distribute-fields-type-global.c:13:3-13:29)
+    write with [mhp:{created={[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & s) (93-distribute-fields-type-global.c:22:3-22:9)
   [Info][Race] Memory locations race summary:
     safe: 2
     vulnerable: 0
     unsafe: 1
     total memory locations: 3
   [Success][Race] Memory location (struct S).field (safe):
-    read with thread:[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40] (conf. 100)  (exp: & tmp->field) (93-distribute-fields-type-global.c:13:3-13:29)
+    read with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40]] (conf. 100)  (exp: & tmp->field) (93-distribute-fields-type-global.c:13:3-13:29)
   [Success][Race] Memory location s (safe): (93-distribute-fields-type-global.c:8:10-8:11)
-    write with [mhp:{created={[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40]}}, thread:[main]] (conf. 110)  (exp: & s) (93-distribute-fields-type-global.c:22:3-22:9)
+    write with [mhp:{created={[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & s) (93-distribute-fields-type-global.c:22:3-22:9)
   [Info][Deadcode] Logical lines of code (LLoC) summary:
     live: 7
     dead: 0
@@ -27,17 +27,17 @@
 
   $ diff default-output.txt full-output.txt
   3,4c3,4
-  <   read with thread:[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40] (conf. 100)  (exp: & tmp->field) (93-distribute-fields-type-global.c:13:3-13:29)
-  <   write with [mhp:{created={[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40]}}, thread:[main]] (conf. 110)  (exp: & s) (93-distribute-fields-type-global.c:22:3-22:9)
+  <   read with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40]] (conf. 100)  (exp: & tmp->field) (93-distribute-fields-type-global.c:13:3-13:29)
+  <   write with [mhp:{created={[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & s) (93-distribute-fields-type-global.c:22:3-22:9)
   ---
-  >   read with [mhp:{tid=[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#⊤]}, thread:[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#⊤]] (conf. 100)  (exp: & tmp->field) (93-distribute-fields-type-global.c:13:3-13:29)
-  >   write with [mhp:{tid=[main]; created={[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#⊤]}}, thread:[main]] (conf. 110)  (exp: & s) (93-distribute-fields-type-global.c:22:3-22:9)
+  >   read with [mhp:{tid=[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#⊤]] (conf. 100)  (exp: & tmp->field) (93-distribute-fields-type-global.c:13:3-13:29)
+  >   write with [mhp:{tid=[main]; created={[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & s) (93-distribute-fields-type-global.c:22:3-22:9)
   11c11
-  <   read with thread:[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40] (conf. 100)  (exp: & tmp->field) (93-distribute-fields-type-global.c:13:3-13:29)
+  <   read with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40]] (conf. 100)  (exp: & tmp->field) (93-distribute-fields-type-global.c:13:3-13:29)
   ---
-  >   read with [mhp:{tid=[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#⊤]}, thread:[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#⊤]] (conf. 100)  (exp: & tmp->field) (93-distribute-fields-type-global.c:13:3-13:29)
+  >   read with [mhp:{tid=[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#⊤]] (conf. 100)  (exp: & tmp->field) (93-distribute-fields-type-global.c:13:3-13:29)
   13c13
-  <   write with [mhp:{created={[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40]}}, thread:[main]] (conf. 110)  (exp: & s) (93-distribute-fields-type-global.c:22:3-22:9)
+  <   write with [mhp:{created={[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & s) (93-distribute-fields-type-global.c:22:3-22:9)
   ---
-  >   write with [mhp:{tid=[main]; created={[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#⊤]}}, thread:[main]] (conf. 110)  (exp: & s) (93-distribute-fields-type-global.c:22:3-22:9)
+  >   write with [mhp:{tid=[main]; created={[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & s) (93-distribute-fields-type-global.c:22:3-22:9)
   [1]
diff --git a/tests/regression/06-symbeq/14-list_entry_rc.t b/tests/regression/06-symbeq/14-list_entry_rc.t
index 0e5ec3ce9f..a94e910a9d 100644
--- a/tests/regression/06-symbeq/14-list_entry_rc.t
+++ b/tests/regression/06-symbeq/14-list_entry_rc.t
@@ -6,15 +6,15 @@
     dead: 0
     total lines: 23
   [Warning][Race] Memory location (alloc@sid:$SID@tid:[main])[?].datum (race with conf. 110): (14-list_entry_rc.c:41:3-41:35)
-    write with thread:[main, t_fun@14-list_entry_rc.c:45:3-45:40] (conf. 110)  (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13)
-    write with [mhp:{created={[main, t_fun@14-list_entry_rc.c:45:3-45:40]}}, thread:[main]] (conf. 110)  (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13)
-    read with thread:[main, t_fun@14-list_entry_rc.c:45:3-45:40] (conf. 110)  (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13)
-    read with [mhp:{created={[main, t_fun@14-list_entry_rc.c:45:3-45:40]}}, thread:[main]] (conf. 110)  (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13)
+    write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@14-list_entry_rc.c:45:3-45:40]] (conf. 110)  (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13)
+    write with [mhp:{created={[main, t_fun@14-list_entry_rc.c:45:3-45:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13)
+    read with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@14-list_entry_rc.c:45:3-45:40]] (conf. 110)  (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13)
+    read with [mhp:{created={[main, t_fun@14-list_entry_rc.c:45:3-45:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13)
   [Info][Race] Memory locations race summary:
-    safe: 1
+    safe: 2
     vulnerable: 0
     unsafe: 1
-    total memory locations: 2
+    total memory locations: 3
 
   $ goblint --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --enable dbg.full-output 14-list_entry_rc.c 2>&1 | sed -r 's/sid:[0-9]+/sid:$SID/' > full-output.txt
 
@@ -25,14 +25,14 @@
   > [Warning][Unknown] unlocking mutex ((alloc@sid:$SID@tid:[main](#top))[def_exc:1].mutex) which may not be held (14-list_entry_rc.c:28:3-28:34)
   7,11c7,11
   < [Warning][Race] Memory location (alloc@sid:$SID@tid:[main])[?].datum (race with conf. 110): (14-list_entry_rc.c:41:3-41:35)
-  <   write with thread:[main, t_fun@14-list_entry_rc.c:45:3-45:40] (conf. 110)  (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13)
-  <   write with [mhp:{created={[main, t_fun@14-list_entry_rc.c:45:3-45:40]}}, thread:[main]] (conf. 110)  (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13)
-  <   read with thread:[main, t_fun@14-list_entry_rc.c:45:3-45:40] (conf. 110)  (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13)
-  <   read with [mhp:{created={[main, t_fun@14-list_entry_rc.c:45:3-45:40]}}, thread:[main]] (conf. 110)  (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13)
+  <   write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@14-list_entry_rc.c:45:3-45:40]] (conf. 110)  (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13)
+  <   write with [mhp:{created={[main, t_fun@14-list_entry_rc.c:45:3-45:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13)
+  <   read with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@14-list_entry_rc.c:45:3-45:40]] (conf. 110)  (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13)
+  <   read with [mhp:{created={[main, t_fun@14-list_entry_rc.c:45:3-45:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13)
   ---
   > [Warning][Race] Memory location (alloc@sid:$SID@tid:[main](#top))[?].datum (race with conf. 110): (14-list_entry_rc.c:41:3-41:35)
-  >   write with [mhp:{tid=[main, t_fun@14-list_entry_rc.c:45:3-45:40#⊤]}, thread:[main, t_fun@14-list_entry_rc.c:45:3-45:40#⊤]] (conf. 110)  (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13)
-  >   write with [mhp:{tid=[main]; created={[main, t_fun@14-list_entry_rc.c:45:3-45:40#⊤]}}, thread:[main]] (conf. 110)  (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13)
-  >   read with [mhp:{tid=[main, t_fun@14-list_entry_rc.c:45:3-45:40#⊤]}, thread:[main, t_fun@14-list_entry_rc.c:45:3-45:40#⊤]] (conf. 110)  (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13)
-  >   read with [mhp:{tid=[main]; created={[main, t_fun@14-list_entry_rc.c:45:3-45:40#⊤]}}, thread:[main]] (conf. 110)  (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13)
+  >   write with [mhp:{tid=[main, t_fun@14-list_entry_rc.c:45:3-45:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@14-list_entry_rc.c:45:3-45:40#⊤]] (conf. 110)  (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13)
+  >   write with [mhp:{tid=[main]; created={[main, t_fun@14-list_entry_rc.c:45:3-45:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13)
+  >   read with [mhp:{tid=[main, t_fun@14-list_entry_rc.c:45:3-45:40#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@14-list_entry_rc.c:45:3-45:40#⊤]] (conf. 110)  (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13)
+  >   read with [mhp:{tid=[main]; created={[main, t_fun@14-list_entry_rc.c:45:3-45:40#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & s->datum) (14-list_entry_rc.c:27:3-27:13)
   [1]
diff --git a/tests/regression/06-symbeq/16-type_rc.t b/tests/regression/06-symbeq/16-type_rc.t
index a5f977008d..703b73e0d0 100644
--- a/tests/regression/06-symbeq/16-type_rc.t
+++ b/tests/regression/06-symbeq/16-type_rc.t
@@ -6,8 +6,8 @@ Disable info messages because race summary contains (safe) memory location count
   [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:33:3-33:16)
   [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:36:3-36:9)
   [Warning][Race] Memory location (struct s).datum (race with conf. 100):
-    write with thread:[main, t_fun@16-type_rc.c:35:3-35:37] (conf. 100)  (exp: & s->datum) (16-type_rc.c:21:3-21:15)
-    write with [mhp:{created={[main, t_fun@16-type_rc.c:35:3-35:37]}}, thread:[main]] (conf. 100)  (exp: & *d) (16-type_rc.c:36:3-36:9)
+    write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@16-type_rc.c:35:3-35:37]] (conf. 100)  (exp: & s->datum) (16-type_rc.c:21:3-21:15)
+    write with [mhp:{created={[main, t_fun@16-type_rc.c:35:3-35:37]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100)  (exp: & *d) (16-type_rc.c:36:3-36:9)
   [Error][Imprecise][Unsound] Function definition missing for get_s (16-type_rc.c:20:12-20:24)
   [Error][Imprecise][Unsound] Function definition missing for get_s (16-type_rc.c:31:3-31:14)
   [Error][Imprecise][Unsound] Function definition missing
@@ -18,7 +18,7 @@ Disable info messages because race summary contains (safe) memory location count
   [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:33:3-33:16)
   [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:36:3-36:9)
   [Success][Race] Memory location (struct s).datum (safe):
-    write with thread:[main, t_fun@16-type_rc.c:35:3-35:37] (conf. 100)  (exp: & s->datum) (16-type_rc.c:21:3-21:15)
+    write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@16-type_rc.c:35:3-35:37]] (conf. 100)  (exp: & s->datum) (16-type_rc.c:21:3-21:15)
   [Error][Imprecise][Unsound] Function definition missing for get_s (16-type_rc.c:20:12-20:24)
   [Error][Imprecise][Unsound] Function definition missing for get_s (16-type_rc.c:31:3-31:14)
   [Error][Imprecise][Unsound] Function definition missing
@@ -27,18 +27,18 @@ Disable info messages because race summary contains (safe) memory location count
 
   $ diff default-output-1.txt full-output-1.txt
   6,7c6,7
-  <   write with thread:[main, t_fun@16-type_rc.c:35:3-35:37] (conf. 100)  (exp: & s->datum) (16-type_rc.c:21:3-21:15)
-  <   write with [mhp:{created={[main, t_fun@16-type_rc.c:35:3-35:37]}}, thread:[main]] (conf. 100)  (exp: & *d) (16-type_rc.c:36:3-36:9)
+  <   write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@16-type_rc.c:35:3-35:37]] (conf. 100)  (exp: & s->datum) (16-type_rc.c:21:3-21:15)
+  <   write with [mhp:{created={[main, t_fun@16-type_rc.c:35:3-35:37]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100)  (exp: & *d) (16-type_rc.c:36:3-36:9)
   ---
-  >   write with [mhp:{tid=[main, t_fun@16-type_rc.c:35:3-35:37#⊤]}, thread:[main, t_fun@16-type_rc.c:35:3-35:37#⊤]] (conf. 100)  (exp: & s->datum) (16-type_rc.c:21:3-21:15)
-  >   write with [mhp:{tid=[main]; created={[main, t_fun@16-type_rc.c:35:3-35:37#⊤]}}, thread:[main]] (conf. 100)  (exp: & *d) (16-type_rc.c:36:3-36:9)
+  >   write with [mhp:{tid=[main, t_fun@16-type_rc.c:35:3-35:37#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@16-type_rc.c:35:3-35:37#⊤]] (conf. 100)  (exp: & s->datum) (16-type_rc.c:21:3-21:15)
+  >   write with [mhp:{tid=[main]; created={[main, t_fun@16-type_rc.c:35:3-35:37#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100)  (exp: & *d) (16-type_rc.c:36:3-36:9)
   [1]
 
   $ goblint --enable warn.deterministic --disable warn.info --disable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'"  --set ana.activated[+] "'symb_locks'" --enable allglobs --enable dbg.full-output 16-type_rc.c > full-output-2.txt 2>&1
 
   $ diff default-output-2.txt full-output-2.txt
   6c6
-  <   write with thread:[main, t_fun@16-type_rc.c:35:3-35:37] (conf. 100)  (exp: & s->datum) (16-type_rc.c:21:3-21:15)
+  <   write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@16-type_rc.c:35:3-35:37]] (conf. 100)  (exp: & s->datum) (16-type_rc.c:21:3-21:15)
   ---
-  >   write with [mhp:{tid=[main, t_fun@16-type_rc.c:35:3-35:37#⊤]}, thread:[main, t_fun@16-type_rc.c:35:3-35:37#⊤]] (conf. 100)  (exp: & s->datum) (16-type_rc.c:21:3-21:15)
+  >   write with [mhp:{tid=[main, t_fun@16-type_rc.c:35:3-35:37#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@16-type_rc.c:35:3-35:37#⊤]] (conf. 100)  (exp: & s->datum) (16-type_rc.c:21:3-21:15)
   [1]
diff --git a/tests/regression/06-symbeq/21-mult_accs_rc.t b/tests/regression/06-symbeq/21-mult_accs_rc.t
index 2eacd0382e..3b1c54990e 100644
--- a/tests/regression/06-symbeq/21-mult_accs_rc.t
+++ b/tests/regression/06-symbeq/21-mult_accs_rc.t
@@ -8,8 +8,8 @@ Disable info messages because race summary contains (safe) memory location count
   [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (21-mult_accs_rc.c:29:3-29:15)
   [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (21-mult_accs_rc.c:34:3-34:9)
   [Warning][Race] Memory location (struct s).data (race with conf. 100):
-    write with thread:[main, t_fun@21-mult_accs_rc.c:31:3-31:37] (conf. 100)  (exp: & s->data) (21-mult_accs_rc.c:16:3-16:14)
-    write with [symblock:{p-lock:*.mutex}, mhp:{created={[main, t_fun@21-mult_accs_rc.c:31:3-31:37]}}, thread:[main]] (conf. 100)  (exp: & *d) (21-mult_accs_rc.c:34:3-34:9)
+    write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@21-mult_accs_rc.c:31:3-31:37]] (conf. 100)  (exp: & s->data) (21-mult_accs_rc.c:16:3-16:14)
+    write with [symblock:{p-lock:*.mutex}, mhp:{created={[main, t_fun@21-mult_accs_rc.c:31:3-31:37]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100)  (exp: & *d) (21-mult_accs_rc.c:34:3-34:9)
   [Warning][Unknown] locking NULL mutex (21-mult_accs_rc.c:14:3-14:32)
   [Warning][Unknown] unlocking NULL mutex (21-mult_accs_rc.c:17:3-17:34)
   [Warning][Unknown] unlocking unknown mutex which may not be held (21-mult_accs_rc.c:17:3-17:34)
@@ -29,7 +29,7 @@ Disable info messages because race summary contains (safe) memory location count
   [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (21-mult_accs_rc.c:29:3-29:15)
   [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (21-mult_accs_rc.c:34:3-34:9)
   [Success][Race] Memory location (struct s).data (safe):
-    write with thread:[main, t_fun@21-mult_accs_rc.c:31:3-31:37] (conf. 100)  (exp: & s->data) (21-mult_accs_rc.c:16:3-16:14)
+    write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@21-mult_accs_rc.c:31:3-31:37]] (conf. 100)  (exp: & s->data) (21-mult_accs_rc.c:16:3-16:14)
   [Warning][Unknown] locking NULL mutex (21-mult_accs_rc.c:14:3-14:32)
   [Warning][Unknown] unlocking NULL mutex (21-mult_accs_rc.c:17:3-17:34)
   [Warning][Unknown] unlocking unknown mutex which may not be held (21-mult_accs_rc.c:17:3-17:34)
@@ -45,18 +45,18 @@ Disable info messages because race summary contains (safe) memory location count
 
   $ diff default-output-1.txt full-output-1.txt
   8,9c8,9
-  <   write with thread:[main, t_fun@21-mult_accs_rc.c:31:3-31:37] (conf. 100)  (exp: & s->data) (21-mult_accs_rc.c:16:3-16:14)
-  <   write with [symblock:{p-lock:*.mutex}, mhp:{created={[main, t_fun@21-mult_accs_rc.c:31:3-31:37]}}, thread:[main]] (conf. 100)  (exp: & *d) (21-mult_accs_rc.c:34:3-34:9)
+  <   write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@21-mult_accs_rc.c:31:3-31:37]] (conf. 100)  (exp: & s->data) (21-mult_accs_rc.c:16:3-16:14)
+  <   write with [symblock:{p-lock:*.mutex}, mhp:{created={[main, t_fun@21-mult_accs_rc.c:31:3-31:37]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100)  (exp: & *d) (21-mult_accs_rc.c:34:3-34:9)
   ---
-  >   write with [mhp:{tid=[main, t_fun@21-mult_accs_rc.c:31:3-31:37#⊤]}, thread:[main, t_fun@21-mult_accs_rc.c:31:3-31:37#⊤]] (conf. 100)  (exp: & s->data) (21-mult_accs_rc.c:16:3-16:14)
-  >   write with [symblock:{p-lock:*.mutex}, mhp:{tid=[main]; created={[main, t_fun@21-mult_accs_rc.c:31:3-31:37#⊤]}}, thread:[main]] (conf. 100)  (exp: & *d) (21-mult_accs_rc.c:34:3-34:9)
+  >   write with [mhp:{tid=[main, t_fun@21-mult_accs_rc.c:31:3-31:37#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@21-mult_accs_rc.c:31:3-31:37#⊤]] (conf. 100)  (exp: & s->data) (21-mult_accs_rc.c:16:3-16:14)
+  >   write with [symblock:{p-lock:*.mutex}, mhp:{tid=[main]; created={[main, t_fun@21-mult_accs_rc.c:31:3-31:37#⊤]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 100)  (exp: & *d) (21-mult_accs_rc.c:34:3-34:9)
   [1]
 
   $ goblint --enable warn.deterministic --disable warn.info --disable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'"  --set ana.activated[+] "'symb_locks'" --enable allglobs --enable dbg.full-output 21-mult_accs_rc.c > full-output-2.txt 2>&1
 
   $ diff default-output-2.txt full-output-2.txt
   8c8
-  <   write with thread:[main, t_fun@21-mult_accs_rc.c:31:3-31:37] (conf. 100)  (exp: & s->data) (21-mult_accs_rc.c:16:3-16:14)
+  <   write with [threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@21-mult_accs_rc.c:31:3-31:37]] (conf. 100)  (exp: & s->data) (21-mult_accs_rc.c:16:3-16:14)
   ---
-  >   write with [mhp:{tid=[main, t_fun@21-mult_accs_rc.c:31:3-31:37#⊤]}, thread:[main, t_fun@21-mult_accs_rc.c:31:3-31:37#⊤]] (conf. 100)  (exp: & s->data) (21-mult_accs_rc.c:16:3-16:14)
+  >   write with [mhp:{tid=[main, t_fun@21-mult_accs_rc.c:31:3-31:37#⊤]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@21-mult_accs_rc.c:31:3-31:37#⊤]] (conf. 100)  (exp: & s->data) (21-mult_accs_rc.c:16:3-16:14)
   [1]
diff --git a/tests/regression/13-privatized/63-access-threadspawn-lval.t b/tests/regression/13-privatized/63-access-threadspawn-lval.t
index 313459637c..d0d7f90bee 100644
--- a/tests/regression/13-privatized/63-access-threadspawn-lval.t
+++ b/tests/regression/13-privatized/63-access-threadspawn-lval.t
@@ -12,10 +12,11 @@ Should have (safe) write accesses to id1 and id2:
     dead: 0
     total lines: 13
   [Success][Race] Memory location id1 (safe): (63-access-threadspawn-lval.c:4:11-4:14)
-    write with [multi:false, thread:[main]] (conf. 110)  (exp: & *((pthread_t * __restrict  )(& id1))) (63-access-threadspawn-lval.c:27:3-27:37)
+    write with [threadflag:(MT mode:Singlethreaded, bool:false), thread:[main]] (conf. 110)  (exp: (pthread_t * __restrict  )(& id1)) (63-access-threadspawn-lval.c:27:3-27:37)
+    write with [threadflag:(MT mode:Singlethreaded, bool:false), thread:[main]] (conf. 110)  (exp: & *((pthread_t * __restrict  )(& id1))) (63-access-threadspawn-lval.c:27:3-27:37)
   [Success][Race] Memory location id2 (safe): (63-access-threadspawn-lval.c:5:11-5:14)
-    write with [mhp:{created={[main, f@63-access-threadspawn-lval.c:27:3-27:37]}}, thread:[main]] (conf. 110)  (exp: (pthread_t * __restrict  )(& id2)) (63-access-threadspawn-lval.c:28:3-28:37)
-    write with [mhp:{created={[main, f@63-access-threadspawn-lval.c:27:3-27:37]}}, thread:[main]] (conf. 110)  (exp: & *((pthread_t * __restrict  )(& id2))) (63-access-threadspawn-lval.c:28:3-28:37)
+    write with [mhp:{created={[main, f@63-access-threadspawn-lval.c:27:3-27:37]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: (pthread_t * __restrict  )(& id2)) (63-access-threadspawn-lval.c:28:3-28:37)
+    write with [mhp:{created={[main, f@63-access-threadspawn-lval.c:27:3-27:37]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & *((pthread_t * __restrict  )(& id2))) (63-access-threadspawn-lval.c:28:3-28:37)
   [Info][Race] Memory locations race summary:
     safe: 2
     vulnerable: 0
diff --git a/tests/regression/13-privatized/64-access-invalidate.t b/tests/regression/13-privatized/64-access-invalidate.t
index 28227ec475..165fbe9aea 100644
--- a/tests/regression/13-privatized/64-access-invalidate.t
+++ b/tests/regression/13-privatized/64-access-invalidate.t
@@ -12,7 +12,8 @@ Should have (safe) write access to id1 and magic2 invalidate to A:
     dead: 0
     total lines: 10
   [Success][Race] Memory location id (safe): (64-access-invalidate.c:4:11-4:13)
-    write with [multi:false, thread:[main]] (conf. 110)  (exp: & *((pthread_t * __restrict  )(& id))) (64-access-invalidate.c:21:3-21:36)
+    write with [threadflag:(MT mode:Singlethreaded, bool:false), thread:[main]] (conf. 110)  (exp: (pthread_t * __restrict  )(& id)) (64-access-invalidate.c:21:3-21:36)
+    write with [threadflag:(MT mode:Singlethreaded, bool:false), thread:[main]] (conf. 110)  (exp: & *((pthread_t * __restrict  )(& id))) (64-access-invalidate.c:21:3-21:36)
   [Info][Race] Memory locations race summary:
     safe: 1
     vulnerable: 0
diff --git a/tests/regression/29-svcomp/16-atomic_priv.t b/tests/regression/29-svcomp/16-atomic_priv.t
index 1662f881b7..04fb1994a6 100644
--- a/tests/regression/29-svcomp/16-atomic_priv.t
+++ b/tests/regression/29-svcomp/16-atomic_priv.t
@@ -9,9 +9,9 @@
     dead: 0
     total lines: 17
   [Warning][Race] Memory location myglobal (race with conf. 110): (16-atomic_priv.c:8:5-8:17)
-    write with [lock:{[__VERIFIER_atomic]}, thread:[main, t_fun@16-atomic_priv.c:23:3-23:40]] (conf. 110)  (exp: & myglobal) (16-atomic_priv.c:13:3-13:13)
-    write with [lock:{[__VERIFIER_atomic]}, thread:[main, t_fun@16-atomic_priv.c:23:3-23:40]] (conf. 110)  (exp: & myglobal) (16-atomic_priv.c:15:3-15:13)
-    read with [mhp:{created={[main, t_fun@16-atomic_priv.c:23:3-23:40]}}, thread:[main]] (conf. 110)  (exp: & myglobal) (16-atomic_priv.c:24:3-24:33)
+    write with [lock:{[__VERIFIER_atomic]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@16-atomic_priv.c:23:3-23:40]] (conf. 110)  (exp: & myglobal) (16-atomic_priv.c:13:3-13:13)
+    write with [lock:{[__VERIFIER_atomic]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@16-atomic_priv.c:23:3-23:40]] (conf. 110)  (exp: & myglobal) (16-atomic_priv.c:15:3-15:13)
+    read with [mhp:{created={[main, t_fun@16-atomic_priv.c:23:3-23:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & myglobal) (16-atomic_priv.c:24:3-24:33)
   [Info][Witness] witness generation summary:
     location invariants: 0
     loop invariants: 0
@@ -63,9 +63,9 @@ Non-atomic privatization:
     dead: 0
     total lines: 17
   [Warning][Race] Memory location myglobal (race with conf. 110): (16-atomic_priv.c:8:5-8:17)
-    write with [lock:{[__VERIFIER_atomic]}, thread:[main, t_fun@16-atomic_priv.c:23:3-23:40]] (conf. 110)  (exp: & myglobal) (16-atomic_priv.c:13:3-13:13)
-    write with [lock:{[__VERIFIER_atomic]}, thread:[main, t_fun@16-atomic_priv.c:23:3-23:40]] (conf. 110)  (exp: & myglobal) (16-atomic_priv.c:15:3-15:13)
-    read with [mhp:{created={[main, t_fun@16-atomic_priv.c:23:3-23:40]}}, thread:[main]] (conf. 110)  (exp: & myglobal) (16-atomic_priv.c:24:3-24:33)
+    write with [lock:{[__VERIFIER_atomic]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@16-atomic_priv.c:23:3-23:40]] (conf. 110)  (exp: & myglobal) (16-atomic_priv.c:13:3-13:13)
+    write with [lock:{[__VERIFIER_atomic]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@16-atomic_priv.c:23:3-23:40]] (conf. 110)  (exp: & myglobal) (16-atomic_priv.c:15:3-15:13)
+    read with [mhp:{created={[main, t_fun@16-atomic_priv.c:23:3-23:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & myglobal) (16-atomic_priv.c:24:3-24:33)
   [Info][Witness] witness generation summary:
     location invariants: 0
     loop invariants: 0
diff --git a/tests/regression/36-apron/12-traces-min-rpb1.t b/tests/regression/36-apron/12-traces-min-rpb1.t
index 2a760c0dcb..d6ce4301ee 100644
--- a/tests/regression/36-apron/12-traces-min-rpb1.t
+++ b/tests/regression/36-apron/12-traces-min-rpb1.t
@@ -7,11 +7,11 @@
     dead: 0
     total lines: 18
   [Warning][Race] Memory location h (race with conf. 110): (12-traces-min-rpb1.c:8:5-8:10)
-    write with [lock:{A}, thread:[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]] (conf. 110)  (exp: & h) (12-traces-min-rpb1.c:15:3-15:8)
-    read with [mhp:{created={[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]}}, thread:[main]] (conf. 110)  (exp: & h) (12-traces-min-rpb1.c:27:3-27:26)
+    write with [lock:{A}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]] (conf. 110)  (exp: & h) (12-traces-min-rpb1.c:15:3-15:8)
+    read with [mhp:{created={[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & h) (12-traces-min-rpb1.c:27:3-27:26)
   [Warning][Race] Memory location g (race with conf. 110): (12-traces-min-rpb1.c:7:5-7:10)
-    write with [lock:{A}, thread:[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]] (conf. 110)  (exp: & g) (12-traces-min-rpb1.c:14:3-14:8)
-    read with [mhp:{created={[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]}}, thread:[main]] (conf. 110)  (exp: & g) (12-traces-min-rpb1.c:27:3-27:26)
+    write with [lock:{A}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]] (conf. 110)  (exp: & g) (12-traces-min-rpb1.c:14:3-14:8)
+    read with [mhp:{created={[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & g) (12-traces-min-rpb1.c:27:3-27:26)
   [Info][Witness] witness generation summary:
     location invariants: 3
     loop invariants: 0
@@ -64,11 +64,11 @@
   [Success][Assert] Assertion "g == h" will succeed (12-traces-min-rpb1.c:16:3-16:26)
   [Success][Assert] Assertion "g == h" will succeed (12-traces-min-rpb1.c:29:3-29:26)
   [Warning][Race] Memory location g (race with conf. 110): (12-traces-min-rpb1.c:7:5-7:10)
-    write with [lock:{A}, thread:[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]] (conf. 110)  (exp: & g) (12-traces-min-rpb1.c:14:3-14:8)
-    read with [mhp:{created={[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]}}, thread:[main]] (conf. 110)  (exp: & g) (12-traces-min-rpb1.c:27:3-27:26)
+    write with [lock:{A}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]] (conf. 110)  (exp: & g) (12-traces-min-rpb1.c:14:3-14:8)
+    read with [mhp:{created={[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & g) (12-traces-min-rpb1.c:27:3-27:26)
   [Warning][Race] Memory location h (race with conf. 110): (12-traces-min-rpb1.c:8:5-8:10)
-    write with [lock:{A}, thread:[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]] (conf. 110)  (exp: & h) (12-traces-min-rpb1.c:15:3-15:8)
-    read with [mhp:{created={[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]}}, thread:[main]] (conf. 110)  (exp: & h) (12-traces-min-rpb1.c:27:3-27:26)
+    write with [lock:{A}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]] (conf. 110)  (exp: & h) (12-traces-min-rpb1.c:15:3-15:8)
+    read with [mhp:{created={[main, t_fun@12-traces-min-rpb1.c:25:3-25:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & h) (12-traces-min-rpb1.c:27:3-27:26)
   [Info][Race] Memory locations race summary:
     safe: 0
     vulnerable: 0
diff --git a/tests/regression/45-escape/51-fresh-global.t b/tests/regression/45-escape/51-fresh-global.t
index ceb21425e8..aa6e06e153 100644
--- a/tests/regression/45-escape/51-fresh-global.t
+++ b/tests/regression/45-escape/51-fresh-global.t
@@ -4,8 +4,8 @@
     dead: 0
     total lines: 15
   [Warning][Race] Memory location (alloc@sid:$SID@tid:main) (race with conf. 110): (51-fresh-global.c:25:7-25:31)
-    write with lock:{A} (conf. 110)  (exp: & *i) (51-fresh-global.c:10:3-10:10)
-    write with thread:main (conf. 110)  (exp: & *i) (51-fresh-global.c:27:3-27:9)
+    write with [lock:{A}, threadflag:(MT mode:Multithreaded (other), bool:true)] (conf. 110)  (exp: & *i) (51-fresh-global.c:10:3-10:10)
+    write with [threadflag:(MT mode:Multithreaded (main), bool:true), thread:main] (conf. 110)  (exp: & *i) (51-fresh-global.c:27:3-27:9)
   [Info][Race] Memory locations race summary:
     safe: 1
     vulnerable: 0
diff --git a/tests/regression/46-apron2/95-witness-mm-escape.t b/tests/regression/46-apron2/95-witness-mm-escape.t
index 11cd3691c5..9724c1a9a9 100644
--- a/tests/regression/46-apron2/95-witness-mm-escape.t
+++ b/tests/regression/46-apron2/95-witness-mm-escape.t
@@ -27,3 +27,8 @@
     unsupported: 0
     disabled: 0
     total validation entries: 15
+  [Info][Race] Memory locations race summary:
+    safe: 1
+    vulnerable: 0
+    unsafe: 0
+    total memory locations: 1
diff --git a/tests/regression/56-witness/68-ghost-ambiguous-idx.t b/tests/regression/56-witness/68-ghost-ambiguous-idx.t
index 40025acf17..03fd9bd708 100644
--- a/tests/regression/56-witness/68-ghost-ambiguous-idx.t
+++ b/tests/regression/56-witness/68-ghost-ambiguous-idx.t
@@ -6,9 +6,9 @@
     dead: 0
     total lines: 15
   [Warning][Race] Memory location data (race with conf. 110): (68-ghost-ambiguous-idx.c:4:5-4:9)
-    write with [lock:{m[4]}, thread:[main, t_fun@68-ghost-ambiguous-idx.c:20:3-20:40]] (conf. 110)  (exp: & data) (68-ghost-ambiguous-idx.c:9:3-9:9)
-    write with [lock:{m[4]}, thread:[main, t_fun@68-ghost-ambiguous-idx.c:20:3-20:40]] (conf. 110)  (exp: & data) (68-ghost-ambiguous-idx.c:10:3-10:9)
-    read with [mhp:{created={[main, t_fun@68-ghost-ambiguous-idx.c:20:3-20:40]}}, thread:[main]] (conf. 110)  (exp: & data) (68-ghost-ambiguous-idx.c:24:3-24:29)
+    write with [lock:{m[4]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@68-ghost-ambiguous-idx.c:20:3-20:40]] (conf. 110)  (exp: & data) (68-ghost-ambiguous-idx.c:9:3-9:9)
+    write with [lock:{m[4]}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@68-ghost-ambiguous-idx.c:20:3-20:40]] (conf. 110)  (exp: & data) (68-ghost-ambiguous-idx.c:10:3-10:9)
+    read with [mhp:{created={[main, t_fun@68-ghost-ambiguous-idx.c:20:3-20:40]}}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & data) (68-ghost-ambiguous-idx.c:24:3-24:29)
   [Info][Witness] witness generation summary:
     location invariants: 0
     loop invariants: 0
diff --git a/tests/regression/56-witness/69-ghost-ptr-protection.t b/tests/regression/56-witness/69-ghost-ptr-protection.t
index 0c5fb0201c..c4c1f7519e 100644
--- a/tests/regression/56-witness/69-ghost-ptr-protection.t
+++ b/tests/regression/56-witness/69-ghost-ptr-protection.t
@@ -5,9 +5,9 @@
     dead: 0
     total lines: 15
   [Warning][Race] Memory location p (race with conf. 110): (69-ghost-ptr-protection.c:7:5-7:12)
-    write with [lock:{m2}, thread:[main, t_fun@69-ghost-ptr-protection.c:22:3-22:40]] (conf. 110)  (exp: & p) (69-ghost-ptr-protection.c:14:3-14:9)
-    write with [lock:{m2}, thread:[main, t_fun@69-ghost-ptr-protection.c:22:3-22:40]] (conf. 110)  (exp: & p) (69-ghost-ptr-protection.c:15:3-15:9)
-    read with [mhp:{created={[main, t_fun@69-ghost-ptr-protection.c:22:3-22:40]}}, lock:{m1}, thread:[main]] (conf. 110)  (exp: & p) (69-ghost-ptr-protection.c:26:3-26:27)
+    write with [lock:{m2}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@69-ghost-ptr-protection.c:22:3-22:40]] (conf. 110)  (exp: & p) (69-ghost-ptr-protection.c:14:3-14:9)
+    write with [lock:{m2}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@69-ghost-ptr-protection.c:22:3-22:40]] (conf. 110)  (exp: & p) (69-ghost-ptr-protection.c:15:3-15:9)
+    read with [mhp:{created={[main, t_fun@69-ghost-ptr-protection.c:22:3-22:40]}}, lock:{m1}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & p) (69-ghost-ptr-protection.c:26:3-26:27)
   [Info][Witness] witness generation summary:
     location invariants: 0
     loop invariants: 0
@@ -124,9 +124,9 @@ Same with vojdani.
     dead: 0
     total lines: 15
   [Warning][Race] Memory location p (race with conf. 110): (69-ghost-ptr-protection.c:7:5-7:12)
-    write with [lock:{m2}, thread:[main, t_fun@69-ghost-ptr-protection.c:22:3-22:40]] (conf. 110)  (exp: & p) (69-ghost-ptr-protection.c:14:3-14:9)
-    write with [lock:{m2}, thread:[main, t_fun@69-ghost-ptr-protection.c:22:3-22:40]] (conf. 110)  (exp: & p) (69-ghost-ptr-protection.c:15:3-15:9)
-    read with [mhp:{created={[main, t_fun@69-ghost-ptr-protection.c:22:3-22:40]}}, lock:{m1}, thread:[main]] (conf. 110)  (exp: & p) (69-ghost-ptr-protection.c:26:3-26:27)
+    write with [lock:{m2}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@69-ghost-ptr-protection.c:22:3-22:40]] (conf. 110)  (exp: & p) (69-ghost-ptr-protection.c:14:3-14:9)
+    write with [lock:{m2}, threadflag:(MT mode:Multithreaded (other), bool:true), thread:[main, t_fun@69-ghost-ptr-protection.c:22:3-22:40]] (conf. 110)  (exp: & p) (69-ghost-ptr-protection.c:15:3-15:9)
+    read with [mhp:{created={[main, t_fun@69-ghost-ptr-protection.c:22:3-22:40]}}, lock:{m1}, threadflag:(MT mode:Multithreaded (main), bool:true), thread:[main]] (conf. 110)  (exp: & p) (69-ghost-ptr-protection.c:26:3-26:27)
   [Info][Witness] witness generation summary:
     location invariants: 0
     loop invariants: 0
diff --git a/tests/regression/71-doublelocking/07-rec-dyn-osx.c b/tests/regression/71-doublelocking/07-rec-dyn-osx.c
index bb3cf65657..4059356371 100644
--- a/tests/regression/71-doublelocking/07-rec-dyn-osx.c
+++ b/tests/regression/71-doublelocking/07-rec-dyn-osx.c
@@ -1,6 +1,5 @@
-// PARAM: --set ana.activated[+] 'maylocks' --set ana.activated[+] 'pthreadMutexType' --set pre.cppflags[+] "-DGOBLINT_NO_PTHREAD_ONCE"
+// PARAM: --set ana.activated[+] 'maylocks' --set ana.activated[+] 'pthreadMutexType'
 // Here, we do not include pthread.h, so MutexAttr.recursive_int remains at `2`, emulating the behavior of OS X.
-#define GOBLINT_NO_PTHREAD_ONCE 1
 typedef signed char __int8_t;
 typedef unsigned char __uint8_t;
 typedef short __int16_t;
diff --git a/tests/regression/71-doublelocking/20-default-init-osx.c b/tests/regression/71-doublelocking/20-default-init-osx.c
index 4d3ec1f8d7..eaa6ec58be 100644
--- a/tests/regression/71-doublelocking/20-default-init-osx.c
+++ b/tests/regression/71-doublelocking/20-default-init-osx.c
@@ -1,4 +1,4 @@
-// PARAM: --set ana.activated[+] 'maylocks' --set ana.activated[+] 'pthreadMutexType' --set pre.cppflags[+] "-DGOBLINT_NO_PTHREAD_ONCE"
+// PARAM: --set ana.activated[+] 'maylocks' --set ana.activated[+] 'pthreadMutexType'
 // Here, we do not include pthread.h, to emulate the behavior of OS X.
 #define NULL ((void *)0)
 typedef signed char __int8_t;
diff --git a/tests/regression/74-invalid_deref/01-oob-heap-simple.t b/tests/regression/74-invalid_deref/01-oob-heap-simple.t
index ac3ec99fa8..0f241692cd 100644
--- a/tests/regression/74-invalid_deref/01-oob-heap-simple.t
+++ b/tests/regression/74-invalid_deref/01-oob-heap-simple.t
@@ -6,6 +6,11 @@
     live: 8
     dead: 0
     total lines: 8
+  [Info][Race] Memory locations race summary:
+    safe: 2
+    vulnerable: 0
+    unsafe: 0
+    total memory locations: 2
 
   $ goblint --set ana.activated[+] memOutOfBounds --enable ana.int.interval --enable dbg.full-output 01-oob-heap-simple.c > full-output.txt 2>&1
 
diff --git a/tests/regression/82-barrier/01-simple.c b/tests/regression/82-barrier/01-simple.c
new file mode 100644
index 0000000000..285da1a6fb
--- /dev/null
+++ b/tests/regression/82-barrier/01-simple.c
@@ -0,0 +1,26 @@
+// NOMAC PARAM: --set ana.activated[+] 'pthreadBarriers'
+#include<pthread.h>
+#include<stdio.h>
+#include<unistd.h>
+
+int g;
+
+pthread_barrier_t barrier;
+
+
+int main(int argc, char const *argv[])
+{
+    int top;
+    int i = 0;
+    
+    pthread_barrier_init(&barrier, NULL, 2);
+    
+    if(top) {
+        pthread_barrier_wait(&barrier);
+        // Unreachable
+        i = 1;
+    }
+
+    __goblint_check(i == 0);
+    return 0;
+}
diff --git a/tests/regression/82-barrier/02-more.c b/tests/regression/82-barrier/02-more.c
new file mode 100644
index 0000000000..53b4e99de2
--- /dev/null
+++ b/tests/regression/82-barrier/02-more.c
@@ -0,0 +1,45 @@
+// NOMAC PARAM: --set ana.activated[+] 'pthreadBarriers'
+#include<pthread.h>
+#include<stdio.h>
+#include<unistd.h>
+
+int g;
+
+pthread_barrier_t barrier;
+
+void* f2(void* ptr) {
+    pthread_barrier_wait(&barrier);
+    return NULL;
+}
+
+void* f1(void* ptr) {
+    pthread_barrier_wait(&barrier);
+
+    // This is past the barrier, so it will not be reached
+    pthread_t t2;
+    pthread_create(&t2,NULL,f2,NULL);
+
+    return NULL;
+}
+
+int main(int argc, char const *argv[])
+{
+    int top;
+    int i = 0;
+    
+    pthread_barrier_init(&barrier, NULL, 3);
+
+    pthread_t t1;
+    pthread_create(&t1,NULL,f1,NULL);
+    
+    if(top) {
+        pthread_barrier_wait(&barrier);
+        // Unreachable
+        i = 1;
+    }
+
+    __goblint_check(i == 0);
+
+
+    return 0;
+}
diff --git a/tests/regression/82-barrier/03-problem.c b/tests/regression/82-barrier/03-problem.c
new file mode 100644
index 0000000000..2d80706b92
--- /dev/null
+++ b/tests/regression/82-barrier/03-problem.c
@@ -0,0 +1,36 @@
+// NOMAC PARAM: --set ana.activated[+] 'pthreadBarriers'
+#include<pthread.h>
+#include<stdio.h>
+#include<unistd.h>
+
+int g;
+
+pthread_barrier_t barrier;
+
+
+void* f1(void* ptr) {
+    pthread_barrier_wait(&barrier);
+    return NULL;
+}
+
+int main(int argc, char const *argv[])
+{
+    int top;
+    int i = 0;
+    
+    pthread_barrier_init(&barrier, NULL, 2);
+
+    pthread_t t1;
+    pthread_create(&t1,NULL,f1,NULL);
+    
+    if(top) {
+        pthread_barrier_wait(&barrier);
+        // Live!
+        i = 1;
+    }
+
+    __goblint_check(i == 0); //UNKNOWN!
+
+
+    return 0;
+}
diff --git a/tests/regression/82-barrier/04-challenge.c b/tests/regression/82-barrier/04-challenge.c
new file mode 100644
index 0000000000..73d66e5c51
--- /dev/null
+++ b/tests/regression/82-barrier/04-challenge.c
@@ -0,0 +1,49 @@
+// NOMAC PARAM: --set ana.activated[+] 'pthreadBarriers'
+#include<pthread.h>
+#include<stdio.h>
+#include<unistd.h>
+
+int g;
+
+pthread_barrier_t barrier;
+
+void* f2(void* ptr) {
+    pthread_barrier_wait(&barrier);
+    return NULL;
+}
+
+void* f1(void* ptr) {
+    pthread_barrier_wait(&barrier);
+
+    // This is past the barrier, so it will not be reached
+    pthread_t t2;
+    pthread_create(&t2,NULL,f2,NULL);
+
+    return NULL;
+}
+
+int main(int argc, char const *argv[])
+{
+    int top;
+    int i = 0;
+    
+    pthread_barrier_init(&barrier, NULL, 3);
+
+    pthread_t t1;
+    pthread_create(&t1,NULL,f1,NULL);
+    
+    if(top) {
+        pthread_barrier_wait(&barrier);
+        // Unreachable
+        i = 1;
+    }
+
+    // Created too late to have any effect
+    pthread_t t2;
+    pthread_create(&t2,NULL,f1,NULL);
+
+    __goblint_check(i == 0);
+
+
+    return 0;
+}
diff --git a/tests/regression/82-barrier/05-mhp-not-enough.c b/tests/regression/82-barrier/05-mhp-not-enough.c
new file mode 100644
index 0000000000..b289f3b0c0
--- /dev/null
+++ b/tests/regression/82-barrier/05-mhp-not-enough.c
@@ -0,0 +1,44 @@
+// NOMAC PARAM: --set ana.activated[+] 'pthreadBarriers'
+#include<pthread.h>
+#include<stdio.h>
+#include<unistd.h>
+
+int g;
+
+pthread_barrier_t barrier;
+
+
+void* f1(void* ptr) {
+    pthread_barrier_wait(&barrier);
+
+    // This should not be reached as either main calls wait or the other thread is created
+    // -> In the concrete, there never are three threads calling wait
+
+    return NULL;
+}
+
+int main(int argc, char const *argv[])
+{
+    int top;
+    int i = 0;
+    
+    pthread_barrier_init(&barrier, NULL, 3);
+
+    pthread_t t1;
+    pthread_create(&t1,NULL,f1,NULL);
+    
+    if(top) {
+        pthread_barrier_wait(&barrier);
+        // Unreachable
+        i = 1;
+    } else {
+        pthread_t t2;
+        pthread_create(&t2,NULL,f1,NULL);    
+    }
+
+
+    __goblint_check(i == 0);
+
+
+    return 0;
+}
diff --git a/tests/regression/82-barrier/06-multiprocess.c b/tests/regression/82-barrier/06-multiprocess.c
new file mode 100644
index 0000000000..f55790cfab
--- /dev/null
+++ b/tests/regression/82-barrier/06-multiprocess.c
@@ -0,0 +1,35 @@
+// NOMAC PARAM: --set ana.activated[+] 'pthreadBarriers'
+#include<pthread.h>
+#include<stdio.h>
+#include<unistd.h>
+
+int g;
+
+pthread_barrier_t barrier;
+
+
+int main(int argc, char const *argv[])
+{
+    int top;
+    int i = 0;
+    
+    pthread_barrierattr_t barattr;
+    pthread_barrierattr_setpshared(&barattr, PTHREAD_PROCESS_SHARED);
+
+    pthread_barrier_init(&barrier, &barattr, 2);
+
+    fork();
+    pthread_t t1;
+    
+    if(top) {
+        pthread_barrier_wait(&barrier);
+        // Reachable if both processes go into this branch
+        i = 1;
+    }
+
+
+    __goblint_check(i == 0); //UNKNOWN!
+
+
+    return 0;
+}
diff --git a/tests/regression/82-barrier/07-lockset.c b/tests/regression/82-barrier/07-lockset.c
new file mode 100644
index 0000000000..d1c68f3d7f
--- /dev/null
+++ b/tests/regression/82-barrier/07-lockset.c
@@ -0,0 +1,39 @@
+// NOMAC PARAM: --set ana.activated[+] 'pthreadBarriers'
+#include<pthread.h>
+#include<stdio.h>
+#include<unistd.h>
+
+int g;
+
+pthread_barrier_t barrier;
+pthread_mutex_t mutex;
+
+void* f1(void* ptr) {
+    pthread_mutex_lock(&mutex);
+    pthread_barrier_wait(&barrier);
+    pthread_mutex_unlock(&mutex);
+    return NULL;
+}
+
+int main(int argc, char const *argv[])
+{
+    int top;
+    int i = 0;
+    
+    pthread_barrier_init(&barrier, NULL, 2);
+
+    pthread_t t1;
+    pthread_create(&t1,NULL,f1,NULL);
+    
+    if(top) {
+        pthread_mutex_lock(&mutex);
+        pthread_barrier_wait(&barrier);
+        // Deadlocks
+        pthread_mutex_unlock(&mutex);
+        i = 1;
+    }
+
+    __goblint_check(i == 0);
+
+    return 0;
+}
diff --git a/tests/regression/82-barrier/08-lockset-more.c b/tests/regression/82-barrier/08-lockset-more.c
new file mode 100644
index 0000000000..a33ecc1a78
--- /dev/null
+++ b/tests/regression/82-barrier/08-lockset-more.c
@@ -0,0 +1,47 @@
+// NOMAC PARAM: --set ana.activated[+] 'pthreadBarriers'
+#include<pthread.h>
+#include<stdio.h>
+#include<unistd.h>
+
+int g;
+
+pthread_barrier_t barrier;
+pthread_mutex_t mutex;
+
+void* f1(void* ptr) {
+    pthread_mutex_lock(&mutex);
+    pthread_barrier_wait(&barrier);
+    pthread_mutex_unlock(&mutex);
+    return NULL;
+}
+
+void* f2(void* ptr) {
+    pthread_mutex_lock(&mutex);
+    pthread_barrier_wait(&barrier);
+    pthread_mutex_unlock(&mutex);
+    return NULL;
+}
+
+int main(int argc, char const *argv[])
+{
+    int top;
+    int i = 0;
+    
+    pthread_barrier_init(&barrier, NULL, 2);
+
+    pthread_t t1;
+    pthread_create(&t1,NULL,f1,NULL);
+
+    pthread_t t2;
+    pthread_create(&t2,NULL,f2,NULL);
+    
+    
+    if(top) {
+        pthread_barrier_wait(&barrier);
+        i = 1;
+    }
+
+    __goblint_check(i == 0); //UNKNOWN!
+
+    return 0;
+}
diff --git a/tests/regression/82-barrier/09-race.c b/tests/regression/82-barrier/09-race.c
new file mode 100644
index 0000000000..fad6ad6243
--- /dev/null
+++ b/tests/regression/82-barrier/09-race.c
@@ -0,0 +1,36 @@
+// NOMAC PARAM: --set ana.activated[+] 'pthreadBarriers'
+#include<pthread.h>
+#include<stdio.h>
+#include<unistd.h>
+
+int g;
+int h;
+
+pthread_barrier_t barrier;
+pthread_mutex_t mutex;
+
+void* f1(void* ptr) {
+    g = 2; //NORACE
+    h = 3; //RACE
+    pthread_barrier_wait(&barrier);
+
+    return NULL;
+}
+
+int main(int argc, char const *argv[])
+{
+    int top;
+    int i = 0;
+    
+    pthread_barrier_init(&barrier, NULL, 2);
+
+    pthread_t t1;
+    pthread_create(&t1,NULL,f1,NULL);
+
+    h = 5; //RACE
+
+    pthread_barrier_wait(&barrier);
+    g = 3; //NORACE
+
+    return 0;
+}
diff --git a/tests/regression/82-barrier/10-several.c b/tests/regression/82-barrier/10-several.c
new file mode 100644
index 0000000000..6fc9f57681
--- /dev/null
+++ b/tests/regression/82-barrier/10-several.c
@@ -0,0 +1,36 @@
+// NOMAC PARAM: --set ana.activated[+] 'pthreadBarriers'
+#include<pthread.h>
+#include<stdio.h>
+#include<unistd.h>
+
+int g;
+
+pthread_barrier_t barrier;
+
+void* f1(void* ptr) {
+    pthread_barrier_wait(&barrier);
+
+    return NULL;
+}
+
+int main(int argc, char const *argv[])
+{
+    int top;
+    int i = 0;
+    
+    pthread_barrier_init(&barrier, NULL, 4);
+
+    pthread_t t1, t2, t3;
+    pthread_create(&t1,NULL,f1,NULL);
+    pthread_create(&t2,NULL,f1,NULL);
+    pthread_create(&t3,NULL,f1,NULL);
+
+    if(top) {
+        pthread_barrier_wait(&barrier);
+        i = 1;
+    }
+
+    __goblint_check(i == 0); //UNKNOWN!
+
+    return 0;
+}
diff --git a/tests/regression/82-barrier/11-race-more.c b/tests/regression/82-barrier/11-race-more.c
new file mode 100644
index 0000000000..ed6c7ef29d
--- /dev/null
+++ b/tests/regression/82-barrier/11-race-more.c
@@ -0,0 +1,37 @@
+// NOMAC PARAM: --set ana.activated[+] 'pthreadBarriers'
+#include<pthread.h>
+#include<stdio.h>
+#include<unistd.h>
+
+int g;
+
+pthread_barrier_t barrier;
+pthread_mutex_t mutex;
+
+void* f1(void* ptr) {
+    pthread_mutex_lock(&mutex);
+    g = 4711; //NORACE
+    pthread_mutex_unlock(&mutex);
+    pthread_barrier_wait(&barrier);
+
+    return NULL;
+}
+
+int main(int argc, char const *argv[])
+{
+    int top;
+    int i = 0;
+    
+    pthread_barrier_init(&barrier, NULL, 4);
+
+    pthread_t t1, t2, t3;
+    pthread_create(&t1,NULL,f1,NULL);
+    pthread_create(&t2,NULL,f1,NULL);
+    pthread_create(&t3,NULL,f1,NULL);
+
+    pthread_barrier_wait(&barrier);
+
+    g = 3; //NORACE
+
+    return 0;
+}
diff --git a/tests/regression/83-once/01-sanity.c b/tests/regression/83-once/01-sanity.c
new file mode 100644
index 0000000000..8a26012571
--- /dev/null
+++ b/tests/regression/83-once/01-sanity.c
@@ -0,0 +1,27 @@
+// PARAM: --set ana.activated[+] pthreadOnce
+#include <pthread.h>
+#include <stdio.h>
+
+int g;
+pthread_once_t once = PTHREAD_ONCE_INIT;
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+
+void fun() {
+  g++;
+}
+
+
+int main(void) {
+  pthread_t id;
+
+  pthread_once(&once, fun);
+  pthread_once(&once, fun);
+
+  __goblint_check(g < 2);
+
+  if(g = 1) {
+    __goblint_check(1); //Reachable
+  }
+
+  return 0;
+}
diff --git a/tests/regression/83-once/02-normal.c b/tests/regression/83-once/02-normal.c
new file mode 100644
index 0000000000..ee10a7d6b4
--- /dev/null
+++ b/tests/regression/83-once/02-normal.c
@@ -0,0 +1,34 @@
+// PARAM: --set ana.activated[+] pthreadOnce
+#include <pthread.h>
+#include <stdio.h>
+
+int g;
+pthread_once_t once = PTHREAD_ONCE_INIT;
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+
+void fun() {
+  g = 42; //NORACE
+}
+
+
+void *t_fun(void *arg) {
+  pthread_once(&once, fun);
+
+  pthread_mutex_lock(&mutex1);
+  g = 10; //NORACE
+  pthread_mutex_unlock(&mutex1);
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  pthread_once(&once, fun);
+
+  pthread_mutex_lock(&mutex1);
+  g = 11; //NORACE
+  pthread_mutex_unlock(&mutex1);
+  pthread_join (id, NULL);
+  return 0;
+}
diff --git a/tests/regression/83-once/03-unknown.c b/tests/regression/83-once/03-unknown.c
new file mode 100644
index 0000000000..16cb2c5a12
--- /dev/null
+++ b/tests/regression/83-once/03-unknown.c
@@ -0,0 +1,44 @@
+// PARAM: --set ana.activated[+] pthreadOnce
+#include <pthread.h>
+#include <stdio.h>
+
+int g;
+pthread_once_t once1 = PTHREAD_ONCE_INIT;
+pthread_once_t once2; // PTHREAD_ONCE_INIT is `0`
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+
+pthread_once_t *ptr;
+
+void fun() {
+  g = 42; //RACE
+}
+
+
+void *t_fun(void *arg) {
+  pthread_once(ptr, fun);
+
+  pthread_mutex_lock(&mutex1);
+  g = 10; //RACE
+  pthread_mutex_unlock(&mutex1);
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  int top;
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  ptr = &once1;
+
+  if(top) {
+    ptr = &once2;
+  }
+
+  pthread_once(ptr, fun);
+
+  pthread_mutex_lock(&mutex1);
+  g = 11; //RACE
+  pthread_mutex_unlock(&mutex1);
+  pthread_join (id, NULL);
+  return 0;
+}
diff --git a/tests/regression/83-once/04-thread.c b/tests/regression/83-once/04-thread.c
new file mode 100644
index 0000000000..c467bacc22
--- /dev/null
+++ b/tests/regression/83-once/04-thread.c
@@ -0,0 +1,58 @@
+// PARAM: --set ana.activated[+] pthreadOnce
+#include <pthread.h>
+#include <stdio.h>
+
+int g;
+int h;
+int i;
+pthread_once_t once = PTHREAD_ONCE_INIT;
+pthread_once_t i_once = PTHREAD_ONCE_INIT;
+pthread_mutex_t mut;
+
+void *t_other(void* arg) {
+  g = 17; //RACE
+
+  pthread_mutex_lock(&mut);
+  i = 7; //NORACE
+  pthread_mutex_unlock(&mut);
+}
+
+void nesting() {
+  h = 5; //NORACE
+}
+
+void fun() {
+  // Even though this is only called inside the once, the accesses in the new thread and the accesses here can happen in parallel
+  // Checks that active is not passed to the created thread, but seen is passed
+  pthread_t tid = pthread_create(&tid, NULL, t_other, NULL);
+  g = 42; //RACE
+
+  h = 8; //NORACE
+  // Active onces get passed to the callee and back to the caller
+  nesting();
+  h = 12; //NORACE
+}
+
+void ifun() {
+  i = 11; //NORACE
+}
+
+void *t_fun(void *arg) {
+  pthread_once(&i_once, ifun);
+  pthread_once(&once, fun);
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  int top;
+
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  pthread_once(&i_once, ifun);
+  pthread_once(&once, fun);
+
+  h = 5; //NORACE
+
+  return 0;
+}
diff --git a/tests/regression/83-once/05-unknown-tid.c b/tests/regression/83-once/05-unknown-tid.c
new file mode 100644
index 0000000000..f6aa7956ba
--- /dev/null
+++ b/tests/regression/83-once/05-unknown-tid.c
@@ -0,0 +1,28 @@
+// PARAM: --set ana.activated[+] pthreadOnce
+#include <pthread.h>
+#include <stdio.h>
+
+int g;
+pthread_once_t once = PTHREAD_ONCE_INIT;
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+
+void fun() {
+  g++; //NORACE
+}
+
+
+void* thread(void* arg) {
+  pthread_once(&once, fun);
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+
+  for(int i=0; i < 100; i++) {
+    // Will receive unknown TID
+    pthread_create(&id, NULL, thread, NULL);
+  }
+
+  return 0;
+}
diff --git a/tests/regression/83-once/06-multiple-inside-once.c b/tests/regression/83-once/06-multiple-inside-once.c
new file mode 100644
index 0000000000..b388c85963
--- /dev/null
+++ b/tests/regression/83-once/06-multiple-inside-once.c
@@ -0,0 +1,27 @@
+// PARAM: --set ana.activated[+] pthreadOnce
+#include <pthread.h>
+#include <stdio.h>
+
+int g;
+pthread_once_t once = PTHREAD_ONCE_INIT;
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+
+void fun() {
+  g++; //NORACE
+  g++; //NORACE
+}
+
+
+void* thread(void* arg) {
+  pthread_once(&once, fun);
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+
+  pthread_create(&id, NULL, thread, NULL);
+  pthread_once(&once, fun);
+
+  return 0;
+}
diff --git a/tests/regression/83-once/07-different-onces.c b/tests/regression/83-once/07-different-onces.c
new file mode 100644
index 0000000000..7e9bf83968
--- /dev/null
+++ b/tests/regression/83-once/07-different-onces.c
@@ -0,0 +1,29 @@
+// PARAM: --set ana.activated[+] pthreadOnce
+// Developer used tow different pthread_once_t variables by mistake
+#include <pthread.h>
+#include <stdio.h>
+
+int g;
+pthread_once_t once = PTHREAD_ONCE_INIT;
+pthread_once_t once1 = PTHREAD_ONCE_INIT;
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+
+void fun() {
+  g++; //RACE!
+  g++; //RACE!
+}
+
+
+void* thread(void* arg) {
+  pthread_once(&once, fun);
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+
+  pthread_create(&id, NULL, thread, NULL);
+  pthread_once(&once1, fun);
+
+  return 0;
+}
diff --git a/tests/regression/83-once/08-pointers.c b/tests/regression/83-once/08-pointers.c
new file mode 100644
index 0000000000..b2df8c6c05
--- /dev/null
+++ b/tests/regression/83-once/08-pointers.c
@@ -0,0 +1,39 @@
+// PARAM: --set ana.activated[+] pthreadOnce
+// Function to be called by once is passed as a pointer
+#include <pthread.h>
+#include <stdio.h>
+
+int g;
+void init0();
+
+void* initp = &init0;
+pthread_once_t once = PTHREAD_ONCE_INIT;
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+
+void init0() {
+  g++; //NORACE
+}
+
+
+void init1() {
+  g++; //NORACE
+}
+
+
+void* thread(void* arg) {
+  pthread_once(&once, initp);
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  int top;
+
+  if(top) { initp = &init1; }
+
+  pthread_create(&id, NULL, thread, NULL);
+
+  pthread_once(&once, initp);
+
+  return 0;
+}
diff --git a/tests/regression/83-once/09-pointers2.c b/tests/regression/83-once/09-pointers2.c
new file mode 100644
index 0000000000..3cf93c19a1
--- /dev/null
+++ b/tests/regression/83-once/09-pointers2.c
@@ -0,0 +1,38 @@
+// PARAM: --set ana.activated[+] pthreadOnce
+// Function to be called by once is passed as a pointer
+#include <pthread.h>
+#include <stdio.h>
+
+int g;
+void init0();
+
+void* initp = &init0;
+pthread_once_t once = PTHREAD_ONCE_INIT;
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+
+void init0() {
+  g++; //NORACE
+}
+
+
+void init1() {
+  g++; //NORACE
+}
+
+
+void* thread(void* arg) {
+  pthread_once(&once, initp);
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  int top;
+
+  pthread_create(&id, NULL, thread, NULL);
+  if(top) { initp = &init1; }
+  pthread_once(&once, initp);
+
+
+  return 0;
+}
diff --git a/tests/regression/83-once/10-pointer-once.c b/tests/regression/83-once/10-pointer-once.c
new file mode 100644
index 0000000000..c074c55994
--- /dev/null
+++ b/tests/regression/83-once/10-pointer-once.c
@@ -0,0 +1,33 @@
+// PARAM: --set ana.activated[+] pthreadOnce
+// pthread_once object is passed as a pointer (and it may change)
+#include <pthread.h>
+#include <stdio.h>
+
+int g;
+void init0();
+
+pthread_once_t* optr;
+pthread_once_t once = PTHREAD_ONCE_INIT;
+pthread_once_t once1 = PTHREAD_ONCE_INIT;
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+
+void init0() {
+  g++; //RACE
+}
+
+
+void* thread(void* arg) {
+  pthread_once(&once, init0);
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  int top;
+
+  pthread_create(&id, NULL, thread, NULL);
+  if(top) { optr = &once1; }
+  pthread_once(optr, init0);
+
+  return 0;
+}
diff --git a/tests/regression/83-once/11-combination.c b/tests/regression/83-once/11-combination.c
new file mode 100644
index 0000000000..f7e943f80c
--- /dev/null
+++ b/tests/regression/83-once/11-combination.c
@@ -0,0 +1,45 @@
+// PARAM: --set ana.activated[+] pthreadOnce --set ana.activated[+] threadJoins --set ana.path_sens[+] threadflag --set ana.base.privatization mutex-meet-tid
+// pthread_once object is passed as a pointer (and it may change)
+#include <pthread.h>
+#include <stdio.h>
+
+int* g;
+pthread_once_t once = PTHREAD_ONCE_INIT;
+pthread_mutex_t mtx;
+
+void init0() {
+  g = malloc(sizeof(int));
+}
+
+
+void* thread(void* arg) {
+  pthread_once(&once, init0);
+
+  pthread_mutex_lock(&mtx);
+  if(g == NULL) {
+    // Will not happen!
+    // Also showing that g is not NULL here requires "Extended Support for pthread once" as explained in appendix C.
+    // It was added manually here so we can show off that at the end we can exclude the in initial value even
+    // though main didn't write
+    exit();
+  }
+  *g = 4711; //NORACE
+  pthread_mutex_unlock(&mtx);
+
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id, id2;
+  int top;
+
+  pthread_create(&id, NULL, thread, NULL);
+  pthread_create(&id2, NULL, thread, NULL);
+
+  pthread_join(id, NULL);
+  pthread_join(id2, NULL);
+
+  *g = 47; //NORACE
+
+  return 0;
+}