diff --git a/sledge/src/llair/term.ml b/sledge/src/llair/term.ml
index dbcbec9cb..07c6014ac 100644
--- a/sledge/src/llair/term.ml
+++ b/sledge/src/llair/term.ml
@@ -497,7 +497,7 @@ let simp_extract ~unsigned bits arg =
   | _ -> Ap1 (Extract {unsigned; bits}, arg)
 
 let simp_convert ~unsigned dst src arg =
-  if (not unsigned) && Typ.castable dst src then arg
+  if (not unsigned) && Typ.equivalent dst src then arg
   else
     match (dst, src, arg) with
     | Integer {bits= m}, Integer {bits= n}, Integer {data} ->
diff --git a/sledge/src/llair/typ.ml b/sledge/src/llair/typ.ml
index c425749d7..beb333f6d 100644
--- a/sledge/src/llair/typ.ml
+++ b/sledge/src/llair/typ.ml
@@ -121,6 +121,16 @@ let rec prim_bit_size_of = function
       Option.map (prim_bit_size_of elt) ~f:(fun n -> n * len)
   | Function _ | Tuple _ | Struct _ | Opaque _ -> None
 
+let rec equivalent t0 t1 =
+  match (t0, t1) with
+  | (Pointer _ | Integer _), (Pointer _ | Integer _) -> (
+    match (prim_bit_size_of t0, prim_bit_size_of t1) with
+    | Some n0, Some n1 -> n0 = n1
+    | _ -> false )
+  | Array {elt= t; len= m}, Array {elt= u; len= n} ->
+      m = n && equivalent t u
+  | _ -> equal t0 t1
+
 let rec castable t0 t1 =
   match (t0, t1) with
   | (Pointer _ | Integer _), (Pointer _ | Integer _) -> (
diff --git a/sledge/src/llair/typ.mli b/sledge/src/llair/typ.mli
index 37fbf6f80..e1fbaaef2 100644
--- a/sledge/src/llair/typ.mli
+++ b/sledge/src/llair/typ.mli
@@ -54,6 +54,10 @@ val prim_bit_size_of : t -> int option
 val is_sized : t -> bool
 (** Holds of types which are first-class and have a statically-known size. *)
 
+val equivalent : t -> t -> bool
+(** Equivalent types are those that denote the same sets of values in the
+    semantic model. An equivalence relation. *)
+
 val castable : t -> t -> bool
 (** Castable types are those that can be cast between without loss of
     information. An equivalence relation. *)