diff --git a/src/core/Backtrackable_ref.ml b/src/backtrack/Backtrackable_ref.ml
similarity index 100%
rename from src/core/Backtrackable_ref.ml
rename to src/backtrack/Backtrackable_ref.ml
diff --git a/src/core/Backtrackable_ref.mli b/src/backtrack/Backtrackable_ref.mli
similarity index 100%
rename from src/core/Backtrackable_ref.mli
rename to src/backtrack/Backtrackable_ref.mli
diff --git a/src/backtrack/Msat_backtrack.ml b/src/backtrack/Msat_backtrack.ml
new file mode 100644
index 00000000..14857855
--- /dev/null
+++ b/src/backtrack/Msat_backtrack.ml
@@ -0,0 +1,2 @@
+
+module Ref = Backtrackable_ref
diff --git a/src/backtrack/dune b/src/backtrack/dune
new file mode 100644
index 00000000..48740ab9
--- /dev/null
+++ b/src/backtrack/dune
@@ -0,0 +1,11 @@
+
+(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/core/Msat.ml b/src/core/Msat.ml
index 2ef93ebe..a913e968 100644
--- a/src/core/Msat.ml
+++ b/src/core/Msat.ml
@@ -68,8 +68,6 @@ module Make_mcsat = Solver.Make_mcsat
 module Make_cdcl_t = Solver.Make_cdcl_t
 module Make_pure_sat = Solver.Make_pure_sat
 
-module Backtrackable_ref = Backtrackable_ref
-
 (**/**)
 module Vec = Vec
 module Log = Log
diff --git a/src/sudoku/dune b/src/sudoku/dune
index 0800a980..ad4a2b92 100644
--- a/src/sudoku/dune
+++ b/src/sudoku/dune
@@ -2,7 +2,7 @@
 (executable
   (name sudoku_solve)
   (modes native)
-  (libraries msat sequence containers)
+  (libraries msat msat.backtrack sequence containers)
   (flags :standard -warn-error -a -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string)
   (ocamlopt_flags :standard -O3 -bin-annot
                   -unbox-closures -unbox-closures-factor 20)
diff --git a/src/sudoku/sudoku_solve.ml b/src/sudoku/sudoku_solve.ml
index 2b2f6de4..ffbba32c 100644
--- a/src/sudoku/sudoku_solve.ml
+++ b/src/sudoku/sudoku_solve.ml
@@ -125,7 +125,7 @@ end = struct
     a
 end
 
-module B_ref = Msat.Backtrackable_ref
+module B_ref = Msat_backtrack.Ref
 
 module Solver : sig
   type t