diff --git a/Makefile b/Makefile
index aba219b0..2f4a1990 100644
--- a/Makefile
+++ b/Makefile
@@ -67,7 +67,7 @@ reindent:
 
 WATCH=@all
 watch:
-	@dune build $(WATCH) -w
+	@dune build $(WATCH) -w $(OPTS) --profile=release
 	#@dune build @all -w # TODO: once tests pass
 
 .PHONY: clean doc all bench install uninstall remove reinstall bin test
diff --git a/sidekick-bin.opam b/sidekick-bin.opam
index 50202b34..3ebd039f 100644
--- a/sidekick-bin.opam
+++ b/sidekick-bin.opam
@@ -19,10 +19,13 @@ depends: [
   "sidekick" { = version }
   "sidekick-base" { = version }
   "menhir"
-  "mtime"
   "ocaml" { >= "4.04" }
   "odoc" {with-doc}
 ]
+depopts: [
+  "memtrace"
+  "mtime"
+]
 tags: [ "sat" "smt" ]
 homepage: "https://github.com/c-cube/sidekick"
 dev-repo: "git+https://github.com/c-cube/sidekick.git"
diff --git a/src/main/dune b/src/main/dune
index e17a42e6..11c38908 100644
--- a/src/main/dune
+++ b/src/main/dune
@@ -5,7 +5,8 @@
  (public_name sidekick)
  (package sidekick-bin)
  (libraries containers iter result sidekick.sat sidekick.core sidekick-base
-            sidekick.msat-solver sidekick-bin.smtlib sidekick.tef)
+            sidekick.msat-solver sidekick-bin.smtlib sidekick.tef
+            sidekick.memtrace)
  (flags :standard -safe-string -color always -open Sidekick_util))
 
 (rule
diff --git a/src/main/main.ml b/src/main/main.ml
index 64c1c8b0..15a7eae7 100644
--- a/src/main/main.ml
+++ b/src/main/main.ml
@@ -147,8 +147,12 @@ let main_cnf () : _ result =
   Pure_sat_solver.solve solver
 
 let main () =
+
+  (* instrumentation and tracing *)
   Sidekick_tef.setup();
   at_exit Sidekick_tef.teardown;
+  Sidekick_memtrace.trace_if_requested ~context:"sidekick" ();
+
   CCFormat.set_color_default true;
   (* Administrative duties *)
   Arg.parse argspec input_file usage;
diff --git a/src/memtrace/dune b/src/memtrace/dune
new file mode 100644
index 00000000..95085599
--- /dev/null
+++ b/src/memtrace/dune
@@ -0,0 +1,10 @@
+
+(library
+  (name sidekick_memtrace)
+  (public_name sidekick.memtrace)
+  (libraries
+    (select sidekick_memtrace.ml from
+            (memtrace -> sidekick_memtrace.real.ml)
+            (-> sidekick_memtrace.dummy.ml)))
+  (flags :standard -warn-error -a+8))
+
diff --git a/src/memtrace/sidekick_memtrace.dummy.ml b/src/memtrace/sidekick_memtrace.dummy.ml
new file mode 100644
index 00000000..fd147541
--- /dev/null
+++ b/src/memtrace/sidekick_memtrace.dummy.ml
@@ -0,0 +1,2 @@
+
+let trace_if_requested ?context:_ ?sampling_rate:_ () = ()
diff --git a/src/memtrace/sidekick_memtrace.mli b/src/memtrace/sidekick_memtrace.mli
new file mode 100644
index 00000000..28211463
--- /dev/null
+++ b/src/memtrace/sidekick_memtrace.mli
@@ -0,0 +1,3 @@
+
+
+val trace_if_requested : ?context:string -> ?sampling_rate:float -> unit -> unit
diff --git a/src/memtrace/sidekick_memtrace.real.ml b/src/memtrace/sidekick_memtrace.real.ml
new file mode 100644
index 00000000..f2e78004
--- /dev/null
+++ b/src/memtrace/sidekick_memtrace.real.ml
@@ -0,0 +1 @@
+let trace_if_requested = Memtrace.trace_if_requested