diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml
index cba093ba3..d1f2c8bb7 100644
--- a/sledge/src/domain_sh.ml
+++ b/sledge/src/domain_sh.ml
@@ -83,15 +83,15 @@ let exec_intrinsic ~skip_throw q r i es =
     (List.map ~f:Term.of_exp es)
   |> Option.map ~f:(Option.map ~f:simplify)
 
-let term_eq_class_has_only_vars_in fvs cong term =
+let term_eq_class_has_only_vars_in fvs ctx term =
   [%Trace.call fun {pf} ->
-    pf "@[<v> fvs: @[%a@] @,cong: @[%a@] @,term: @[%a@]@]" Var.Set.pp fvs
-      Context.pp cong Term.pp term]
+    pf "@[<v> fvs: @[%a@] @,ctx: @[%a@] @,term: @[%a@]@]" Var.Set.pp fvs
+      Context.pp ctx Term.pp term]
   ;
   let term_has_only_vars_in fvs term =
     Var.Set.is_subset (Term.fv term) ~of_:fvs
   in
-  let term_eq_class = Context.class_of cong term in
+  let term_eq_class = Context.class_of ctx term in
   List.exists ~f:(term_has_only_vars_in fvs) term_eq_class
   |>
   [%Trace.retn fun {pf} -> pf "%b"]
@@ -106,8 +106,8 @@ let garbage_collect (q : t) ~wrt =
     else
       let new_set =
         List.fold ~init:current q.heap ~f:(fun current seg ->
-            if term_eq_class_has_only_vars_in current q.cong seg.loc then
-              List.fold (Context.class_of q.cong seg.seq) ~init:current
+            if term_eq_class_has_only_vars_in current q.ctx seg.loc then
+              List.fold (Context.class_of q.ctx seg.seq) ~init:current
                 ~f:(fun c e -> Var.Set.union c (Term.fv e))
             else current )
       in
@@ -115,7 +115,7 @@ let garbage_collect (q : t) ~wrt =
   in
   let r_vars = all_reachable_vars Var.Set.empty wrt q in
   Sh.filter_heap q ~f:(fun seg ->
-      term_eq_class_has_only_vars_in r_vars q.cong seg.loc )
+      term_eq_class_has_only_vars_in r_vars q.ctx seg.loc )
   |>
   [%Trace.retn fun {pf} -> pf "%a" pp]
 
diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml
index 32085d07e..a6178b946 100644
--- a/sledge/src/sh.ml
+++ b/sledge/src/sh.ml
@@ -17,7 +17,7 @@ type seg = {loc: Term.t; bas: Term.t; len: Term.t; siz: Term.t; seq: Term.t}
 type starjunction =
   { us: Var.Set.t
   ; xs: Var.Set.t
-  ; cong: Context.t
+  ; ctx: Context.t
   ; pure: Term.t
   ; heap: seg list
   ; djns: disjunction list }
@@ -32,7 +32,7 @@ type t = starjunction [@@deriving compare, equal, sexp]
 let emp =
   { us= Var.Set.empty
   ; xs= Var.Set.empty
-  ; cong= Context.true_
+  ; ctx= Context.true_
   ; pure= Term.true_
   ; heap= []
   ; djns= [] }
@@ -56,16 +56,16 @@ let map_seg ~f h =
   then h
   else {loc; bas; len; siz; seq}
 
-let map ~f_sjn ~f_cong ~f_trm ({us; xs= _; cong; pure; heap; djns} as q) =
+let map ~f_sjn ~f_ctx ~f_trm ({us; xs= _; ctx; pure; heap; djns} as q) =
   let pure = f_trm pure in
   if Term.is_false pure then false_ us
   else
-    let cong = f_cong cong in
+    let ctx = f_ctx ctx in
     let heap = List.map_endo heap ~f:(map_seg ~f:f_trm) in
     let djns = List.map_endo djns ~f:(List.map_endo ~f:f_sjn) in
-    if cong == q.cong && pure == q.pure && heap == q.heap && djns == q.djns
+    if ctx == q.ctx && pure == q.pure && heap == q.heap && djns == q.djns
     then q
-    else {q with cong; pure; heap; djns}
+    else {q with ctx; pure; heap; djns}
 
 let fold_terms_seg {loc; bas; len; siz; seq} ~init ~f =
   let f b s = f s b in
@@ -74,18 +74,17 @@ let fold_terms_seg {loc; bas; len; siz; seq} ~init ~f =
 let fold_vars_seg seg ~init ~f =
   fold_terms_seg seg ~init ~f:(fun init -> Term.fold_vars ~f ~init)
 
-let fold_vars_stem ?ignore_cong {us= _; xs= _; cong; pure; heap; djns= _}
+let fold_vars_stem ?ignore_ctx {us= _; xs= _; ctx; pure; heap; djns= _}
     ~init ~f =
   List.fold ~init heap ~f:(fun init -> fold_vars_seg ~f ~init)
   |> fun init ->
   Term.fold_vars ~f ~init pure
   |> fun init ->
-  if Option.is_some ignore_cong then init
-  else
-    Context.fold_terms ~init cong ~f:(fun init -> Term.fold_vars ~f ~init)
+  if Option.is_some ignore_ctx then init
+  else Context.fold_terms ~init ctx ~f:(fun init -> Term.fold_vars ~f ~init)
 
-let fold_vars ?ignore_cong fold_vars q ~init ~f =
-  fold_vars_stem ?ignore_cong ~init ~f q
+let fold_vars ?ignore_ctx fold_vars q ~init ~f =
+  fold_vars_stem ?ignore_ctx ~init ~f q
   |> fun init ->
   List.fold ~init q.djns ~f:(fun init -> List.fold ~init ~f:fold_vars)
 
@@ -100,7 +99,7 @@ let rec var_strength_ xs m q =
   in
   let xs = Var.Set.union xs q.xs in
   let m_stem =
-    fold_vars_stem ~ignore_cong:() q ~init:m ~f:(fun m var ->
+    fold_vars_stem ~ignore_ctx:() q ~init:m ~f:(fun m var ->
         if not (Var.Set.mem xs var) then
           Var.Map.set m ~key:var ~data:`Universal
         else add m var )
@@ -135,9 +134,9 @@ let pp_seg x fs {loc; bas; len; siz; seq} =
         Format.fprintf fs " %a, %a " term_pp bas term_pp len )
     (bas, len) (pp_chunk x) (siz, seq)
 
-let pp_seg_norm cong fs seg =
+let pp_seg_norm ctx fs seg =
   let x _ = None in
-  pp_seg x fs (map_seg seg ~f:(Context.normalize cong))
+  pp_seg x fs (map_seg seg ~f:(Context.normalize ctx))
 
 let pp_block x fs segs =
   let is_full_alloc segs =
@@ -171,7 +170,7 @@ let pp_block x fs segs =
         pp_chunks segs
   | [] -> ()
 
-let pp_heap x ?pre cong fs heap =
+let pp_heap x ?pre ctx fs heap =
   let bas_off e =
     match Term.const_of e with
     | Some const -> (Term.sub e (Term.rational const), const)
@@ -179,17 +178,15 @@ let pp_heap x ?pre cong fs heap =
   in
   let compare s1 s2 =
     [%compare: Term.t * (Term.t * Q.t)]
-      ( Context.normalize cong s1.bas
-      , bas_off (Context.normalize cong s1.loc) )
-      ( Context.normalize cong s2.bas
-      , bas_off (Context.normalize cong s2.loc) )
+      (Context.normalize ctx s1.bas, bas_off (Context.normalize ctx s1.loc))
+      (Context.normalize ctx s2.bas, bas_off (Context.normalize ctx s2.loc))
   in
   let break s1 s2 =
     (not (Term.equal s1.bas s2.bas))
     || (not (Term.equal s1.len s2.len))
-    || not (Context.entails_eq cong (Term.add s1.loc s1.siz) s2.loc)
+    || not (Context.entails_eq ctx (Term.add s1.loc s1.siz) s2.loc)
   in
-  let heap = List.map heap ~f:(map_seg ~f:(Context.normalize cong)) in
+  let heap = List.map heap ~f:(map_seg ~f:(Context.normalize ctx)) in
   let blocks = List.group ~break (List.sort ~compare heap) in
   List.pp ?pre "@ * " (pp_block x) fs blocks
 
@@ -203,8 +200,8 @@ let pp_us ?(pre = ("" : _ fmt)) ?vs () fs us =
         [%Trace.fprintf
           fs "%( %)@[%a@] .@ " pre (Var.Set.pp_diff Var.pp) (vs, us)]
 
-let rec pp_ ?var_strength vs parent_xs parent_cong fs
-    {us; xs; cong; pure; heap; djns} =
+let rec pp_ ?var_strength vs parent_xs parent_ctx fs
+    {us; xs; ctx; pure; heap; djns} =
   Format.pp_open_hvbox fs 0 ;
   let x v = Option.bind ~f:(fun (_, m) -> Var.Map.find m v) var_strength in
   pp_us ~vs () fs us ;
@@ -218,14 +215,14 @@ let rec pp_ ?var_strength vs parent_xs parent_cong fs
     if not (Var.Set.is_empty xs_d_vs) then Format.fprintf fs "@ " ) ;
   if not (Var.Set.is_empty xs_d_vs) then
     Format.fprintf fs "@<2>∃ @[%a@] .@ " (Var.Set.ppx x) xs_d_vs ;
-  let clss = Context.diff_classes cong parent_cong in
+  let clss = Context.diff_classes ctx parent_ctx in
   let first = Term.Map.is_empty clss in
   if not first then Format.fprintf fs "  " ;
   Context.ppx_classes x fs clss ;
   let pure =
     if Option.is_none var_strength then [pure]
     else
-      let pure' = Context.normalize cong pure in
+      let pure' = Context.normalize ctx pure in
       if Term.is_true pure' then [] else [pure']
   in
   List.pp
@@ -236,7 +233,7 @@ let rec pp_ ?var_strength vs parent_xs parent_cong fs
     Format.fprintf fs
       ( if first then if List.is_empty djns then "  emp" else ""
       else "@ @<5>∧ emp" )
-  else pp_heap x ~pre:(if first then "  " else "@ @<2>∧ ") cong fs heap ;
+  else pp_heap x ~pre:(if first then "  " else "@ @<2>∧ ") ctx fs heap ;
   let first = first && List.is_empty heap in
   List.pp
     ~pre:(if first then "  " else "@ * ")
@@ -244,11 +241,11 @@ let rec pp_ ?var_strength vs parent_xs parent_cong fs
     (pp_djn ?var_strength
        (Var.Set.union vs (Var.Set.union us xs))
        (Var.Set.union parent_xs xs)
-       cong)
+       ctx)
     fs djns ;
   Format.pp_close_box fs ()
 
-and pp_djn ?var_strength vs xs cong fs = function
+and pp_djn ?var_strength vs xs ctx fs = function
   | [] -> Format.fprintf fs "false"
   | djn ->
       Format.fprintf fs "@[<hv>( %a@ )@]"
@@ -258,22 +255,22 @@ and pp_djn ?var_strength vs xs cong fs = function
                var_strength_ xs var_strength_stem sjn
              in
              Format.fprintf fs "@[<hv 1>(%a)@]"
-               (pp_ ?var_strength vs (Var.Set.union xs sjn.xs) cong)
+               (pp_ ?var_strength vs (Var.Set.union xs sjn.xs) ctx)
                sjn ))
         djn
 
-let pp_diff_eq ?(us = Var.Set.empty) ?(xs = Var.Set.empty) cong fs q =
-  pp_ ~var_strength:(var_strength ~xs q) us xs cong fs q
+let pp_diff_eq ?(us = Var.Set.empty) ?(xs = Var.Set.empty) ctx fs q =
+  pp_ ~var_strength:(var_strength ~xs q) us xs ctx fs q
 
 let pp fs q = pp_diff_eq Context.true_ fs q
 let pp_djn fs d = pp_djn Var.Set.empty Var.Set.empty Context.true_ fs d
 let pp_raw fs q = pp_ Var.Set.empty Var.Set.empty Context.true_ fs q
 let fv_seg seg = fold_vars_seg seg ~f:Var.Set.add ~init:Var.Set.empty
 
-let fv ?ignore_cong q =
+let fv ?ignore_ctx q =
   let rec fv_union init q =
     Var.Set.diff
-      (fold_vars ?ignore_cong fv_union q ~init ~f:Var.Set.add)
+      (fold_vars ?ignore_ctx fv_union q ~init ~f:Var.Set.add)
       q.xs
   in
   fv_union Var.Set.empty q
@@ -287,7 +284,7 @@ let invariant_seg _ = ()
 
 let rec invariant q =
   let@ () = Invariant.invariant [%here] q [%sexp_of: t] in
-  let {us; xs; cong; pure; heap; djns} = q in
+  let {us; xs; ctx; pure; heap; djns} = q in
   try
     assert (
       Var.Set.disjoint us xs
@@ -297,13 +294,13 @@ let rec invariant q =
       Var.Set.is_subset (fv q) ~of_:us
       || fail "unbound but free: %a" Var.Set.pp (Var.Set.diff (fv q) us) ()
     ) ;
-    Context.invariant cong ;
+    Context.invariant ctx ;
     ( match djns with
     | [[]] ->
-        assert (Context.is_true cong) ;
+        assert (Context.is_true ctx) ;
         assert (Term.is_true pure) ;
         assert (List.is_empty heap)
-    | _ -> assert (not (Context.is_false cong)) ) ;
+    | _ -> assert (not (Context.is_false ctx)) ) ;
     invariant_pure pure ;
     List.iter heap ~f:invariant_seg ;
     List.iter djns ~f:(fun djn ->
@@ -320,7 +317,7 @@ let rec invariant q =
     invariant *)
 let rec apply_subst sub q =
   map q ~f_sjn:(rename sub)
-    ~f_cong:(fun r -> Context.rename r sub)
+    ~f_ctx:(fun r -> Context.rename r sub)
     ~f_trm:(Term.rename sub)
   |> check (fun q' ->
          assert (Var.Set.disjoint (fv q') (Var.Subst.domain sub)) )
@@ -435,19 +432,18 @@ let elim_exists xs q =
 
 (** Construct *)
 
-(** conjoin an equality relation assuming vocabulary is compatible *)
-let and_cong_ cong q =
-  assert (Var.Set.is_subset (Context.fv cong) ~of_:q.us) ;
-  let xs, cong = Context.and_ (Var.Set.union q.us q.xs) q.cong cong in
-  if Context.is_false cong then false_ q.us
-  else exists_fresh xs {q with cong}
+(** conjoin an FOL context assuming vocabulary is compatible *)
+let and_ctx_ ctx q =
+  assert (Var.Set.is_subset (Context.fv ctx) ~of_:q.us) ;
+  let xs, ctx = Context.and_ (Var.Set.union q.us q.xs) q.ctx ctx in
+  if Context.is_false ctx then false_ q.us else exists_fresh xs {q with ctx}
 
-let and_cong cong q =
-  [%Trace.call fun {pf} -> pf "%a@ %a" Context.pp cong pp q]
+let and_ctx ctx q =
+  [%Trace.call fun {pf} -> pf "%a@ %a" Context.pp ctx pp q]
   ;
   ( match q.djns with
   | [[]] -> q
-  | _ -> and_cong_ cong (extend_us (Context.fv cong) q) )
+  | _ -> and_ctx_ ctx (extend_us (Context.fv ctx) q) )
   |>
   [%Trace.retn fun {pf} q ->
     pf "%a" pp q ;
@@ -459,30 +455,30 @@ let star q1 q2 =
   ( match (q1, q2) with
   | {djns= [[]]; _}, _ | _, {djns= [[]]; _} ->
       false_ (Var.Set.union q1.us q2.us)
-  | {us= _; xs= _; cong; pure; heap= []; djns= []}, _
-    when Context.is_true cong && Term.is_true pure ->
+  | {us= _; xs= _; ctx; pure; heap= []; djns= []}, _
+    when Context.is_true ctx && Term.is_true pure ->
       let us = Var.Set.union q1.us q2.us in
       if us == q2.us then q2 else {q2 with us}
-  | _, {us= _; xs= _; cong; pure; heap= []; djns= []}
-    when Context.is_true cong && Term.is_true pure ->
+  | _, {us= _; xs= _; ctx; pure; heap= []; djns= []}
+    when Context.is_true ctx && Term.is_true pure ->
       let us = Var.Set.union q1.us q2.us in
       if us == q1.us then q1 else {q1 with us}
   | _ ->
       let us = Var.Set.union q1.us q2.us in
       let q1 = freshen_xs q1 ~wrt:(Var.Set.union us q2.xs) in
       let q2 = freshen_xs q2 ~wrt:(Var.Set.union us q1.xs) in
-      let {us= us1; xs= xs1; cong= c1; pure= p1; heap= h1; djns= d1} = q1 in
-      let {us= us2; xs= xs2; cong= c2; pure= p2; heap= h2; djns= d2} = q2 in
+      let {us= us1; xs= xs1; ctx= c1; pure= p1; heap= h1; djns= d1} = q1 in
+      let {us= us2; xs= xs2; ctx= c2; pure= p2; heap= h2; djns= d2} = q2 in
       assert (Var.Set.equal us (Var.Set.union us1 us2)) ;
-      let xs, cong =
+      let xs, ctx =
         Context.and_ (Var.Set.union us (Var.Set.union xs1 xs2)) c1 c2
       in
-      if Context.is_false cong then false_ us
+      if Context.is_false ctx then false_ us
       else
         exists_fresh xs
           { us
           ; xs= Var.Set.union xs1 xs2
-          ; cong
+          ; ctx
           ; pure= Term.and_ p1 p2
           ; heap= List.append h1 h2
           ; djns= List.append d1 d2 } )
@@ -504,17 +500,17 @@ let or_ q1 q2 =
   | {djns= [[]]; _}, _ -> extend_us q1.us q2
   | _, {djns= [[]]; _} -> extend_us q2.us q1
   | ( ({djns= []; _} as q)
-    , ({us= _; xs; cong= _; pure; heap= []; djns= [djn]} as d) )
+    , ({us= _; xs; ctx= _; pure; heap= []; djns= [djn]} as d) )
     when Var.Set.is_empty xs && Term.is_true pure ->
       {d with us= Var.Set.union q.us d.us; djns= [q :: djn]}
-  | ( ({us= _; xs; cong= _; pure; heap= []; djns= [djn]} as d)
+  | ( ({us= _; xs; ctx= _; pure; heap= []; djns= [djn]} as d)
     , ({djns= []; _} as q) )
     when Var.Set.is_empty xs && Term.is_true pure ->
       {d with us= Var.Set.union q.us d.us; djns= [q :: djn]}
   | _ ->
       { us= Var.Set.union q1.us q2.us
       ; xs= Var.Set.empty
-      ; cong= Context.true_
+      ; ctx= Context.true_
       ; pure= Term.true_
       ; heap= []
       ; djns= [[q1; q2]] } )
@@ -534,9 +530,9 @@ let pure (e : Term.t) =
   ;
   List.fold (Term.disjuncts e) ~init:(false_ Var.Set.empty) ~f:(fun q b ->
       let us = Term.fv b in
-      let xs, cong = Context.(and_term us b true_) in
-      if Context.is_false cong then false_ us
-      else or_ q (exists_fresh xs {emp with us; cong; pure= b}) )
+      let xs, ctx = Context.(and_term us b true_) in
+      if Context.is_false ctx then false_ us
+      else or_ q (exists_fresh xs {emp with us; ctx; pure= b}) )
   |>
   [%Trace.retn fun {pf} q ->
     pf "%a" pp q ;
@@ -589,23 +585,23 @@ let filter_heap ~f q =
 (** Query *)
 
 let is_emp = function
-  | {us= _; xs= _; cong= _; pure; heap= []; djns= []} -> Term.is_true pure
+  | {us= _; xs= _; ctx= _; pure; heap= []; djns= []} -> Term.is_true pure
   | _ -> false
 
 let is_false = function
   | {djns= [[]]; _} -> true
-  | {cong; pure; heap; _} ->
-      Term.is_false (Context.normalize cong pure)
+  | {ctx; pure; heap; _} ->
+      Term.is_false (Context.normalize ctx pure)
       || List.exists heap ~f:(fun seg ->
-             Context.entails_eq cong seg.loc Term.zero )
+             Context.entails_eq ctx seg.loc Term.zero )
 
-let rec pure_approx ({us; xs; cong; pure; heap= _; djns} as q) =
+let rec pure_approx ({us; xs; ctx; pure; heap= _; djns} as q) =
   let heap = emp.heap in
   let djns =
     List.map_endo djns ~f:(fun djn -> List.map_endo djn ~f:pure_approx)
   in
   if heap == q.heap && djns == q.djns then q
-  else {us; xs; cong; pure; heap; djns} |> check invariant
+  else {us; xs; ctx; pure; heap; djns} |> check invariant
 
 let pure_approx q =
   [%Trace.call fun {pf} -> pf "%a" pp q]
@@ -650,10 +646,10 @@ let rec norm_ s q =
   [%Trace.call fun {pf} -> pf "@[%a@]@ %a" Context.Subst.pp s pp_raw q]
   ;
   let q =
-    map q ~f_sjn:(norm_ s) ~f_cong:Fn.id ~f_trm:(Context.Subst.subst s)
+    map q ~f_sjn:(norm_ s) ~f_ctx:Fn.id ~f_trm:(Context.Subst.subst s)
   in
-  let xs, cong = Context.apply_subst (Var.Set.union q.us q.xs) s q.cong in
-  exists_fresh xs {q with cong}
+  let xs, ctx = Context.apply_subst (Var.Set.union q.us q.xs) s q.ctx in
+  exists_fresh xs {q with ctx}
   |>
   [%Trace.retn fun {pf} q' ->
     pf "%a" pp_raw q' ;
@@ -693,9 +689,9 @@ let rec freshen_nested_xs q =
     pf "%a" pp q' ;
     invariant q']
 
-let rec propagate_equality_ ancestor_vs ancestor_cong q =
+let rec propagate_context_ ancestor_vs ancestor_ctx q =
   [%Trace.call fun {pf} ->
-    pf "(%a)@ %a" Context.pp_classes ancestor_cong pp q]
+    pf "(%a)@ %a" Context.pp_classes ancestor_ctx pp q]
   ;
   (* extend vocabulary with variables in scope above *)
   let ancestor_vs = Var.Set.union ancestor_vs (Var.Set.union q.us q.xs) in
@@ -703,33 +699,33 @@ let rec propagate_equality_ ancestor_vs ancestor_cong q =
   let xs, stem, djns =
     (q.xs, {q with us= ancestor_vs; xs= emp.xs; djns= emp.djns}, q.djns)
   in
-  (* strengthen equality relation with that from above *)
-  let ancestor_stem = and_cong_ ancestor_cong stem in
-  let ancestor_cong = ancestor_stem.cong in
+  (* strengthen context with that from above *)
+  let ancestor_stem = and_ctx_ ancestor_ctx stem in
+  let ancestor_ctx = ancestor_stem.ctx in
   exists xs
     (List.fold djns ~init:ancestor_stem ~f:(fun q' djn ->
-         let dj_congs, djn =
+         let dj_ctxs, djn =
            List.rev_map_unzip djn ~f:(fun dj ->
-               let dj = propagate_equality_ ancestor_vs ancestor_cong dj in
-               (dj.cong, dj) )
+               let dj = propagate_context_ ancestor_vs ancestor_ctx dj in
+               (dj.ctx, dj) )
          in
-         let new_xs, djn_cong = Context.orN ancestor_vs dj_congs in
-         (* hoist xs appearing in disjunction's equality relation *)
-         let djn_xs = Var.Set.diff (Context.fv djn_cong) q'.us in
+         let new_xs, djn_ctx = Context.orN ancestor_vs dj_ctxs in
+         (* hoist xs appearing in disjunction's context *)
+         let djn_xs = Var.Set.diff (Context.fv djn_ctx) q'.us in
          let djn = List.map ~f:(elim_exists djn_xs) djn in
-         let cong_djn = and_cong_ djn_cong (orN djn) in
-         assert (is_false cong_djn || Var.Set.is_subset new_xs ~of_:djn_xs) ;
-         star (exists djn_xs cong_djn) q' ))
+         let ctx_djn = and_ctx_ djn_ctx (orN djn) in
+         assert (is_false ctx_djn || Var.Set.is_subset new_xs ~of_:djn_xs) ;
+         star (exists djn_xs ctx_djn) q' ))
   |>
   [%Trace.retn fun {pf} q' ->
     pf "%a" pp q' ;
     invariant q']
 
-let propagate_equality ancestor_vs ancestor_cong q =
+let propagate_context ancestor_vs ancestor_ctx q =
   [%Trace.call fun {pf} ->
-    pf "(%a)@ %a" Context.pp_classes ancestor_cong pp q]
+    pf "(%a)@ %a" Context.pp_classes ancestor_ctx pp q]
   ;
-  propagate_equality_ ancestor_vs ancestor_cong q
+  propagate_context_ ancestor_vs ancestor_ctx q
   |>
   [%Trace.retn fun {pf} q' ->
     pf "%a" pp q' ;
@@ -745,19 +741,19 @@ let remove_absent_xs ks q =
   if Var.Set.is_empty ks then q
   else
     let xs = Var.Set.diff q.xs ks in
-    let cong = Context.elim ks q.cong in
+    let ctx = Context.elim ks q.ctx in
     let djns =
       let rec trim_ks ks djns =
         List.map djns ~f:(fun djn ->
             List.map djn ~f:(fun sjn ->
                 { sjn with
                   us= Var.Set.diff sjn.us ks
-                ; cong= Context.elim ks sjn.cong
+                ; ctx= Context.elim ks sjn.ctx
                 ; djns= trim_ks ks sjn.djns } ) )
       in
       trim_ks ks q.djns
     in
-    {q with xs; cong; djns}
+    {q with xs; ctx; djns}
 
 let rec simplify_ us rev_xss q =
   [%Trace.call fun {pf} -> pf "%a@ %a" pp_vss (List.rev rev_xss) pp_raw q]
@@ -772,8 +768,8 @@ let rec simplify_ us rev_xss q =
                 orN (List.map djn ~f:(fun sjn -> simplify_ us rev_xss sjn)) )
          ))
   in
-  (* try to solve equations in cong for variables in xss *)
-  let subst = Context.solve_for_vars (us :: List.rev rev_xss) q.cong in
+  (* try to solve equations in ctx for variables in xss *)
+  let subst = Context.solve_for_vars (us :: List.rev rev_xss) q.ctx in
   (* simplification can reveal inconsistency *)
   ( if is_false q then false_ q.us
   else if Context.Subst.is_empty subst then q
@@ -784,7 +780,7 @@ let rec simplify_ us rev_xss q =
     let removed =
       Var.Set.diff
         (Var.Set.union_list rev_xss)
-        (fv ~ignore_cong:() (elim_exists q.xs q))
+        (fv ~ignore_ctx:() (elim_exists q.xs q))
     in
     let keep, removed, _ = Context.Subst.partition_valid removed subst in
     let q = and_subst keep q in
@@ -799,7 +795,7 @@ let simplify q =
   [%Trace.call fun {pf} -> pf "%a" pp_raw q]
   ;
   let q = freshen_nested_xs q in
-  let q = propagate_equality Var.Set.empty Context.true_ q in
+  let q = propagate_context Var.Set.empty Context.true_ q in
   let q = simplify_ q.us [] q in
   q
   |>
diff --git a/sledge/src/sh.mli b/sledge/src/sh.mli
index a3df73030..f96e54581 100644
--- a/sledge/src/sh.mli
+++ b/sledge/src/sh.mli
@@ -17,7 +17,8 @@ type seg = {loc: Term.t; bas: Term.t; len: Term.t; siz: Term.t; seq: Term.t}
 type starjunction = private
   { us: Var.Set.t  (** vocabulary / variable context of formula *)
   ; xs: Var.Set.t  (** existentially-bound variables *)
-  ; cong: Context.t  (** congruence induced by rest of formula *)
+  ; ctx: Context.t
+        (** first-order logical context induced by rest of formula *)
   ; pure: Term.t  (** pure boolean constraints *)
   ; heap: seg list  (** star-conjunction of segment atomic formulas *)
   ; djns: disjunction list  (** star-conjunction of disjunctions *) }
@@ -61,8 +62,8 @@ val pure : Term.t -> t
 val and_ : Term.t -> t -> t
 (** Conjoin a boolean constraint to a formula. *)
 
-val and_cong : Context.t -> t -> t
-(** Conjoin constraints of a congruence to a formula, extending to a common
+val and_ctx : Context.t -> t -> t
+(** Conjoin a context to that of a formula, extending to a common
     vocabulary, and avoiding capturing existentials. *)
 
 val and_subst : Context.Subst.t -> t -> t
@@ -73,9 +74,9 @@ val and_subst : Context.Subst.t -> t -> t
 
 val with_pure : Term.t -> t -> t
 (** [with_pure pure q] is [{q with pure}], which assumes that [q.pure] and
-    [pure] are defined in the same vocabulary. Note that [cong] is not
-    weakened, so if [pure] and [q.pure] do not induce the same congruence,
-    then the result will have a stronger [cong] than induced by its [pure]. *)
+    [pure] are defined in the same vocabulary. Note that [ctx] is not
+    weakened, so if [pure] and [q.pure] do not induce the same context, then
+    the result will have a stronger [ctx] than induced by its [pure]. *)
 
 val rem_seg : seg -> t -> t
 (** [star (seg s) (rem_seg s q)] is equivalent to [q], assuming that [s] is
@@ -116,13 +117,13 @@ val extend_us : Var.Set.t -> t -> t
 (** Query *)
 
 val is_emp : t -> bool
-(** Holds of [emp], with any vocabulary, existentials, and congruence. *)
+(** Holds of [emp], with any vocabulary, existentials, and context. *)
 
 val is_false : t -> bool
 (** Holds only of inconsistent formulas, does not hold of all inconsistent
     formulas. *)
 
-val fv : ?ignore_cong:unit -> t -> Var.Set.t
+val fv : ?ignore_ctx:unit -> t -> Var.Set.t
 (** Free variables, a subset of vocabulary. *)
 
 val pure_approx : t -> t
diff --git a/sledge/src/solver.ml b/sledge/src/solver.ml
index 5a137502f..9b6752e8f 100644
--- a/sledge/src/solver.ml
+++ b/sledge/src/solver.ml
@@ -26,10 +26,9 @@ module Goal : sig
   type t = private
     { us: Var.Set.t  (** (universal) vocabulary of entire judgment *)
     ; com: Sh.t  (** common star-conjunct of minuend and subtrahend *)
-    ; min: Sh.t
-          (** minuend, cong strengthened by pure_approx (com * min) *)
+    ; min: Sh.t  (** minuend, ctx strengthened by pure_approx (com * min) *)
     ; xs: Var.Set.t  (** existentials over subtrahend and remainder *)
-    ; sub: Sh.t  (** subtrahend, cong strengthened by min.cong *)
+    ; sub: Sh.t  (** subtrahend, ctx strengthened by min.ctx *)
     ; zs: Var.Set.t  (** existentials over remainder *)
     ; pgs: bool  (** indicates whether a deduction rule has been applied *)
     }
@@ -71,7 +70,7 @@ end = struct
     Format.fprintf fs "@[<hv>%s %a@ | %a@ @[\\- %a%a@]@]"
       (if pgs then "t" else "f")
       Sh.pp com Sh.pp min Var.Set.pp_xs xs
-      (Sh.pp_diff_eq ~us:(Var.Set.union min.us sub.us) ~xs min.cong)
+      (Sh.pp_diff_eq ~us:(Var.Set.union min.us sub.us) ~xs min.ctx)
       sub
 
   let invariant g =
@@ -156,15 +155,15 @@ let excise_exists goal =
     let solutions_for_xs =
       let xs =
         Var.Set.diff goal.xs
-          (Sh.fv ~ignore_cong:() (Sh.with_pure Term.true_ goal.sub))
+          (Sh.fv ~ignore_ctx:() (Sh.with_pure Term.true_ goal.sub))
       in
-      Context.solve_for_vars [Var.Set.empty; goal.us; xs] goal.sub.cong
+      Context.solve_for_vars [Var.Set.empty; goal.us; xs] goal.sub.ctx
     in
     if Context.Subst.is_empty solutions_for_xs then goal
     else
       let removed =
         Var.Set.diff goal.xs
-          (Sh.fv ~ignore_cong:() (Sh.norm solutions_for_xs goal.sub))
+          (Sh.fv ~ignore_ctx:() (Sh.norm solutions_for_xs goal.sub))
       in
       if Var.Set.is_empty removed then goal
       else
@@ -183,7 +182,7 @@ let excise_exists goal =
 
 let excise_pure ({min; sub} as goal) =
   trace (fun {pf} -> pf "@[<2>excise_pure@ %a@]" pp goal) ;
-  let pure' = Context.normalize min.cong sub.pure in
+  let pure' = Context.normalize min.ctx sub.pure in
   if Term.is_false pure' then None
   else Some (goal |> with_ ~sub:(Sh.with_pure pure' sub))
 
@@ -202,8 +201,8 @@ let excise_pure ({min; sub} as goal) =
  *)
 let excise_seg_same ({com; min; sub} as goal) msg ssg =
   excise (fun {pf} ->
-      pf "@[<hv 2>excise_seg_same@ %a@ \\- %a@]" (Sh.pp_seg_norm sub.cong)
-        msg (Sh.pp_seg_norm sub.cong) ssg ) ;
+      pf "@[<hv 2>excise_seg_same@ %a@ \\- %a@]" (Sh.pp_seg_norm sub.ctx)
+        msg (Sh.pp_seg_norm sub.ctx) ssg ) ;
   let {Sh.bas= b; len= m; seq= a} = msg in
   let {Sh.bas= b'; len= m'; seq= a'} = ssg in
   let com = Sh.star (Sh.seg msg) com in
@@ -231,7 +230,7 @@ let excise_seg_sub_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg o_n
     =
   excise (fun {pf} ->
       pf "@[<hv 2>excise_seg_sub_prefix@ %a@ \\- %a@]"
-        (Sh.pp_seg_norm sub.cong) msg (Sh.pp_seg_norm sub.cong) ssg ) ;
+        (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ;
   let {Sh.loc= k; bas= b; len= m; siz= o; seq= a} = msg in
   let {Sh.bas= b'; len= m'; siz= n; seq= a'} = ssg in
   let o_n = Term.integer o_n in
@@ -271,7 +270,7 @@ let excise_seg_min_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg n_o
     =
   excise (fun {pf} ->
       pf "@[<hv 2>excise_seg_min_prefix@ %a@ \\- %a@]"
-        (Sh.pp_seg_norm sub.cong) msg (Sh.pp_seg_norm sub.cong) ssg ) ;
+        (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ;
   let {Sh.bas= b; len= m; siz= o; seq= a} = msg in
   let {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in
   let n_o = Term.integer n_o in
@@ -307,7 +306,7 @@ let excise_seg_sub_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
     =
   excise (fun {pf} ->
       pf "@[<hv 2>excise_seg_sub_suffix@ %a@ \\- %a@]"
-        (Sh.pp_seg_norm sub.cong) msg (Sh.pp_seg_norm sub.cong) ssg ) ;
+        (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ;
   let {Sh.loc= k; bas= b; len= m; siz= o; seq= a} = msg in
   let {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in
   let l_k = Term.integer l_k in
@@ -349,7 +348,7 @@ let excise_seg_sub_infix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
     ko_ln =
   excise (fun {pf} ->
       pf "@[<hv 2>excise_seg_sub_infix@ %a@ \\- %a@]"
-        (Sh.pp_seg_norm sub.cong) msg (Sh.pp_seg_norm sub.cong) ssg ) ;
+        (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ;
   let {Sh.loc= k; bas= b; len= m; siz= o; seq= a} = msg in
   let {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in
   let l_k = Term.integer l_k in
@@ -396,7 +395,7 @@ let excise_seg_min_skew ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
     ko_l ln_ko =
   excise (fun {pf} ->
       pf "@[<hv 2>excise_seg_min_skew@ %a@ \\- %a@]"
-        (Sh.pp_seg_norm sub.cong) msg (Sh.pp_seg_norm sub.cong) ssg ) ;
+        (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ;
   let {Sh.loc= k; bas= b; len= m; siz= o; seq= a} = msg in
   let {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in
   let l_k = Term.integer l_k in
@@ -446,7 +445,7 @@ let excise_seg_min_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
     =
   excise (fun {pf} ->
       pf "@[<hv 2>excise_seg_min_suffix@ %a@ \\- %a@]"
-        (Sh.pp_seg_norm sub.cong) msg (Sh.pp_seg_norm sub.cong) ssg ) ;
+        (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ;
   let {Sh.bas= b; len= m; siz= o; seq= a} = msg in
   let {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in
   let k_l = Term.integer k_l in
@@ -483,7 +482,7 @@ let excise_seg_min_infix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
     ln_ko =
   excise (fun {pf} ->
       pf "@[<hv 2>excise_seg_min_infix@ %a@ \\- %a@]"
-        (Sh.pp_seg_norm sub.cong) msg (Sh.pp_seg_norm sub.cong) ssg ) ;
+        (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ;
   let {Sh.loc= k; bas= b; len= m; siz= o; seq= a} = msg in
   let {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in
   let k_l = Term.integer k_l in
@@ -524,7 +523,7 @@ let excise_seg_sub_skew ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
     ln_k ko_ln =
   excise (fun {pf} ->
       pf "@[<hv 2>excise_seg_sub_skew@ %a@ \\- %a@]"
-        (Sh.pp_seg_norm sub.cong) msg (Sh.pp_seg_norm sub.cong) ssg ) ;
+        (Sh.pp_seg_norm sub.ctx) msg (Sh.pp_seg_norm sub.ctx) ssg ) ;
   let {Sh.loc= k; bas= b; len= m; siz= o; seq= a} = msg in
   let {Sh.loc= l; bas= b'; len= m'; siz= n; seq= a'} = ssg in
   let k_l = Term.integer k_l in
@@ -558,14 +557,14 @@ let excise_seg_sub_skew ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
 (* C ❮ k-[b;m)->⟨o,α⟩ * M ⊢ ∃xs. l-[b';m')->⟨n,α'⟩ * S ❯ R *)
 let excise_seg ({sub} as goal) msg ssg =
   trace (fun {pf} ->
-      pf "@[<2>excise_seg@ %a@  |-  %a@]" (Sh.pp_seg_norm sub.cong) msg
-        (Sh.pp_seg_norm sub.cong) ssg ) ;
+      pf "@[<2>excise_seg@ %a@  |-  %a@]" (Sh.pp_seg_norm sub.ctx) msg
+        (Sh.pp_seg_norm sub.ctx) ssg ) ;
   let {Sh.loc= k; bas= b; len= m; siz= o} = msg in
   let {Sh.loc= l; bas= b'; len= m'; siz= n} = ssg in
-  let* k_l = Context.difference sub.cong k l in
+  let* k_l = Context.difference sub.ctx k l in
   if
-    (not (Context.entails_eq sub.cong b b'))
-    || not (Context.entails_eq sub.cong m m')
+    (not (Context.entails_eq sub.ctx b b'))
+    || not (Context.entails_eq sub.ctx m m')
   then
     Some
       ( goal
@@ -578,11 +577,11 @@ let excise_seg ({sub} as goal) msg ssg =
     | Neg -> (
         let ko = Term.add k o in
         let ln = Term.add l n in
-        let* ko_ln = Context.difference sub.cong ko ln in
+        let* ko_ln = Context.difference sub.ctx ko ln in
         match Int.sign (Z.sign ko_ln) with
         (* k+o-(l+n) < 0 so k+o < l+n *)
         | Neg -> (
-            let* l_ko = Context.difference sub.cong l ko in
+            let* l_ko = Context.difference sub.ctx l ko in
             match Int.sign (Z.sign l_ko) with
             (* l-(k+o) < 0     [k;   o)
              * so l < k+o    ⊢    [l;  n) *)
@@ -600,7 +599,7 @@ let excise_seg ({sub} as goal) msg ssg =
         )
     (* k-l = 0 so k = l *)
     | Zero -> (
-        let* o_n = Context.difference sub.cong o n in
+        let* o_n = Context.difference sub.ctx o n in
         match Int.sign (Z.sign o_n) with
         (* o-n < 0      [k; o)
          * so o < n   ⊢ [l;   n) *)
@@ -615,7 +614,7 @@ let excise_seg ({sub} as goal) msg ssg =
     | Pos -> (
         let ko = Term.add k o in
         let ln = Term.add l n in
-        let* ko_ln = Context.difference sub.cong ko ln in
+        let* ko_ln = Context.difference sub.ctx ko ln in
         match Int.sign (Z.sign ko_ln) with
         (* k+o-(l+n) < 0        [k; o)
          * so k+o < l+n    ⊢ [l;      n) *)
@@ -625,7 +624,7 @@ let excise_seg ({sub} as goal) msg ssg =
         | Zero -> Some (excise_seg_min_suffix goal msg ssg k_l)
         (* k+o-(l+n) > 0 so k+o > l+n *)
         | Pos -> (
-            let* k_ln = Context.difference sub.cong k ln in
+            let* k_ln = Context.difference sub.ctx k ln in
             match Int.sign (Z.sign k_ln) with
             (* k-(l+n) < 0        [k;  o)
              * so k < l+n    ⊢ [l;   n) *)
@@ -673,7 +672,7 @@ let excise_dnf : Sh.t -> Var.Set.t -> Sh.t -> Sh.t option =
         List.find_map dnf_subtrahend ~f:(fun sub ->
             [%Trace.call fun {pf} -> pf "@[<2>subtrahend@ %a@]" Sh.pp sub]
             ;
-            let sub = Sh.and_cong min.cong (Sh.extend_us us sub) in
+            let sub = Sh.and_ctx min.ctx (Sh.extend_us us sub) in
             excise (goal ~us ~com ~min ~xs ~sub ~zs ~pgs:true)
             |>
             [%Trace.retn fun {pf} -> pf "%a" (Option.pp "%a" Sh.pp)] )