diff --git a/sledge/src/symbheap/equality.ml b/sledge/src/symbheap/equality.ml
index ad540b638..550841549 100644
--- a/sledge/src/symbheap/equality.ml
+++ b/sledge/src/symbheap/equality.ml
@@ -22,10 +22,19 @@ type t =
             'rep(resentative)' of [a] *) }
 [@@deriving compare, equal, sexp]
 
+(** apply a subst to a term *)
+let apply s a = Map.find s a |> Option.value ~default:a
+
 let classes r =
+  let add key data cls =
+    if Term.equal key data then cls
+    else Map.add_multi cls ~key:data ~data:key
+  in
   Map.fold r.rep ~init:empty_map ~f:(fun ~key ~data cls ->
-      if Term.equal key data then cls
-      else Map.add_multi cls ~key:data ~data:key )
+      match Term.classify key with
+      | `Interpreted | `Atomic -> add key data cls
+      | `Simplified | `Uninterpreted ->
+          add (Term.map ~f:(apply r.rep) key) data cls )
 
 (** Pretty-printing *)
 
@@ -106,9 +115,6 @@ let invariant r =
 
 let true_ = {sat= true; rep= empty_map} |> check invariant
 
-(** apply a subst to a term *)
-let apply s a = Map.find s a |> Option.value ~default:a
-
 (** apply a subst to maximal non-interpreted subterms *)
 let rec norm s a =
   match Term.classify a with
diff --git a/sledge/src/symbheap/equality_test.ml b/sledge/src/symbheap/equality_test.ml
index fdccd60bc..d0e5563ff 100644
--- a/sledge/src/symbheap/equality_test.ml
+++ b/sledge/src/symbheap/equality_test.ml
@@ -140,8 +140,8 @@ let%test_module _ =
       pp r3 ;
       [%expect
         {|
-      %t_1 = %u_2 = %v_3 = %w_4 = %x_5 = %z_7 = (%y_6 rem %v_3)
-      = (%y_6 rem %z_7)
+      %t_1 = %u_2 = %v_3 = %w_4 = %x_5 = %z_7 = (%y_6 rem %t_1)
+      = (%y_6 rem %t_1)
 
       {sat= true;
        rep= [[%u_2 ↦ %t_1];
@@ -343,8 +343,7 @@ let%test_module _ =
     let r15 = of_eqs [(b, b); (x, !1)]
 
     let%expect_test _ =
-      pp r15 ; [%expect {|
-          {sat= true; rep= [[%x_5 ↦ 1]]} |}]
+      pp r15 ; [%expect {| {sat= true; rep= [[%x_5 ↦ 1]]} |}]
 
     let%test _ = entails_eq r15 b (Term.signed 1 !1)
     let%test _ = entails_eq r15 (Term.unsigned 1 b) !1
@@ -391,6 +390,6 @@ let%test_module _ =
                [((u8) %x_5) ↦ %x_5];
                [((u8) %y_6) ↦ ]]}
 
-        (((u8) %y_6) + 1) = %y_6
-        ∧ %x_5 = ((u8) %x_5) |}]
+        (((u8) %y_6) + 1) = %y_6 ∧ %x_5 = ((u8) %x_5)
+        ∧ ((u8) %y_6) = ((u8) (((u8) %y_6) + 1)) |}]
   end )
diff --git a/sledge/src/symbheap/solver_test.ml b/sledge/src/symbheap/solver_test.ml
index edc1bb65c..75f57f32a 100644
--- a/sledge/src/symbheap/solver_test.ml
+++ b/sledge/src/symbheap/solver_test.ml
@@ -196,6 +196,7 @@ let%test_module _ =
         ) infer_frame:
           ∃ %a0_10, %a1_11 .
             %a_2 = %a0_10
+          ∧ ⟨%n_9,%a0_10⟩ = ⟨16,%a_2⟩
           ∧ ⟨32,%a_1⟩ = ⟨%n_9,%a0_10⟩^⟨16,%a1_11⟩
           ∧ 16 = %m_8 = %n_9
           ∧ (%k_5 + 16) -[ %k_5, 16 )-> ⟨16,%a1_11⟩ |}]