diff --git a/sat/sat.ml b/sat/sat.ml
index 6c68d8e0..2a570338 100644
--- a/sat/sat.ml
+++ b/sat/sat.ml
@@ -71,7 +71,7 @@ module Make(Dummy : sig end) = struct
   type clause = SatSolver.St.clause
   type proof = SatSolver.Proof.proof
 
-  let tag_clause cl = SatSolver.St.(cl.tag)
+  let tag_clause = SatSolver.tag_clause
 
   type res =
     | Sat
diff --git a/solver/solver.ml b/solver/solver.ml
index c71e07c7..0915797d 100644
--- a/solver/solver.ml
+++ b/solver/solver.ml
@@ -101,5 +101,6 @@ module Make (E : Formula_intf.S)
 
   include S
 
+  let tag_clause cl = St.(cl.tag)
 end
 
diff --git a/solver/solver.mli b/solver/solver.mli
index 56bd14ad..aec7be1f 100644
--- a/solver/solver.mli
+++ b/solver/solver.mli
@@ -38,6 +38,9 @@ module Make (F : Formula_intf.S)
       Modifies the sat solver state in place.
       @raise Unsat if a conflict is detect when adding the clauses *)
 
+  val tag_clause : St.clause -> int option
+  (** Recover tag from a clause, if any *)
+
   val eval : F.t -> bool
   (** Returns the valuation of a formula in the current state
       of the sat solver. *)