diff --git a/rsc/extra/worker_json_example.json b/rsc/extra/worker_json_example.json
index 5a7fef8fe..5e8983f49 100644
--- a/rsc/extra/worker_json_example.json
+++ b/rsc/extra/worker_json_example.json
@@ -10,7 +10,7 @@
     "debug": false, "debug_ac": false, "debug_adt": false,
     "debug_arith": false, "debug_arrays": false, "debug_bitv": false,
     "debug_cc": false, "debug_combine": false, "debug_constr": false,
-    "debug_explanation": false, "debug_fm": false, "debug_fpa": 0,
+    "debug_explanations": false, "debug_fm": false, "debug_fpa": 0,
     "debug_gc": false, "debug_interpretation": false, "debug_ite": false,
     "debug_matching": 0, "debug_sat": false, "debug_split": false,
     "debug_triggers": false, "debug_types": false,
diff --git a/src/bin/common/parse_command.ml b/src/bin/common/parse_command.ml
index 0ad1689ef..32a8dfe0c 100644
--- a/src/bin/common/parse_command.ml
+++ b/src/bin/common/parse_command.ml
@@ -154,7 +154,8 @@ module Debug = struct
     | Cc
     | Combine
     | Constr
-    | Explanation
+    | Explanation (* deprecated *)
+    | Explanations
     | Fm
     | Fpa
     | Gc
@@ -176,7 +177,7 @@ module Debug = struct
 
   let all = [
     Debug; Ac; Adt; Arith; Arrays; Bitv; Sum; Ite;
-    Cc; Combine; Constr; Explanation; Fm; Fpa; Gc;
+    Cc; Combine; Constr; Explanation; Explanations; Fm; Fpa; Gc;
     Interpretation; Intervals; Matching; Sat; Split; Triggers;
     Types; Typing; Uf; Unsat_core; Use; Warnings;
     Commands; Optimize
@@ -195,6 +196,7 @@ module Debug = struct
     | Combine -> "combine"
     | Constr -> "constr"
     | Explanation -> "explanation"
+    | Explanations -> "explanations"
     | Fm -> "fm"
     | Fpa -> "fpa"
     | Gc -> "gc"
@@ -216,51 +218,56 @@ module Debug = struct
   let set_level src = Logs.Src.set_level src (Some Debug)
 
   let mk ~verbosity flags =
-    let module S = Sources in
+    let module S = Options.Sources in
     List.concat flags
     |> List.iter (function
         | Debug ->
           Options.set_debug true
         | Ac ->
           Options.set_debug_ac true;
-          set_level S.ac
+          set_level Ac.src
         | Adt ->
           Options.set_debug_adt true;
-          set_level S.adt;
-          set_level S.adt_rel
+          set_level Adt.src;
+          set_level Adt_rel.src
         | Arith ->
           Options.set_debug_arith true;
-          set_level S.arith;
-          set_level S.interval_calculus
+          set_level Arith.src;
+          set_level IntervalCalculus.src
         | Arrays ->
           Options.set_debug_arrays true;
-          set_level S.arrays_rel
+          set_level Arrays_rel.src
         | Bitv ->
           Options.set_debug_bitv true;
-          set_level S.bitv
+          set_level Bitv.src
         | Sum ->
           Printer.print_wrn
             "The debug flag 'sum' is deprecated and is replaced by 'adt'. \
              It has the same effect as 'adt' and will be removed in a future \
              version.";
           Options.set_debug_adt true;
-          set_level S.adt;
-          set_level S.adt_rel
+          set_level Adt.src;
+          set_level Adt_rel.src
         | Ite ->
           Options.set_debug_ite true;
-          set_level S.ite_rel
+          set_level Ite_rel.src
         | Cc ->
           Options.set_debug_cc true;
-          set_level S.cc
+          set_level Ccx.src
         | Combine ->
           Options.set_debug_combine true;
-          set_level S.combine
+          set_level Shostak.Combine.src
         | Constr ->
           Options.set_debug_constr true;
           set_level S.constr
         | Explanation ->
-          Options.set_debug_explanation true;
-          set_level S.explanation
+          Printer.print_wrn
+            "The debug flag 'explanation' is deprecated and is replaced \
+             by 'explanations'. It has the same effect as 'explanations' \
+             and will be removed in a future version.";
+          Options.set_debug_explanations true
+        | Explanations ->
+          Options.set_debug_explanations true
         | Fm ->
           Options.set_debug_fm true;
           set_level S.fm
@@ -268,18 +275,20 @@ module Debug = struct
           Options.set_debug_fpa verbosity
         | Gc ->
           Options.set_debug_gc true;
-          set_level S.gc_debug
+          set_level Gc_debug.src
         | Interpretation ->
           Options.set_debug_interpretation true;
           set_level S.interpretation
         | Intervals ->
           Options.set_debug_intervals true;
-          set_level S.intervals
+          set_level Intervals.src
         | Matching ->
-          Options.set_debug_matching verbosity
+          Options.set_debug_matching verbosity;
+          set_level Matching.src
         | Sat ->
           Options.set_debug_sat true;
-          set_level S.sat
+          set_level Satml.src;
+          set_level Satml_frontend.src
         | Split ->
           Options.set_debug_split true;
           set_level S.split
@@ -295,22 +304,21 @@ module Debug = struct
              future version."
         | Uf ->
           Options.set_debug_uf true;
-          set_level S.uf
+          set_level Uf.src
         | Unsat_core ->
           Options.set_debug_unsat_core true;
           set_level S.unsat_core
         | Use ->
           Options.set_debug_use true;
-          set_level S.use
+          set_level Use.src
         | Warnings ->
           Printer.print_wrn
             "The debug flag 'warning' is deprecated and will be removed in a \
              future version.";
-          Options.set_debug_warnings true;
-          set_level S.warnings
+          Options.set_debug_warnings true
         | Commands ->
           Options.set_debug_commands true;
-          set_level S.commands
+          set_level Commands.src
         | Optimize ->
           Options.set_debug_optimize true;
           set_level S.optimize
diff --git a/src/bin/js/options_interface.ml b/src/bin/js/options_interface.ml
index a9791a1e3..e27c0b044 100644
--- a/src/bin/js/options_interface.ml
+++ b/src/bin/js/options_interface.ml
@@ -106,7 +106,7 @@ let set_options r =
   set_options_opt Options.set_debug_cc r.debug_cc;
   set_options_opt Options.set_debug_combine r.debug_combine;
   set_options_opt Options.set_debug_constr r.debug_constr;
-  set_options_opt Options.set_debug_explanation r.debug_explanation;
+  set_options_opt Options.set_debug_explanations r.debug_explanations;
   set_options_opt Options.set_debug_fm r.debug_fm;
   set_options_opt Options.set_debug_fpa r.debug_fpa;
   set_options_opt Options.set_debug_gc r.debug_gc;
diff --git a/src/bin/js/worker_interface.ml b/src/bin/js/worker_interface.ml
index 2a2b84ceb..a39bfd7f1 100644
--- a/src/bin/js/worker_interface.ml
+++ b/src/bin/js/worker_interface.ml
@@ -185,7 +185,7 @@ type options = {
   debug_cc : bool option;
   debug_combine : bool option;
   debug_constr : bool option;
-  debug_explanation : bool option;
+  debug_explanations : bool option;
   debug_fm : bool option;
   debug_fpa : int option;
   debug_gc : bool option;
@@ -286,7 +286,7 @@ let init_options () = {
   debug_cc = None;
   debug_combine = None;
   debug_constr = None;
-  debug_explanation = None;
+  debug_explanations = None;
   debug_fm = None;
   debug_fpa = None;
   debug_gc = None;
@@ -392,7 +392,7 @@ let opt_dbg1_encoding =
        (opt "debug_cc" bool)
        (opt "debug_combine" bool)
        (opt "debug_constr" bool)
-       (opt "debug_explanation" bool)
+       (opt "debug_explanations" bool)
     )
 
 let opt_dbg2_encoding =
@@ -555,7 +555,7 @@ let options_to_json opt =
      opt.debug_cc,
      opt.debug_combine,
      opt.debug_constr,
-     opt.debug_explanation)
+     opt.debug_explanations)
   in
   let dbg_opt2 =
     (opt.debug_fm,
@@ -685,7 +685,7 @@ let options_from_json options =
          debug_cc,
          debug_combine,
          debug_constr,
-         debug_explanation) =
+         debug_explanations) =
       dbg_opt1 in
     let (debug_fm,
          debug_fpa,
@@ -771,7 +771,7 @@ let options_from_json options =
       debug_cc;
       debug_combine;
       debug_constr;
-      debug_explanation;
+      debug_explanations;
       debug_fm;
       debug_fpa;
       debug_gc;
diff --git a/src/bin/js/worker_interface.mli b/src/bin/js/worker_interface.mli
index 03d5c4b51..b52303ad1 100644
--- a/src/bin/js/worker_interface.mli
+++ b/src/bin/js/worker_interface.mli
@@ -68,7 +68,7 @@ type options = {
   debug_cc : bool option;
   debug_combine : bool option;
   debug_constr : bool option;
-  debug_explanation : bool option;
+  debug_explanations : bool option;
   debug_fm : bool option;
   debug_fpa : int option;
   debug_gc : bool option;
diff --git a/src/lib/dune b/src/lib/dune
index 3b6afe476..2d7f7575e 100644
--- a/src/lib/dune
+++ b/src/lib/dune
@@ -62,7 +62,7 @@
     ; util
     Emap Gc_debug Hconsing Hstring Heap Loc Numbers Uqueue
     Options Timers Util Vec Version Steps Printer
-    My_zip My_unix My_list Theories Nest Compat Sources
+    My_zip My_unix My_list Theories Nest Compat
   )
 
  (js_of_ocaml
diff --git a/src/lib/reasoners/ac.ml b/src/lib/reasoners/ac.ml
index 95645ba25..bedf31684 100644
--- a/src/lib/reasoners/ac.ml
+++ b/src/lib/reasoners/ac.ml
@@ -28,6 +28,9 @@
 module HS = Hstring
 module Sy = Symbols
 
+let src = Logs.Src.create ~doc:"Ac" __MODULE__
+module Log = (val Logs.src_log src : Logs.LOG)
+
 module type S = sig
 
   (* embeded AC semantic values *)
diff --git a/src/lib/reasoners/ac.mli b/src/lib/reasoners/ac.mli
index 992118898..b2cb57c94 100644
--- a/src/lib/reasoners/ac.mli
+++ b/src/lib/reasoners/ac.mli
@@ -25,6 +25,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+val src : Logs.src
+
 module type S = sig
 
   (* the type of amalgamated AC semantic values *)
diff --git a/src/lib/reasoners/adt.ml b/src/lib/reasoners/adt.ml
index 947175285..76c1a617b 100644
--- a/src/lib/reasoners/adt.ml
+++ b/src/lib/reasoners/adt.ml
@@ -28,6 +28,9 @@
 module Sy = Symbols
 module E  = Expr
 
+let src = Logs.Src.create ~doc:"Adt" __MODULE__
+module Log = (val Logs.src_log src : Logs.LOG)
+
 type 'a abstract =
   | Constr of {
       c_name : Uid.term_cst;
@@ -79,7 +82,6 @@ module Shostak (X : ALIEN) = struct
   module SX = Set.Make(struct type t = r let compare = X.hash_cmp end)
 
   let name = "Adt"
-
   let timer = Timers.M_Adt
 
   [@@ocaml.ppwarning "XXX: IsConstr not interpreted currently. Maybe \
diff --git a/src/lib/reasoners/adt.mli b/src/lib/reasoners/adt.mli
index fea79eb1e..2cd25de23 100644
--- a/src/lib/reasoners/adt.mli
+++ b/src/lib/reasoners/adt.mli
@@ -25,6 +25,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+val src : Logs.src
+
 type 'a abstract =
   | Constr of {
       c_name : Uid.term_cst;
diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml
index 9e52bb78f..87b8655d1 100644
--- a/src/lib/reasoners/adt_rel.ml
+++ b/src/lib/reasoners/adt_rel.ml
@@ -40,6 +40,9 @@ module DE = Dolmen.Std.Expr
 module DT = Dolmen.Std.Expr.Ty
 module B = Dolmen.Std.Builtin
 
+let src = Logs.Src.create ~doc:"Adt_rel" __MODULE__
+module Log = (val Logs.src_log src : Logs.LOG)
+
 module TSet =
   Set.Make
     (struct
diff --git a/src/lib/reasoners/arith.ml b/src/lib/reasoners/arith.ml
index c95bdb1a5..296d15ce3 100644
--- a/src/lib/reasoners/arith.ml
+++ b/src/lib/reasoners/arith.ml
@@ -32,6 +32,9 @@ module ZA = Z
 module Z = Numbers.Z
 module Q = Numbers.Q
 
+let src = Logs.Src.create ~doc:"Arith" __MODULE__
+module Log = (val Logs.src_log src : Logs.LOG)
+
 let is_mult h = Sy.equal (Sy.Op Sy.Mult) h
 let mod_symb = Sy.name ~ns:Internal "@mod"
 
@@ -83,7 +86,6 @@ module Shostak
   type r = P.r
 
   let name = "arith"
-
   let timer = Timers.M_Arith
 
   (*BISECT-IGNORE-BEGIN*)
diff --git a/src/lib/reasoners/arith.mli b/src/lib/reasoners/arith.mli
index ce95a86b2..63489d53e 100644
--- a/src/lib/reasoners/arith.mli
+++ b/src/lib/reasoners/arith.mli
@@ -25,6 +25,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+val src : Logs.src
+
 (** [calc_power x y t] Compute x^y. Raise Exit if y is not an Int
     (castable in Int). *)
 val calc_power : Numbers.Q.t -> Numbers.Q.t -> Ty.t -> Numbers.Q.t
diff --git a/src/lib/reasoners/arrays_rel.ml b/src/lib/reasoners/arrays_rel.ml
index 2551f2947..4d3f9f5fb 100644
--- a/src/lib/reasoners/arrays_rel.ml
+++ b/src/lib/reasoners/arrays_rel.ml
@@ -35,6 +35,9 @@ module Ex = Explanation
 
 module LR = Uf.LX
 
+let src = Logs.Src.create ~doc:"Arrays_rel" __MODULE__
+module Log = (val Logs.src_log src : Logs.LOG)
+
 (* map get |-> { set } des associations (get,set) deja splites *)
 module Tmap = struct
   include E.Map
diff --git a/src/lib/reasoners/bitv.ml b/src/lib/reasoners/bitv.ml
index a61f10623..12c782ded 100644
--- a/src/lib/reasoners/bitv.ml
+++ b/src/lib/reasoners/bitv.ml
@@ -28,6 +28,9 @@
 module Sy = Symbols
 module E = Expr
 
+let src = Logs.Src.create ~doc:"Bitv" __MODULE__
+module Log = (val Logs.src_log src : Logs.LOG)
+
 type sort_var = A | B | C
 (* The variables used by the bitvector solver can be split into three
    categories that have associated invariants.
@@ -364,7 +367,6 @@ module Shostak(X : ALIEN) = struct
   type r = X.r
 
   let name = "bitv"
-
   let timer = Timers.M_Bitv
 
   let is_mine_symb sy =
diff --git a/src/lib/reasoners/bitv.mli b/src/lib/reasoners/bitv.mli
index 3b5064cb1..77b68f080 100644
--- a/src/lib/reasoners/bitv.mli
+++ b/src/lib/reasoners/bitv.mli
@@ -25,6 +25,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+val src : Logs.src
+
 type 'a alpha_term = {
   bv : 'a;
   sz : int;
diff --git a/src/lib/reasoners/bitv_rel.ml b/src/lib/reasoners/bitv_rel.ml
index e3ee1c5f1..9c6bdbda8 100644
--- a/src/lib/reasoners/bitv_rel.ml
+++ b/src/lib/reasoners/bitv_rel.ml
@@ -25,6 +25,9 @@ module MX = Shostak.MXH
 module HX = Shostak.HX
 module L = Xliteral
 
+let src = Logs.Src.create ~doc:"Bitv_rel" __MODULE__
+module Log = (val Logs.src_log src : Logs.LOG)
+
 let timer = Timers.M_Bitv
 
 let is_bv_ty = function
diff --git a/src/lib/reasoners/ccx.ml b/src/lib/reasoners/ccx.ml
index 5642c89d4..5d9f56787 100644
--- a/src/lib/reasoners/ccx.ml
+++ b/src/lib/reasoners/ccx.ml
@@ -33,6 +33,9 @@ module SE = Expr.Set
 
 module Sy = Symbols
 
+let src = Logs.Src.create ~doc:"Ccx" __MODULE__
+module Log = (val Logs.src_log src : Logs.LOG)
+
 module type S = sig
 
   type t
diff --git a/src/lib/reasoners/ccx.mli b/src/lib/reasoners/ccx.mli
index c121d46c3..83c09ed50 100644
--- a/src/lib/reasoners/ccx.mli
+++ b/src/lib/reasoners/ccx.mli
@@ -25,6 +25,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+val src : Logs.src
+
 module type S = sig
 
   type t
diff --git a/src/lib/reasoners/fun_sat.ml b/src/lib/reasoners/fun_sat.ml
index d382b2f3b..347ef6cc4 100644
--- a/src/lib/reasoners/fun_sat.ml
+++ b/src/lib/reasoners/fun_sat.ml
@@ -30,6 +30,9 @@ module SE = E.Set
 module ME = E.Map
 module Ex = Explanation
 
+let src = Logs.Src.create ~doc:"Sat" __MODULE__
+module Log = (val Logs.src_log src : Logs.LOG)
+
 module Make (Th : Theory.S) = struct
   module Inst = Instances.Make(Th)
   module CDCL = Satml_frontend_hybrid.Make(Th)
diff --git a/src/lib/reasoners/fun_sat.mli b/src/lib/reasoners/fun_sat.mli
index 73376ebab..6e018f04e 100644
--- a/src/lib/reasoners/fun_sat.mli
+++ b/src/lib/reasoners/fun_sat.mli
@@ -25,6 +25,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+val src : Logs.src
+
 (** A functional SAT solver implementation. *)
 module Make (_ : Theory.S) : sig
   type t
diff --git a/src/lib/reasoners/fun_sat_frontend.ml b/src/lib/reasoners/fun_sat_frontend.ml
index abeb97259..af11bfcc8 100644
--- a/src/lib/reasoners/fun_sat_frontend.ml
+++ b/src/lib/reasoners/fun_sat_frontend.ml
@@ -16,6 +16,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
+let src = Logs.Src.create ~doc:"Sat" __MODULE__
+module Log = (val Logs.src_log src : Logs.LOG)
+
 module Make (Th : Theory.S) : Sat_solver_sig.S = struct
   exception Sat
   exception Unsat of Explanation.t
diff --git a/src/lib/reasoners/intervalCalculus.ml b/src/lib/reasoners/intervalCalculus.ml
index aeb8ca415..a11045bf6 100644
--- a/src/lib/reasoners/intervalCalculus.ml
+++ b/src/lib/reasoners/intervalCalculus.ml
@@ -50,6 +50,9 @@ module SX = Shostak.SXH
 module MX0 = Shostak.MXH
 module MPL = Expr.Map
 
+let src = Logs.Src.create ~doc:"IntervalCalculus" __MODULE__
+module Log = (val Logs.src_log src : Logs.LOG)
+
 let oracle =
   lazy (
     let module OracleContainer = (val Inequalities.get_current ()) in
diff --git a/src/lib/reasoners/intervals.ml b/src/lib/reasoners/intervals.ml
index 6e1296b38..61e2a96a1 100644
--- a/src/lib/reasoners/intervals.ml
+++ b/src/lib/reasoners/intervals.ml
@@ -27,25 +27,8 @@
 
 open Intervals_intf
 
-(* Let us pretend we are using [Logs]. *)
-module Log = struct
-  type ('a, 'b) msgf =
-    (?header:string ->
-     ('a, Stdlib.Format.formatter, unit, 'b) Stdlib.format4 -> 'a)
-    -> 'b
-
-  type 'a log = ('a, unit) msgf -> unit
-
-  let module_name = "AltErgoLib.Intervals"
-
-  let debug : 'a log =
-    fun k ->
-    if Options.get_debug_intervals () then
-      k (fun ?header:function_name fmt ->
-          let header = Option.is_some function_name in
-          Printer.print_dbg ~header ~module_name ?function_name fmt
-        )
-end
+let src = Logs.Src.create ~doc:"Intervals" __MODULE__
+module Log = (val Logs.src_log src : Logs.LOG)
 
 let map_bound f = function
   | Unbounded -> Unbounded
diff --git a/src/lib/reasoners/intervals.mli b/src/lib/reasoners/intervals.mli
index 04b7b569e..ebdd8cc8e 100644
--- a/src/lib/reasoners/intervals.mli
+++ b/src/lib/reasoners/intervals.mli
@@ -27,6 +27,8 @@
 
 open Intervals_intf
 
+val src : Logs.src
+
 val map_bound : ('a -> 'b) -> 'a bound -> 'b bound
 (** [map_bound f b] applies [f] to a finite (open or closed) bound [b] and
     does not change an unbounded bound. *)
diff --git a/src/lib/reasoners/ite_rel.ml b/src/lib/reasoners/ite_rel.ml
index 2d7c90759..ccbf93145 100644
--- a/src/lib/reasoners/ite_rel.ml
+++ b/src/lib/reasoners/ite_rel.ml
@@ -51,6 +51,9 @@ module TB =
         if c <> 0 then c else Bool.compare b1 b2
     end)
 
+let src = Logs.Src.create ~doc:"Ite_rel" __MODULE__
+module Log = (val Logs.src_log src : Logs.LOG)
+
 let timer = Timers.M_Ite
 
 (* The present theory simplifies the ite terms t of the form
diff --git a/src/lib/reasoners/matching.ml b/src/lib/reasoners/matching.ml
index e7faf625e..8e9dedd3d 100644
--- a/src/lib/reasoners/matching.ml
+++ b/src/lib/reasoners/matching.ml
@@ -29,6 +29,9 @@ module E = Expr
 module ME = E.Map
 module SubstE = Var.Map
 
+let src = Logs.Src.create ~doc:"Matching" __MODULE__
+module Log = (val Logs.src_log src : Logs.LOG)
+
 module type S = sig
   type t
   type theory
diff --git a/src/lib/reasoners/matching.mli b/src/lib/reasoners/matching.mli
index ac57eac60..249c92307 100644
--- a/src/lib/reasoners/matching.mli
+++ b/src/lib/reasoners/matching.mli
@@ -25,6 +25,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+val src : Logs.src
+
 module type S = sig
   type t
   type theory
diff --git a/src/lib/reasoners/records_rel.ml b/src/lib/reasoners/records_rel.ml
index 0463fac01..84f2a54ea 100644
--- a/src/lib/reasoners/records_rel.ml
+++ b/src/lib/reasoners/records_rel.ml
@@ -27,6 +27,9 @@
 
 type t = unit
 
+let src = Logs.Src.create ~doc:"Records" __MODULE__
+module Log = (val Logs.src_log src : Logs.LOG)
+
 let timer = Timers.M_Records
 
 let empty uf = (), Uf.domains uf
diff --git a/src/lib/reasoners/relation.ml b/src/lib/reasoners/relation.ml
index d36a88526..11b87be87 100644
--- a/src/lib/reasoners/relation.ml
+++ b/src/lib/reasoners/relation.ml
@@ -41,6 +41,9 @@ module Rel5 : Sig_rel.RELATION = Adt_rel
 
 module Rel6 : Sig_rel.RELATION = Ite_rel
 
+(* This source is unused. *)
+let src = Logs.Src.create ~doc:__MODULE__ ("AltErgoLib." ^ __MODULE__)
+
 (* This value is unused. *)
 let timer = Timers.M_None
 
diff --git a/src/lib/reasoners/sat_solver_sig.ml b/src/lib/reasoners/sat_solver_sig.ml
index 6d4a547f5..c8450e6d3 100644
--- a/src/lib/reasoners/sat_solver_sig.ml
+++ b/src/lib/reasoners/sat_solver_sig.ml
@@ -157,5 +157,7 @@ end
 
 
 module type SatContainer = sig
+  val src : Logs.src
+
   module Make (_ : Theory.S) : S
 end
diff --git a/src/lib/reasoners/sat_solver_sig.mli b/src/lib/reasoners/sat_solver_sig.mli
index bb79c01d4..9380bbbbc 100644
--- a/src/lib/reasoners/sat_solver_sig.mli
+++ b/src/lib/reasoners/sat_solver_sig.mli
@@ -137,5 +137,7 @@ end
 
 
 module type SatContainer = sig
+  val src : Logs.src
+
   module Make (_ : Theory.S) : S
 end
diff --git a/src/lib/reasoners/satml.ml b/src/lib/reasoners/satml.ml
index 6345abe07..59248fffa 100644
--- a/src/lib/reasoners/satml.ml
+++ b/src/lib/reasoners/satml.ml
@@ -67,6 +67,9 @@ module FF = Satml_types.Flat_Formula
 
 module Ex = Explanation
 
+let src = Logs.Src.create ~doc:"Sat" __MODULE__
+module Log = (val Logs.src_log src : Logs.LOG)
+
 exception Sat
 exception Unsat of Atom.clause list option
 exception Last_UIP_reason of Atom.Set.t
diff --git a/src/lib/reasoners/satml.mli b/src/lib/reasoners/satml.mli
index 8772104d0..166b2ff5a 100644
--- a/src/lib/reasoners/satml.mli
+++ b/src/lib/reasoners/satml.mli
@@ -36,6 +36,8 @@ type conflict_origin =
   | C_bool of Atom.clause
   | C_theory of Explanation.t
 
+val src : Logs.src
+
 module type SAT_ML = sig
 
   (*module Make (Dummy : sig end) : sig*)
diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml
index 2952a1ea1..2200a8e0a 100644
--- a/src/lib/reasoners/satml_frontend.ml
+++ b/src/lib/reasoners/satml_frontend.ml
@@ -27,6 +27,9 @@
 
 module X = Shostak.Combine
 
+let src = Logs.Src.create ~doc:"Sat" __MODULE__
+module Log = (val Logs.src_log src : Logs.LOG)
+
 module Make (Th : Theory.S) : Sat_solver_sig.S = struct
   module SAT = Satml.Make(Th)
   module Inst = Instances.Make(Th)
diff --git a/src/lib/reasoners/shostak.ml b/src/lib/reasoners/shostak.ml
index 8b308859b..919783407 100644
--- a/src/lib/reasoners/shostak.ml
+++ b/src/lib/reasoners/shostak.ml
@@ -680,6 +680,9 @@ and AC : Ac.S
 module Combine = struct
   include CX
 
+  let src = Logs.Src.create ~doc:"Combine" "AltErgoLib__Combine"
+  module Log = (val Logs.src_log src : Logs.LOG)
+
   module H = Ephemeron.K1.Make(Expr)
 
   let make, save_cache, reinit_cache =
diff --git a/src/lib/reasoners/shostak.mli b/src/lib/reasoners/shostak.mli
index 42d9d7bfa..0fdc94591 100644
--- a/src/lib/reasoners/shostak.mli
+++ b/src/lib/reasoners/shostak.mli
@@ -28,6 +28,8 @@
 module Combine : sig
   include Sig.X
 
+  val src : Logs.src
+
   val top : r
   val bot : r
 end
diff --git a/src/lib/reasoners/sig_rel.mli b/src/lib/reasoners/sig_rel.mli
index c82f9fc80..b8ea9d62d 100644
--- a/src/lib/reasoners/sig_rel.mli
+++ b/src/lib/reasoners/sig_rel.mli
@@ -49,6 +49,8 @@ type 'a result = {
 module type RELATION = sig
   type t
 
+  val src : Logs.src
+
   val timer : Timers.ty_module
 
   val empty : Uf.t -> t * Uf.GlobalDomains.t
diff --git a/src/lib/reasoners/uf.ml b/src/lib/reasoners/uf.ml
index 46f330070..eefe70e82 100644
--- a/src/lib/reasoners/uf.ml
+++ b/src/lib/reasoners/uf.ml
@@ -37,6 +37,9 @@ module SE = Expr.Set
 module LX = Shostak.L
 module MapL = Emap.Make(LX)
 
+let src = Logs.Src.create ~doc:"Uf" __MODULE__
+module Log = (val Logs.src_log src : Logs.LOG)
+
 module MapX = struct
   include Shostak.MXH
   let find m x = Steps.incr (Steps.Uf); find m x
diff --git a/src/lib/reasoners/uf.mli b/src/lib/reasoners/uf.mli
index f231441e6..f73f3f794 100644
--- a/src/lib/reasoners/uf.mli
+++ b/src/lib/reasoners/uf.mli
@@ -34,6 +34,8 @@ type r = Shostak.Combine.r
 type _ id = ..
 (** Extensible type for global domains identifiers, see {!GlobalDomains}. *)
 
+val src : Logs.src
+
 module type GlobalDomain = sig
   (** Module signature for global domains used by the union-find module.
 
diff --git a/src/lib/reasoners/use.ml b/src/lib/reasoners/use.ml
index b02fef1fe..1d6670acd 100644
--- a/src/lib/reasoners/use.ml
+++ b/src/lib/reasoners/use.ml
@@ -39,6 +39,9 @@ module X = Shostak.Combine
 
 module MX = Shostak.MXH
 
+let src = Logs.Src.create ~doc:"Use" __MODULE__
+module Log = (val Logs.src_log src : Logs.LOG)
+
 type t = (SE.t * SA.t) MX.t
 type r = X.r
 
diff --git a/src/lib/reasoners/use.mli b/src/lib/reasoners/use.mli
index 76a9329c6..98e059dee 100644
--- a/src/lib/reasoners/use.mli
+++ b/src/lib/reasoners/use.mli
@@ -30,6 +30,7 @@ module SA : Set.S with type elt = Expr.t * Explanation.t
 type t
 type r = Shostak.Combine.r
 
+val src : Logs.src
 val empty : t
 val find : r -> t -> Expr.Set.t * SA.t
 val add : r -> Expr.Set.t * SA.t -> t -> t
diff --git a/src/lib/structures/commands.ml b/src/lib/structures/commands.ml
index f06b4a5dd..47856b2a4 100644
--- a/src/lib/structures/commands.ml
+++ b/src/lib/structures/commands.ml
@@ -27,6 +27,9 @@
 
 (* Sat entry *)
 
+let src = Logs.Src.create ~doc:"Commands" __MODULE__
+module Log = (val Logs.src_log src : Logs.LOG)
+
 type sat_decl_aux =
   | Decl of Id.typed
   | Assume of string * Expr.t * bool
diff --git a/src/lib/structures/commands.mli b/src/lib/structures/commands.mli
index bc1cafb49..152f1ca0b 100644
--- a/src/lib/structures/commands.mli
+++ b/src/lib/structures/commands.mli
@@ -43,4 +43,6 @@ type sat_tdecl = {
   st_decl : sat_decl_aux
 }
 
+val src : Logs.src
+
 val print : Format.formatter -> sat_tdecl -> unit
diff --git a/src/lib/structures/explanation.ml b/src/lib/structures/explanation.ml
index 28d54f7b9..2896e7b75 100644
--- a/src/lib/structures/explanation.ml
+++ b/src/lib/structures/explanation.ml
@@ -106,7 +106,7 @@ let add_fresh fe s = S.add fe s
 
 let print fmt ex =
   let open Format in
-  if Options.get_debug_explanation () then begin
+  if Options.get_debug_explanations () then begin
     fprintf fmt "{";
     S.iter (function
         | Literal a -> fprintf fmt "{Literal:%a}, " Satml_types.Atom.pr_atom a
diff --git a/src/lib/util/gc_debug.ml b/src/lib/util/gc_debug.ml
index b63e79108..7f36b0201 100644
--- a/src/lib/util/gc_debug.ml
+++ b/src/lib/util/gc_debug.ml
@@ -37,6 +37,9 @@
  major_words; (* num of alloc words in major heap, since beginning *)
 *)
 
+let src = Logs.Src.create ~doc:"Gc_debug" __MODULE__
+module Log = (val Logs.src_log src : Logs.LOG)
+
 let init () =
   if Options.get_debug_gc() then
     begin
diff --git a/src/lib/util/gc_debug.mli b/src/lib/util/gc_debug.mli
index 5fa64511e..c127ae5b3 100644
--- a/src/lib/util/gc_debug.mli
+++ b/src/lib/util/gc_debug.mli
@@ -25,6 +25,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
+val src : Logs.src
+
 (** Prints some debug info about the GC's activity. *)
 val init : unit -> unit
 
diff --git a/src/lib/util/options.ml b/src/lib/util/options.ml
index 6965c53f5..05a24f270 100644
--- a/src/lib/util/options.ml
+++ b/src/lib/util/options.ml
@@ -91,6 +91,21 @@ module Output = struct
   let get_fmt_models () = to_formatter !dump_models_output
 end
 
+module Sources = struct
+  let constr = Logs.Src.create ~doc:"Constr" "AltErgoLib.constr"
+  let fm = Logs.Src.create ~doc:"fm" "AltErgoLib.fm"
+  let fpa = Logs.Src.create ~doc:"fpa" "AltErgoLib.fpa"
+  let interpretation =
+    Logs.Src.create ~doc:"Interpretation" "AltErgoLib.Interpretation"
+  let model = Logs.Src.create ~doc:"Model" "AltErgoLib.Model"
+  let optimize = Logs.Src.create ~doc:"Optimize" "AltErgoLib.Optimize"
+  let split = Logs.Src.create ~doc:"Split" "AltErgoLib.Split"
+  let triggers = Logs.Src.create ~doc:"Triggers" "AltErgoLib.Triggers"
+  let types = Logs.Src.create ~doc:"Types" "AltErgoLib.Types"
+  let typing = Logs.Src.create ~doc:"Typing" "AltErgoLib.Typing"
+  let unsat_core = Logs.Src.create ~doc:"Unsat_core" "AltErgoLib.Unsat_core"
+end
+
 (* Declaration of all the options as refs with default values *)
 
 type instantiation_heuristic = INormal | IAuto | IGreedy
@@ -145,7 +160,7 @@ let debug_bitv = ref false
 let debug_cc = ref false
 let debug_combine = ref false
 let debug_constr = ref false
-let debug_explanation = ref false
+let debug_explanations = ref false
 let debug_fm = ref false
 let debug_intervals = ref false
 let debug_fpa = ref 0
@@ -174,7 +189,7 @@ let set_debug_bitv b = debug_bitv := b
 let set_debug_cc b = debug_cc := b
 let set_debug_combine b = debug_combine := b
 let set_debug_constr b = debug_constr := b
-let set_debug_explanation b = debug_explanation := b
+let set_debug_explanations b = debug_explanations := b
 let set_debug_fm b = debug_fm := b
 let set_debug_intervals b = debug_intervals := b
 let set_debug_fpa i = debug_fpa := i
@@ -203,7 +218,7 @@ let get_debug_bitv () = !debug_bitv
 let get_debug_cc () = !debug_cc
 let get_debug_combine () = !debug_combine
 let get_debug_constr () = !debug_constr
-let get_debug_explanation () = !debug_explanation
+let get_debug_explanations () = !debug_explanations
 let get_debug_fm () = !debug_fm
 let get_debug_intervals () = !debug_intervals
 let get_debug_fpa () = !debug_fpa
diff --git a/src/lib/util/options.mli b/src/lib/util/options.mli
index 3b421b0b8..37006c235 100644
--- a/src/lib/util/options.mli
+++ b/src/lib/util/options.mli
@@ -120,8 +120,8 @@ val set_debug_combine : bool -> unit
 (** Set [debug_constr] accessible with {!val:get_debug_constr} *)
 val set_debug_constr : bool -> unit
 
-(** Set [debug_explanation] accessible with {!val:get_debug_explanation} *)
-val set_debug_explanation : bool -> unit
+(** Set [debug_explanations] accessible with {!val:get_debug_explanations} *)
+val set_debug_explanations : bool -> unit
 
 (** Set [debug_fm] accessible with {!val:get_debug_fm} *)
 val set_debug_fm : bool -> unit
@@ -552,8 +552,8 @@ val get_debug_split : unit -> bool
 *)
 val get_debug_matching : unit -> int
 
-(** Get the debugging flag of explanation. *)
-val get_debug_explanation : unit -> bool
+(** Get the debugging flag of explanations. *)
+val get_debug_explanations : unit -> bool
 
 (** Get the debugging flag of triggers. *)
 val get_debug_triggers : unit -> bool
@@ -1163,6 +1163,20 @@ module Output : sig
       Default to [Format.err_formatter]. *)
 end
 
+module Sources : sig
+  val constr : Logs.src
+  val fm : Logs.src
+  val fpa : Logs.src
+  val interpretation : Logs.src
+  val model : Logs.src
+  val optimize : Logs.src
+  val split : Logs.src
+  val triggers : Logs.src
+  val types : Logs.src
+  val typing : Logs.src
+  val unsat_core : Logs.src
+end
+
 (** Print message as comment in the corresponding output format *)
 val pp_comment: Format.formatter -> string -> unit
 
diff --git a/src/lib/util/printer.ml b/src/lib/util/printer.ml
index 126a33a0e..5a76274e0 100644
--- a/src/lib/util/printer.ml
+++ b/src/lib/util/printer.ml
@@ -414,7 +414,7 @@ let reporter =
         Fmt.kpf k (Options.Output.get_fmt_regular ())
           ("%a@[" ^^ fmt ^^ "@]@.")
           pp_smtlib_header level
-      else if Logs.Src.equal src Sources.model then
+      else if Logs.Src.equal src Options.Sources.model then
         Fmt.kpf k (Options.Output.get_fmt_models ())
           ("@[" ^^ fmt ^^ "@]@.")
       else
diff --git a/src/lib/util/sources.ml b/src/lib/util/sources.ml
deleted file mode 100644
index 65687cab9..000000000
--- a/src/lib/util/sources.ml
+++ /dev/null
@@ -1,87 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*     Alt-Ergo: The SMT Solver For Software Verification                 *)
-(*     Copyright (C) --- OCamlPro SAS                                     *)
-(*                                                                        *)
-(*     This file is distributed under the terms of OCamlPro               *)
-(*     Non-Commercial Purpose License, version 1.                         *)
-(*                                                                        *)
-(*     As an exception, Alt-Ergo Club members at the Gold level can       *)
-(*     use this file under the terms of the Apache Software License       *)
-(*     version 2.0.                                                       *)
-(*                                                                        *)
-(*     ---------------------------------------------------------------    *)
-(*                                                                        *)
-(*     More details can be found in the directory licenses/               *)
-(*                                                                        *)
-(**************************************************************************)
-
-let ac = Logs.Src.create ~doc:"Ac" "AltErgoLib.Ac"
-let adt = Logs.Src.create ~doc:"Adt" "AltErgoLib.Adt"
-let adt_rel = Logs.Src.create ~doc:"Adt_rel" "AltErgoLib.Adt_rel"
-let arith = Logs.Src.create ~doc:"Arith" "AltErgoLib.Arith"
-let arrays_rel = Logs.Src.create ~doc:"Arrays_rel" "AltErgoLib.Arrays_rel"
-let bitv = Logs.Src.create ~doc:"Bitv" "AltErgoLib.Bitv"
-let bitv_rel = Logs.Src.create ~doc:"Bitv_rel" "AltErgoLib.Bitv_rel"
-let cc = Logs.Src.create ~doc:"Cc" "AltErgoLib.Cc"
-let combine = Logs.Src.create ~doc:"combine" "AltErgoLib.combine"
-let commands = Logs.Src.create ~doc:"Commands" "AltErgoLib.commands"
-let constr = Logs.Src.create ~doc:"Constr" "AltErgoLib.constr"
-let explanation =
-  Logs.Src.create ~doc:"explanations" "AltErgoLib.explanation"
-let fm = Logs.Src.create ~doc:"fm" "AltErgoLib.fm"
-let intervals = Logs.Src.create ~doc:"Intervals" "AltErgoLib.Intervals"
-let interval_calculus =
-  Logs.Src.create ~doc:"IntervalCalculus" "AltErgoLib.IntervalCalculus"
-let fpa = Logs.Src.create ~doc:"fpa" "AltErgoLib.fpa"
-let gc_debug = Logs.Src.create ~doc:"Gc_debug" "AltErgoLib.Gc_debug"
-let interpretation =
-  Logs.Src.create ~doc:"Interpretation" "AltErgoLib.Interpretation"
-let ite_rel = Logs.Src.create ~doc:"Ite_rel" "AltErgoLib.Ite_rel"
-let matching = Logs.Src.create ~doc:"Matching" "AltErgoLib.Matching"
-let model = Logs.Src.create ~doc:"Model" "AltErgoLib.Model"
-let optimize = Logs.Src.create ~doc:"Optimize" "AltErgoLib.Optimize"
-let sat = Logs.Src.create ~doc:"Sat" "AltErgoLib.Sat"
-let split = Logs.Src.create ~doc:"Split" "AltErgoLib.Split"
-let triggers = Logs.Src.create ~doc:"Triggers" "AltErgoLib.Triggers"
-let types = Logs.Src.create ~doc:"Types" "AltErgoLib.Types"
-let typing = Logs.Src.create ~doc:"Typing" "AltErgoLib.Typing"
-let uf = Logs.Src.create ~doc:"Uf" "AltErgoLib.Uf"
-let unsat_core = Logs.Src.create ~doc:"Unsat_core" "AltErgoLib.Unsat_core"
-let use = Logs.Src.create ~doc:"Use" "AltErgoLib.Use"
-let warnings = Logs.Src.create ~doc:"Warnings" "AltErgoLib.Warnings"
-
-let all = [
-  ac;
-  adt;
-  adt_rel;
-  arith;
-  arrays_rel;
-  bitv;
-  bitv_rel;
-  cc;
-  combine;
-  commands;
-  constr;
-  explanation;
-  fm;
-  intervals;
-  fpa;
-  gc_debug;
-  interpretation;
-  intervals;
-  interval_calculus;
-  ite_rel;
-  matching;
-  model;
-  optimize;
-  sat;
-  split;
-  triggers;
-  types;
-  typing;
-  uf;
-  unsat_core;
-  use;
-  warnings
-]