diff --git a/src/lib/reasoners/fun_sat_frontend.ml b/src/lib/reasoners/fun_sat_frontend.ml
index 548d0660c..af11bfcc8 100644
--- a/src/lib/reasoners/fun_sat_frontend.ml
+++ b/src/lib/reasoners/fun_sat_frontend.ml
@@ -71,6 +71,4 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
     raise (Util.Not_implemented "optimization is not supported by FunSAT.")
 
   let supports_optimization = false
-
-  let is_unsat _env = assert false
 end
diff --git a/src/lib/reasoners/sat_solver_sig.ml b/src/lib/reasoners/sat_solver_sig.ml
index 5fee28bc7..88871e497 100644
--- a/src/lib/reasoners/sat_solver_sig.ml
+++ b/src/lib/reasoners/sat_solver_sig.ml
@@ -159,7 +159,6 @@ module type S = sig
 
   val supports_optimization : bool
   (** Returns whether the solver supports optimization. *)
-  val is_unsat : t -> bool
 end
 
 
diff --git a/src/lib/reasoners/sat_solver_sig.mli b/src/lib/reasoners/sat_solver_sig.mli
index 9708be562..e76f38c24 100644
--- a/src/lib/reasoners/sat_solver_sig.mli
+++ b/src/lib/reasoners/sat_solver_sig.mli
@@ -139,7 +139,6 @@ module type S = sig
 
   val supports_optimization : bool
   (** Returns whether the solver supports optimization. *)
-  val is_unsat : t -> bool
 end
 
 
diff --git a/src/lib/reasoners/satml.ml b/src/lib/reasoners/satml.ml
index 07212fb86..66f2028b6 100644
--- a/src/lib/reasoners/satml.ml
+++ b/src/lib/reasoners/satml.ml
@@ -140,8 +140,6 @@ module type SAT_ML = sig
   val pop : t -> unit
 
   val optimize : t -> Objective.Function.t -> unit
-
-  val is_unsat : t -> bool
 end
 
 module MFF = FF.Map
@@ -2290,6 +2288,4 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
     else
       Vec.replace (fun fns -> fn :: fns) env.objectives
         (Vec.size env.objectives - 1)
-
-  let is_unsat env = env.is_unsat
 end
diff --git a/src/lib/reasoners/satml.mli b/src/lib/reasoners/satml.mli
index bbc039c26..166b2ff5a 100644
--- a/src/lib/reasoners/satml.mli
+++ b/src/lib/reasoners/satml.mli
@@ -97,8 +97,6 @@ module type SAT_ML = sig
       [env].
 
       @raise invalid_argurment if the decision level of [env] is not zero. *)
-
-  val is_unsat : t -> bool
 end
 
 module Make (Th : Theory.S) : SAT_ML with type th = Th.t
diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml
index d5a6088b0..5df266d06 100644
--- a/src/lib/reasoners/satml_frontend.ml
+++ b/src/lib/reasoners/satml_frontend.ml
@@ -1478,7 +1478,6 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
     Shostak.Combine.save_cache ();
     Uf.save_cache ()
 
-  let is_unsat env = SAT.is_unsat env.satml
 end
 
 (*