diff --git a/solver/mcsolver.ml b/solver/mcsolver.ml
index 8549cf3b..fd1bcb45 100644
--- a/solver/mcsolver.ml
+++ b/solver/mcsolver.ml
@@ -8,7 +8,7 @@ module Make (E : Expr_intf.S)
     (Th : Plugin_intf.S with type term = E.Term.t and type formula = E.Formula.t and type proof = E.proof)
     (Dummy: sig end) = struct
 
-  module St = Solver_types.McMake(E)
+  module St = Solver_types.McMake(E)(struct end)
 
   module M = Internal.Make(St)(Th)(struct end)
 
diff --git a/solver/solver.ml b/solver/solver.ml
index 22b12a5a..b6b53e88 100644
--- a/solver/solver.ml
+++ b/solver/solver.ml
@@ -104,7 +104,7 @@ module Make (E : Formula_intf.S)
 
   module P = Plugin(E)(Th)
 
-  module St = Solver_types.SatMake(E)
+  module St = Solver_types.SatMake(E)(struct end)
 
   module S = Internal.Make(St)(P)(struct end)
 
diff --git a/solver/solver_types.ml b/solver/solver_types.ml
index 084e0495..297cbdc6 100644
--- a/solver/solver_types.ml
+++ b/solver/solver_types.ml
@@ -18,7 +18,7 @@ module type S = Solver_types_intf.S
 (* Solver types for McSat Solving *)
 (* ************************************************************************ *)
 
-module McMake (E : Expr_intf.S) = struct
+module McMake (E : Expr_intf.S)(Dummy : sig end) = struct
 
   (* Flag for Mcsat v.s Pure Sat *)
   let mcsat = true
@@ -297,12 +297,12 @@ end
 (* Solver types for pure SAT Solving *)
 (* ************************************************************************ *)
 
-module SatMake (E : Formula_intf.S) = struct
+module SatMake (E : Formula_intf.S)(Dummy : sig end) = struct
   include McMake(struct
       include E
       module Term = E
       module Formula = E
-    end)
+    end)(struct end)
 
   let mcsat = false
 end
diff --git a/solver/solver_types.mli b/solver/solver_types.mli
index 58b5efc3..550e0736 100644
--- a/solver/solver_types.mli
+++ b/solver/solver_types.mli
@@ -14,12 +14,12 @@
 module type S = Solver_types_intf.S
 
 module McMake :
-  functor (E : Expr_intf.S) ->
+  functor (E : Expr_intf.S)(Dummy : sig end) ->
     S with type term = E.Term.t and type formula = E.Formula.t and type proof = E.proof
 (** Functor to instantiate the types of clauses for a solver. *)
 
 module SatMake :
-  functor (E : Formula_intf.S) ->
+  functor (E : Formula_intf.S)(Dummy : sig end) ->
     S with type term = E.t and type formula = E.t and type proof = E.proof
 (** Functor to instantiate the types of clauses for a solver. *)