diff --git a/sledge/lib/equality.ml b/sledge/lib/equality.ml
index 2e669e240..465c69b4a 100644
--- a/sledge/lib/equality.ml
+++ b/sledge/lib/equality.ml
@@ -9,7 +9,7 @@
 
 (** Classification of Terms by Theory *)
 
-type kind = Interpreted | Simplified | Atomic | Uninterpreted
+type kind = Interpreted | Atomic | Uninterpreted
 [@@deriving compare, equal]
 
 let classify e =
@@ -19,7 +19,6 @@ let classify e =
    |Ap3 (Extract, _, _, _)
    |ApN (Concat, _) ->
       Interpreted
-  | Ap2 ((Eq | Dq), _, _) -> Simplified
   | Ap1 _ | Ap2 _ | Ap3 _ | ApN _ -> Uninterpreted
   | RecN _ | Var _ | Integer _ | Rational _ | Float _ | Nondet _ | Label _
     ->
@@ -86,10 +85,7 @@ end = struct
 
   (** apply a substitution to maximal non-interpreted subterms *)
   let rec norm s a =
-    match classify a with
-    | Interpreted -> Term.map ~f:(norm s) a
-    | Simplified -> apply s (Term.map ~f:(norm s) a)
-    | Atomic | Uninterpreted -> apply s a
+    if interpreted a then Term.map ~f:(norm s) a else apply s a
 
   (** compose two substitutions *)
   let compose r s =
@@ -353,8 +349,8 @@ let classes r =
   Subst.fold r.rep ~init:Term.Map.empty ~f:(fun ~key ~data cls ->
       match classify key with
       | Interpreted | Atomic -> add key data cls
-      | Simplified | Uninterpreted ->
-          add (Term.map ~f:(Subst.apply r.rep) key) data cls )
+      | Uninterpreted -> add (Term.map ~f:(Subst.apply r.rep) key) data cls
+  )
 
 let cls_of r e =
   let e' = Subst.apply r.rep e in
@@ -469,29 +465,26 @@ let rec canon r a =
   ( match classify a with
   | Atomic -> Subst.apply r.rep a
   | Interpreted -> Term.map ~f:(canon r) a
-  | Simplified | Uninterpreted -> (
+  | Uninterpreted -> (
       let a' = Term.map ~f:(canon r) a in
       match classify a' with
       | Atomic -> Subst.apply r.rep a'
       | Interpreted -> a'
-      | Simplified | Uninterpreted -> lookup r a' ) )
+      | Uninterpreted -> lookup r a' ) )
   |>
   [%Trace.retn fun {pf} -> pf "%a" Term.pp]
 
 let rec extend_ a r =
   (* omit identity mappings for constants *)
   if Term.is_constant a then r
-  else
-    match classify a with
     (* omit interpreted terms, but consider their subterms *)
-    | Interpreted | Simplified -> Term.fold ~f:extend_ a ~init:r
+  else if interpreted a then Term.fold ~f:extend_ a ~init:r
+  else
     (* add uninterpreted terms *)
-    | Uninterpreted -> (
-      match Subst.extend a r with
-      (* and their subterms if newly added *)
-      | Some r -> Term.fold ~f:extend_ a ~init:r
-      | None -> r )
-    | Atomic -> r
+    match Subst.extend a r with
+    (* and their subterms if newly added *)
+    | Some r -> Term.fold ~f:extend_ a ~init:r
+    | None -> r
 
 (** add a term to the carrier *)
 let extend a r =
diff --git a/sledge/lib/equality_test.ml b/sledge/lib/equality_test.ml
index 0e620605a..793b164a9 100644
--- a/sledge/lib/equality_test.ml
+++ b/sledge/lib/equality_test.ml
@@ -64,19 +64,24 @@ let%test_module _ =
     let f2 = of_eqs [(x, x + !1)]
 
     let%test _ = is_false f2
-    let%expect_test _ = pp f2 ; [%expect {| {sat= false; rep= []} |}]
+
+    let%expect_test _ =
+      pp f2 ; [%expect {| {sat= false; rep= [[%x_5 ↦ ]]} |}]
 
     let f3 = of_eqs [(x + !0, x + !1)]
 
     let%test _ = is_false f3
-    let%expect_test _ = pp f3 ; [%expect {| {sat= false; rep= []} |}]
+
+    let%expect_test _ =
+      pp f3 ; [%expect {| {sat= false; rep= [[%x_5 ↦ ]]} |}]
 
     let f4 = of_eqs [(x, y); (x + !0, y + !1)]
 
     let%test _ = is_false f4
 
     let%expect_test _ =
-      pp f4 ; [%expect {| {sat= false; rep= [[%y_6 ↦ %x_5]]} |}]
+      pp f4 ;
+      [%expect {| {sat= false; rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]]} |}]
 
     let t1 = of_eqs [(!1, !1)]
 
@@ -103,8 +108,8 @@ let%test_module _ =
       [%expect
         {|
         %x_5 = %y_6
-    
-      {sat= true; rep= [[%y_6 ↦ %x_5]]} |}]
+
+      {sat= true; rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]]} |}]
 
     let%test _ = entails_eq r1 x y
 
@@ -118,7 +123,10 @@ let%test_module _ =
         %x_5 = %y_6 = %z_7 = ((u8) %x_5)
 
       {sat= true;
-       rep= [[%y_6 ↦ %x_5]; [%z_7 ↦ %x_5]; [((u8) %x_5) ↦ %x_5]]} |}]
+       rep= [[%x_5 ↦ ];
+             [%y_6 ↦ %x_5];
+             [%z_7 ↦ %x_5];
+             [((u8) %x_5) ↦ %x_5]]} |}]
 
     let%test _ = entails_eq r2 x z
     let%test _ = entails_eq (or_ r1 r2) x y
@@ -139,11 +147,11 @@ let%test_module _ =
       pp rs ;
       [%expect
         {|
-        {sat= true; rep= [[%y_6 ↦ %w_4]; [%z_7 ↦ %w_4]]}
+        {sat= true; rep= [[%w_4 ↦ ]; [%y_6 ↦ %w_4]; [%z_7 ↦ %w_4]]}
     
-        {sat= true; rep= [[%y_6 ↦ %x_5]; [%z_7 ↦ %x_5]]}
+        {sat= true; rep= [[%x_5 ↦ ]; [%y_6 ↦ %x_5]; [%z_7 ↦ %x_5]]}
     
-        {sat= true; rep= [[%z_7 ↦ %y_6]]} |}]
+        {sat= true; rep= [[%y_6 ↦ ]; [%z_7 ↦ %y_6]]} |}]
 
     let%test _ =
       let r = of_eqs [(w, y); (y, z)] in
@@ -162,10 +170,12 @@ let%test_module _ =
         = (%y_6 rem %t_1)
 
       {sat= true;
-       rep= [[%u_2 ↦ %t_1];
+       rep= [[%t_1 ↦ ];
+             [%u_2 ↦ %t_1];
              [%v_3 ↦ %t_1];
              [%w_4 ↦ %t_1];
              [%x_5 ↦ %t_1];
+             [%y_6 ↦ ];
              [%z_7 ↦ %t_1];
              [(%y_6 rem %v_3) ↦ %t_1];
              [(%y_6 rem %z_7) ↦ %t_1]]} |}]
@@ -186,7 +196,8 @@ let%test_module _ =
       {sat= true;
        rep= [[%w_4 ↦ (%z_7 + 3)];
              [%x_5 ↦ (%z_7 + 8)];
-             [%y_6 ↦ (%z_7 + -4)]]} |}]
+             [%y_6 ↦ (%z_7 + -4)];
+             [%z_7 ↦ ]]} |}]
 
     let%test _ = entails_eq r4 x (w + !5)
     let%test _ = difference r4 x w |> Poly.equal (Some (Z.of_int 5))
@@ -219,10 +230,19 @@ let%test_module _ =
         {|
           %v_3 = %x_5 ∧ %w_4 = %y_6 = %z_7
     
-        {sat= true; rep= [[%x_5 ↦ %v_3]; [%y_6 ↦ %w_4]; [%z_7 ↦ %w_4]]}
+        {sat= true;
+         rep= [[%v_3 ↦ ];
+               [%w_4 ↦ ];
+               [%x_5 ↦ %v_3];
+               [%y_6 ↦ %w_4];
+               [%z_7 ↦ %w_4]]}
 
         {sat= true;
-         rep= [[%w_4 ↦ %v_3]; [%x_5 ↦ %v_3]; [%y_6 ↦ %v_3]; [%z_7 ↦ %v_3]]}
+         rep= [[%v_3 ↦ ];
+               [%w_4 ↦ %v_3];
+               [%x_5 ↦ %v_3];
+               [%y_6 ↦ %v_3];
+               [%z_7 ↦ %v_3]]}
 
           %v_3 = %w_4 = %x_5 = %y_6 = %z_7 |}]
 
@@ -248,7 +268,11 @@ let%test_module _ =
         %v_3 = %w_4 = %x_5 = %y_6 = %z_7
 
       {sat= true;
-       rep= [[%w_4 ↦ %v_3]; [%x_5 ↦ %v_3]; [%y_6 ↦ %v_3]; [%z_7 ↦ %v_3]]} |}]
+       rep= [[%v_3 ↦ ];
+             [%w_4 ↦ %v_3];
+             [%x_5 ↦ %v_3];
+             [%y_6 ↦ %v_3];
+             [%z_7 ↦ %v_3]]} |}]
 
     let%test _ = normalize r7' w |> Term.equal v
 
@@ -267,7 +291,7 @@ let%test_module _ =
         {|
         (13 × %z_7) = %x_5 ∧ 14 = %y_6
     
-      {sat= true; rep= [[%x_5 ↦ (13 × %z_7)]; [%y_6 ↦ 14]]} |}]
+      {sat= true; rep= [[%x_5 ↦ (13 × %z_7)]; [%y_6 ↦ 14]; [%z_7 ↦ ]]} |}]
 
     let%test _ = entails_eq r8 y !14
 
@@ -280,7 +304,7 @@ let%test_module _ =
         {|
         (%z_7 + -16) = %x_5
     
-      {sat= true; rep= [[%x_5 ↦ (%z_7 + -16)]]} |}]
+      {sat= true; rep= [[%x_5 ↦ (%z_7 + -16)]; [%z_7 ↦ ]]} |}]
 
     let%test _ = difference r9 z (x + !8) |> Poly.equal (Some (Z.of_int 8))
 
@@ -297,7 +321,7 @@ let%test_module _ =
         {|
           (%z_7 + -16) = %x_5
     
-        {sat= true; rep= [[%x_5 ↦ (%z_7 + -16)]]}
+        {sat= true; rep= [[%x_5 ↦ (%z_7 + -16)]; [%z_7 ↦ ]]}
     
         (-1 × %x_5 + %z_7 + -8)
 
@@ -327,7 +351,11 @@ let%test_module _ =
       [%expect
         {|
       {sat= true;
-       rep= [[%z_7 ↦ %y_6]; [(%x_5 = 2) ↦ %y_6]; [(%x_5 ≠ 2) ↦ %y_6]]} |}]
+       rep= [[%x_5 ↦ ];
+             [%y_6 ↦ ];
+             [%z_7 ↦ %y_6];
+             [(%x_5 = 2) ↦ %y_6];
+             [(%x_5 ≠ 2) ↦ %y_6]]} |}]
 
     let%test _ = not (is_false r13) (* incomplete *)
 
@@ -335,7 +363,9 @@ let%test_module _ =
     let r14 = of_eqs [(a, a); (x, !1)]
 
     let%expect_test _ =
-      pp r14 ; [%expect {| {sat= true; rep= [[%x_5 ↦ 1]]} |}]
+      pp r14 ;
+      [%expect
+        {| {sat= true; rep= [[%x_5 ↦ 1]; [(%x_5 ≠ 0) ↦ -1]]} |}]
 
     let%test _ = entails_eq r14 a Term.true_
 
@@ -346,7 +376,8 @@ let%test_module _ =
       pp r14 ;
       [%expect
         {|
-          {sat= true; rep= [[%x_5 ↦ 1]; [(%y_6 ≠ 0) ↦ -1]]} |}]
+          {sat= true;
+           rep= [[%x_5 ↦ 1]; [%y_6 ↦ ]; [(%x_5 ≠ 0) ↦ -1]; [(%y_6 ≠ 0) ↦ -1]]} |}]
 
     let%test _ = entails_eq r14 a Term.true_
     let%test _ = entails_eq r14 b Term.true_
@@ -355,7 +386,9 @@ 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]; [(%x_5 ≠ 0) ↦ -1]]} |}]
 
     let%test _ = entails_eq r15 b (Term.signed 1 !1)
     let%test _ = entails_eq r15 (Term.unsigned 1 b) !1
@@ -370,6 +403,7 @@ let%test_module _ =
         {|
       {sat= false;
        rep= [[%x_5 ↦ (%y_6 + 1)];
+             [%y_6 ↦ ];
              [((u8) %y_6) ↦ (%y_6 + -2)];
              [((u8) (%x_5 + -1)) ↦ (%y_6 + 3)]]} |}]
 
@@ -383,7 +417,8 @@ let%test_module _ =
       [%expect
         {|
       {sat= false;
-       rep= [[%y_6 ↦ %x_5];
+       rep= [[%x_5 ↦ ];
+             [%y_6 ↦ %x_5];
              [((u8) %x_5) ↦ %x_5];
              [((u8) %y_6) ↦ (%x_5 + -1)]]} |}]
 
@@ -396,7 +431,10 @@ let%test_module _ =
       [%expect
         {|
         {sat= true;
-         rep= [[((u8) %x_5) ↦ %x_5]; [((u8) %y_6) ↦ (%y_6 + -1)]]}
+         rep= [[%x_5 ↦ ];
+               [%y_6 ↦ ];
+               [((u8) %x_5) ↦ %x_5];
+               [((u8) %y_6) ↦ (%y_6 + -1)]]}
 
           %x_5 = ((u8) %x_5) ∧ (%y_6 + -1) = ((u8) %y_6) |}]