diff --git a/sledge/nonstdlib/map.ml b/sledge/nonstdlib/map.ml
index c52d8c3ee..0ff64b2f5 100644
--- a/sledge/nonstdlib/map.ml
+++ b/sledge/nonstdlib/map.ml
@@ -169,6 +169,19 @@ end) : S with type key = Key.t = struct
     in
     Option.map ~f:(fun v -> (v, m)) !found
 
+  let find_or_add k v m =
+    let found = ref None in
+    let m =
+      M.update k
+        (function
+          | None -> Some v
+          | v ->
+              found := v ;
+              v )
+        m
+    in
+    match !found with Some v -> `Found v | None -> `Added m
+
   let pop m = choose m |> Option.map ~f:(fun (k, v) -> (k, v, remove k m))
 
   let pop_min_binding m =
diff --git a/sledge/nonstdlib/map_intf.ml b/sledge/nonstdlib/map_intf.ml
index 4f7a4efbf..fc146c73e 100644
--- a/sledge/nonstdlib/map_intf.ml
+++ b/sledge/nonstdlib/map_intf.ml
@@ -88,6 +88,10 @@ module type S = sig
   val find_and_remove : key -> 'a t -> ('a * 'a t) option
   (** Find and remove the binding for a key. *)
 
+  val find_or_add : key -> 'a -> 'a t -> [`Added of 'a t | `Found of 'a]
+  (** Find the value bound to the given key if there is one, or otherwise
+      add a binding for the given key and value. *)
+
   val pop : 'a t -> (key * 'a * 'a t) option
   (** Find and remove an unspecified binding. Different bindings may be
       chosen for equivalent maps. [O(1)]. *)
diff --git a/sledge/src/fol/context.ml b/sledge/src/fol/context.ml
index fa2d79ad4..9d3d87ebf 100644
--- a/sledge/src/fol/context.ml
+++ b/sledge/src/fol/context.ml
@@ -31,7 +31,6 @@ module Subst : sig
   val for_alli : t -> f:(key:Trm.t -> data:Trm.t -> bool) -> bool
   val to_iter : t -> (Trm.t * Trm.t) iter
   val to_list : t -> (Trm.t * Trm.t) list
-  val extend : Trm.t -> t -> t option
   val compose1 : key:Trm.t -> data:Trm.t -> t -> t
   val compose : t -> t -> t
   val map_entries : f:(Trm.t -> Trm.t) -> t -> t
@@ -105,17 +104,6 @@ end = struct
       let r' = Trm.Map.map_endo ~f:(norm s) r in
       Trm.Map.add ~key ~data r' )
 
-  (** add an identity entry if the term is not already present *)
-  let extend e s =
-    let exception Found in
-    match
-      Trm.Map.update e s ~f:(function
-        | Some _ -> raise_notrace Found
-        | None -> e )
-    with
-    | exception Found -> None
-    | s -> Some s
-
   (** map over a subst, applying [f] to both domain and range, requires that
       [f] is injective and for any set of terms [E], [f\[E\]] is disjoint
       from [E] *)
@@ -405,23 +393,34 @@ let invariant r =
 
 (* Extending the carrier ==================================================*)
 
-let rec extend_ a s =
+let rec norm_extend_ a x =
   [%trace]
-    ~call:(fun {pf} -> pf "@ %a@ %a" Trm.pp a Subst.pp s)
-    ~retn:(fun {pf} s' -> pf "%a" Subst.pp_diff (s, s'))
+    ~call:(fun {pf} -> pf "@ %a@ %a" Trm.pp a pp_raw x)
+    ~retn:(fun {pf} (a', x') ->
+      pf "%a@ %a" Trm.pp a' pp_diff (x, x') ;
+      assert (Trm.equal a' (Subst.norm x'.rep a)) )
   @@ fun () ->
-  match Theory.classify a with
-  | InterpAtom -> s
-  | InterpApp -> Iter.fold ~f:extend_ (Trm.trms a) s
-  | NonInterpAtom ->
-      (* add uninterpreted terms if missing *)
-      Trm.Map.change a s ~f:(function None -> Some a | a' -> a')
-  | UninterpApp -> (
-    (* add uninterpreted terms if missing *)
-    match Subst.extend a s with
-    | None -> s
-    (* and their subterms if newly added *)
-    | Some s -> Iter.fold ~f:extend_ (Trm.trms a) s )
+  if Theory.is_noninterpreted a then
+    (* add noninterpreted terms *)
+    match Trm.Map.find_or_add a a x.rep with
+    | `Found a' -> (a', x)
+    | `Added rep ->
+        (* and their subterms if newly added *)
+        let x = {x with rep} in
+        let a', x = Trm.fold_map ~f:norm_extend_ a x in
+        (a', x)
+  else
+    (* add subterms of interpreted terms *)
+    Trm.fold_map ~f:norm_extend_ a x
+
+let norm_extend a x =
+  [%trace]
+    ~call:(fun {pf} -> pf "@ %a@ %a" Trm.pp a pp_raw x)
+    ~retn:(fun {pf} (a', x') ->
+      pf "%a@ %a" Trm.pp a' pp_diff (x, x') ;
+      pre_invariant x' ;
+      assert (Trm.equal a' (Subst.norm x'.rep a)) )
+  @@ fun () -> norm_extend_ a x
 
 (** add a term to the carrier *)
 let extend a x =
@@ -430,9 +429,7 @@ let extend a x =
     ~retn:(fun {pf} x' ->
       pf "%a" pp_diff (x, x') ;
       pre_invariant x' )
-  @@ fun () ->
-  let rep = extend_ a x.rep in
-  if rep == x.rep then x else {x with rep}
+  @@ fun () -> snd (norm_extend a x)
 
 (* Propagation ============================================================*)
 
@@ -614,7 +611,12 @@ let implies r b =
   [%Trace.retn fun {pf} -> pf "%b"]
 
 let refutes r b = Fml.equal Fml.ff (canon_f r b)
-let normalize r e = Term.map_trms ~f:(canon r) e
+
+let normalize x a =
+  [%trace]
+    ~call:(fun {pf} -> pf "@ %a@ %a" Term.pp a pp x)
+    ~retn:(fun {pf} -> pf "%a" Term.pp)
+  @@ fun () -> Term.map_trms ~f:(canon x) a
 
 let cls_of r e =
   let e' = Subst.apply r.rep e in
diff --git a/sledge/src/test/context_test.ml b/sledge/src/test/context_test.ml
index 2ec16e59d..17b2acbe0 100644
--- a/sledge/src/test/context_test.ml
+++ b/sledge/src/test/context_test.ml
@@ -113,4 +113,34 @@ let%test_module _ =
                      (Var (id 0) (name 2))))))
               (pnd ())))|} ;
       [%expect {| |}]
+
+    let%expect_test _ =
+      replay
+        {|(Dnf
+            (Eq0
+              (Arith
+                (((((Var (id 0) (name 11)) 1) ((Var (id 0) (name 12)) 1)) 1)
+                  ((((Var (id 11) (name a)) 1)) -1)))))|} ;
+      [%expect {| |}]
+
+    let%expect_test _ =
+      replay
+        {|(Normalize
+            ((xs ()) (sat true)
+              (rep
+                (((Var (id 7) (name 16)) (Z 8)) ((Var (id 0) (name 8)) (Q 3/2))
+                  ((Var (id 0) (name 17)) (Z 3)) ((Var (id 0) (name 12)) (Z 8))
+                  ((Var (id 0) (name 11)) (Z 8))
+                  ((Var (id 0) (name 10)) (Var (id 0) (name 10)))
+                  ((Var (id 0) (name 1)) (Z 3)) ((Var (id 0) (name 0)) (Z 8))))
+              (cls
+                (((Q 3/2) ((Var (id 0) (name 8))))
+                  ((Z 8)
+                    ((Var (id 0) (name 12)) (Var (id 0) (name 0))
+                      (Var (id 7) (name 16)) (Var (id 0) (name 11))))
+                  ((Z 3) ((Var (id 0) (name 17)) (Var (id 0) (name 1))))))
+              (pnd ()))
+            (Trm
+              (Arith (((((Var (id 0) (name 11)) 1) ((Var (id 0) (name 12)) 1)) 1)))))|} ;
+      [%expect {| |}]
   end )