diff --git a/sledge/src/fol/context.ml b/sledge/src/fol/context.ml
index afd5d824d..0724ba7fd 100644
--- a/sledge/src/fol/context.ml
+++ b/sledge/src/fol/context.ml
@@ -14,16 +14,15 @@ open Exp
 type kind = Interpreted | Atomic | Uninterpreted
 [@@deriving compare, equal]
 
-let rec classify e =
+let classify e =
   match (e : Trm.t) with
+  | Var _ | Z _ | Q _ | Concat [||] | Apply (_, [||]) -> Atomic
   | Arith a -> (
     match Trm.Arith.classify a with
-    | Trm t -> classify t
-    | Const _ -> Atomic
+    | Trm _ | Const _ -> violates Trm.invariant e
     | Interpreted -> Interpreted
     | Uninterpreted -> Uninterpreted )
   | Splat _ | Sized _ | Extract _ | Concat _ -> Interpreted
-  | Var _ | Z _ | Q _ -> Atomic
   | Apply _ -> Uninterpreted
 
 let interpreted e = equal_kind (classify e) Interpreted
diff --git a/sledge/src/fol/trm.ml b/sledge/src/fol/trm.ml
index 3336387b0..18886f9c2 100644
--- a/sledge/src/fol/trm.ml
+++ b/sledge/src/fol/trm.ml
@@ -88,6 +88,9 @@ and Trm : sig
 
   val ppx : Var.strength -> t pp
   val pp : t pp
+
+  include Invariant.S with type t := t
+
   val _Var : int -> string -> t
   val _Z : Z.t -> t
   val _Q : Q.t -> t
diff --git a/sledge/src/fol/trm.mli b/sledge/src/fol/trm.mli
index d2d05d002..eb76a33c2 100644
--- a/sledge/src/fol/trm.mli
+++ b/sledge/src/fol/trm.mli
@@ -47,6 +47,8 @@ val ppx : Var.strength -> t pp
 val pp : t pp
 val pp_diff : (t * t) pp
 
+include Invariant.S with type t := t
+
 (** Construct *)
 
 (* variables *)