diff --git a/sledge/src/fol/arithmetic.ml b/sledge/src/fol/arithmetic.ml
index 532727e68..1e0b82317 100644
--- a/sledge/src/fol/arithmetic.ml
+++ b/sledge/src/fol/arithmetic.ml
@@ -180,6 +180,15 @@ struct
         | _ -> Uninterpreted )
       | `Many -> Interpreted
 
+    let is_uninterpreted poly =
+      match Sum.only_elt poly with
+      | Some (mono, _) -> (
+        match Prod.classify mono with
+        | `Zero -> false
+        | `One (_, 1) -> false
+        | _ -> true )
+      | None -> false
+
     let get_const poly =
       match Sum.classify poly with
       | `Zero -> Some Q.zero
diff --git a/sledge/src/fol/arithmetic_intf.ml b/sledge/src/fol/arithmetic_intf.ml
index 1a092010a..f7d186f8a 100644
--- a/sledge/src/fol/arithmetic_intf.ml
+++ b/sledge/src/fol/arithmetic_intf.ml
@@ -35,6 +35,9 @@ module type S = sig
       [get_const a] is [Some q], [Interpreted] if the principal operation of
       [a] is interpreted, and [Uninterpreted] otherwise. *)
 
+  val is_uninterpreted : t -> bool
+  (** [is_uninterpreted a] iff [classify a = Uninterpreted] *)
+
   (** Construct compound terms *)
 
   val neg : t -> t