diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml
index 5003eb716..0615e4064 100644
--- a/sledge/src/llair/exp.ml
+++ b/sledge/src/llair/exp.ml
@@ -1319,7 +1319,8 @@ let rec is_constant e =
   | _ -> true
 
 let classify = function
-  | Add _ | Mul _ | App {op= Eq | Dq | App {op= Eq | Dq}} -> `Interpreted
+  | Add _ | Mul _ -> `Interpreted
+  | App {op= Eq | Dq | App {op= Eq | Dq}} -> `Simplified
   | App _ -> `Uninterpreted
   | _ -> `Atomic
 
diff --git a/sledge/src/llair/exp.mli b/sledge/src/llair/exp.mli
index 82f61b4d1..c82866c11 100644
--- a/sledge/src/llair/exp.mli
+++ b/sledge/src/llair/exp.mli
@@ -206,5 +206,5 @@ val fv : t -> Var.Set.t
 val is_true : t -> bool
 val is_false : t -> bool
 val typ : t -> Typ.t option
-val classify : t -> [> `Atomic | `Interpreted | `Uninterpreted]
+val classify : t -> [> `Atomic | `Interpreted | `Simplified | `Uninterpreted]
 val solve : t -> t -> (t, t, comparator_witness) Map.t option
diff --git a/sledge/src/symbheap/equality.ml b/sledge/src/symbheap/equality.ml
index 8a9ce6f81..1fa9527b7 100644
--- a/sledge/src/symbheap/equality.ml
+++ b/sledge/src/symbheap/equality.ml
@@ -111,7 +111,8 @@ let apply s a = try Map.find_exn s a with Caml.Not_found -> a
 let rec norm s a =
   match Exp.classify a with
   | `Interpreted -> Exp.map ~f:(norm s) a
-  | _ -> apply s a
+  | `Simplified -> apply s (Exp.map ~f:(norm s) a)
+  | `Atomic | `Uninterpreted -> apply s a
 
 (** exps are congruent if equal after normalizing subexps *)
 let congruent r a b =
@@ -132,14 +133,14 @@ let lookup r a =
 let rec canon r a =
   match Exp.classify a with
   | `Interpreted -> Exp.map ~f:(canon r) a
-  | `Uninterpreted -> lookup r (Exp.map ~f:(canon r) a)
+  | `Simplified | `Uninterpreted -> lookup r (Exp.map ~f:(canon r) a)
   | `Atomic -> apply r.rep a
 
 (** add an exp to the carrier *)
 let rec extend a r =
   match Exp.classify a with
-  | `Interpreted -> Exp.fold ~f:extend a ~init:r
-  | _ ->
+  | `Interpreted | `Simplified -> Exp.fold ~f:extend a ~init:r
+  | `Atomic | `Uninterpreted ->
       Map.find_or_add r.rep a
         ~if_found:(fun _ -> r)
         ~default:a
@@ -154,7 +155,7 @@ let compose r s =
         if Exp.equal v1 v2 then v1
         else fail "domains intersect: %a" Exp.pp key () )
   in
-  {r with rep} |> check invariant
+  {r with rep}
 
 let merge a b r =
   [%Trace.call fun {pf} -> pf "%a@ %a@ %a" Exp.pp a Exp.pp b pp r]
@@ -187,6 +188,15 @@ let rec close r =
     | Some (a', b') -> close (merge a' b' r)
     | None -> r
 
+let close r =
+  [%Trace.call fun {pf} -> pf "%a" pp r]
+  ;
+  close r
+  |>
+  [%Trace.retn fun {pf} r' ->
+    pf "%a" pp_diff (r, r') ;
+    invariant r']
+
 let and_eq a b r =
   if not r.sat then r
   else
@@ -266,7 +276,9 @@ let map_exps ({sat= _; rep} as r) ~f =
   in
   (if rep' == rep then r else {r with rep= rep'})
   |>
-  [%Trace.retn fun {pf} r -> pf "%a" pp r ; invariant r]
+  [%Trace.retn fun {pf} r' ->
+    pf "%a" pp_diff (r, r') ;
+    invariant r']
 
 let rename r sub = map_exps r ~f:(fun e -> Exp.rename e sub)
 
diff --git a/sledge/src/symbheap/equality_test.ml b/sledge/src/symbheap/equality_test.ml
index 9ce11e30c..127d9b95b 100644
--- a/sledge/src/symbheap/equality_test.ml
+++ b/sledge/src/symbheap/equality_test.ml
@@ -9,9 +9,9 @@ let%test_module _ =
   ( module struct
     open Equality
 
-    (* let () = Trace.init ~margin:160 ~config:all () *)
-
     let () = Trace.init ~margin:68 ~config:none ()
+
+    (* let () = Trace.init ~margin:160 ~config:all () *)
     let printf pp = Format.printf "@\n%a@." pp
     let pp = printf pp
     let pp_classes = printf pp_classes
@@ -327,4 +327,67 @@ let%test_module _ =
     let r12 = of_eqs [(!16, z - x); (x + !8 - z, z + !16 + !8 - z)]
 
     let%expect_test _ = pp_classes r12 ; [%expect {| (%z_7 + -16) = %x_5 |}]
+
+    let r13 = of_eqs [(Exp.eq x !2, y); (Exp.dq x !2, z); (y, z)]
+
+    let%expect_test _ =
+      pp r13 ;
+      [%expect
+        {|
+      {sat= true;
+       rep= [[%x_5 ↦ ];
+             [%y_6 ↦ ];
+             [%z_7 ↦ %y_6];
+             [(%x_5 = 2) ↦ %y_6];
+             [(%x_5 ≠ 2) ↦ %y_6];
+             [= ↦ ];
+             [≠ ↦ ];
+             [2 ↦ ]]} |}]
+
+    let%test _ = not (is_false r13) (* incomplete *)
+
+    let a = Exp.dq x !0
+    let r14 = of_eqs [(a, a); (x, !1)]
+
+    let%expect_test _ =
+      pp r14 ;
+      [%expect
+        {| {sat= true; rep= [[%x_5 ↦ 1]; [≠ ↦ ]; [0 ↦ ]; [1 ↦ ]]} |}]
+
+    let%test _ = entails_eq r14 a (Exp.bool true)
+
+    let b = Exp.dq y !0
+    let r14 = of_eqs [(a, b); (x, !1)]
+
+    let%expect_test _ =
+      pp r14 ;
+      [%expect
+        {|
+          {sat= true;
+           rep= [[%x_5 ↦ 1];
+                 [%y_6 ↦ ];
+                 [(%y_6 ≠ 0) ↦ -1];
+                 [≠ ↦ ];
+                 [0 ↦ ];
+                 [1 ↦ ]]} |}]
+
+    let%test _ = entails_eq r14 a (Exp.bool true)
+    let%test _ = entails_eq r14 b (Exp.bool true)
+
+    let b = Exp.convert ~dst:i64 ~src:i8 (Exp.dq x !0)
+    let r15 = of_eqs [(b, b); (x, !1)]
+
+    let%expect_test _ =
+      pp r15 ;
+      [%expect
+        {|
+          {sat= true;
+           rep= [[%x_5 ↦ 1];
+                 [((i64)(i8) (%x_5 ≠ 0)) ↦ 1];
+                 [≠ ↦ ];
+                 [(i64)(i8) ↦ ];
+                 [0 ↦ ];
+                 [1 ↦ ]]} |}]
+
+    let%test _ = entails_eq r15 b !1
   end )