diff --git a/src/backend/Coq.ml b/src/backend/Coq.ml
deleted file mode 100644
index ffb736fd..00000000
--- a/src/backend/Coq.ml
+++ /dev/null
@@ -1,193 +0,0 @@
-(*
-MSAT is free software, using the Apache license, see file LICENSE
-Copyright 2015 Guillaume Bury
-*)
-
-module type S = Backend_intf.S
-
-module type Arg = sig
-
-  type hyp
-  type lemma
-  type assumption
-
-  val prove_hyp : Format.formatter -> string -> hyp -> unit
-  val prove_lemma : Format.formatter -> string -> lemma -> unit
-  val prove_assumption : Format.formatter -> string -> assumption -> unit
-
-end
-
-module Make(S : Msat.S)(A : Arg with type hyp := S.clause
-                                and type lemma := S.clause
-                                and type assumption := S.clause) = struct
-
-  module Atom = S.Atom
-  module Clause = S.Clause
-  module M = Map.Make(S.Atom)
-  module C_tbl = S.Clause.Tbl
-  module P = S.Proof
-
-  let name = Clause.name
-
-  let clause_map c =
-    let rec aux acc a i =
-      if i >= Array.length a then acc
-      else begin
-        let name = Format.sprintf "A%d" i in
-        aux (M.add a.(i) name acc) a (i + 1)
-      end
-    in
-    aux M.empty (Clause.atoms c) 0
-
-  let clause_iter m format fmt clause =
-    let aux atom = Format.fprintf fmt format (M.find atom m) in
-    Array.iter aux (Clause.atoms clause)
-
-  let elim_duplicate fmt goal hyp _ =
-    (** Printing info comment in coq *)
-    Format.fprintf fmt
-      "(* Eliminating doublons. Goal : %s ; Hyp : %s *)@\n"
-      (name goal) (name hyp);
-    (** Prove the goal: intro the atoms, then use them with the hyp *)
-    let m = clause_map goal in
-    Format.fprintf fmt "pose proof @[<hov>(fun %a=>@ %s%a) as %s@].@\n"
-      (clause_iter m "%s@ ") goal (name hyp)
-      (clause_iter m "@ %s") hyp (name goal)
-
-  let resolution_aux m a h1 h2 fmt () =
-    Format.fprintf fmt "%s%a" (name h1)
-      (fun fmt -> Array.iter (fun b ->
-           if b == a then begin
-             Format.fprintf fmt "@ (fun p =>@ %s%a)"
-               (name h2) (fun fmt -> (Array.iter (fun c ->
-                   if Atom.equal c (Atom.neg a) then
-                     Format.fprintf fmt "@ (fun np => np p)"
-                   else
-                     Format.fprintf fmt "@ %s" (M.find c m)))
-                 ) (Clause.atoms h2)
-           end else
-             Format.fprintf fmt "@ %s" (M.find b m)
-         )) (Clause.atoms h1)
-
-  let resolution fmt goal hyp1 hyp2 atom =
-    let a = Atom.abs atom in
-    let h1, h2 =
-      if Array.exists (Atom.equal a) (Clause.atoms hyp1) then hyp1, hyp2
-      else (
-        assert (Array.exists (Atom.equal a) (Clause.atoms hyp2));
-        hyp2, hyp1
-      )
-    in
-    (** Print some debug info *)
-    Format.fprintf fmt
-      "(* Clausal resolution. Goal : %s ; Hyps : %s, %s *)@\n"
-      (name goal) (name h1) (name h2);
-    (** Prove the goal: intro the axioms, then perform resolution *)
-    if Array.length (Clause.atoms goal) = 0 then (
-      let m = M.empty in
-      Format.fprintf fmt "exact @[<hov 1>(%a)@].@\n" (resolution_aux m a h1 h2) ();
-      false
-    ) else (
-      let m = clause_map goal in
-      Format.fprintf fmt "pose proof @[<hov>(fun %a=>@ %a)@ as %s.@]@\n"
-        (clause_iter m "%s@ ") goal (resolution_aux m a h1 h2) () (name goal);
-      true
-    )
-
-  (* Count uses of hypotheses *)
-  let incr_use h c =
-    let i = try C_tbl.find h c with Not_found -> 0 in
-    C_tbl.add h c (i + 1)
-
-  let decr_use h c =
-    let i = C_tbl.find h c - 1 in
-    assert (i >= 0);
-    let () = C_tbl.add h c i in
-    i <= 0
-
-  let clear fmt c =
-    Format.fprintf fmt "clear %s." (name c)
-
-  let rec clean_aux fmt = function
-    | [] -> ()
-    | [x] ->
-      Format.fprintf fmt "%a@\n" clear x
-    | x :: ((_ :: _) as r) ->
-      Format.fprintf fmt "%a@ %a" clear x clean_aux r
-
-  let clean h fmt l =
-    match List.filter (decr_use h) l with
-    | [] -> ()
-    | l' ->
-      Format.fprintf fmt "(* Clearing unused clauses *)@\n%a" clean_aux l'
-
-  let prove_node t fmt node =
-    let clause = node.P.conclusion in
-    match node.P.step with
-    | P.Hypothesis _ ->
-      A.prove_hyp fmt (name clause) clause
-    | P.Assumption ->
-      A.prove_assumption fmt (name clause) clause
-    | P.Lemma _ ->
-      A.prove_lemma fmt (name clause) clause
-    | P.Duplicate (p, l) ->
-      let c = P.conclusion p in
-      let () = elim_duplicate fmt clause c l in
-      clean t fmt [c]
-    | P.Hyper_res hr ->
-      let (p1, p2, a) = P.res_of_hyper_res hr in
-      let c1 = P.conclusion p1 in
-      let c2 = P.conclusion p2 in
-      if resolution fmt clause c1 c2 a then clean t fmt [c1; c2]
-
-  let count_uses p =
-    let h = C_tbl.create 128 in
-    let aux () node =
-      List.iter (fun p' -> incr_use h P.(conclusion p')) (P.parents node.P.step)
-    in
-    let () = P.fold aux () p in
-    h
-
-  (* Here the main idea is to always try and have exactly
-     one goal to prove, i.e False. So each  *)
-  let pp fmt p =
-    let h = count_uses p in
-    let aux () node =
-      Format.fprintf fmt "%a" (prove_node h) node
-    in
-    Format.fprintf fmt "(* Coq proof generated by mSAT*)@\n";
-    P.fold aux () p
-end
-
-
-module Simple(S : Msat.S)
-    (A : Arg with type hyp = S.formula list
-              and type lemma := S.lemma
-              and type assumption := S.formula) =
-  Make(S)(struct
-    module P = S.Proof
-
-    (* Some helpers *)
-    let lit = S.Atom.formula
-
-    let get_assumption c =
-      match S.Clause.atoms_l c with
-      | [ x ] -> x
-      | _ -> assert false
-
-    let get_lemma c =
-      match P.expand (P.prove c) with
-      | {P.step=P.Lemma p; _} -> p
-      | _ -> assert false
-
-    let prove_hyp fmt name c =
-      A.prove_hyp fmt name (List.map lit (S.Clause.atoms_l c))
-
-    let prove_lemma fmt name c =
-      A.prove_lemma fmt name (get_lemma c)
-
-    let prove_assumption fmt name c =
-      A.prove_assumption fmt name (lit (get_assumption c))
-
-  end)
-
diff --git a/src/backend/Coq.mli b/src/backend/Coq.mli
deleted file mode 100644
index 3d34f549..00000000
--- a/src/backend/Coq.mli
+++ /dev/null
@@ -1,46 +0,0 @@
-(*
-MSAT is free software, using the Apache license, see file LICENSE
-Copyright 2015 Guillaume Bury
-*)
-
-(** Coq Backend
-
-    This module provides an easy way to produce coq scripts
-    corresponding to the resolution proofs output by the
-    sat solver. *)
-
-module type S = Backend_intf.S
-(** Interface for exporting proofs. *)
-
-module type Arg = sig
-  (** Term printing for Coq *)
-
-  type hyp
-  type lemma
-  type assumption
-  (** The types of hypotheses, lemmas, and assumptions *)
-
-  val prove_hyp : Format.formatter -> string -> hyp -> unit
-  val prove_lemma : Format.formatter -> string -> lemma -> unit
-  val prove_assumption : Format.formatter -> string -> assumption -> unit
-  (** Proving function for hypotheses, lemmas and assumptions.
-      [prove_x fmt name x] should prove [x], and be such that after
-      executing it, [x] is among the coq hypotheses under the name [name].
-      The hypothesis should be the encoding of the given clause, i.e
-      for a clause [a \/ not b \/ c], the proved hypothesis should be:
-      [ ~ a -> ~ ~ b -> ~ c -> False ], keeping the same order as the
-      one in the atoms array of the clause. *)
-
-end
-
-module Make(S : Msat.S)(A : Arg with type hyp := S.clause
-                                and type lemma := S.clause
-                                and type assumption := S.clause) : S with type t := S.proof
-(** Base functor to output Coq proofs *)
-
-
-module Simple(S : Msat.S)(A : Arg with type hyp = S.formula list
-                                  and type lemma := S.lemma
-                                  and type assumption := S.formula) : S with type t := S.proof
-(** Simple functor to output Coq proofs *)
-
diff --git a/src/backend/Dedukti.ml b/src/backend/Dedukti.ml
deleted file mode 100644
index 7f8526eb..00000000
--- a/src/backend/Dedukti.ml
+++ /dev/null
@@ -1,62 +0,0 @@
-(*
-MSAT is free software, using the Apache license, see file LICENSE
-Copyright 2015 Guillaume Bury
-*)
-
-module type S = Backend_intf.S
-
-module type Arg = sig
-
-  type proof
-  type lemma
-  type formula
-
-  val pp : Format.formatter -> formula -> unit
-  val prove : Format.formatter -> lemma -> unit
-  val context : Format.formatter -> proof -> unit
-end
-
-module Make(S : Msat.S)(A : Arg with type formula := S.formula
-                                and type lemma := S.lemma
-                                and type proof := S.proof) = struct
-  module P = S.Proof
-
-  let pp_nl fmt = Format.fprintf fmt "@\n"
-  let fprintf fmt format = Format.kfprintf pp_nl fmt format
-
-  let _clause_name = S.Clause.name
-
-  let _pp_clause fmt c =
-    let rec aux fmt = function
-      | [] -> ()
-      | a :: r ->
-        let f, pos =
-          if S.Atom.sign a then
-            S.Atom.formula a, true
-          else
-            S.Atom.formula (S.Atom.neg a), false
-        in
-        fprintf fmt "%s _b %a ->@ %a"
-          (if pos then "_pos" else "_neg") A.pp f aux r
-    in
-    fprintf fmt "_b : Prop ->@ %a ->@ _proof _b" aux (S.Clause.atoms_l c)
-
-  let context fmt p =
-    fprintf fmt "(; Embedding ;)";
-    fprintf fmt "Prop : Type.";
-    fprintf fmt "_proof : Prop -> Type.";
-    fprintf fmt "(; Notations for clauses ;)";
-    fprintf fmt "_pos : Prop -> Prop -> Type.";
-    fprintf fmt "_neg : Prop -> Prop -> Type.";
-    fprintf fmt "[b: Prop, p: Prop] _pos b p --> _proof p -> _proof b.";
-    fprintf fmt "[b: Prop, p: Prop] _neg b p --> _pos b p -> _proof b.";
-    A.context fmt p
-
-  let pp fmt p =
-    fprintf fmt "#NAME Proof.";
-    fprintf fmt "(; Dedukti file automatically generated by mSAT ;)";
-    context fmt p;
-    ()
-
-end
-
diff --git a/src/backend/Dedukti.mli b/src/backend/Dedukti.mli
deleted file mode 100644
index ef7cc88e..00000000
--- a/src/backend/Dedukti.mli
+++ /dev/null
@@ -1,32 +0,0 @@
-(*
-MSAT is free software, using the Apache license, see file LICENSE
-Copyright 2014 Guillaume Bury
-Copyright 2014 Simon Cruanes
-*)
-
-(** Deduki backend for proofs
-
-    Work in progress...
-*)
-
-module type S = Backend_intf.S
-
-module type Arg = sig
-
-  type lemma
-  type proof
-  type formula
-
-  val pp : Format.formatter -> formula -> unit
-  val prove : Format.formatter -> lemma -> unit
-  val context : Format.formatter -> proof -> unit
-end
-
-module Make :
-  functor(S : Msat.S) ->
-  functor(A : Arg
-          with type formula := S.formula
-           and type lemma := S.lemma
-           and type proof := S.proof) ->
-    S with type t := S.proof
-(** Functor to generate a backend to output proofs for the dedukti type checker. *)
diff --git a/src/backend/Dot.ml b/src/backend/Dot.ml
index 9097cc45..632f39a7 100644
--- a/src/backend/Dot.ml
+++ b/src/backend/Dot.ml
@@ -28,7 +28,7 @@ module type Arg = sig
 
 end
 
-module Default(S : Msat.S) = struct
+module Default(S : Sidekick_sat.S) = struct
   module Atom = S.Atom
   module Clause = S.Clause
 
@@ -49,7 +49,7 @@ module Default(S : Msat.S) = struct
 end
 
 (** Functor to provide dot printing *)
-module Make(S : Msat.S)(A : Arg with type atom := S.atom
+module Make(S : Sidekick_sat.S)(A : Arg with type atom := S.atom
                                 and type hyp := S.clause
                                 and type lemma := S.clause
                                 and type assumption := S.clause) = struct
@@ -151,7 +151,7 @@ module Make(S : Msat.S)(A : Arg with type atom := S.atom
 
 end
 
-module Simple(S : Msat.S)
+module Simple(S : Sidekick_sat.S)
     (A : Arg with type atom := S.formula
               and type hyp = S.formula list
               and type lemma := S.lemma
diff --git a/src/backend/Dot.mli b/src/backend/Dot.mli
index 70adffa1..13ccc703 100644
--- a/src/backend/Dot.mli
+++ b/src/backend/Dot.mli
@@ -47,20 +47,20 @@ module type Arg = sig
 
 end
 
-module Default(S : Msat.S) : Arg with type atom := S.atom
+module Default(S : Sidekick_sat.S) : Arg with type atom := S.atom
                                  and type hyp := S.clause
                                  and type lemma := S.clause
                                  and type assumption := S.clause
 (** Provides a reasonnable default to instantiate the [Make] functor, assuming
     the original printing functions are compatible with DOT html labels. *)
 
-module Make(S : Msat.S)(A : Arg with type atom := S.atom
+module Make(S : Sidekick_sat.S)(A : Arg with type atom := S.atom
                                 and type hyp := S.clause
                                 and type lemma := S.clause
                                 and type assumption := S.clause) : S with type t := S.proof
 (** Functor for making a module to export proofs to the DOT format. *)
 
-module Simple(S : Msat.S)(A : Arg with type atom := S.formula
+module Simple(S : Sidekick_sat.S)(A : Arg with type atom := S.formula
                                   and type hyp = S.formula list
                                   and type lemma := S.lemma
                                   and type assumption = S.formula) : S with type t := S.proof
diff --git a/src/backend/dune b/src/backend/dune
index 7febb3bc..316c6d7a 100644
--- a/src/backend/dune
+++ b/src/backend/dune
@@ -1,10 +1,6 @@
 (library
-  (name msat_backend)
-  (public_name msat.backend)
-  (synopsis "proof backends for msat")
-  (libraries msat)
-  (flags :standard -w +a-4-42-44-48-50-58-32-60@8 -warn-error -27 -color always -safe-string)
-  (ocamlopt_flags :standard -O3 -bin-annot
-                  -unbox-closures -unbox-closures-factor 20)
-  )
+  (name sidekick_backend)
+  (public_name sidekick.backend)
+  (synopsis "Proof backends for sidekick")
+  (libraries sidekick.sat))
 
diff --git a/src/backtrack/Backtrackable_ref.ml b/src/backtrack/Backtrackable_ref.ml
deleted file mode 100644
index bc91cfd5..00000000
--- a/src/backtrack/Backtrackable_ref.ml
+++ /dev/null
@@ -1,29 +0,0 @@
-
-type 'a t = {
-  mutable cur: 'a;
-  stack: 'a Vec.t;
-  copy: ('a -> 'a) option;
-}
-
-let create ?copy x: _ t =
-  {cur=x; stack=Vec.create(); copy}
-
-let[@inline] get self = self.cur
-let[@inline] set self x = self.cur <- x
-let[@inline] update self f = self.cur <- f self.cur
-
-let[@inline] n_levels self = Vec.size self.stack
-
-let[@inline] push_level self : unit =
-  let x = self.cur in
-  let x = match self.copy with None -> x | Some f -> f x in
-  Vec.push self.stack x
-
-let pop_levels self n : unit =
-  assert (n>=0);
-  if n > Vec.size self.stack then invalid_arg "Backtrackable_ref.pop_levels";
-  let i = Vec.size self.stack-n in
-  let x = Vec.get self.stack i in
-  self.cur <- x;
-  Vec.shrink self.stack i;
-  ()
diff --git a/src/backtrack/Backtrackable_ref.mli b/src/backtrack/Backtrackable_ref.mli
deleted file mode 100644
index a1755115..00000000
--- a/src/backtrack/Backtrackable_ref.mli
+++ /dev/null
@@ -1,30 +0,0 @@
-
-(** {1 Backtrackable ref} *)
-
-type 'a t
-
-val create : ?copy:('a -> 'a) -> 'a -> 'a t
-(** Create a backtrackable reference holding the given value initially.
-    @param copy if provided, will be used to copy the value when [push_level]
-    is called. *)
-
-val set : 'a t -> 'a -> unit
-(** Set the reference's current content *)
-
-val get : 'a t -> 'a
-(** Get the reference's current content *)
-
-val update : 'a t -> ('a -> 'a) -> unit
-(** Update the reference's current content *)
-  
-val push_level : _ t -> unit
-(** Push a backtracking level, copying the current value on top of some
-    stack. The [copy] function will be used if it was provided in {!create}. *)
-
-val n_levels : _ t -> int
-(** Number of saved values *)
-
-val pop_levels : _ t -> int -> unit
-(** Pop [n] levels, restoring to the value the reference was storing [n] calls
-    to [push_level] earlier.
-    @raise Invalid_argument if [n] is bigger than [n_levels]. *)
diff --git a/src/backtrack/Msat_backtrack.ml b/src/backtrack/Msat_backtrack.ml
deleted file mode 100644
index 14857855..00000000
--- a/src/backtrack/Msat_backtrack.ml
+++ /dev/null
@@ -1,2 +0,0 @@
-
-module Ref = Backtrackable_ref
diff --git a/src/backtrack/dune b/src/backtrack/dune
deleted file mode 100644
index 48740ab9..00000000
--- a/src/backtrack/dune
+++ /dev/null
@@ -1,11 +0,0 @@
-
-(library
-  (name msat_backtrack)
-  (public_name msat.backtrack)
-  (libraries msat)
-  (synopsis "backtrackable data structures for msat")
-  (flags :standard -warn-error -3 -w +a-4-42-44-48-50-58-32-60@8
-         -color always -safe-string -open Msat)
-  (ocamlopt_flags :standard -O3 -bin-annot
-                  -unbox-closures -unbox-closures-factor 20)
-  )
diff --git a/src/base/Base_types.ml b/src/base/Base_types.ml
index 97fc2562..c788cf97 100644
--- a/src/base/Base_types.ml
+++ b/src/base/Base_types.ml
@@ -1,7 +1,7 @@
 (** Basic type definitions for Sidekick_base *)
 
-module Vec = Msat.Vec
-module Log = Msat.Log
+module Vec = Sidekick_util.Vec
+module Log = Sidekick_util.Log
 module Fmt = CCFormat
 
 module CC_view = Sidekick_core.CC_view
diff --git a/src/main/main.ml b/src/main/main.ml
index 8b61bb49..6651aca3 100644
--- a/src/main/main.ml
+++ b/src/main/main.ml
@@ -11,7 +11,6 @@ module Fmt = CCFormat
 module Term = Sidekick_base.Term
 module Solver = Sidekick_smtlib.Solver
 module Process = Sidekick_smtlib.Process
-module Vec = Msat.Vec
 
 type 'a or_error = ('a, string) E.t
 
diff --git a/src/msat-solver/Sidekick_msat_solver.ml b/src/msat-solver/Sidekick_msat_solver.ml
index 139d2694..e9881926 100644
--- a/src/msat-solver/Sidekick_msat_solver.ml
+++ b/src/msat-solver/Sidekick_msat_solver.ml
@@ -1,12 +1,10 @@
-(** {1 Implementation of a Solver using Msat} *)
+(** Core of the SMT solver using Sidekick_sat
 
-(** {{: https://github.com/Gbury/mSAT/} Msat} is a modular SAT solver in
+    Sidekick_sat (in src/sat/) is a modular SAT solver in
     pure OCaml.
 
-    This builds a {!Sidekick_core.SOLVER} on top of it. *)
-
-module Log = Msat.Log
-(** A logging module *)
+    This builds a {!Sidekick_core.SOLVER} on top of it.
+*)
 
 (** Argument to pass to the functor {!Make} in order to create a
     new Msat-based SMT solver. *)
@@ -76,7 +74,7 @@ module Make(A : ARG)
   type lit = Lit_.t
 
   (* actions from msat *)
-  type msat_acts = (Msat.void, lit, Msat.void, P.t) Msat.acts
+  type msat_acts = (Sidekick_sat.void, lit, Sidekick_sat.void, P.t) Sidekick_sat.acts
 
   (* the full argument to the congruence closure *)
   module CC_actions = struct
@@ -91,10 +89,10 @@ module Make(A : ARG)
       module Lit = Lit
       type t = msat_acts
       let[@inline] raise_conflict a lits pr =
-        a.Msat.acts_raise_conflict lits pr
+        a.Sidekick_sat.acts_raise_conflict lits pr
       let[@inline] propagate a lit ~reason =
-        let reason = Msat.Consequence reason in
-        a.Msat.acts_propagate lit reason
+        let reason = Sidekick_sat.Consequence reason in
+        a.Sidekick_sat.acts_propagate lit reason
     end
   end
 
@@ -218,7 +216,7 @@ module Make(A : ARG)
       include Lit
       let norm lit =
         let lit', sign = norm_sign lit in
-        lit', if sign then Msat.Same_sign else Msat.Negated
+        lit', if sign then Sidekick_sat.Same_sign else Sidekick_sat.Negated
     end
     module Eq_class = CC.N
     module Expl = CC.Expl
@@ -244,22 +242,22 @@ module Make(A : ARG)
 
     let push_decision (_self:t) (acts:actions) (lit:lit) : unit =
       let sign = Lit.sign lit in
-      acts.Msat.acts_add_decision_lit (Lit.abs lit) sign
+      acts.Sidekick_sat.acts_add_decision_lit (Lit.abs lit) sign
 
     let[@inline] raise_conflict self acts c proof : 'a =
       Stat.incr self.count_conflict;
-      acts.Msat.acts_raise_conflict c proof
+      acts.Sidekick_sat.acts_raise_conflict c proof
 
     let[@inline] propagate self acts p ~reason : unit =
       Stat.incr self.count_propagate;
-      acts.Msat.acts_propagate p (Msat.Consequence reason)
+      acts.Sidekick_sat.acts_propagate p (Sidekick_sat.Consequence reason)
 
     let[@inline] propagate_l self acts p cs proof : unit =
       propagate self acts p ~reason:(fun()->cs,proof)
 
     let add_sat_clause_ self acts ~keep lits (proof:P.t) : unit =
       Stat.incr self.count_axiom;
-      acts.Msat.acts_add_clause ~keep lits proof
+      acts.Sidekick_sat.acts_add_clause ~keep lits proof
 
     let preprocess_term_ (self:t) ~add_clause (t:term) : term * proof =
       let mk_lit t = Lit.atom self.tst t in (* no further simplification *)
@@ -377,7 +375,7 @@ module Make(A : ARG)
     let[@inline] add_clause_permanent self acts lits (proof:P.t) : unit =
       add_sat_clause_ self acts ~keep:true lits proof
 
-    let add_lit _self acts lit : unit = acts.Msat.acts_mk_lit lit
+    let add_lit _self acts lit : unit = acts.Sidekick_sat.acts_mk_lit lit
 
     let add_lit_t self acts ?sign t =
       let lit = mk_lit self acts ?sign t in
@@ -429,7 +427,7 @@ module Make(A : ARG)
 
     (* handle a literal assumed by the SAT solver *)
     let assert_lits_ ~final (self:t) (acts:actions) (lits:Lit.t Iter.t) : unit =
-      Msat.Log.debugf 2
+      Sidekick_sat.Log.debugf 2
         (fun k->k "(@[<hv1>@{<green>msat-solver.assume_lits@}%s[lvl=%d]@ %a@])"
             (if final then "[final]" else "") self.level (Util.pp_iter ~sep:"; " Lit.pp) lits);
       (* transmit to CC *)
@@ -458,26 +456,26 @@ module Make(A : ARG)
 
     let[@inline] iter_atoms_ acts : _ Iter.t =
       fun f ->
-      acts.Msat.acts_iter_assumptions
+      acts.Sidekick_sat.acts_iter_assumptions
         (function
-          | Msat.Lit a -> f a
-          | Msat.Assign _ -> assert false)
+          | Sidekick_sat.Lit a -> f a
+          | Sidekick_sat.Assign _ -> assert false)
 
     (* propagation from the bool solver *)
     let check_ ~final (self:t) (acts: msat_acts) =
       let pb = if final then Profile.begin_ "solver.final-check" else Profile.null_probe in
       let iter = iter_atoms_ acts in
-      Msat.Log.debugf 5 (fun k->k "(msat-solver.assume :len %d)" (Iter.length iter));
+      Sidekick_sat.Log.debugf 5 (fun k->k "(msat-solver.assume :len %d)" (Iter.length iter));
       self.on_progress();
       assert_lits_ ~final self acts iter;
       Profile.exit pb
 
     (* propagation from the bool solver *)
-    let[@inline] partial_check (self:t) (acts:_ Msat.acts) : unit =
+    let[@inline] partial_check (self:t) (acts:_ Sidekick_sat.acts) : unit =
       check_ ~final:false self acts
 
     (* perform final check of the model *)
-    let[@inline] final_check (self:t) (acts:_ Msat.acts) : unit =
+    let[@inline] final_check (self:t) (acts:_ Sidekick_sat.acts) : unit =
       check_ ~final:true self acts
 
     let create ~stat (tst:Term.store) (ty_st:Ty.store) () : t =
@@ -510,7 +508,7 @@ module Make(A : ARG)
   module Lit = Solver_internal.Lit
 
   (** the parametrized SAT Solver *)
-  module Sat_solver = Msat.Make_cdcl_t(Solver_internal)
+  module Sat_solver = Sidekick_sat.Make_cdcl_t(Solver_internal)
 
   module Atom = Sat_solver.Atom
 
@@ -528,7 +526,7 @@ module Make(A : ARG)
 
     let pp_dot =
       let module Dot =
-        Msat_backend.Dot.Make(Sat_solver)(Msat_backend.Dot.Default(Sat_solver)) in
+        Sidekick_backend.Dot.Make(Sat_solver)(Sidekick_backend.Dot.Default(Sat_solver)) in
       let pp out self = Dot.pp out self.msat in
       Some pp
 
@@ -925,9 +923,9 @@ module Make(A : ARG)
           let pr = us.get_proof () in
           if check then Sat_solver.Proof.check pr;
           Some (Pre_proof.make pr (List.rev self.si.t_defs))
-        with Msat.Solver_intf.No_proof -> None
+        with Sidekick_sat.Solver_intf.No_proof -> None
       ) in
-      let unsat_core = lazy (us.Msat.unsat_assumptions ()) in
+      let unsat_core = lazy (us.Sidekick_sat.unsat_assumptions ()) in
       do_on_exit ();
       Unsat {proof; unsat_core}
 
diff --git a/src/msat-solver/dune b/src/msat-solver/dune
index 8e6100cd..78d55808 100644
--- a/src/msat-solver/dune
+++ b/src/msat-solver/dune
@@ -2,5 +2,5 @@
  (name Sidekick_msat_solver)
  (public_name sidekick.msat-solver)
  (libraries containers iter sidekick.core sidekick.util
-            sidekick.cc sidekick.sat)
+            sidekick.cc sidekick.sat sidekick.backend)
  (flags :standard -open Sidekick_util))
diff --git a/src/sat/Heap_intf.ml b/src/sat/Heap_intf.ml
index bee623e6..e7d4aee7 100644
--- a/src/sat/Heap_intf.ml
+++ b/src/sat/Heap_intf.ml
@@ -1,8 +1,13 @@
 
 module type RANKED = sig
   type t
-  val idx: t -> int (** Index in heap. return -1 if never set *)
-  val set_idx : t -> int -> unit (** Update index in heap *)
+
+  val idx: t -> int
+  (** Index in heap. return -1 if never set *)
+
+  val set_idx : t -> int -> unit
+  (** Update index in heap *)
+
   val cmp : t -> t -> bool
 end
 
diff --git a/src/sat/Msat.ml b/src/sat/Sidekick_sat.ml
similarity index 100%
rename from src/sat/Msat.ml
rename to src/sat/Sidekick_sat.ml
diff --git a/src/sat/dune b/src/sat/dune
index 85a23d9a..25a4c2cf 100644
--- a/src/sat/dune
+++ b/src/sat/dune
@@ -1,10 +1,10 @@
 
 (library
-  (name msat)
-  (public_name msat)
-  (libraries iter)
-  (synopsis "core data structures and algorithms for msat")
-  (flags :standard -warn-error -3 -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string)
+  (name sidekick_sat)
+  (public_name sidekick.sat)
+  (libraries iter sidekick.util)
+  (synopsis "Pure OCaml SAT solver implementation for sidekick")
+  (flags :standard -open Sidekick_util)
   (ocamlopt_flags :standard -O3 -bin-annot
                   -unbox-closures -unbox-closures-factor 20)
   )
diff --git a/src/util/Backtrack_stack.ml b/src/util/Backtrack_stack.ml
index 890be02f..81b78f37 100644
--- a/src/util/Backtrack_stack.ml
+++ b/src/util/Backtrack_stack.ml
@@ -1,6 +1,4 @@
 
-module Vec = Msat.Vec
-
 type 'a t = {
   vec: 'a Vec.t;
   lvls: int Vec.t;
diff --git a/src/sat/Log.ml b/src/util/Log.ml
similarity index 83%
rename from src/sat/Log.ml
rename to src/util/Log.ml
index f60603ea..b93d4a7f 100644
--- a/src/sat/Log.ml
+++ b/src/util/Log.ml
@@ -1,8 +1,3 @@
-(*
-MSAT is free software, using the Apache license, see file LICENSE
-Copyright 2014 Guillaume Bury
-Copyright 2014 Simon Cruanes
-*)
 
 (** {1 Logging functions, real version} *)
 
diff --git a/src/sat/Log.mli b/src/util/Log.mli
similarity index 60%
rename from src/sat/Log.mli
rename to src/util/Log.mli
index 8923f8e3..f6b7f435 100644
--- a/src/sat/Log.mli
+++ b/src/util/Log.mli
@@ -1,15 +1,13 @@
-(*
-MSAT is free software, using the Apache license, see file LICENSE
-Copyright 2014 Guillaume Bury
-Copyright 2014 Simon Cruanes
-*)
 
-(** {1 Logging function, for debugging} *)
+(** Logging function, for debugging *)
 
 val enabled : bool
 
-val set_debug : int -> unit (** Set debug level *)
-val get_debug : unit -> int (** Current debug level *)
+val set_debug : int -> unit
+(** Set debug level *)
+
+val get_debug : unit -> int
+(** Current debug level *)
 
 val debugf :
   int ->
diff --git a/src/util/Sidekick_util.ml b/src/util/Sidekick_util.ml
index 01ae1f46..09b56058 100644
--- a/src/util/Sidekick_util.ml
+++ b/src/util/Sidekick_util.ml
@@ -1,9 +1,10 @@
 (* re-exports *)
 module Fmt = CCFormat
-module Vec = Msat.Vec
-module Log = Msat.Log
+
 
 module Util = Util
+module Vec = Vec
+module Log = Log
 module Backtrack_stack = Backtrack_stack
 module Backtrackable_tbl = Backtrackable_tbl
 module Error = Error
diff --git a/src/sat/Vec.ml b/src/util/Vec.ml
similarity index 100%
rename from src/sat/Vec.ml
rename to src/util/Vec.ml
diff --git a/src/sat/Vec.mli b/src/util/Vec.mli
similarity index 91%
rename from src/sat/Vec.mli
rename to src/util/Vec.mli
index d51a2b69..b4994de4 100644
--- a/src/sat/Vec.mli
+++ b/src/util/Vec.mli
@@ -1,4 +1,11 @@
 
+(** Vectors
+
+    A resizable array, workhorse of imperative programming :-).
+    This implementation originated in alt-ergo-zero but has been basically rewritten
+    from scratch several times since.
+*)
+
 type 'a t
 (** Abstract type of vectors of 'a *)