diff --git a/src/base-solver/dune b/src/base-solver/dune
index 4f2e8417..c3ef9eae 100644
--- a/src/base-solver/dune
+++ b/src/base-solver/dune
@@ -3,7 +3,7 @@
   (public_name sidekick-base.solver)
   (synopsis "Instantiation of solver and theories for Sidekick_base")
   (libraries sidekick-base sidekick.core sidekick.smt-solver
-             sidekick.th-bool-static
+             sidekick.th-bool-static sidekick.th-dyn-trans
              sidekick.mini-cc sidekick.th-data
              sidekick.arith-lra sidekick.zarith)
   (flags :standard -warn-error -a+8 -safe-string -color always -open Sidekick_util))
diff --git a/src/base-solver/sidekick_base_solver.ml b/src/base-solver/sidekick_base_solver.ml
index 090da86f..9ba3f407 100644
--- a/src/base-solver/sidekick_base_solver.ml
+++ b/src/base-solver/sidekick_base_solver.ml
@@ -116,6 +116,11 @@ module Th_lra = Sidekick_arith_lra.Make(struct
   end
 end)
 
+module Th_dyn_trans = Sidekick_th_dyn_trans.Make(struct
+    module Solver = Solver
+    end)
+
 let th_bool : Solver.theory = Th_bool.theory
 let th_data : Solver.theory = Th_data.theory
 let th_lra : Solver.theory = Th_lra.theory
+let th_dyn_trans : Solver.theory = Th_dyn_trans.theory
diff --git a/src/main/main.ml b/src/main/main.ml
index 483bc4f0..bd01970e 100644
--- a/src/main/main.ml
+++ b/src/main/main.ml
@@ -107,6 +107,7 @@ let main_smt () : _ result =
         Process.th_bool;
         Process.th_data;
         Process.th_lra;
+        Process.th_dyn_trans;
       ]
     in
     Process.Solver.create ~proof ~theories tst () ()
diff --git a/src/smtlib/Process.ml b/src/smtlib/Process.ml
index b9e2b435..05995298 100644
--- a/src/smtlib/Process.ml
+++ b/src/smtlib/Process.ml
@@ -282,7 +282,9 @@ let process_stmt
 module Th_data = SBS.Th_data
 module Th_bool = SBS.Th_bool
 module Th_lra = SBS.Th_lra
+module Th_dyn_trans = SBS.Th_dyn_trans
 
 let th_bool : Solver.theory = Th_bool.theory
 let th_data : Solver.theory = Th_data.theory
 let th_lra : Solver.theory = Th_lra.theory
+let th_dyn_trans : Solver.theory = Th_dyn_trans.theory
diff --git a/src/smtlib/Process.mli b/src/smtlib/Process.mli
index eba0bed4..e9cb983b 100644
--- a/src/smtlib/Process.mli
+++ b/src/smtlib/Process.mli
@@ -12,6 +12,7 @@ module Solver
 val th_bool : Solver.theory
 val th_data : Solver.theory
 val th_lra : Solver.theory
+val th_dyn_trans : Solver.theory
 
 type 'a or_error = ('a, string) CCResult.t