diff --git a/.github/workflows/options.yml b/.github/workflows/options.yml
index 94c49e4bf6..7ef8b6929e 100644
--- a/.github/workflows/options.yml
+++ b/.github/workflows/options.yml
@@ -26,10 +26,10 @@ jobs:
         run: npm install -g ajv-cli
 
       - name: Migrate schema # https://github.com/ajv-validator/ajv-cli/issues/199
-        run: ajv migrate -s src/common/util/options.schema.json
+        run: ajv migrate -s src/config/options.schema.json
 
       - name: Validate conf
-        run: ajv validate -s src/common/util/options.schema.json -d "conf/**/*.json"
+        run: ajv validate -s src/config/options.schema.json -d "conf/**/*.json"
 
       - name: Validate incremental tests
-        run: ajv validate -s src/common/util/options.schema.json -d "tests/incremental/*/*.json"
+        run: ajv validate -s src/config/options.schema.json -d "tests/incremental/*/*.json"
diff --git a/.readthedocs.yaml b/.readthedocs.yaml
index 08044d195c..22f9c86121 100644
--- a/.readthedocs.yaml
+++ b/.readthedocs.yaml
@@ -20,4 +20,4 @@ build:
       - pip install json-schema-for-humans
     post_build:
       - mkdir _readthedocs/html/jsfh/
-      - generate-schema-doc --config-file jsfh.yml src/common/util/options.schema.json _readthedocs/html/jsfh/
+      - generate-schema-doc --config-file jsfh.yml src/config/options.schema.json _readthedocs/html/jsfh/
diff --git a/docs/user-guide/configuring.md b/docs/user-guide/configuring.md
index 9a32a14a4c..cae57fc8cd 100644
--- a/docs/user-guide/configuring.md
+++ b/docs/user-guide/configuring.md
@@ -24,7 +24,7 @@ In `.vscode/settings.json` add the following:
                 "/conf/*.json",
                 "/tests/incremental/*/*.json"
             ],
-            "url": "/src/common/util/options.schema.json"
+            "url": "/src/config/options.schema.json"
         }
     ]
 }
diff --git a/gobview b/gobview
index d4eb66b9eb..3de13d7412 160000
--- a/gobview
+++ b/gobview
@@ -1 +1 @@
-Subproject commit d4eb66b9eb277349a75141cb01899dbab9d3ef5d
+Subproject commit 3de13d74124ab7bc30d8be299f02570d8f498b84
diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml
index e42cd5a309..f9a4a22f44 100644
--- a/src/analyses/basePriv.ml
+++ b/src/analyses/basePriv.ml
@@ -230,7 +230,7 @@ struct
       CPA.find x st.cpa
   (* let read_global ask getg cpa x =
      let (cpa', v) as r = read_global ask getg cpa x in
-     ignore (Pretty.printf "READ GLOBAL %a (%a, %B) = %a\n" CilType.Varinfo.pretty x CilType.Location.pretty !Tracing.current_loc (is_unprotected ask x) VD.pretty v);
+     ignore (Pretty.printf "READ GLOBAL %a (%a, %B) = %a\n" CilType.Varinfo.pretty x CilType.Location.pretty !Goblint_tracing.current_loc (is_unprotected ask x) VD.pretty v);
      r *)
   let write_global ?(invariant=false) ask getg sideg (st: BaseComponents (D).t) x v =
     let cpa' = CPA.add x v st.cpa in
@@ -1665,7 +1665,7 @@ struct
   let read_global ask getg st x =
     let v = Priv.read_global ask getg st x in
     if !AnalysisState.postsolving && !is_dumping then
-      LVH.modify_def (VD.bot ()) (!Tracing.current_loc, x) (VD.join v) lvh;
+      LVH.modify_def (VD.bot ()) (!Goblint_tracing.current_loc, x) (VD.join v) lvh;
     v
 
   let dump () =
diff --git a/src/analyses/extractPthread.ml b/src/analyses/extractPthread.ml
index f084a21edb..8412a65683 100644
--- a/src/analyses/extractPthread.ml
+++ b/src/analyses/extractPthread.ml
@@ -220,7 +220,7 @@ module Tbls = struct
       let make_new_val table k =
         (* TODO: all same key occurrences instead *)
         let line = -5 - all_keys_count table in
-        let loc = { !Tracing.current_loc with line } in
+        let loc = { !Goblint_tracing.current_loc with line } in
         MyCFG.Statement
           { (mkStmtOneInstr @@ Set (var dummyFunDec.svar, zero, loc, loc)) with
             sid = new_sid ()
diff --git a/src/analyses/mCPRegistry.ml b/src/analyses/mCPRegistry.ml
index 810da827ff..5d0174d44c 100644
--- a/src/analyses/mCPRegistry.ml
+++ b/src/analyses/mCPRegistry.ml
@@ -215,7 +215,7 @@ struct
 
   let arbitrary () =
     let arbs = map (fun (n, (module D: Printable.S)) -> QCheck.map ~rev:(fun (_, o) -> obj o) (fun x -> (n, repr x)) @@ D.arbitrary ()) @@ domain_list () in
-    MyCheck.Arbitrary.sequence arbs
+    GobQCheck.Arbitrary.sequence arbs
 
   let relift = unop_map (fun (module S: Printable.S) x -> Obj.repr (S.relift (Obj.obj x)))
 end
diff --git a/src/analyses/stackTrace.ml b/src/analyses/stackTrace.ml
index 3c3bd56640..dd2cedf871 100644
--- a/src/analyses/stackTrace.ml
+++ b/src/analyses/stackTrace.ml
@@ -36,7 +36,7 @@ struct
   (* transfer functions *)
 
   let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
-    [ctx.local, D.push !Tracing.current_loc ctx.local]
+    [ctx.local, D.push !Goblint_tracing.current_loc ctx.local]
 
   let combine_env ctx lval fexp f args fc au f_ask =
     ctx.local (* keep local as opposed to IdentitySpec *)
@@ -46,7 +46,7 @@ struct
   let exitstate  v = D.top ()
 
   let threadenter ctx ~multiple lval f args =
-    [D.push !Tracing.current_loc ctx.local]
+    [D.push !Goblint_tracing.current_loc ctx.local]
 end
 
 
diff --git a/src/cdomains/intDomain.ml b/src/cdomains/intDomain.ml
index 054030017f..5d5174744f 100644
--- a/src/cdomains/intDomain.ml
+++ b/src/cdomains/intDomain.ml
@@ -996,12 +996,12 @@ struct
 
   let arbitrary ik =
     let open QCheck.Iter in
-    (* let int_arb = QCheck.map ~rev:Ints_t.to_bigint Ints_t.of_bigint MyCheck.Arbitrary.big_int in *)
+    (* let int_arb = QCheck.map ~rev:Ints_t.to_bigint Ints_t.of_bigint GobQCheck.Arbitrary.big_int in *)
     (* TODO: apparently bigints are really slow compared to int64 for domaintest *)
-    let int_arb = QCheck.map ~rev:Ints_t.to_int64 Ints_t.of_int64 MyCheck.Arbitrary.int64 in
+    let int_arb = QCheck.map ~rev:Ints_t.to_int64 Ints_t.of_int64 GobQCheck.Arbitrary.int64 in
     let pair_arb = QCheck.pair int_arb int_arb in
     let shrink = function
-      | Some (l, u) -> (return None) <+> (MyCheck.shrink pair_arb (l, u) >|= of_interval ik >|= fst)
+      | Some (l, u) -> (return None) <+> (GobQCheck.shrink pair_arb (l, u) >|= of_interval ik >|= fst)
       | None -> empty
     in
     QCheck.(set_shrink shrink @@ set_print show @@ map (*~rev:BatOption.get*) (fun x -> of_interval ik x |> fst ) pair_arb)
@@ -1601,13 +1601,13 @@ struct
 
   let arbitrary ik =
     let open QCheck.Iter in
-    (* let int_arb = QCheck.map ~rev:Ints_t.to_bigint Ints_t.of_bigint MyCheck.Arbitrary.big_int in *)
+    (* let int_arb = QCheck.map ~rev:Ints_t.to_bigint Ints_t.of_bigint GobQCheck.Arbitrary.big_int in *)
     (* TODO: apparently bigints are really slow compared to int64 for domaintest *)
-    let int_arb = QCheck.map ~rev:Ints_t.to_int64 Ints_t.of_int64 MyCheck.Arbitrary.int64 in
+    let int_arb = QCheck.map ~rev:Ints_t.to_int64 Ints_t.of_int64 GobQCheck.Arbitrary.int64 in
     let pair_arb = QCheck.pair int_arb int_arb in
     let list_pair_arb = QCheck.small_list pair_arb in
     let canonize_randomly_generated_list = (fun x -> norm_intvs ik  x |> fst) in
-    let shrink xs = MyCheck.shrink list_pair_arb xs >|= canonize_randomly_generated_list
+    let shrink xs = GobQCheck.shrink list_pair_arb xs >|= canonize_randomly_generated_list
     in QCheck.(set_shrink shrink @@ set_print show @@ map (*~rev:BatOption.get*) canonize_randomly_generated_list list_pair_arb)
 end
 
@@ -1695,7 +1695,7 @@ struct
   let logand n1 n2 = of_bool ((to_bool' n1) && (to_bool' n2))
   let logor  n1 n2 = of_bool ((to_bool' n1) || (to_bool' n2))
   let cast_to ?torg t x =  failwith @@ "Cast_to not implemented for " ^ (name ()) ^ "."
-  let arbitrary ik = QCheck.map ~rev:Ints_t.to_int64 Ints_t.of_int64 MyCheck.Arbitrary.int64 (* TODO: use ikind *)
+  let arbitrary ik = QCheck.map ~rev:Ints_t.to_int64 Ints_t.of_int64 GobQCheck.Arbitrary.int64 (* TODO: use ikind *)
   let invariant _ _ = Invariant.none (* TODO *)
 end
 
@@ -2402,8 +2402,8 @@ struct
     let excluded s = from_excl ik s in
     let definite x = of_int ik x in
     let shrink = function
-      | `Excluded (s, _) -> MyCheck.shrink (S.arbitrary ()) s >|= excluded (* S TODO: possibly shrink excluded to definite *)
-      | `Definite x -> (return `Bot) <+> (MyCheck.shrink (BigInt.arbitrary ()) x >|= definite)
+      | `Excluded (s, _) -> GobQCheck.shrink (S.arbitrary ()) s >|= excluded (* S TODO: possibly shrink excluded to definite *)
+      | `Definite x -> (return `Bot) <+> (GobQCheck.shrink (BigInt.arbitrary ()) x >|= definite)
       | `Bot -> empty
     in
     QCheck.frequency ~shrink ~print:show [
@@ -2816,8 +2816,8 @@ module Enums : S with type int_t = BigInt.t = struct
     let neg s = of_excl_list ik (BISet.elements s) in
     let pos s = norm ik (Inc s) in
     let shrink = function
-      | Exc (s, _) -> MyCheck.shrink (BISet.arbitrary ()) s >|= neg (* S TODO: possibly shrink neg to pos *)
-      | Inc s -> MyCheck.shrink (BISet.arbitrary ()) s >|= pos
+      | Exc (s, _) -> GobQCheck.shrink (BISet.arbitrary ()) s >|= neg (* S TODO: possibly shrink neg to pos *)
+      | Inc s -> GobQCheck.shrink (BISet.arbitrary ()) s >|= pos
     in
     QCheck.frequency ~shrink ~print:show [
       20, QCheck.map neg (BISet.arbitrary ());
@@ -3307,7 +3307,7 @@ struct
 
   let arbitrary ik =
     let open QCheck in
-    let int_arb = map ~rev:Ints_t.to_int64 Ints_t.of_int64 MyCheck.Arbitrary.int64 in
+    let int_arb = map ~rev:Ints_t.to_int64 Ints_t.of_int64 GobQCheck.Arbitrary.int64 in
     let cong_arb = pair int_arb int_arb in
     let of_pair ik p = normalize ik (Some p) in
     let to_pair = Option.get in
diff --git a/src/cdomains/offset.ml b/src/cdomains/offset.ml
index eca85e08a4..52cfe9eb41 100644
--- a/src/cdomains/offset.ml
+++ b/src/cdomains/offset.ml
@@ -22,7 +22,7 @@ struct
     include CilType.Exp
     let name () = "exp index"
 
-    let any = CastE (TInt (Cilfacade.ptrdiff_ikind (), []), mkString "any_index")
+    let any = Cilfacade.any_index_exp
     let all = CastE (TInt (Cilfacade.ptrdiff_ikind (), []), mkString "all_index")
 
     (* Override output *)
diff --git a/src/cdomains/valueDomain.ml b/src/cdomains/valueDomain.ml
index cba4b04c18..e6f3122cb0 100644
--- a/src/cdomains/valueDomain.ml
+++ b/src/cdomains/valueDomain.ml
@@ -502,7 +502,7 @@ struct
 
   let warn_type op x y =
     if GobConfig.get_bool "dbg.verbose" then
-      ignore @@ printf "warn_type %s: incomparable abstr. values %s and %s at %a: %a and %a\n" op (tag_name (x:t)) (tag_name (y:t)) CilType.Location.pretty !Tracing.current_loc pretty x pretty y
+      ignore @@ printf "warn_type %s: incomparable abstr. values %s and %s at %a: %a and %a\n" op (tag_name (x:t)) (tag_name (y:t)) CilType.Location.pretty !Goblint_tracing.current_loc pretty x pretty y
 
   let rec leq x y =
     match (x,y) with
diff --git a/src/common/cdomains/basetype.ml b/src/common/cdomains/basetype.ml
index 55b5dbde07..1b846309aa 100644
--- a/src/common/cdomains/basetype.ml
+++ b/src/common/cdomains/basetype.ml
@@ -20,8 +20,6 @@ struct
     | _ -> Local
   let name () = "variables"
   let printXml f x = BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" (XmlUtil.escape (show x))
-
-  let arbitrary () = MyCheck.Arbitrary.varinfo
 end
 
 module RawStrings: Printable.S with type t = string =
@@ -35,12 +33,6 @@ struct
   let printXml f x = BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" (XmlUtil.escape (show x))
 end
 
-module Strings: Lattice.S with type t = [`Bot | `Lifted of string | `Top] =
-  Lattice.Flat (RawStrings) (struct
-    let top_name = "?"
-    let bot_name = "-"
-  end)
-
 module RawBools: Printable.S with type t = bool =
 struct
   include Printable.StdLeaf
@@ -52,12 +44,6 @@ struct
   let printXml f x = BatPrintf.fprintf f "<value>\n<data>\n%s\n</data>\n</value>\n" (show x)
 end
 
-module Bools: Lattice.S with type t = [`Bot | `Lifted of bool | `Top] =
-  Lattice.Flat (RawBools) (struct
-    let top_name = "?"
-    let bot_name = "-"
-  end)
-
 module CilExp =
 struct
   include CilType.Exp
diff --git a/src/common/common.mld b/src/common/common.mld
index 662c789572..2ad88c3758 100644
--- a/src/common/common.mld
+++ b/src/common/common.mld
@@ -10,6 +10,7 @@ For better context, see {!Goblint_lib} which also documents these modules.
 Node
 Edge
 MyCFG
+CfgTools
 }
 
 {2 Specification}
@@ -18,19 +19,10 @@ AnalysisState
 ControlSpecC
 }
 
-{2 Configuration}
-{!modules:
-GobConfig
-AfterConfig
-JsonSchema
-Options
-}
-
 
 {1 Domains}
 {!modules:
 Printable
-Lattice
 }
 
 {2 Analysis-specific}
@@ -42,7 +34,6 @@ Lattice
 {1 I/O}
 {!modules:
 Messages
-Tracing
 }
 
 
@@ -69,6 +60,3 @@ RichVarinfo
 
 {2 Standard library}
 {!modules:GobFormat}
-
-{2 Other libraries}
-{!modules:MyCheck}
diff --git a/src/common/domains/printable.ml b/src/common/domains/printable.ml
index 3499cfdb04..cc01718ee8 100644
--- a/src/common/domains/printable.ml
+++ b/src/common/domains/printable.ml
@@ -233,9 +233,9 @@ struct
   let arbitrary () =
     let open QCheck.Iter in
     let shrink = function
-      | `Lifted x -> (return `Bot) <+> (MyCheck.shrink (Base.arbitrary ()) x >|= lift)
+      | `Lifted x -> (return `Bot) <+> (GobQCheck.shrink (Base.arbitrary ()) x >|= lift)
       | `Bot -> empty
-      | `Top -> MyCheck.Iter.of_arbitrary ~n:20 (Base.arbitrary ()) >|= lift
+      | `Top -> GobQCheck.Iter.of_arbitrary ~n:20 (Base.arbitrary ()) >|= lift
     in
     QCheck.frequency ~shrink ~print:show [
       20, QCheck.map lift (Base.arbitrary ());
@@ -626,8 +626,8 @@ struct
   let arbitrary () =
     let open QCheck.Iter in
     let shrink = function
-      | `Lifted x -> MyCheck.shrink (Base.arbitrary ()) x >|= lift
-      | `Top -> MyCheck.Iter.of_arbitrary ~n:20 (Base.arbitrary ()) >|= lift
+      | `Lifted x -> GobQCheck.shrink (Base.arbitrary ()) x >|= lift
+      | `Top -> GobQCheck.Iter.of_arbitrary ~n:20 (Base.arbitrary ()) >|= lift
     in
     QCheck.frequency ~shrink ~print:show [
       20, QCheck.map lift (Base.arbitrary ());
diff --git a/src/common/dune b/src/common/dune
index c8f1564782..7994798579 100644
--- a/src/common/dune
+++ b/src/common/dune
@@ -8,22 +8,18 @@
    batteries.unthreaded
    zarith
    goblint_std
+   goblint_config
+   goblint_tracing
    goblint-cil
    fpath
    yojson
-   json-data-encoding
-   cpu
    goblint_timing
-   goblint_build_info
-   goblint.sites
    qcheck-core.runner)
  (flags :standard -open Goblint_std)
  (preprocess
   (pps
     ppx_deriving.std
     ppx_deriving_hash
-    ppx_deriving_yojson
-    ppx_blob))
- (preprocessor_deps (file util/options.schema.json)))
+    ppx_deriving_yojson)))
 
 (documentation)
diff --git a/src/framework/cfgTools.ml b/src/common/framework/cfgTools.ml
similarity index 98%
rename from src/framework/cfgTools.ml
rename to src/common/framework/cfgTools.ml
index 7b673f99bc..78aba17060 100644
--- a/src/framework/cfgTools.ml
+++ b/src/common/framework/cfgTools.ml
@@ -122,10 +122,6 @@ let rec pretty_edges () = function
   | [_,x] -> Edge.pretty_plain () x
   | (_,x)::xs -> Pretty.dprintf "%a; %a" Edge.pretty_plain x pretty_edges xs
 
-let get_pseudo_return_id fd =
-  let start_id = 10_000_000_000 in (* TODO get max_sid? *)
-  let sid = Hashtbl.hash fd.svar.vid in (* Need pure sid instead of Cil.new_sid for incremental, similar to vid in Cilfacade.create_var. We only add one return stmt per loop, so the hash from the functions vid should be unique. *)
-  if sid < start_id then sid + start_id else sid
 
 let node_scc_global = NH.create 113
 
@@ -260,7 +256,7 @@ let createCFG (file: file) =
           if Messages.tracing then Messages.trace "cfg" "adding pseudo-return to the function %s.\n" fd.svar.vname;
           let fd_end_loc = {fd_loc with line = fd_loc.endLine; byte = fd_loc.endByte; column = fd_loc.endColumn} in
           let newst = mkStmt (Return (None, fd_end_loc)) in
-          newst.sid <- get_pseudo_return_id fd;
+          newst.sid <- Cilfacade.get_pseudo_return_id fd;
           Cilfacade.StmtH.add Cilfacade.pseudo_return_to_fun newst fd;
           Cilfacade.IntH.replace Cilfacade.pseudo_return_stmt_sids newst.sid newst;
           let newst_node = Statement newst in
@@ -685,7 +681,7 @@ let getGlobalInits (file: file) : edges  =
       lval
     in
     let rec any_index_offset = function
-      | Index (e,o) -> Index (Offset.Index.Exp.any, any_index_offset o)
+      | Index (e,o) -> Index (Cilfacade.any_index_exp, any_index_offset o)
       | Field (f,o) -> Field (f, any_index_offset o)
       | NoOffset -> NoOffset
     in
diff --git a/src/common/util/cilfacade.ml b/src/common/util/cilfacade.ml
index 26a2f082a4..eff97da404 100644
--- a/src/common/util/cilfacade.ml
+++ b/src/common/util/cilfacade.ml
@@ -531,6 +531,12 @@ let stmt_fundecs: fundec StmtH.t ResettableLazy.t =
       h
     )
 
+
+let get_pseudo_return_id fd =
+  let start_id = 10_000_000_000 in (* TODO get max_sid? *)
+  let sid = Hashtbl.hash fd.svar.vid in (* Need pure sid instead of Cil.new_sid for incremental, similar to vid in Cilfacade.create_var. We only add one return stmt per loop, so the hash from the functions vid should be unique. *)
+  if sid < start_id then sid + start_id else sid
+
 let pseudo_return_to_fun = StmtH.create 113
 
 (** Find [fundec] which the [stmt] is in. *)
@@ -706,4 +712,10 @@ let add_function_declarations (file: Cil.file): unit =
   in
   let fun_decls = List.filter_map declaration_from_GFun functions in
   let globals = upto_last_type @ fun_decls @ non_types @ functions in
-  file.globals <- globals
\ No newline at end of file
+  file.globals <- globals
+
+
+(** Special index expression for some unknown index.
+    Weakly updates array in assignment.
+    Used for [exp.fast_global_inits]. *)
+let any_index_exp = CastE (TInt (ptrdiff_ikind (), []), mkString "any_index") (* TODO: move back to Offset *)
diff --git a/src/common/util/messages.ml b/src/common/util/messages.ml
index 42a3118978..d7afec43c5 100644
--- a/src/common/util/messages.ml
+++ b/src/common/util/messages.ml
@@ -339,4 +339,23 @@ let msg_final severity ?(tags=[]) ?(category=Category.Unknown) fmt =
   else
     GobPretty.igprintf () fmt
 
-include Tracing
+
+include Goblint_tracing
+
+open Pretty
+
+let tracel sys ?var fmt =
+  let loc = !current_loc in
+  let docloc sys doc =
+    printtrace sys (dprintf "(%a)@?" CilType.Location.pretty loc ++ indent 2 doc);
+  in
+  gtrace true docloc sys var ~loc ignore fmt
+
+let traceli sys ?var ?(subsys=[]) fmt =
+  let loc = !current_loc in
+  let g () = activate sys subsys in
+  let docloc sys doc: unit =
+    printtrace sys (dprintf "(%a)" CilType.Location.pretty loc ++ indent 2 doc);
+    traceIndent ()
+  in
+  gtrace true docloc sys var ~loc g fmt
diff --git a/src/common/util/afterConfig.ml b/src/config/afterConfig.ml
similarity index 100%
rename from src/common/util/afterConfig.ml
rename to src/config/afterConfig.ml
diff --git a/src/config/config.mld b/src/config/config.mld
new file mode 100644
index 0000000000..160eaa9a11
--- /dev/null
+++ b/src/config/config.mld
@@ -0,0 +1,14 @@
+{0 Library goblint.config}
+This library is unwrapped and provides the following top-level modules.
+For better context, see {!Goblint_lib} which also documents these modules.
+
+
+{1 Framework}
+
+{2 Configuration}
+{!modules:
+GobConfig
+AfterConfig
+JsonSchema
+Options
+}
diff --git a/src/config/dune b/src/config/dune
new file mode 100644
index 0000000000..1508e2553e
--- /dev/null
+++ b/src/config/dune
@@ -0,0 +1,23 @@
+(include_subdirs no)
+
+(library
+ (name goblint_config)
+ (public_name goblint.config)
+ (wrapped false) ; TODO: wrap
+ (libraries
+   batteries.unthreaded
+   goblint_std
+   goblint_tracing
+   fpath
+   yojson
+   json-data-encoding
+   cpu
+   goblint.sites
+   qcheck-core.runner)
+ (flags :standard -open Goblint_std)
+ (preprocess
+  (pps
+    ppx_blob))
+ (preprocessor_deps (file options.schema.json)))
+
+(documentation)
diff --git a/src/common/util/gobConfig.ml b/src/config/gobConfig.ml
similarity index 96%
rename from src/common/util/gobConfig.ml
rename to src/config/gobConfig.ml
index c517ba150d..24a1701ce6 100644
--- a/src/common/util/gobConfig.ml
+++ b/src/config/gobConfig.ml
@@ -21,7 +21,6 @@
 *)
 
 open Batteries
-open Tracing
 open Printf
 
 exception ConfigError of string
@@ -300,7 +299,7 @@ struct
     try
       let st = String.trim st in
       let x = get_value !json_conf (parse_path st) in
-      if tracing then trace "conf-reads" "Reading '%s', it is %a.\n" st GobYojson.pretty x;
+      if Goblint_tracing.tracing then Goblint_tracing.trace "conf-reads" "Reading '%s', it is %a.\n" st GobYojson.pretty x;
       try f x
       with Yojson.Safe.Util.Type_error (s, _) ->
         eprintf "The value for '%s' has the wrong type: %s\n" st s;
@@ -332,7 +331,7 @@ struct
 
   let wrap_get f x =
     (* self-observe options, which Spec construction depends on *)
-    if !building_spec && Tracing.tracing then Tracing.trace "config" "get during building_spec: %s\n" x;
+    if !building_spec && Goblint_tracing.tracing then Goblint_tracing.trace "config" "get during building_spec: %s\n" x;
     (* TODO: blacklist such building_spec option from server mode modification since it will have no effect (spec is already built) *)
     f x
 
@@ -352,7 +351,7 @@ struct
 
   (** Helper function for writing values. Handles the tracing. *)
   let set_path_string st v =
-    if tracing then trace "conf" "Setting '%s' to %a.\n" st GobYojson.pretty v;
+    if Goblint_tracing.tracing then Goblint_tracing.trace "conf" "Setting '%s' to %a.\n" st GobYojson.pretty v;
     set_value v json_conf (parse_path st)
 
   let set_json st j =
@@ -402,7 +401,7 @@ struct
     | Some fn ->
       let v = Yojson.Safe.from_channel % BatIO.to_input_channel |> File.with_file_in (Fpath.to_string fn) in
       merge v;
-      if tracing then trace "conf" "Merging with '%a', resulting\n%a.\n" GobFpath.pretty fn GobYojson.pretty !json_conf
+      if Goblint_tracing.tracing then Goblint_tracing.trace "conf" "Merging with '%a', resulting\n%a.\n" GobFpath.pretty fn GobYojson.pretty !json_conf
     | None -> raise (Sys_error (Printf.sprintf "%s: No such file or diretory" (Fpath.to_string fn)))
 end
 
diff --git a/src/common/util/jsonSchema.ml b/src/config/jsonSchema.ml
similarity index 100%
rename from src/common/util/jsonSchema.ml
rename to src/config/jsonSchema.ml
diff --git a/src/common/util/options.ml b/src/config/options.ml
similarity index 98%
rename from src/common/util/options.ml
rename to src/config/options.ml
index 3046f70809..125da3330b 100644
--- a/src/common/util/options.ml
+++ b/src/config/options.ml
@@ -1,4 +1,4 @@
-(** [src/common/util/options.schema.json] low-level access. *)
+(** [src/config/options.schema.json] low-level access. *)
 
 open Json_schema
 
diff --git a/src/common/util/options.schema.json b/src/config/options.schema.json
similarity index 100%
rename from src/common/util/options.schema.json
rename to src/config/options.schema.json
diff --git a/src/domains/boolDomain.ml b/src/domain/boolDomain.ml
similarity index 83%
rename from src/domains/boolDomain.ml
rename to src/domain/boolDomain.ml
index e088c3605c..43e15e1405 100644
--- a/src/domains/boolDomain.ml
+++ b/src/domain/boolDomain.ml
@@ -38,4 +38,10 @@ struct
   let widen = (&&)
   let meet = (||)
   let narrow = (||)
-end
\ No newline at end of file
+end
+
+module FlatBool: Lattice.S with type t = [`Bot | `Lifted of bool | `Top] =
+  Lattice.Flat (Bool) (struct
+    let top_name = "?"
+    let bot_name = "-"
+  end)
diff --git a/src/domains/disjointDomain.ml b/src/domain/disjointDomain.ml
similarity index 100%
rename from src/domains/disjointDomain.ml
rename to src/domain/disjointDomain.ml
diff --git a/src/domain/domain.mld b/src/domain/domain.mld
new file mode 100644
index 0000000000..ce7e1a5859
--- /dev/null
+++ b/src/domain/domain.mld
@@ -0,0 +1,21 @@
+{0 Library goblint.domain}
+This library is unwrapped and provides the following top-level modules.
+For better context, see {!Goblint_lib} which also documents these modules.
+
+
+{1 Domains}
+{!modules:
+Lattice
+}
+
+{2 General}
+{!modules:
+BoolDomain
+SetDomain
+MapDomain
+TrieDomain
+DisjointDomain
+HoareDomain
+PartitionDomain
+FlagHelper
+}
diff --git a/src/domain/dune b/src/domain/dune
new file mode 100644
index 0000000000..169f4a1d5c
--- /dev/null
+++ b/src/domain/dune
@@ -0,0 +1,19 @@
+(include_subdirs no)
+
+(library
+ (name goblint_domain)
+ (public_name goblint.domain)
+ (wrapped false) ; TODO: wrap
+ (libraries
+   batteries.unthreaded
+   goblint_std
+   goblint_common
+   goblint-cil)
+ (flags :standard -open Goblint_std)
+ (preprocess
+  (pps
+    ppx_deriving.std
+    ppx_deriving_hash
+    ppx_deriving_yojson)))
+
+(documentation)
diff --git a/src/domains/flagHelper.ml b/src/domain/flagHelper.ml
similarity index 100%
rename from src/domains/flagHelper.ml
rename to src/domain/flagHelper.ml
diff --git a/src/domains/hoareDomain.ml b/src/domain/hoareDomain.ml
similarity index 100%
rename from src/domains/hoareDomain.ml
rename to src/domain/hoareDomain.ml
diff --git a/src/common/domains/lattice.ml b/src/domain/lattice.ml
similarity index 96%
rename from src/common/domains/lattice.ml
rename to src/domain/lattice.ml
index 51306d637f..9ea3f74635 100644
--- a/src/common/domains/lattice.ml
+++ b/src/domain/lattice.ml
@@ -148,18 +148,14 @@ struct
 end
 
 (* HAS SIDE-EFFECTS ---- PLEASE INSTANCIATE ONLY ONCE!!! *)
-module HConsed (Base:S) =
+module HConsed (Base:S) (Arg: sig val assume_idempotent: bool end) =
 struct
   include Printable.HConsed (Base)
 
-  (* We do refine int values on narrow and meet {!IntDomain.IntDomTupleImpl}, which can lead to fixpoint issues if we assume x op x = x *)
-  (* see https://github.com/goblint/analyzer/issues/1005 *)
-  let int_refine_active = GobConfig.get_string "ana.int.refinement" <> "never"
-
   let lift_f2 f x y = f (unlift x) (unlift y)
-  let narrow x y = if (not int_refine_active) && x.BatHashcons.tag == y.BatHashcons.tag then x else lift (lift_f2 Base.narrow x y)
+  let narrow x y = if Arg.assume_idempotent && x.BatHashcons.tag == y.BatHashcons.tag then x else lift (lift_f2 Base.narrow x y)
   let widen x y = if x.BatHashcons.tag == y.BatHashcons.tag then x else lift (lift_f2 Base.widen x y)
-  let meet x y = if (not int_refine_active) && x.BatHashcons.tag == y.BatHashcons.tag then x else lift (lift_f2 Base.meet x y)
+  let meet x y = if Arg.assume_idempotent && x.BatHashcons.tag == y.BatHashcons.tag then x else lift (lift_f2 Base.meet x y)
   let join x y = if x.BatHashcons.tag == y.BatHashcons.tag then x else lift (lift_f2 Base.join x y)
   let leq x y = (x.BatHashcons.tag == y.BatHashcons.tag) || lift_f2 Base.leq x y
   let is_top = lift_f Base.is_top
diff --git a/src/domains/mapDomain.ml b/src/domain/mapDomain.ml
similarity index 99%
rename from src/domains/mapDomain.ml
rename to src/domain/mapDomain.ml
index 76dec6f0d2..9013b036e5 100644
--- a/src/domains/mapDomain.ml
+++ b/src/domain/mapDomain.ml
@@ -259,11 +259,12 @@ struct
 end
 
 (* TODO: this is very slow because every add/remove in a fold-loop relifts *)
+(* TODO: currently hardcoded to assume_idempotent *)
 module HConsed (M: S) : S with
   type key = M.key and
   type value = M.value =
 struct
-  include Lattice.HConsed (M)
+  include Lattice.HConsed (M) (struct let assume_idempotent = false end)
 
   type key = M.key
   type value = M.value
diff --git a/src/domains/partitionDomain.ml b/src/domain/partitionDomain.ml
similarity index 100%
rename from src/domains/partitionDomain.ml
rename to src/domain/partitionDomain.ml
diff --git a/src/domains/setDomain.ml b/src/domain/setDomain.ml
similarity index 100%
rename from src/domains/setDomain.ml
rename to src/domain/setDomain.ml
diff --git a/src/domains/trieDomain.ml b/src/domain/trieDomain.ml
similarity index 100%
rename from src/domains/trieDomain.ml
rename to src/domain/trieDomain.ml
diff --git a/src/domains/queries.ml b/src/domains/queries.ml
index b9fa28f5be..228320bef3 100644
--- a/src/domains/queries.ml
+++ b/src/domains/queries.ml
@@ -32,7 +32,11 @@ module FlatYojson = Lattice.Flat (Printable.Yojson) (struct
     let bot_name = "bot yojson"
   end)
 
-module SD = Basetype.Strings
+module SD: Lattice.S with type t = [`Bot | `Lifted of string | `Top] =
+  Lattice.Flat (Basetype.RawStrings) (struct
+    let top_name = "?"
+    let bot_name = "-"
+  end)
 module VD = ValueDomain.Compound
 module AD = ValueDomain.AD
 
diff --git a/src/dune b/src/dune
index 61b6f8c521..eac6640451 100644
--- a/src/dune
+++ b/src/dune
@@ -7,7 +7,7 @@
   (name goblint_lib)
   (public_name goblint.lib)
   (modules :standard \ goblint privPrecCompare apronPrecCompare messagesCompare)
-  (libraries goblint.sites goblint.build-info goblint-cil.all-features batteries.unthreaded qcheck-core.runner sha json-data-encoding jsonrpc cpu arg-complete fpath yaml yaml.unix uuidm goblint_timing catapult goblint_backtrace fileutils goblint_std goblint_common
+  (libraries goblint.sites goblint.build-info goblint-cil.all-features batteries.unthreaded qcheck-core.runner sha json-data-encoding jsonrpc cpu arg-complete fpath yaml yaml.unix uuidm goblint_timing catapult goblint_backtrace fileutils goblint_std goblint_config goblint_common goblint_domain goblint_library goblint_incremental goblint_tracing
     ; 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.
     ; See: https://dune.readthedocs.io/en/stable/concepts.html#alternative-dependencies.
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index b6046d023b..77d3a38186 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -12,12 +12,17 @@ module M = Messages
 
 (** Lifts a [Spec] so that the domain is [Hashcons]d *)
 module HashconsLifter (S:Spec)
-  : Spec with module D = Lattice.HConsed (S.D)
-          and module G = S.G
+  : Spec with module G = S.G
           and module C = S.C
 =
 struct
-  module D = Lattice.HConsed (S.D)
+  module HConsedArg =
+  struct
+    (* We do refine int values on narrow and meet {!IntDomain.IntDomTupleImpl}, which can lead to fixpoint issues if we assume x op x = x *)
+    (* see https://github.com/goblint/analyzer/issues/1005 *)
+    let assume_idempotent = GobConfig.get_string "ana.int.refinement" = "never"
+  end
+  module D = Lattice.HConsed (S.D) (HConsedArg)
   module G = S.G
   module C = S.C
   module V = S.V
@@ -820,13 +825,13 @@ struct
     )
 
   let tf var getl sidel getg sideg prev_node (_,edge) d (f,t) =
-    let old_loc  = !Tracing.current_loc in
-    let old_loc2 = !Tracing.next_loc in
-    Tracing.current_loc := f;
-    Tracing.next_loc := t;
+    let old_loc  = !Goblint_tracing.current_loc in
+    let old_loc2 = !Goblint_tracing.next_loc in
+    Goblint_tracing.current_loc := f;
+    Goblint_tracing.next_loc := t;
     Goblint_backtrace.protect ~mark:(fun () -> TfLocation f) ~finally:(fun () ->
-        Tracing.current_loc := old_loc;
-        Tracing.next_loc := old_loc2
+        Goblint_tracing.current_loc := old_loc;
+        Goblint_tracing.next_loc := old_loc2
       ) (fun () ->
         let d       = tf var getl sidel getg sideg prev_node edge d in
         d
@@ -999,7 +1004,7 @@ struct
 
     let dummy_pseudo_return_node f =
       (* not the same as in CFG, but compares equal because of sid *)
-      Node.Statement ({Cil.dummyStmt with sid = CfgTools.get_pseudo_return_id f})
+      Node.Statement ({Cil.dummyStmt with sid = Cilfacade.get_pseudo_return_id f})
     in
     let add_nodes_of_fun (functions: fundec list) (withEntry: fundec -> bool) =
       let add_stmts (f: fundec) =
@@ -1344,7 +1349,7 @@ struct
 
   module EM =
   struct
-    include MapDomain.MapBot (Basetype.CilExp) (Basetype.Bools)
+    include MapDomain.MapBot (Basetype.CilExp) (BoolDomain.FlatBool)
     let name () = "branches"
   end
 
diff --git a/src/framework/control.ml b/src/framework/control.ml
index 0c9b61739b..00a6034e27 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -142,12 +142,12 @@ struct
     if List.mem "termination" @@ get_string_list "ana.activated" then (
       (* check if we have upjumping gotos *)
       let open Cilfacade in
-      let warn_for_upjumps fundec gotos = 
+      let warn_for_upjumps fundec gotos =
         if FunSet.mem live_funs fundec then (
           (* set nortermiantion flag *)
           AnalysisState.svcomp_may_not_terminate := true;
           (* iterate through locations to produce warnings *)
-          LocSet.iter (fun l _ -> 
+          LocSet.iter (fun l _ ->
               M.warn ~loc:(M.Location.CilLocation l) ~category:Termination "The program might not terminate! (Upjumping Goto)"
             ) gotos
         )
@@ -313,7 +313,7 @@ struct
         if M.tracing then M.trace "con" "Initializer %a\n" CilType.Location.pretty loc;
         (*incr count;
           if (get_bool "dbg.verbose")&& (!count mod 1000 = 0)  then Printf.printf "%d %!" !count;    *)
-        Tracing.current_loc := loc;
+        Goblint_tracing.current_loc := loc;
         match edge with
         | MyCFG.Entry func        ->
           if M.tracing then M.trace "global_inits" "Entry %a\n" d_lval (var func.svar);
@@ -335,9 +335,9 @@ struct
       in
       let with_externs = do_extern_inits ctx file in
       (*if (get_bool "dbg.verbose") then Printf.printf "Number of init. edges : %d\nWorking:" (List.length edges);    *)
-      let old_loc = !Tracing.current_loc in
+      let old_loc = !Goblint_tracing.current_loc in
       let result : Spec.D.t = List.fold_left transfer_func with_externs edges in
-      Tracing.current_loc := old_loc;
+      Goblint_tracing.current_loc := old_loc;
       if M.tracing then M.trace "global_inits" "startstate: %a\n" Spec.D.pretty result;
       result, !funs
     in
diff --git a/src/goblint_lib.ml b/src/goblint_lib.ml
index 08691fa273..5a2e0d3e0e 100644
--- a/src/goblint_lib.ml
+++ b/src/goblint_lib.ml
@@ -51,7 +51,7 @@ module VarQuery = VarQuery
 (** {2 Configuration}
 
     Runtime configuration is represented as JSON.
-    Options are specified and documented by the JSON schema [src/common/util/options.schema.json]. *)
+    Options are specified and documented by the JSON schema [src/config/options.schema.json]. *)
 
 module GobConfig = GobConfig
 module AfterConfig = AfterConfig
@@ -325,7 +325,6 @@ module SolverBox = SolverBox
     Various input/output interfaces and formats. *)
 
 module Messages = Messages
-module Tracing = Tracing
 
 (** {2 Front-end}
 
@@ -462,9 +461,3 @@ module ApronPrecCompareUtil = ApronPrecCompareUtil
     OCaml standard library extensions which are not provided by {!Batteries}. *)
 
 module GobFormat = GobFormat
-
-(** {2 Other libraries}
-
-    External library extensions. *)
-
-module MyCheck = MyCheck
diff --git a/src/util/cilMaps.ml b/src/incremental/cilMaps.ml
similarity index 100%
rename from src/util/cilMaps.ml
rename to src/incremental/cilMaps.ml
diff --git a/src/incremental/compareCFG.ml b/src/incremental/compareCFG.ml
index 225cbb1c76..55b3fa8fc5 100644
--- a/src/incremental/compareCFG.ml
+++ b/src/incremental/compareCFG.ml
@@ -17,7 +17,7 @@ let (&&<>) (prev_result: bool * rename_mapping) f : bool * rename_mapping =
 
 let eq_node (x, fun1) (y, fun2) ~rename_mapping =
   let isPseudoReturn f sid =
-    let pid = CfgTools.get_pseudo_return_id f in
+    let pid = Cilfacade.get_pseudo_return_id f in
     sid == pid in
   match x,y with
   | Statement s1, Statement s2 ->
diff --git a/src/incremental/dune b/src/incremental/dune
new file mode 100644
index 0000000000..595dba22f7
--- /dev/null
+++ b/src/incremental/dune
@@ -0,0 +1,22 @@
+(include_subdirs no)
+
+(library
+ (name goblint_incremental)
+ (public_name goblint.incremental)
+ (wrapped false) ; TODO: wrap
+ (libraries
+   batteries.unthreaded
+   zarith
+   goblint_std
+   goblint_config
+   goblint_common
+   goblint-cil
+   fpath)
+ (flags :standard -open Goblint_std)
+ (preprocess
+  (pps
+    ppx_deriving.std
+    ppx_deriving_hash
+    ppx_deriving_yojson)))
+
+(documentation)
diff --git a/src/incremental/incremental.mld b/src/incremental/incremental.mld
new file mode 100644
index 0000000000..bf9b6e6a58
--- /dev/null
+++ b/src/incremental/incremental.mld
@@ -0,0 +1,16 @@
+{0 Library goblint.incremental}
+This library is unwrapped and provides the following top-level modules.
+For better context, see {!Goblint_lib} which also documents these modules.
+
+
+{1 Incremental}
+
+{!modules:
+CompareCIL
+CompareAST
+CompareCFG
+UpdateCil
+MaxIdUtil
+Serialize
+CilMaps
+}
diff --git a/src/index.mld b/src/index.mld
index 2afbbc97ae..76b9d230dd 100644
--- a/src/index.mld
+++ b/src/index.mld
@@ -7,9 +7,21 @@ The following libraries make up Goblint's main codebase.
 {!modules:Goblint_lib}
 This library currently contains the majority of Goblint and is in the process of being split into smaller libraries.
 
+{2 Library goblint.config}
+This {{!page-config}unwrapped library} contains various configuration modules extracted from {!Goblint_lib}.
+
 {2 Library goblint.common}
 This {{!page-common}unwrapped library} contains various common modules extracted from {!Goblint_lib}.
 
+{2 Library goblint.domain}
+This {{!page-domain}unwrapped library} contains various domain modules extracted from {!Goblint_lib}.
+
+{2 Library goblint.library}
+This {{!page-library}unwrapped library} contains various library specification modules extracted from {!Goblint_lib}.
+
+{2 Library goblint.incremental}
+This {{!page-incremental}unwrapped library} contains various incremental modules extracted from {!Goblint_lib}.
+
 
 {1 Library extensions}
 The following libraries provide extensions to other OCaml libraries.
@@ -43,6 +55,9 @@ The following libraries provide utilities which are completely independent of Go
 {2 Library goblint.timing}
 {!modules:Goblint_timing}
 
+{2 Library goblint.tracing}
+{!modules:Goblint_tracing}
+
 
 {1 Vendored}
 The following libraries are vendored in Goblint.
diff --git a/src/maingoblint.ml b/src/maingoblint.ml
index dcee9abb13..2c7d353594 100644
--- a/src/maingoblint.ml
+++ b/src/maingoblint.ml
@@ -53,7 +53,7 @@ let rec option_spec_list: Arg_complete.speclist Lazy.t = lazy (
   let add_string l = let f str = l := str :: !l in Arg_complete.String (f, Arg_complete.empty) in
   let add_int    l = let f str = l := str :: !l in Arg_complete.Int (f, Arg_complete.empty) in
   let set_trace sys =
-    if Messages.tracing then Tracing.addsystem sys
+    if Messages.tracing then Goblint_tracing.addsystem sys
     else (prerr_endline "Goblint has been compiled without tracing, recompile in trace profile (./scripts/trace_on.sh)"; raise Stdlib.Exit)
   in
   let configure_html () =
@@ -112,8 +112,8 @@ let rec option_spec_list: Arg_complete.speclist Lazy.t = lazy (
   ; "--print_options"      , Arg_complete.Unit (fun () -> Options.print_options (); exit 0), ""
   ; "--print_all_options"  , Arg_complete.Unit (fun () -> Options.print_all_options (); exit 0), ""
   ; "--trace"              , Arg_complete.String (set_trace, Arg_complete.empty), ""
-  ; "--tracevars"          , add_string Tracing.tracevars, ""
-  ; "--tracelocs"          , add_int Tracing.tracelocs, ""
+  ; "--tracevars"          , add_string Goblint_tracing.tracevars, ""
+  ; "--tracelocs"          , add_int Goblint_tracing.tracelocs, ""
   ; "--help"               , Arg_complete.Unit (fun _ -> print_help stdout),""
   ; "--html"               , Arg_complete.Unit (fun _ -> configure_html ()),""
   ; "--sarif"               , Arg_complete.Unit (fun _ -> configure_sarif ()),""
diff --git a/src/domains/accessKind.ml b/src/util/library/accessKind.ml
similarity index 100%
rename from src/domains/accessKind.ml
rename to src/util/library/accessKind.ml
diff --git a/src/util/library/dune b/src/util/library/dune
new file mode 100644
index 0000000000..075c01c35d
--- /dev/null
+++ b/src/util/library/dune
@@ -0,0 +1,18 @@
+(include_subdirs no)
+
+(library
+ (name goblint_library)
+ (public_name goblint.library)
+ (wrapped false) ; TODO: wrap
+ (libraries
+   batteries.unthreaded
+   goblint_common
+   goblint_domain
+   goblint_config
+   goblint-cil)
+ (preprocess
+  (pps
+    ppx_deriving.std
+    ppx_deriving_hash)))
+
+(documentation)
diff --git a/src/util/library/library.mld b/src/util/library/library.mld
new file mode 100644
index 0000000000..f55db3f2ff
--- /dev/null
+++ b/src/util/library/library.mld
@@ -0,0 +1,14 @@
+{0 Library goblint.library}
+This library is unwrapped and provides the following top-level modules.
+For better context, see {!Goblint_lib} which also documents these modules.
+
+
+{1 Utilities}
+
+{2 Library specification}
+{!modules:
+AccessKind
+LibraryDesc
+LibraryDsl
+LibraryFunctions
+}
diff --git a/src/analyses/libraryDesc.ml b/src/util/library/libraryDesc.ml
similarity index 100%
rename from src/analyses/libraryDesc.ml
rename to src/util/library/libraryDesc.ml
diff --git a/src/analyses/libraryDsl.ml b/src/util/library/libraryDsl.ml
similarity index 100%
rename from src/analyses/libraryDsl.ml
rename to src/util/library/libraryDsl.ml
diff --git a/src/analyses/libraryDsl.mli b/src/util/library/libraryDsl.mli
similarity index 100%
rename from src/analyses/libraryDsl.mli
rename to src/util/library/libraryDsl.mli
diff --git a/src/analyses/libraryFunctions.ml b/src/util/library/libraryFunctions.ml
similarity index 96%
rename from src/analyses/libraryFunctions.ml
rename to src/util/library/libraryFunctions.ml
index 8152e5b886..2c65f7ae61 100644
--- a/src/analyses/libraryFunctions.ml
+++ b/src/util/library/libraryFunctions.ml
@@ -1233,88 +1233,88 @@ open Invalidate
  * We assume that no known functions that are reachable are executed/spawned. For that we use ThreadCreate above. *)
 (* WTF: why are argument numbers 1-indexed (in partition)? *)
 let invalidate_actions = [
-    "__printf_chk", readsAll;(*safe*)
-    "printk", readsAll;(*safe*)
-    "__mutex_init", readsAll;(*safe*)
-    "__builtin___snprintf_chk", writes [1];(*keep [1]*)
-    "__vfprintf_chk", writes [1];(*keep [1]*)
-    "__builtin_va_arg", readsAll;(*safe*)
-    "__builtin_va_end", readsAll;(*safe*)
-    "__builtin_va_start", readsAll;(*safe*)
-    "__ctype_b_loc", readsAll;(*safe*)
-    "__errno", readsAll;(*safe*)
-    "__errno_location", readsAll;(*safe*)
-    "__strdup", readsAll;(*safe*)
-    "strtoul__extinline", readsAll;(*safe*)
-    "readdir_r", writesAll;(*unsafe*)
-    "atoi__extinline", readsAll;(*safe*)
-    "_IO_getc", writesAll;(*unsafe*)
-    "pipe", writesAll;(*unsafe*)
-    "strerror_r", writesAll;(*unsafe*)
-    "raise", writesAll;(*unsafe*)
-    "_strlen", readsAll;(*safe*)
-    "stat__extinline", writesAllButFirst 1 readsAll;(*drop 1*)
-    "lstat__extinline", writesAllButFirst 1 readsAll;(*drop 1*)
-    "waitpid", readsAll;(*safe*)
-    "__open_alias", readsAll;(*safe*)
-    "__open_2", readsAll;(*safe*)
-    "ioctl", writesAll;(*unsafe*)
-    "fstat__extinline", writesAll;(*unsafe*)
-    "scandir", writes [1;3;4];(*keep [1;3;4]*)
-    "bindtextdomain", readsAll;(*safe*)
-    "textdomain", readsAll;(*safe*)
-    "dcgettext", readsAll;(*safe*)
-    "putw", readsAll;(*safe*)
-    "__getdelim", writes [3];(*keep [3]*)
-    "__h_errno_location", readsAll;(*safe*)
-    "__fxstat", readsAll;(*safe*)
-    "openlog", readsAll;(*safe*)
-    "umask", readsAll;(*safe*)
-    "clntudp_create", writesAllButFirst 3 readsAll;(*drop 3*)
-    "svctcp_create", readsAll;(*safe*)
-    "clntudp_bufcreate", writesAll;(*unsafe*)
-    "authunix_create_default", readsAll;(*safe*)
-    "clnt_broadcast", writesAll;(*unsafe*)
-    "clnt_sperrno", readsAll;(*safe*)
-    "pmap_unset", writesAll;(*unsafe*)
-    "svcudp_create", readsAll;(*safe*)
-    "svc_register", writesAll;(*unsafe*)
-    "svc_run", writesAll;(*unsafe*)
-    "dup", readsAll; (*safe*)
-    "__builtin___vsnprintf", writesAllButFirst 3 readsAll; (*drop 3*)
-    "__builtin___vsnprintf_chk", writesAllButFirst 3 readsAll; (*drop 3*)
-    "__error", readsAll; (*safe*)
-    "__maskrune", writesAll; (*unsafe*)
-    "times", writesAll; (*unsafe*)
-    "timespec_get", writes [1];
-    "__tolower", readsAll; (*safe*)
-    "signal", writesAll; (*unsafe*)
-    "BF_cfb64_encrypt", writes [1;3;4;5]; (*keep [1;3;4,5]*)
-    "BZ2_bzBuffToBuffDecompress", writes [3;4]; (*keep [3;4]*)
-    "uncompress", writes [3;4]; (*keep [3;4]*)
-    "__xstat", writes [3]; (*keep [1]*)
-    "__lxstat", writes [3]; (*keep [1]*)
-    "remove", readsAll;
-    "BZ2_bzBuffToBuffCompress", writes [3;4]; (*keep [3;4]*)
-    "compress2", writes [3]; (*keep [3]*)
-    "__toupper", readsAll; (*safe*)
-    "BF_set_key", writes [3]; (*keep [3]*)
-    "PL_NewHashTable", readsAll; (*safe*)
-    "assert_failed", readsAll; (*safe*)
-    "munmap", readsAll;(*safe*)
-    "mmap", readsAll;(*safe*)
-    "__builtin_va_arg_pack_len", readsAll;
-    "__open_too_many_args", readsAll;
-    "usb_submit_urb", readsAll; (* first argument is written to but according to specification must not be read from anymore *)
-    "dev_driver_string", readsAll;
-    "__spin_lock_init", writes [1];
-    "kmem_cache_create", readsAll;
-    "idr_pre_get", readsAll;
-    "zil_replay", writes [1;2;3;5];
-    (* ddverify *)
-    "sema_init", readsAll;
-    "__goblint_assume_join", readsAll;
-  ]
+  "__printf_chk", readsAll;(*safe*)
+  "printk", readsAll;(*safe*)
+  "__mutex_init", readsAll;(*safe*)
+  "__builtin___snprintf_chk", writes [1];(*keep [1]*)
+  "__vfprintf_chk", writes [1];(*keep [1]*)
+  "__builtin_va_arg", readsAll;(*safe*)
+  "__builtin_va_end", readsAll;(*safe*)
+  "__builtin_va_start", readsAll;(*safe*)
+  "__ctype_b_loc", readsAll;(*safe*)
+  "__errno", readsAll;(*safe*)
+  "__errno_location", readsAll;(*safe*)
+  "__strdup", readsAll;(*safe*)
+  "strtoul__extinline", readsAll;(*safe*)
+  "readdir_r", writesAll;(*unsafe*)
+  "atoi__extinline", readsAll;(*safe*)
+  "_IO_getc", writesAll;(*unsafe*)
+  "pipe", writesAll;(*unsafe*)
+  "strerror_r", writesAll;(*unsafe*)
+  "raise", writesAll;(*unsafe*)
+  "_strlen", readsAll;(*safe*)
+  "stat__extinline", writesAllButFirst 1 readsAll;(*drop 1*)
+  "lstat__extinline", writesAllButFirst 1 readsAll;(*drop 1*)
+  "waitpid", readsAll;(*safe*)
+  "__open_alias", readsAll;(*safe*)
+  "__open_2", readsAll;(*safe*)
+  "ioctl", writesAll;(*unsafe*)
+  "fstat__extinline", writesAll;(*unsafe*)
+  "scandir", writes [1;3;4];(*keep [1;3;4]*)
+  "bindtextdomain", readsAll;(*safe*)
+  "textdomain", readsAll;(*safe*)
+  "dcgettext", readsAll;(*safe*)
+  "putw", readsAll;(*safe*)
+  "__getdelim", writes [3];(*keep [3]*)
+  "__h_errno_location", readsAll;(*safe*)
+  "__fxstat", readsAll;(*safe*)
+  "openlog", readsAll;(*safe*)
+  "umask", readsAll;(*safe*)
+  "clntudp_create", writesAllButFirst 3 readsAll;(*drop 3*)
+  "svctcp_create", readsAll;(*safe*)
+  "clntudp_bufcreate", writesAll;(*unsafe*)
+  "authunix_create_default", readsAll;(*safe*)
+  "clnt_broadcast", writesAll;(*unsafe*)
+  "clnt_sperrno", readsAll;(*safe*)
+  "pmap_unset", writesAll;(*unsafe*)
+  "svcudp_create", readsAll;(*safe*)
+  "svc_register", writesAll;(*unsafe*)
+  "svc_run", writesAll;(*unsafe*)
+  "dup", readsAll; (*safe*)
+  "__builtin___vsnprintf", writesAllButFirst 3 readsAll; (*drop 3*)
+  "__builtin___vsnprintf_chk", writesAllButFirst 3 readsAll; (*drop 3*)
+  "__error", readsAll; (*safe*)
+  "__maskrune", writesAll; (*unsafe*)
+  "times", writesAll; (*unsafe*)
+  "timespec_get", writes [1];
+  "__tolower", readsAll; (*safe*)
+  "signal", writesAll; (*unsafe*)
+  "BF_cfb64_encrypt", writes [1;3;4;5]; (*keep [1;3;4,5]*)
+  "BZ2_bzBuffToBuffDecompress", writes [3;4]; (*keep [3;4]*)
+  "uncompress", writes [3;4]; (*keep [3;4]*)
+  "__xstat", writes [3]; (*keep [1]*)
+  "__lxstat", writes [3]; (*keep [1]*)
+  "remove", readsAll;
+  "BZ2_bzBuffToBuffCompress", writes [3;4]; (*keep [3;4]*)
+  "compress2", writes [3]; (*keep [3]*)
+  "__toupper", readsAll; (*safe*)
+  "BF_set_key", writes [3]; (*keep [3]*)
+  "PL_NewHashTable", readsAll; (*safe*)
+  "assert_failed", readsAll; (*safe*)
+  "munmap", readsAll;(*safe*)
+  "mmap", readsAll;(*safe*)
+  "__builtin_va_arg_pack_len", readsAll;
+  "__open_too_many_args", readsAll;
+  "usb_submit_urb", readsAll; (* first argument is written to but according to specification must not be read from anymore *)
+  "dev_driver_string", readsAll;
+  "__spin_lock_init", writes [1];
+  "kmem_cache_create", readsAll;
+  "idr_pre_get", readsAll;
+  "zil_replay", writes [1;2;3;5];
+  (* ddverify *)
+  "sema_init", readsAll;
+  "__goblint_assume_join", readsAll;
+]
 
 let invalidate_actions =
   let tbl = Hashtbl.create 113 in
diff --git a/src/analyses/libraryFunctions.mli b/src/util/library/libraryFunctions.mli
similarity index 100%
rename from src/analyses/libraryFunctions.mli
rename to src/util/library/libraryFunctions.mli
diff --git a/src/util/std/dune b/src/util/std/dune
index c6961a1725..b074a29937 100644
--- a/src/util/std/dune
+++ b/src/util/std/dune
@@ -9,7 +9,8 @@
    goblint-cil
    fpath
    yojson
-   yaml)
+   yaml
+   qcheck-core)
  (preprocess
   (pps
    ppx_deriving.std
diff --git a/src/common/domains/myCheck.ml b/src/util/std/gobQCheck.ml
similarity index 91%
rename from src/common/domains/myCheck.ml
rename to src/util/std/gobQCheck.ml
index 98583cd2c3..12809d5b46 100644
--- a/src/common/domains/myCheck.ml
+++ b/src/util/std/gobQCheck.ml
@@ -56,7 +56,4 @@ struct
     let gens = List.map gen arbs in
     let shrinks = List.map shrink arbs in
     make ~shrink:(Shrink.sequence shrinks) (Gen.sequence gens)
-
-  open GoblintCil
-  let varinfo: Cil.varinfo arbitrary = QCheck.always (Cil.makeGlobalVar "arbVar" Cil.voidPtrType) (* S TODO: how to generate this *)
 end
diff --git a/src/util/std/goblint_std.ml b/src/util/std/goblint_std.ml
index e716d1df5b..0d548cac08 100644
--- a/src/util/std/goblint_std.ml
+++ b/src/util/std/goblint_std.ml
@@ -19,6 +19,7 @@ module GobUnix = GobUnix
 
 module GobFpath = GobFpath
 module GobPretty = GobPretty
+module GobQCheck = GobQCheck
 module GobYaml = GobYaml
 module GobYojson = GobYojson
 module GobZ = GobZ
diff --git a/src/util/tracing/dune b/src/util/tracing/dune
new file mode 100644
index 0000000000..7e37139567
--- /dev/null
+++ b/src/util/tracing/dune
@@ -0,0 +1,9 @@
+(include_subdirs no)
+
+(library
+ (name goblint_tracing)
+ (public_name goblint.tracing)
+ (libraries
+   goblint_std
+   goblint-cil
+   goblint_build_info))
diff --git a/src/common/util/tracing.ml b/src/util/tracing/goblint_tracing.ml
similarity index 84%
rename from src/common/util/tracing.ml
rename to src/util/tracing/goblint_tracing.ml
index ad8892c396..0e5580b036 100644
--- a/src/common/util/tracing.ml
+++ b/src/util/tracing/goblint_tracing.ml
@@ -4,6 +4,7 @@
  * large domains we output. The original code generated the document object
  * even when the subsystem is not activated. *)
 
+open Goblint_std
 open GoblintCil
 open Pretty
 
@@ -67,13 +68,6 @@ let trace sys ?var fmt = gtrace true printtrace sys var ignore fmt
  * c: continue/normal print w/o indent-change
 *)
 
-let tracel sys ?var fmt =
-  let loc = !current_loc in
-  let docloc sys doc =
-    printtrace sys (dprintf "(%a)@?" CilType.Location.pretty loc ++ indent 2 doc);
-  in
-  gtrace true docloc sys var ~loc ignore fmt
-
 let tracei (sys:string) ?var ?(subsys=[]) fmt =
   let f sys d = printtrace sys d; traceIndent () in
   let g () = activate sys subsys in
@@ -85,13 +79,3 @@ let traceu sys fmt =
   let f sys d = printtrace sys d; traceOutdent () in
   let g () = deactivate sys in
   gtrace true f sys None g fmt
-
-
-let traceli sys ?var ?(subsys=[]) fmt =
-  let loc = !current_loc in
-  let g () = activate sys subsys in
-  let docloc sys doc: unit =
-    printtrace sys (dprintf "(%a)" CilType.Location.pretty loc ++ indent 2 doc);
-    traceIndent ()
-  in
-  gtrace true docloc sys var ~loc g fmt
diff --git a/unittest/dune b/unittest/dune
index 7313aa964b..a08a4b2323 100644
--- a/unittest/dune
+++ b/unittest/dune
@@ -2,7 +2,7 @@
 
 (test
   (name mainTest)
-  (libraries ounit2 qcheck-ounit goblint.lib goblint.sites.dune goblint.build-info.dune)
+  (libraries ounit2 qcheck-ounit goblint.std goblint.lib goblint.sites.dune goblint.build-info.dune)
   (preprocess (pps ppx_deriving.std ppx_deriving_hash ppx_deriving_yojson))
   (flags :standard -linkall))
 
diff --git a/unittest/util/intOpsTest.ml b/unittest/util/intOpsTest.ml
index 611f2f546f..307d9e84b0 100644
--- a/unittest/util/intOpsTest.ml
+++ b/unittest/util/intOpsTest.ml
@@ -1,4 +1,5 @@
 open OUnit2
+open Goblint_std
 open Goblint_lib
 
 (* If the first operand of a div is negative, Zarith rounds the result away from zero.
@@ -10,13 +11,13 @@ let old_div a b = if Z.lt a Z.zero then Z.neg (Z.ediv (Z.neg a) b) else Z.ediv a
 let old_rem a b = Z.sub a (Z.mul b (old_div a b))
 
 let test_bigint_div =
-  QCheck.(Test.make ~name:"div" (pair MyCheck.Arbitrary.big_int MyCheck.Arbitrary.big_int) (fun (x, y) ->
+  QCheck.(Test.make ~name:"div" (pair GobQCheck.Arbitrary.big_int GobQCheck.Arbitrary.big_int) (fun (x, y) ->
       assume (Z.compare y Z.zero <> 0);
       Z.equal (Z.div x y) (old_div x y)
     ))
 
 let test_bigint_rem =
-  QCheck.(Test.make ~name:"rem" (pair MyCheck.Arbitrary.big_int MyCheck.Arbitrary.big_int) (fun (x, y) ->
+  QCheck.(Test.make ~name:"rem" (pair GobQCheck.Arbitrary.big_int GobQCheck.Arbitrary.big_int) (fun (x, y) ->
       assume (Z.compare y Z.zero <> 0);
       Z.equal (Z.rem x y) (old_rem x y)
     ))