diff --git a/src/base/Solver.ml b/src/base/Solver.ml
index 837cabf3..c6adfb2f 100644
--- a/src/base/Solver.ml
+++ b/src/base/Solver.ml
@@ -3,7 +3,6 @@ include Sidekick_smt_solver.Solver
 let default_arg =
   (module struct
     let view_as_cc = Term.view_as_cc
-    let is_valid_literal _ = true
   end : Sidekick_smt_solver.Sigs.ARG)
 
 let create_default ?stat ?size ~proof ~theories tst : t =
diff --git a/src/smt/sigs.ml b/src/smt/sigs.ml
index 20ee7b04..9d7c871d 100644
--- a/src/smt/sigs.ml
+++ b/src/smt/sigs.ml
@@ -42,8 +42,4 @@ type th_combination_conflict = {
     new Msat-based SMT solver. *)
 module type ARG = sig
   val view_as_cc : Sidekick_cc.view_as_cc
-
-  val is_valid_literal : Term.t -> bool
-  (** Is this a valid boolean literal? (e.g. is it a closed term, not inside
-      a quantifier) *)
 end
diff --git a/src/smt/solver.ml b/src/smt/solver.ml
index 5d65eadf..235967f6 100644
--- a/src/smt/solver.ml
+++ b/src/smt/solver.ml
@@ -99,7 +99,6 @@ let create arg ?(stat = Stat.global) ?size ~proof ~theories tst () : t =
 let default_arg =
   (module struct
     let view_as_cc = Default_cc_view.view_as_cc
-    let is_valid_literal _ = true
   end : ARG)
 
 let create_default ?stat ?size ~proof ~theories tst () : t =