diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml
index eda7ceaa..9ed15426 100644
--- a/src/core/Sidekick_core.ml
+++ b/src/core/Sidekick_core.ml
@@ -658,6 +658,5 @@ module type SOLVER = sig
         if any, will be a subset of [assumptions].
       @param on_exit functions to be run before this returns *)
 
-  val pp_term_graph: t CCFormat.printer
   val pp_stats : t CCFormat.printer
 end
diff --git a/src/msat-solver/Sidekick_msat_solver.ml b/src/msat-solver/Sidekick_msat_solver.ml
index 2d2492d0..b625c4ea 100644
--- a/src/msat-solver/Sidekick_msat_solver.ml
+++ b/src/msat-solver/Sidekick_msat_solver.ml
@@ -1,8 +1,6 @@
 (** {1 Implementation of a Solver using Msat} *)
 
-module Vec = Msat.Vec
 module Log = Msat.Log
-module IM = Util.Int_map
 
 module type ARG = sig
   open Sidekick_core
@@ -553,10 +551,6 @@ module Make(A : ARG)
 
   (** {2 Main} *)
 
-  (* print all terms reachable from watched literals *)
-  let pp_term_graph _out (_:t) =
-    () (* TODO *)
-
   let pp_stats out (self:t) : unit =
     Stat.pp_all out (Stat.all @@ stats self)
 
@@ -566,11 +560,6 @@ module Make(A : ARG)
 
   let add_clause_l self c = add_clause self (IArray.of_list c)
 
-  (* TODO: remove? use a special constant + micro theory instead?
-  let[@inline] assume_distinct self l ~neq lit : unit =
-    CC.assert_distinct (cc self) l lit ~neq
-     *)
-
   let mk_model (self:t) (lits:lit Iter.t) : Model.t =
     Log.debug 1 "(smt.solver.mk-model)";
     let module M = Term.Tbl in
@@ -592,13 +581,6 @@ module Make(A : ARG)
     (* TODO: theory combination *)
     Model.Map m
 
-  let check_model (_s:t) : unit =
-    Log.debug 1 "(smt.solver.check-model)";
-    (* TODO
-    Sat_solver.check_model s.solver
-    *)
-    ()
-
   let solve ?(on_exit=[]) ?(check=true) ?(on_progress=fun _ -> ())
       ~assumptions (self:t) : res =
     let do_on_exit () =