diff --git a/.gitignore b/.gitignore
index 99df665304..4c1d89fc10 100644
--- a/.gitignore
+++ b/.gitignore
@@ -58,6 +58,7 @@ goblint.bc.js
 sv-comp/goblint.zip
 
 privPrecCompare*
+apronPrecCompare
 tests/regression/*/run
 
 # csmith
diff --git a/make.sh b/make.sh
index d5167db702..e0f17fbcb6 100755
--- a/make.sh
+++ b/make.sh
@@ -62,6 +62,11 @@ rule() {
       dune build src/privPrecCompare.exe &&
       cp _build/default/src/privPrecCompare.exe privPrecCompare
       chmod +w privPrecCompare
+    ;; apronPrecCompare)
+      eval $(opam config env)
+      dune build src/apronPrecCompare.exe &&
+      cp _build/default/src/apronPrecCompare.exe apronPrecCompare
+      chmod +w apronPrecCompare
     # old rules using ocamlbuild
     ;; ocbnat*)
       ocb -no-plugin $TARGET.native &&
diff --git a/src/analyses/apron/apronAnalysis.apron.ml b/src/analyses/apron/apronAnalysis.apron.ml
index 1a41717c4e..bf93891fe5 100644
--- a/src/analyses/apron/apronAnalysis.apron.ml
+++ b/src/analyses/apron/apronAnalysis.apron.ml
@@ -10,6 +10,7 @@ module SpecFunctor (AD: ApronDomain.S2) (Priv: ApronPriv.S) : Analyses.MCPSpec =
 struct
   include Analyses.DefaultSpec
 
+
   let name () = "apron"
 
   module Priv = Priv(AD)
@@ -19,6 +20,10 @@ struct
 
   open AD
 
+  open ApronPrecCompareUtil
+  (* Result map used for comparison of results *)
+  let results = RH.create 103
+
   let should_join = Priv.should_join
 
   let context fd x =
@@ -378,12 +383,40 @@ struct
       st
 
   let sync ctx reason =
+    (* After the solver is finished, store the results (for later comparison) *)
+    if !GU.postsolving then begin
+      let old_value = RH.find_default results ctx.node (AD.bot ()) in
+      let new_value = AD.join old_value ctx.local.apr in
+      RH.replace results ctx.node new_value;
+    end;
     Priv.sync (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg ctx.local (reason :> [`Normal | `Join | `Return | `Init | `Thread])
 
   let init marshal =
     Priv.init ()
 
+  module OctApron = ApronPrecCompareUtil.OctagonD
+  let store_data file =
+    let convert (m: AD.t RH.t): OctApron.t RH.t =
+      let convert_single (a: AD.t): OctApron.t =
+        let generator = AD.to_lincons_array a in
+        OctApron.of_lincons_array generator
+      in
+      RH.map (fun _ -> convert_single) m
+    in
+    let post_process m =
+      let m = convert m in
+      RH.map (fun _ v -> OctApron.marshal v) m
+    in
+    let results = post_process results in
+    let name = name () ^ "(domain: " ^ (AD.Man.name ()) ^ ", privatization: " ^ (Priv.name ()) ^ ")" in
+    let results: ApronPrecCompareUtil.dump = {marshalled = results; name } in
+    Serialize.marshal results file
+
   let finalize () =
+    let file = GobConfig.get_string "exp.apron.prec-dump" in
+    if file <> "" then begin
+      store_data file
+    end;
     Priv.finalize ()
 end
 
diff --git a/src/analyses/apron/apronPriv.apron.ml b/src/analyses/apron/apronPriv.apron.ml
index 027df9f49a..5b9b3ea009 100644
--- a/src/analyses/apron/apronPriv.apron.ml
+++ b/src/analyses/apron/apronPriv.apron.ml
@@ -18,6 +18,7 @@ module type S =
     module G: Lattice.S
 
     type apron_components_t := ApronDomain.ApronComponents (AD) (D).t
+    val name: unit -> string
     val startstate: unit -> D.t
     val should_join: apron_components_t -> apron_components_t -> bool
 
@@ -46,6 +47,7 @@ struct
   module D = Lattice.Unit
   module G = Lattice.Unit
 
+  let name () = "Dummy"
   let startstate () = ()
   let should_join _ _ = true
 
@@ -120,6 +122,8 @@ struct
     let prot g = make_var (Prot g)
   end
 
+  let name () = "ProtectionBasedPriv"
+
   (** Restrict environment to global invariant variables. *)
   let restrict_global apr =
     AD.remove_filter apr (fun var ->
@@ -318,6 +322,8 @@ struct
 
   module V = ApronDomain.V
 
+  let name () = "PerMutexMeetPriv"
+
   let startstate () = ()
 
   let should_join _ _ = true
@@ -480,6 +486,8 @@ struct
   type apron_components_t =  ApronDomain.ApronComponents (AD) (D).t
   let global_varinfo = RichVarinfo.single ~name:"APRON_GLOBAL"
 
+  let name () = "WriteCenteredPriv"
+
   let startstate () = (W.bot (), P.top ())
 
   let should_join _ _ = true
diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml
index de45a33421..8063869822 100644
--- a/src/analyses/basePriv.ml
+++ b/src/analyses/basePriv.ml
@@ -1418,6 +1418,7 @@ struct
   include Priv
 
   open PrivPrecCompareUtil
+  module LVH = RH
 
   let is_dumping = ref false
   let lvh = LVH.create 113
@@ -1438,7 +1439,7 @@ struct
     (* LVH.iter (fun (l, x) v ->
         ignore (Pretty.printf "%a %a = %a\n" CilType.Location.pretty l d_varinfo x VD.pretty v)
       ) lvh; *)
-    Marshal.output f {name = get_string "exp.privatization"; lvh};
+    Marshal.output f ({name = get_string "exp.privatization"; results = lvh}: result);
     close_out_noerr f
 
   let finalize () =
diff --git a/src/analyses/symbLocks.ml b/src/analyses/symbLocks.ml
index 03000d24c3..dde4ab19ac 100644
--- a/src/analyses/symbLocks.ml
+++ b/src/analyses/symbLocks.ml
@@ -44,7 +44,7 @@ struct
     List.fold_right D.remove_var (fundec.sformals@fundec.slocals) ctx.local
 
   let enter ctx lval f args = [(ctx.local,ctx.local)]
-  let combine ctx lval fexp f args fc st2 = ctx.local
+  let combine ctx lval fexp f args fc st2 = st2
 
   let get_locks e st =
     let add_perel x xs =
diff --git a/src/apronPrecCompare.ml b/src/apronPrecCompare.ml
new file mode 100644
index 0000000000..06acb737ce
--- /dev/null
+++ b/src/apronPrecCompare.ml
@@ -0,0 +1,6 @@
+(* Utility program to compare precision of results of the apron analysis with different privatizations and/or differents apron domains *)
+(* The result files that can be compared here may be created by passing an output file name in "exp.apron.prec-dump" to Goblint *)
+module B = PrecCompare.MakeDump (ApronPrecCompareUtil)
+
+let () =
+  B.main ()
diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml
index 27583169ba..d88cae713a 100644
--- a/src/cdomains/apron/apronDomain.apron.ml
+++ b/src/cdomains/apron/apronDomain.apron.ml
@@ -28,7 +28,7 @@ sig
   type mt
   type t = mt Apron.Manager.t
   val mgr : mt Apron.Manager.t
-  val name : string
+  val name : unit -> string
 end
 
 (** Manager for the Oct domain, i.e. an octagon domain.
@@ -42,7 +42,7 @@ struct
 
   (* Create the manager *)
   let mgr =  Oct.manager_alloc ()
-  let name = "Octagon manager"
+  let name () = "Octagon"
 end
 
 (** Manager for the Polka domain, i.e. a polyhedra domain.
@@ -54,7 +54,7 @@ struct
   type t = mt Manager.t
   (* Create manager that fits to loose polyhedra *)
   let mgr = Polka.manager_alloc_loose ()
-  let name = "Polyhedra Manager"
+  let name () = "Polyhedra"
 end
 
 (** Manager for the Box domain, i.e. an interval domain.
@@ -64,10 +64,10 @@ struct
   type mt = Box.t
   type t = mt Manager.t
   let mgr = Box.manager_alloc ()
-  let name = "Interval Manager"
+  let name () = "Interval"
 end
 
-let priv_manager =
+let manager =
   lazy (
     let options =
       ["octagon", (module OctagonManager: Manager);
@@ -81,7 +81,7 @@ let priv_manager =
   )
 
 let get_manager (): (module Manager) =
-  Lazy.force priv_manager
+  Lazy.force manager
 
 module type Tracked =
 sig
@@ -239,11 +239,28 @@ struct
 
   let copy = A.copy Man.mgr
 
-  let vars d =
+  let vars_as_array d =
     let ivs, fvs = Environment.vars (A.env d) in
     assert (Array.length fvs = 0); (* shouldn't ever contain floats *)
+    ivs
+
+  let vars d =
+    let ivs = vars_as_array d in
     List.of_enum (Array.enum ivs)
 
+  (* marshal type: Abstract0.t and an array of var names *)
+  type marshal = Man.mt Abstract0.t * string array
+
+  let unmarshal ((abstract0, vs): marshal): t =
+    let vars = Array.map Var.of_string vs in
+    (* We do not have real-valued vars, so we pass an empty array in their place. *)
+    let env = Environment.make vars [||] in
+    {abstract0; env}
+
+  let marshal (x: t): marshal =
+    let vars = Array.map Var.to_string (vars_as_array x) in
+    x.abstract0, vars
+
   let mem_var d v = Environment.mem_var (A.env d) v
 
   let add_vars_with nd vs =
@@ -465,6 +482,12 @@ struct
     let earray = Tcons1.array_make (A.env d) 1 in
     Tcons1.array_set earray 0 tcons1;
     A.meet_tcons_array Man.mgr d earray
+
+  let to_lincons_array d =
+    A.to_lincons_array Man.mgr d
+
+  let of_lincons_array (a: Apron.Lincons1.earray) =
+    A.of_lincons_array Man.mgr a.array_env a
 end
 
 
@@ -681,6 +704,8 @@ module DHetero (Man: Manager): SLattice with type t = Man.mt A.t =
 struct
   include DBase (Man)
 
+
+
   let gce (x: Environment.t) (y: Environment.t): Environment.t =
     let (xi, xf) = Environment.vars x in
     (* TODO: check type compatibility *)
@@ -835,7 +860,7 @@ end
 
 type ('a, 'b) aproncomponents_t = { apr : 'a; priv : 'b; } [@@deriving eq, ord, to_yojson]
 
-module D2 (Man: Manager) : S2 =
+module D2 (Man: Manager) : S2 with module Man = Man =
 struct
   include DWithOps (Man) (DHetero (Man))
   module Man = Man
diff --git a/src/cdomains/lockDomain.ml b/src/cdomains/lockDomain.ml
index ec12f41a5e..ab7835f94d 100644
--- a/src/cdomains/lockDomain.ml
+++ b/src/cdomains/lockDomain.ml
@@ -140,7 +140,11 @@ struct
     let no_casts = S.map Expcompare.stripCastsDeepForPtrArith (eq_set ask e) in
     let addrs = S.filter (function AddrOf _ -> true | _ -> false) no_casts in
     S.union addrs st
-  let remove ask e st = S.diff st (eq_set ask e)
+  let remove ask e st = 
+    (* TODO: Removing based on must-equality sets is not sound! *)
+    let no_casts = S.map Expcompare.stripCastsDeepForPtrArith (eq_set ask e) in
+    let addrs = S.filter (function AddrOf _ -> true | _ -> false) no_casts in
+    S.diff st addrs
   let remove_var v st = S.filter (fun x -> not (Exp.contains_var v x)) st
 
   let kill_lval (host,offset) st =
diff --git a/src/dune b/src/dune
index 593e8d85db..cf61a03b9f 100644
--- a/src/dune
+++ b/src/dune
@@ -12,7 +12,7 @@
   (name goblint_lib)
   (public_name goblint.lib)
   (wrapped false)
-  (modules :standard \ goblint mainarinc maindomaintest mainspec privPrecCompare)
+  (modules :standard \ goblint mainarinc maindomaintest mainspec privPrecCompare apronPrecCompare)
   (libraries goblint-cil.all-features batteries.unthreaded zarith_stubs_js qcheck-core.runner dune-site
     ; Conditionally compile based on whether apron optional dependency is installed or not.
     ; Alternative dependencies seem like the only way to optionally depend on optional dependencies.
@@ -21,6 +21,10 @@
       (apron apron.octMPQ apron.boxMPQ apron.polkaMPQ -> apronDomain.apron.ml)
       (-> apronDomain.no-apron.ml)
     )
+    (select apronPrecCompareUtil.ml from
+      (apron -> apronPrecCompareUtil.apron.ml)
+      (-> apronPrecCompareUtil.no-apron.ml)
+    )
     (select apronAnalysis.ml from
       (apron -> apronAnalysis.apron.ml)
       (-> apronAnalysis.no-apron.ml)
@@ -44,6 +48,7 @@
 ; TODO: Remove workaround with dune 3.0, where this should get fixed.
 (copy_files cdomains/apron/*.ml)
 (copy_files analyses/apron/*.ml)
+(copy_files util/apron/*.ml)
 (copy_files witness/z3/*.ml)
 
 (executables
@@ -64,6 +69,14 @@
   (flags :standard -linkall)
 )
 
+(executable
+  (name apronPrecCompare)
+  (modules apronPrecCompare)
+  (libraries goblint.lib)
+  (preprocess (staged_pps ppx_deriving.std ppx_deriving_yojson ppx_distr_guards ocaml-monadic))
+  (flags :standard -linkall)
+)
+
 (rule
   (targets goblint.ml config.ml version.ml)
   (mode fallback) ; do nothing if all targets already exist
diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
index 22caa840c3..0fbd95ecfe 100644
--- a/src/framework/analyses.ml
+++ b/src/framework/analyses.ml
@@ -238,7 +238,7 @@ struct
       let p_list p f xs = BatList.print ~first:"[\n  " ~last:"\n]" ~sep:",\n  " p f xs in
       (*let p_kv f (k,p,v) = fprintf f "\"%s\": %a" k p v in*)
       (*let p_obj f xs = BatList.print ~first:"{\n  " ~last:"\n}" ~sep:",\n  " p_kv xs in*)
-      let p_node f n = BatPrintf.fprintf f "%s" (Node.show_id n) in
+      let p_node f n = BatPrintf.fprintf f "\"%s\"" (Node.show_id n) in
       let p_fun f x = fprintf f "{\n  \"name\": \"%s\",\n  \"nodes\": %a\n}" x (p_list p_node) (SH.find_all funs2node x) in
       (*let p_fun f x = p_obj f [ "name", BatString.print, x; "nodes", p_list p_node, SH.find_all funs2node x ] in*)
       let p_file f x = fprintf f "{\n  \"name\": \"%s\",\n  \"path\": \"%s\",\n  \"functions\": %a\n}" (Filename.basename x) x (p_list p_fun) (SH.find_all file2funs x) in
diff --git a/src/privPrecCompare.ml b/src/privPrecCompare.ml
index 20c412e65c..59f583c828 100644
--- a/src/privPrecCompare.ml
+++ b/src/privPrecCompare.ml
@@ -1,45 +1,6 @@
-open! Defaults (* CircInterval / Enums / ... need initialized conf *)
-open! Batteries
-open Prelude
-open Ana
-open PrivPrecCompareUtil
-open PrecCompare
-
-module VD = BaseDomain.VD
-
-let load filename =
-  let f = open_in_bin filename in
-  let dump: dump = Marshal.from_channel f in
-  close_in_noerr f;
-  dump
-
-module CompareDump = MakeHashtbl (LV) (VD) (LVH)
-
-let compare_dumps {name = name1; lvh = lvh1} {name = name2; lvh = lvh2} =
-  CompareDump.compare ~name1 lvh1 ~name2 lvh2
-
-let count_locations dumps =
-  let module LH = Hashtbl.Make (CilType.Location) in
-  let locations = LH.create 113 in
-  let location_vars = LVH.create 113 in
-  List.iter (fun {lvh; _} ->
-      LVH.iter (fun (l, x) _ ->
-          LH.replace locations l ();
-          LVH.replace location_vars (l, x) ()
-        ) lvh
-    ) dumps;
-  (LH.length locations, LVH.length location_vars)
+(* Utility program to compare precision of results of the base analysis with different privatizations *)
+(* The result files that can be compared here may be created by passing an output file name in "exp.priv-prec-dump" to Goblint *)
+module A = PrecCompare.MakeDump (PrivPrecCompareUtil)
 
 let () =
-  Cil.initCIL (); (* ValueDomain.Compound.leq depends on ptrdiffType initialization *)
-  let filenames = List.tl (Array.to_list Sys.argv) in
-  let dumps = List.map load filenames in
-  let (locations_count, location_vars_count) = count_locations dumps in
-  let i_dumps = List.mapi (fun i dump -> (i, dump)) dumps in
-  List.cartesian_product i_dumps i_dumps
-  (* |> List.filter (fun ((i1, _), (i2, _)) -> i1 < i2) *)
-  |> List.filter (fun ((i1, _), (i2, _)) -> i1 <> i2)
-  |> List.map (Tuple2.map snd snd)
-  |> List.map (uncurry compare_dumps)
-  |> List.iter (fun (_, msg) -> ignore (Pretty.printf "%t\n" (fun () -> msg)));
-  ignore (Pretty.printf "\nTotal locations: %d\nTotal location variables: %d\n" locations_count location_vars_count)
\ No newline at end of file
+  A.main ()
diff --git a/src/util/apron/apronPrecCompareUtil.apron.ml b/src/util/apron/apronPrecCompareUtil.apron.ml
new file mode 100644
index 0000000000..11792cb431
--- /dev/null
+++ b/src/util/apron/apronPrecCompareUtil.apron.ml
@@ -0,0 +1,28 @@
+open PrecCompareUtil
+open ApronDomain
+
+module MyNode =
+struct
+  include Node
+  (* Override the name to "nodes", as plural fits better in the output format of PrePrivPrecCompare *)
+  let name () = "nodes"
+  let to_location n = Node.location n
+end
+
+(* Currently serialization of Apron results only works for octagons. *)
+module OctagonD = ApronDomain.D2 (ApronDomain.OctagonManager)
+module Util =
+struct
+  include Util (MyNode) (OctagonD)
+  type marshal = (OctagonManager.mt Apron.Abstract0.t * string array) RH.t
+  type dump = marshal dump_gen
+  type result = Dom.t RH.t result_gen
+
+  let init () =
+    Apron.Manager.set_deserialize OctagonManager.mgr
+
+  let unmarshal (m: marshal): Dom.t RH.t =
+    RH.map (fun _ -> OctagonD.unmarshal) m
+end
+
+include Util
diff --git a/src/util/apron/apronPrecCompareUtil.no-apron.ml b/src/util/apron/apronPrecCompareUtil.no-apron.ml
new file mode 100644
index 0000000000..76409641dd
--- /dev/null
+++ b/src/util/apron/apronPrecCompareUtil.no-apron.ml
@@ -0,0 +1,3 @@
+(* This module is empty on purpose. It serves only as an alternative dependency
+   in cases where the actual apronPrecComapreUtil can't be used because of a missing library.
+   It was added because we don't want to fully depend on Apron. *)
diff --git a/src/util/apron/dune b/src/util/apron/dune
new file mode 100644
index 0000000000..272864089a
--- /dev/null
+++ b/src/util/apron/dune
@@ -0,0 +1,3 @@
+; Workaround for workaround for alternative dependencies with unqualified subdirs.
+; copy_files causes "dependency cycle that does not involve any files" otherwise
+(include_subdirs no)
diff --git a/src/util/defaults.ml b/src/util/defaults.ml
index 6eef5e0d04..135f7745f6 100644
--- a/src/util/defaults.ml
+++ b/src/util/defaults.ml
@@ -185,6 +185,7 @@ let _ = ()
       ; reg Experimental "exp.priv-prec-dump"    "''"    "File to dump privatization precision data to."
       ; reg Experimental "exp.priv-distr-init"   "false"  "Distribute global initializations to all global invariants for more consistent widening dynamics."
       ; reg Experimental "exp.apron.privatization" "'mutex-meet'" "Which Apron privatization to use? dummy/protection/protection-path/mutex-meet"
+      ; reg Experimental "exp.apron.prec-dump"    "''"    "File to dump apron precision data to."
       ; reg Experimental "exp.cfgdot"            "false" "Output CFG to dot files"
       ; reg Experimental "exp.mincfg"            "false" "Try to minimize the number of CFG nodes."
       ; reg Experimental "exp.earlyglobs"        "false" "Side-effecting of globals right after initialization."
diff --git a/src/util/precCompare.ml b/src/util/precCompare.ml
index cc74ce9375..52397e37eb 100644
--- a/src/util/precCompare.ml
+++ b/src/util/precCompare.ml
@@ -85,3 +85,48 @@ struct
     let msg = Pretty.dprintf "%s %s %s    (more precise: %d, less precise: %d, total: %d)" name1 (Comparison.to_string_infix c) name2 m l (KH.length kh) in
     (c, msg)
 end
+
+module MakeDump (Util: PrecCompareUtil.S) =
+struct
+  open! Defaults (* CircInterval / Enums / ... need initialized conf *)
+  open! Batteries
+  open Util
+
+  let load filename =
+    let f = open_in_bin filename in
+    let dump: dump = Marshal.from_channel f in
+    let dump: result = {name = dump.name; results = unmarshal dump.marshalled } in
+    close_in_noerr f;
+    dump
+
+  module CompareDump = MakeHashtbl (Key) (Dom) (RH)
+
+  let compare_dumps ({name = name1; results = lvh1}: result) ({name = name2; results = lvh2}: result) =
+    CompareDump.compare ~name1 lvh1 ~name2 lvh2
+
+  let count_locations (dumps: result list) =
+    let module LH = Hashtbl.Make (CilType.Location) in
+    let locations = LH.create 113 in
+    let location_vars = RH.create 113 in
+    List.iter (fun ({results; _}: result) ->
+        RH.iter (fun x _ ->
+            LH.replace locations (Key.to_location x) ();
+            RH.replace location_vars x ()
+          ) results
+      ) dumps;
+    (LH.length locations, RH.length location_vars)
+
+  let main () =
+    Util.init ();
+    let filenames = List.tl (Array.to_list Sys.argv) in
+    let dumps = List.map load filenames in
+    let (locations_count, location_vars_count) = count_locations dumps in
+    let i_dumps = List.mapi (fun i dump -> (i, dump)) dumps in
+    List.cartesian_product i_dumps i_dumps
+    (* |> List.filter (fun ((i1, _), (i2, _)) -> i1 < i2) *)
+    |> List.filter (fun ((i1, _), (i2, _)) -> i1 <> i2)
+    |> List.map (Tuple2.map snd snd)
+    |> List.map (uncurry compare_dumps)
+    |> List.iter (fun (_, msg) -> ignore (Pretty.printf "%t\n" (fun () -> msg)));
+    ignore (Pretty.printf "\nTotal locations: %d\nTotal %s: %d\n" locations_count (Key.name ()) location_vars_count)
+end
diff --git a/src/util/precCompareUtil.ml b/src/util/precCompareUtil.ml
new file mode 100644
index 0000000000..a8f0908f01
--- /dev/null
+++ b/src/util/precCompareUtil.ml
@@ -0,0 +1,62 @@
+open Prelude
+
+
+(** A printable, where each element is related to one location.
+    Multiple elements might be related to the same location. *)
+module type LocalizedPrintable =
+sig
+  include Printable.S
+  val to_location: t -> CilType.Location.t
+end
+
+type 'a dump_gen = {
+  name: string;
+  marshalled: 'a;
+}
+
+type 'a result_gen = {
+  name: string;
+  results: 'a;
+}
+
+module type R =
+sig
+  module Key: LocalizedPrintable
+  module Dom: Lattice.S
+
+  (** Module for the result hash map *)
+  module RH : Hashtbl.S with type key = Key.t
+
+  (** Type to which the result hashmap is actually convered before storing it to disc *)
+  type marshal
+
+  (** Wrapper of marhshal type, together with a name for the analysis + privatization combination *)
+  type dump = marshal dump_gen
+
+  (** Type of the actually usable result. To be obtained from the dump via the unmarshal function below  *)
+  type result = Dom.t RH.t result_gen
+
+  (** Maps the marshalled version of the result hashmap back to a usable version *)
+  val unmarshal: marshal -> Dom.t RH.t
+end
+
+module type S =
+sig
+  include R
+  val init: unit -> unit
+end
+
+module Util (Key: LocalizedPrintable) (Dom: Lattice.S) : R with module Key = Key and module Dom = Dom =
+struct
+  module Key = Key
+  module Dom = Dom
+  (* module for result hashmap *)
+  module RH = Hashtbl.Make (Key)
+
+  type marshal = Dom.t RH.t
+  type dump = marshal dump_gen
+  type result = Dom.t RH.t result_gen
+
+  (* Leave loaded value untouched by default *)
+  let unmarshal x = x
+end
diff --git a/src/util/privPrecCompareUtil.ml b/src/util/privPrecCompareUtil.ml
index e5558c1b8d..0d4d40f469 100644
--- a/src/util/privPrecCompareUtil.ml
+++ b/src/util/privPrecCompareUtil.ml
@@ -1,14 +1,20 @@
 open Prelude
+open PrecCompareUtil
 
 module LV =
 struct
   include Printable.Prod (CilType.Location) (Basetype.Variables)
+  let name () = "location variables"
+  type marshal = t
   let pretty () (l, v) = Pretty.dprintf "%a %a" CilType.Location.pretty l Basetype.Variables.pretty v
+  let to_location = fst
 end
-module LVH = Hashtbl.Make (Printable.Prod (CilType.Location) (Basetype.Variables))
-module VD = BaseDomain.VD
 
-type dump = {
-  name: string;
-  lvh: VD.t LVH.t;
-}
\ No newline at end of file
+module Util =
+struct
+  include Util (LV) (BaseDomain.VD)
+  let init () =
+    Cil.initCIL (); (* ValueDomain.Compound.leq depends on ptrdiffType initialization *)
+end
+
+include Util
diff --git a/tests/regression/06-symbeq/26-symb_lockfuns.c b/tests/regression/06-symbeq/26-symb_lockfuns.c
new file mode 100644
index 0000000000..d840c1803a
--- /dev/null
+++ b/tests/regression/06-symbeq/26-symb_lockfuns.c
@@ -0,0 +1,29 @@
+// PARAM: --set ana.activated[+] "'var_eq'"  --set ana.activated[+] "'symb_locks'"
+#include <stdlib.h>
+#include <pthread.h>
+
+typedef struct { int myint; pthread_mutex_t mymutex; } mystruct;
+
+void lock(mystruct *s) { pthread_mutex_lock(&s->mymutex); }
+void unlock(mystruct *s) { pthread_mutex_unlock(&s->mymutex); }
+
+void *foo(void *arg) {
+  mystruct *s = (mystruct *) arg;
+
+  lock(s);
+  s->myint=s->myint+1;
+  unlock(s);
+
+  return NULL;
+}
+
+int main() {
+  mystruct *s = (mystruct *) malloc(sizeof(*s));
+  pthread_mutex_init(&s->mymutex, NULL);
+
+  pthread_t id1, id2;
+  pthread_create(&id1, NULL, foo, s);
+  pthread_create(&id2, NULL, foo, s);
+  pthread_join(id1, NULL);
+  pthread_join(id2, NULL);
+}
diff --git a/tests/regression/06-symbeq/27-symb_no_lockfuns.c b/tests/regression/06-symbeq/27-symb_no_lockfuns.c
new file mode 100644
index 0000000000..1c0277410c
--- /dev/null
+++ b/tests/regression/06-symbeq/27-symb_no_lockfuns.c
@@ -0,0 +1,26 @@
+// PARAM: --set ana.activated[+] "'var_eq'"  --set ana.activated[+] "'symb_locks'"
+#include <stdlib.h>
+#include <pthread.h>
+
+typedef struct { int myint; pthread_mutex_t mymutex; } mystruct;
+
+void *foo(void *arg) {
+  mystruct *s = (mystruct *) arg;
+
+  pthread_mutex_lock(&s->mymutex);
+  s->myint=s->myint+1;
+  pthread_mutex_unlock(&s->mymutex);
+
+  return NULL;
+}
+
+int main() {
+  mystruct *s = (mystruct *) malloc(sizeof(*s));
+  pthread_mutex_init(&s->mymutex, NULL);
+
+  pthread_t id1, id2;
+  pthread_create(&id1, NULL, foo, s);
+  pthread_create(&id2, NULL, foo, s);
+  pthread_join(id1, NULL);
+  pthread_join(id2, NULL);
+}
diff --git a/tests/regression/06-symbeq/28-symb_lockset_unsound.c b/tests/regression/06-symbeq/28-symb_lockset_unsound.c
new file mode 100644
index 0000000000..ff752a8ab4
--- /dev/null
+++ b/tests/regression/06-symbeq/28-symb_lockset_unsound.c
@@ -0,0 +1,28 @@
+// PARAM: --set ana.activated[+] "'var_eq'"  --set ana.activated[+] "'symb_locks'"
+#include <stdlib.h>
+#include <pthread.h>
+
+typedef struct { int myint; pthread_mutex_t mymutex; } mystruct;
+
+
+void *foo(void *arg) {
+  mystruct *p1 = (mystruct *) arg;
+  mystruct *p2 = (mystruct *) arg;
+
+  pthread_mutex_lock(&p1->mymutex);
+  pthread_mutex_unlock(&p2->mymutex);
+  p1->myint++; // RACE
+
+  return NULL;
+}
+
+int main() {
+  mystruct *s = (mystruct *) malloc(sizeof(*s));
+  pthread_mutex_init(&s->mymutex, NULL);
+
+  pthread_t id1, id2;
+  pthread_create(&id1, NULL, foo, s);
+  pthread_create(&id2, NULL, foo, s);
+  pthread_join(id1, NULL);
+  pthread_join(id2, NULL);
+}
diff --git a/tests/regression/06-symbeq/29-symb_lockfun_unsound.c b/tests/regression/06-symbeq/29-symb_lockfun_unsound.c
new file mode 100644
index 0000000000..afaee456b0
--- /dev/null
+++ b/tests/regression/06-symbeq/29-symb_lockfun_unsound.c
@@ -0,0 +1,30 @@
+// PARAM: --set ana.activated[+] "'var_eq'"  --set ana.activated[+] "'symb_locks'"
+#include <stdlib.h>
+#include <pthread.h>
+
+typedef struct { int myint; pthread_mutex_t mymutex; } mystruct;
+
+void unlock(mystruct *s) {
+  pthread_mutex_unlock(&s->mymutex); 
+}
+
+void *foo(void *arg) {
+  mystruct *s = (mystruct *) arg;
+
+  pthread_mutex_lock(&s->mymutex);
+  unlock(s);
+  s->myint=0; // RACE
+
+  return NULL;
+}
+
+int main() {
+  mystruct *s = (mystruct *) malloc(sizeof(*s));
+  pthread_mutex_init(&s->mymutex, NULL);
+
+  pthread_t id1, id2;
+  pthread_create(&id1, NULL, foo, s);
+  pthread_create(&id2, NULL, foo, s);
+  pthread_join(id1, NULL);
+  pthread_join(id2, NULL);
+}
diff --git a/tests/regression/06-symbeq/30-symb_lockset_mayunlock.c b/tests/regression/06-symbeq/30-symb_lockset_mayunlock.c
new file mode 100644
index 0000000000..889312dc82
--- /dev/null
+++ b/tests/regression/06-symbeq/30-symb_lockset_mayunlock.c
@@ -0,0 +1,30 @@
+// PARAM: --set ana.activated[+] "'var_eq'"  --set ana.activated[+] "'symb_locks'"
+#include <stdlib.h>
+#include <pthread.h>
+
+extern int __VERIFIER_nondet_int();
+typedef struct { int myint; pthread_mutex_t mymutex; } mystruct;
+
+
+void *foo(void *arg) {
+  mystruct *p1 = (mystruct *) arg;
+  mystruct *p2 = (mystruct *) arg;
+
+  pthread_mutex_lock(&p1->mymutex);
+  if (__VERIFIER_nondet_int()) p2 = NULL;
+  pthread_mutex_unlock(&p2->mymutex);
+  p1->myint++; // TODO RACE
+
+  return NULL;
+}
+
+int main() {
+  mystruct *s = (mystruct *) malloc(sizeof(*s));
+  pthread_mutex_init(&s->mymutex, NULL);
+
+  pthread_t id1, id2;
+  pthread_create(&id1, NULL, foo, s);
+  pthread_create(&id2, NULL, foo, s);
+  pthread_join(id1, NULL);
+  pthread_join(id2, NULL);
+}
diff --git a/tests/regression/13-privatized/67-pthread_cond_wait.c b/tests/regression/13-privatized/67-pthread_cond_wait.c
index ac867cb42a..0d4c8f072e 100644
--- a/tests/regression/13-privatized/67-pthread_cond_wait.c
+++ b/tests/regression/13-privatized/67-pthread_cond_wait.c
@@ -12,7 +12,8 @@ void* f1(void* ptr) {
     pthread_mutex_lock(&mut);
     g = 1;
     pthread_cond_wait(&cond,&mut);
-    assert(g == 0); // TODO (no cond-flow support)
+    assert(g == 0); //UNKNOWN!
+    assert(g != 1); //UNKNOWN!
     printf("g is %i", g);
     g = 0;
     pthread_mutex_unlock(&mut);