diff --git a/src/lib/reasoners/sat_solver_sig.ml b/src/lib/reasoners/sat_solver_sig.ml
index 81b102b2f..d6c568215 100644
--- a/src/lib/reasoners/sat_solver_sig.ml
+++ b/src/lib/reasoners/sat_solver_sig.ml
@@ -110,13 +110,17 @@ module type S = sig
   (** [optimize env ~is_max o] registers the expression [o] as an objective
       function.
 
+      The solver will try to maximize [o] if [is_max] is [true]. Otherwise,
+      it will try to minimize it.
+
       After optimization, the value of this objective is returned by
       [get_objectives]. *)
 
   val unsat : t -> Expr.gformula -> Explanation.t
-  (** [unsat env f size] checks the unsatisfiability of [f] in [env].
+  (** [unsat env f] checks the unsatisfiability of [f] in [env].
 
-      @raise I_dont_know when the proof tree's height reaches [size].
+      @raise I_dont_know if the solver cannot prove the unsatisfiability
+             of [env].
       @raise Sat if [f] is satisfiable in [env]. *)
 
   val reset_refs : unit -> unit
diff --git a/src/lib/reasoners/sat_solver_sig.mli b/src/lib/reasoners/sat_solver_sig.mli
index dc0c88812..7b6939fcd 100644
--- a/src/lib/reasoners/sat_solver_sig.mli
+++ b/src/lib/reasoners/sat_solver_sig.mli
@@ -90,13 +90,17 @@ module type S = sig
   (** [optimize env ~is_max o] registers the expression [o] as an objective
       function.
 
+      The solver will try to maximize [o] if [is_max] is [true]. Otherwise,
+      it will try to minimize it.
+
       After optimization, the value of this objective is returned by
       [get_objectives]. *)
 
   val unsat : t -> Expr.gformula -> Explanation.t
-  (** [unsat env f size] checks the unsatisfiability of [f] in [env].
+  (** [unsat env f] checks the unsatisfiability of [f] in [env].
 
-      @raise I_dont_know when the proof tree's height reaches [size].
+      @raise I_dont_know if the solver cannot prove the unsatisfiability
+             of [env].
       @raise Sat if [f] is satisfiable in [env]. *)
 
   val reset_refs : unit -> unit