diff --git a/src/lib/reasoners/ac.ml b/src/lib/reasoners/ac.ml
index 95645ba25..955019970 100644
--- a/src/lib/reasoners/ac.ml
+++ b/src/lib/reasoners/ac.ml
@@ -183,10 +183,10 @@ module Make (X : Sig.X) = struct
      presentation in the paper to accomodate those differences, globally,
      between the implementation and theoretical description of AC(X).
 
-     More precisely, `abstract2` will abstract terms that *contain* AC leaves
-     when they appear as argument of an AC symbol. This ensures that AC terms
-     satisfy the T_AC definition from page 22 of the paper, although
-     correctness of the corresponding abstraction process has not been proven.
+     More precisely, `abstract2` will abstract all AC leaves that appear in the
+     arguments of an AC symbol. This ensures that AC terms satisfy the T_AC
+     definition from page 22 of the paper, although correctness of the
+     corresponding abstraction process has not been formally proven.
      See also https://github.com/OCamlPro/alt-ergo/issues/989
 
      [1]: Canonized Rewriting and Ground AC Completion Modulo Shostak Theories:
@@ -196,42 +196,24 @@ module Make (X : Sig.X) = struct
             Volume 8, Issue 3.
           doi:10.2168/LMCS-8(3:16)2012
           https://arxiv.org/pdf/1207.3262.pdf *)
-  let abstract2 sy t r acc =
-    if List.exists (is_other_ac_symbol sy) (X.leaves r) then
-      match X.ac_extract r, Expr.term_view t with
-      | Some ac, { f = Name { hs; kind = Ac; _ } ; xs; ty; _ } ->
-        (* It should have been abstracted when building [r] *)
-        assert (not (Sy.equal sy ac.h));
-        let aro_sy = Sy.name ~ns:Internal ("@" ^ (HS.view hs)) in
-        let aro_t = Expr.mk_term aro_sy xs ty  in
-        let eq = Expr.mk_eq ~iff:false aro_t t in
-        X.term_embed aro_t, eq::acc
-      | Some ac, { f = Op Mult; xs; ty; _ } ->
-        (* It should have been abstracted when building [r] *)
-        assert (not (Sy.equal sy ac.h));
-        let aro_sy = Sy.name ~ns:Internal "@*" in
-        let aro_t = Expr.mk_term aro_sy xs ty  in
-        let eq = Expr.mk_eq ~iff:false aro_t t in
-        X.term_embed aro_t, eq::acc
-      | _, { ty; _ } ->
-        let k = Expr.fresh_ac_name ty in
-        let eq = Expr.mk_eq ~iff:false k t in
-        X.term_embed k, eq::acc
-
-    else
-      r, acc
+  let rec abstract2 sy r =
+    match List.find (is_other_ac_symbol sy) (X.leaves r) with
+    | ac_lv ->
+      (* Abstraction in depth: [f(x, y) + 1] -> [@ac(f(x, y)) + 1]
+         and not [@ac(f(x, y) + 1)]. *)
+      abstract2 sy (X.subst ac_lv (X.abstract ~kind:Ac ac_lv) r)
+    | exception Not_found -> r
 
   let make t =
     match Expr.term_view t with
     | { Expr.f = sy; xs = [a;b]; ty; _ } when Sy.is_ac sy ->
       let ra, ctx1 = X.make a in
       let rb, ctx2 = X.make b in
-      let ra, ctx = abstract2 sy a ra (ctx1 @ ctx2) in
-      let rb, ctx = abstract2 sy b rb ctx in
-      let rxs = [ ra,1 ; rb,1 ] in
-      X.ac_embed {h=sy; l=compact (fold_flatten sy (fun x -> x) rxs); t=ty;
-                  distribute = true},
-      ctx
+      let l = flatten sy (rb, 1) @@ flatten sy (ra, 1) [] in
+      let l = List.map (fun (r, n) -> (abstract2 sy r, n)) l in
+      let l = compact (fold_flatten sy (fun x -> x) l) in
+      X.ac_embed {h=sy; l; t=ty;distribute = true},
+      ctx1 @ ctx2
     | {xs; _} ->
       Printer.print_err
         "AC theory expects only terms with 2 arguments; \
diff --git a/src/lib/reasoners/arith.ml b/src/lib/reasoners/arith.ml
index 01ab0206e..9f681604b 100644
--- a/src/lib/reasoners/arith.ml
+++ b/src/lib/reasoners/arith.ml
@@ -452,12 +452,7 @@ module Shostak
       List.fold_left (fun acc (_, x) -> max acc (nb_vars_in_alien x)) acc l
 
   let contains_a_fresh_alien xp =
-    List.exists
-      (fun x ->
-         match X.term_extract x with
-         | Some t, _ -> E.is_fresh_ac_name t
-         | _ -> false
-      ) (X.leaves xp)
+    List.exists (X.is_abstract ~kind:Ac) (X.leaves xp)
 
   let has_ac p kind =
     List.exists
@@ -540,7 +535,7 @@ module Shostak
     List.fold_left
       (fun (l, sb) (b, y) ->
          if X.ac_extract y != None && X.str_cmp y x > 0 then
-           let k = X.term_embed (E.fresh_ac_name Ty.Tint) in
+           let k = X.abstract ~kind:Ac y in
            (b, k) :: l, (y, embed k)::sb
          else (b, y) :: l, sb)
       ([], []) l
diff --git a/src/lib/reasoners/ccx.ml b/src/lib/reasoners/ccx.ml
index 5642c89d4..c5453c0b5 100644
--- a/src/lib/reasoners/ccx.ml
+++ b/src/lib/reasoners/ccx.ml
@@ -489,7 +489,14 @@ module Main : S = struct
       let { E.xs; _ } = E.term_view t in
       let env = List.fold_left (fun env t -> add_term env facts t ex) env xs in
       (* we update uf and use *)
-      let nuf, ctx  = Uf.add env.uf t in
+      let nuf, abs, ctx  = Uf.add env.uf t in
+      (* process definitional equality of abstracted terms *)
+      List.iter (fun r ->
+          match X.abstract_extract r with
+          | Some r' ->
+            add_fact facts (LSem (LR.mkv_eq r r'), Ex.empty, Th_util.Other)
+          | None -> assert false
+        ) abs;
       Debug.make_cst t ctx;
       List.iter (fun a -> add_fact facts (LTerm a, ex, Th_util.Other)) ctx;
       (*or Ex.empty ?*)
diff --git a/src/lib/reasoners/intervalCalculus.ml b/src/lib/reasoners/intervalCalculus.ml
index aeb8ca415..1d6d322ea 100644
--- a/src/lib/reasoners/intervalCalculus.ml
+++ b/src/lib/reasoners/intervalCalculus.ml
@@ -2234,7 +2234,7 @@ let domain_matching _lem_name tr sbt env uf optimized =
            | E.Interval (t, lb, ub) ->
              let tt = E.apply_subst sbt t in
              assert (E.is_ground tt);
-             let uf, _ = Uf.add uf tt in
+             let uf, _, _ = Uf.add uf tt in
              let rr, _ex = Uf.find uf tt in
              let p = poly_of rr in
              let p', c', d = P.normal_form_pos p in
@@ -2247,7 +2247,7 @@ let domain_matching _lem_name tr sbt env uf optimized =
 
            | E.NotTheoryConst t ->
              let tt = E.apply_subst sbt t in
-             let uf, _ = Uf.add uf tt in
+             let uf, _, _ = Uf.add uf tt in
              if X.leaves (fst (Uf.find uf tt)) == [] ||
                 X.leaves (fst (X.make tt)) == [] then
                raise (Sem_match_fails env);
@@ -2255,7 +2255,7 @@ let domain_matching _lem_name tr sbt env uf optimized =
 
            | E.IsTheoryConst t ->
              let tt = E.apply_subst sbt t in
-             let uf, _ = Uf.add uf tt in
+             let uf, _, _ = Uf.add uf tt in
              let r, _ = X.make tt in
              if X.leaves r != [] then raise (Sem_match_fails env);
              idoms, maps_to, env, uf
@@ -2265,8 +2265,8 @@ let domain_matching _lem_name tr sbt env uf optimized =
              let y = E.apply_subst sbt y in
              if not (terms_linear_dep env [x;y]) then
                raise (Sem_match_fails env);
-             let uf, _ = Uf.add uf x in
-             let uf, _ = Uf.add uf y in
+             let uf, _, _ = Uf.add uf x in
+             let uf, _, _ = Uf.add uf y in
              idoms, maps_to, env, uf
         )(Var.Map.empty, [], env, uf) tr.E.semantic
     in
diff --git a/src/lib/reasoners/shostak.ml b/src/lib/reasoners/shostak.ml
index 8b308859b..c9f28faca 100644
--- a/src/lib/reasoners/shostak.ml
+++ b/src/lib/reasoners/shostak.ml
@@ -27,6 +27,22 @@
 
 (*** Combination module of Shostak theories ***)
 
+let equal_abs_kind k1 k2 =
+  match k1, k2 with
+  | Sig.Ac, Sig.Ac -> true
+
+let hash_abs_kind k =
+  match k with
+  | Sig.Ac -> 1
+
+let compare_abs_kind k1 k2 =
+  match k1, k2 with
+  | Sig.Ac, Sig.Ac -> 0
+
+let pp_abs_kind ppf k =
+  match k with
+  | Sig.Ac -> Fmt.pf ppf "ac"
+
 [@@@ocaml.warning "-60"]
 module rec CX : sig
   include Sig.X
@@ -51,6 +67,7 @@ struct
 
   type rview =
     | Term of Expr.t
+    | Abstract of Sig.abs_kind * CX.r
     | Ac of AC.t
     | Arith of ARITH.t
     | Records of RECORDS.t
@@ -72,6 +89,7 @@ struct
         | Bitv t -> fprintf fmt "%a" BITV.print t
         | Adt t -> fprintf fmt "%a" ADT.print t
         | Term t -> fprintf fmt "%a" Expr.print t
+        | Abstract (k, t) -> fprintf fmt "@@%a(%a)" pp_abs_kind k CX.print t
         | Ac t -> fprintf fmt "%a" AC.print t
       end
       else begin
@@ -86,6 +104,8 @@ struct
           fprintf fmt "Adt(%s):[%a]" ADT.name ADT.print t
         | Term t ->
           fprintf fmt "FT:[%a]" Expr.print t
+        | Abstract (k, t) ->
+          fprintf fmt "K:%a[%a]" pp_abs_kind k CX.print t
         | Ac t ->
           fprintf fmt "Ac:[%a]" AC.print t
       end
@@ -165,6 +185,8 @@ struct
         | Bitv x -> 3 + 10 * BITV.hash x
         | Adt x -> 6 + 10 * ADT.hash x
         | Ac ac -> 9 + 10 * AC.hash ac
+        | Abstract (k, t) ->
+          7 + 10 * (5003 * (hash_abs_kind k) + CX.hash t)
         | Term t -> 8 + 10 * Expr.hash t
       in
       abs res
@@ -176,6 +198,8 @@ struct
       | Bitv x, Bitv y -> BITV.equal x y
       | Adt x, Adt y -> ADT.equal x y
       | Term x, Term y -> Expr.equal x y
+      | Abstract (kx, x), Abstract (ky, y) ->
+        equal_abs_kind kx ky && CX.equal x y
       | Ac x, Ac y -> AC.equal x y
       | _ -> false
 
@@ -214,6 +238,16 @@ struct
 
   let term_embed t = hcons {v = Term t; id = -1000 (* dummy *)}
 
+  let abstract ~kind arg =
+    (* No need to nest abstractions
+       XXX: would it be OK to abstract terms into themselves? *)
+    let arg =
+      match arg.v with
+      | Abstract (_, arg) -> arg
+      | _ -> arg
+    in
+    hcons { v = Abstract (kind, arg); id = -1000 (* dummy *) }
+
   let extract1 = function { v=Arith r; _ } -> Some r | _ -> None
   let extract2 = function { v=Records r; _ } -> Some r | _ -> None
   let extract3 = function { v=Bitv r; _ } -> Some r | _ -> None
@@ -223,6 +257,18 @@ struct
     | { v = Ac t; _ }   -> Some t
     | _ -> None
 
+  let is_abstract ?kind = function
+    | { v = Abstract (k, _); _ } -> (
+        match kind with
+        | None -> true
+        | Some k' -> equal_abs_kind k k'
+      )
+    | _ -> false
+
+  let abstract_extract = function
+    | { v = Abstract (_, r); _ } -> Some r
+    | _ -> None
+
   let term_extract r =
     match r.v with
     | Arith _ -> ARITH.term_extract r
@@ -230,6 +276,7 @@ struct
     | Bitv _ -> BITV.term_extract r
     | Adt _ -> ADT.term_extract r
     | Ac _ -> None, false (* SYLVAIN : TODO *)
+    | Abstract _ -> None, false
     | Term t -> Some t, true
 
   let to_model_term r =
@@ -240,7 +287,7 @@ struct
       | Bitv _ -> BITV.to_model_term r
       | Adt _ -> ADT.to_model_term r
       | Term t when Expr.is_model_term t -> Some t
-      | Ac _ | Term _ -> None
+      | Abstract _ | Ac _ | Term _ -> None
     in
     Option.bind res @@ fun t ->
     assert (Expr.is_model_term t);
@@ -256,15 +303,17 @@ struct
     | { v = Adt t; _ } -> ADT.type_info t
     | { v = Ac x; _ } -> AC.type_info x
     | { v = Term t; _ } -> Expr.type_info t
+    | { v = Abstract (_, t); _ } -> CX.type_info t
 
   (* Constraint that must be maintained:
-     all theories should have Xi < Term < Ac *)
+     all theories should have Xi < Abstract < Term < Ac *)
   let theory_num x = match x with
     | Ac _ -> -1
     | Term  _ -> -2
-    | Arith _ -> -3
-    | Records _ -> -4
-    | Bitv _ -> -5
+    | Abstract _ -> -3
+    | Arith _ -> -4
+    | Records _ -> -5
+    | Bitv _ -> -6
     | Adt _ -> -7
 
   let compare_tag a b = theory_num a - theory_num b
@@ -278,6 +327,11 @@ struct
       | Bitv _, Bitv _ -> BITV.compare a b
       | Adt _, Adt _ -> ADT.compare a b
       | Term x, Term y -> Expr.compare x y
+      | Abstract (kx, x), Abstract (ky, y) ->
+        (* Make sure that new abstractions are smaller, i.e.
+           old abstractions are rewritten into new abstractions. *)
+        let c = Int.compare y.id x.id in
+        if c <> 0 then c else compare_abs_kind kx ky
       | Ac x, Ac y -> AC.compare x y
       | va, vb -> compare_tag va vb
 
@@ -322,7 +376,7 @@ struct
     | Bitv t -> BITV.leaves t
     | Adt t -> ADT.leaves t
     | Ac t -> r :: (AC.leaves t)
-    | Term _ -> [r]
+    | Term _ | Abstract _ -> [r]
 
   let is_constant r =
     match r.v with
@@ -338,7 +392,7 @@ struct
         | Symbols.(True | False), [] -> true
         | _ -> false
       end
-    | Ac _ -> false
+    | Abstract _ | Ac _ -> false
 
   let subst p v r =
     if equal p v then r
@@ -348,6 +402,7 @@ struct
       | Bitv t -> BITV.subst p v t
       | Adt t -> ADT.subst p v t
       | Ac t -> if equal p r then v else AC.subst p v t
+      | Abstract _ -> if equal p r then v else r
       | Term _ -> if equal p r then v else r
 
   let make t =
@@ -416,7 +471,7 @@ struct
      ADT.is_mine_symb sb)
 
   let is_a_leaf r = match r.v with
-    | Term _ | Ac _ -> true
+    | Term _ | Ac _ | Abstract _ -> true
     | _ -> false
 
   let color ac =
@@ -448,7 +503,7 @@ struct
     | Records a -> RECORDS.abstract_selectors a acc
     | Bitv a -> BITV.abstract_selectors a acc
     | Adt a -> ADT.abstract_selectors a acc
-    | Term _ -> a, acc
+    | Term _ | Abstract _ -> a, acc
     | Ac a -> AC.abstract_selectors a acc
 
   let abstract_equality a b =
@@ -483,7 +538,7 @@ struct
     let sbs =
       List.filter (fun (p,_) ->
           match p.v with
-          | Ac _ -> true | Term _ -> SX.mem p original
+          | Ac _ | Abstract _ -> true | Term _ -> SX.mem p original
           | _ ->
             Printer.print_err "%a" CX.print p;
             assert false
diff --git a/src/lib/reasoners/sig.mli b/src/lib/reasoners/sig.mli
index 3050e1f23..7c780ccce 100644
--- a/src/lib/reasoners/sig.mli
+++ b/src/lib/reasoners/sig.mli
@@ -28,6 +28,12 @@
 type 'a ac =
   {h: Symbols.t ; t: Ty.t ; l: ('a * int) list; distribute: bool}
 
+type abs_kind =
+    Ac (** Semantic value abstracted for AC(X) purposes. *)
+(** Type of abstractions that can be used in [abstract]. Used to distinguish
+    the reason for which a semantic value was abstracted, which some code
+    cares about (see {!module-Arith}). *)
+
 type 'a solve_pb = { sbt : ('a * 'a) list; eqs : ('a * 'a) list }
 
 module type SHOSTAK = sig
@@ -184,6 +190,38 @@ module type X = sig
 
   val ac_extract : r -> (r ac) option
 
+  val abstract : kind:abs_kind -> r -> r
+  (** [abstract ~kind r] returns an abstracted constant representing [r].
+
+      The abstract constant [abstract ~kind r] is {e definitionally equal} to
+      [r]: when processed by the {!module-Uf} and {!module-Ccx} modules in any
+      context, the equality [r = abstract ~kind r] is introduced automatically.
+
+      Calling [abstract ~kind r] multiple times with the same [kind] and the
+      same [r] always returns the same abstracted constant.
+
+      Abstracted constants, like terms, are terminal leaves: the only leaf of
+      [abstract ~kind r] is [abstract ~kind r] itself. In particular,
+      substituting the leaves of [r] does not impact [abstract ~kind r].
+  *)
+
+  val is_abstract : ?kind:abs_kind -> r -> bool
+  (** [is_abstract ?kind r] returns [true] if [r] is an abstracted constant
+      created with {!val-abstract} with the provided [kind] (if any).
+  *)
+
+  val abstract_extract : r -> r option
+  (** [abstract_extract r] returns the inner abstracted semantic value
+      embedded in [r], if any.
+
+      If [abstract_extract r] is [Some r'], then [r] is definitionally equal to
+      [r'], that is, the equation [r = r'] holds in all contexts.
+
+      {b Note}: While [abstract_extract (abstract ~kind r)] and [r] are
+      guaranteed to be definitionally equal, they are not, in general,
+      guaranteed to be equal as semantic values according to {!val-equal}.
+  *)
+
   val color : (r ac) -> r
 
   val fully_interpreted : Symbols.t -> bool
diff --git a/src/lib/reasoners/uf.ml b/src/lib/reasoners/uf.ml
index 46f330070..e5b3a0789 100644
--- a/src/lib/reasoners/uf.ml
+++ b/src/lib/reasoners/uf.ml
@@ -587,7 +587,7 @@ module Env = struct
     with GlobalDomains.Inconsistent ex ->
       raise (Ex.Inconsistent (ex, cl_extract env))
 
-  let init_leaf env p =
+  let init_leaf env abs p =
     Debug.init_leaf p;
     let in_repr = MapX.mem p env.repr in
     let rp, ex_rp =
@@ -600,6 +600,11 @@ module Env = struct
       | Some t, true when not (ME.mem t mk_env) -> ME.add t p mk_env
       | _ -> mk_env
     in
+    let abs =
+      match X.abstract_extract rp with
+      | Some _  when not in_repr -> rp :: abs
+      | Some _ | None -> abs
+    in
     let env =
       { env with
         make    = make;
@@ -620,21 +625,28 @@ module Env = struct
           else update_neqs p rp Ex.empty env }
     in
     Debug.check_invariants "init_leaf" env;
-    env
+    env, abs
+
+  let init_leaves env abs v =
+    let env, abs =
+      List.fold_left
+        (fun (env, abs) lv -> init_leaf env abs lv)
+        (env, abs)
+        (X.leaves v)
+    in
+    init_leaf env abs v
 
-  let init_leaves env v =
-    let env = List.fold_left init_leaf env (X.leaves v) in
-    init_leaf env v
+  let is_dyn_leaf r =
+    Option.is_some (X.ac_extract r) || X.is_abstract r
 
-  let init_new_ac_leaves env mkr =
+  let init_new_dyn_leaves env mkr =
     List.fold_left
-      (fun env x ->
-         match X.ac_extract x with
-         | None -> env
-         | Some _ ->
-           if MapX.mem x env.repr then env
-           else init_leaves env x
-      ) env (X.leaves mkr)
+      (fun (env, abs) x ->
+         if is_dyn_leaf x && not (MapX.mem x env.repr) then
+           init_leaves env abs x
+         else
+           env, abs
+      ) (env, []) (X.leaves mkr)
 
   let init_term env t =
     let mkr, ctx = X.make t in
@@ -650,7 +662,8 @@ module Env = struct
          if MapX.mem rp env.neqs then env.neqs (* pourquoi ce test *)
          else MapX.add rp MapL.empty env.neqs}
     in
-    (init_new_ac_leaves env mkr), ctx
+    let env, abs = init_new_dyn_leaves env mkr in
+    env, abs, ctx
 
   let head_cp eqs env pac ({ Sig.h ; _ } as ac) v dep =
     try (*if RS.mem h env.ac_rs then*)
@@ -792,21 +805,27 @@ module Env = struct
       update_aux dep neqs_to_up env, tch
 
   let apply_sigma eqs env tch ((p, v, dep) as sigma) =
-    let env = init_leaves env p in
-    let env = init_leaves env v in
+    let env, abs = init_leaves env [] p in
+    let env, abs = init_leaves env abs v in
     let env = apply_sigma_ac eqs env sigma in
     let env, touched_sigma, tch = apply_sigma_uf env sigma tch in
-    up_uf_rs dep env ((p, touched_sigma, v) :: tch)
+    let env, tch = up_uf_rs dep env ((p, touched_sigma, v) :: tch) in
+    List.iter (fun r ->
+        match X.abstract_extract r with
+        | Some r' -> Queue.push (r, r', Ex.empty) eqs
+        | None -> assert false
+      ) abs;
+    env, tch
 
 end
 
 let add env t =
   Options.tool_req 3 "TR-UFX-Add";
-  if ME.mem t env.make then env, []
+  if ME.mem t env.make then env, [], []
   else
-    let env, l = Env.init_term env t in
+    let env, abs, l = Env.init_term env t in
     Debug.check_invariants "add" env;
-    env, l
+    env, abs, l
 
 let ac_solve eqs dep (env, tch) (p, v) =
   Debug.ac_solve p v dep;
@@ -859,9 +878,9 @@ let union env r1 r2 dep =
   Options.tool_req 3 "TR-UFX-Union";
   let equations = Queue.create () in
   Queue.push (r1,r2, dep) equations;
-  let env, res = ac_x equations env [] in
+  let env, tch = ac_x equations env [] in
   Debug.check_invariants "union" env;
-  env, res
+  env, tch
 
 let union env r1 r2 dep =
   Timers.with_timer Timers.M_UF Timers.F_union @@ fun () ->
@@ -890,7 +909,7 @@ let rec distinct env rl dep =
              with Not_found ->
                MapL.add d uex mdis
            in
-           let env = Env.init_leaf env rr in
+           let env, _ = Env.init_leaf env [] rr in
            let env = {env with neqs = MapX.add rr mdis env.neqs} in
            env, MapX.add rr uex mapr, (rr, ex, mapr)::newds
       )
@@ -992,8 +1011,8 @@ let empty =
     ac_rs = RS.empty
   }
   in
-  let env, _ = add env E.vrai in
-  let env, _ = add env E.faux in
+  let env, _, _ = add env E.vrai in
+  let env, _, _ = add env E.faux in
   distinct env [X.top; X.bot] Ex.empty
 
 let make uf t = ME.find t uf.make
@@ -1065,7 +1084,7 @@ let assign_next env =
           we will not modify env in this function
           !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
         *)
-      let env, _ =  add env s in (* important for termination *)
+      let env, _, _ =  add env s in (* important for termination *)
       let eq = LX.view (LX.mk_eq rep (make env s)) in
       [eq, is_cs, Th_util.CS (Th_util.Th_UF, Numbers.Q.one)], env
   in
diff --git a/src/lib/reasoners/uf.mli b/src/lib/reasoners/uf.mli
index f231441e6..ecbea6b56 100644
--- a/src/lib/reasoners/uf.mli
+++ b/src/lib/reasoners/uf.mli
@@ -117,7 +117,7 @@ end
 module LX = Shostak.L
 
 val empty : t
-val add : t -> Expr.t -> t * Expr.t list
+val add : t -> Expr.t -> t * r list * Expr.t list
 
 val mem : t -> Expr.t -> bool
 
diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml
index e07fc3e1c..1bbe89621 100644
--- a/src/lib/structures/expr.ml
+++ b/src/lib/structures/expr.ml
@@ -987,14 +987,6 @@ let fresh_name ty =
 let mk_abstract ty =
   mk_term (Sy.name ~ns:Abstract @@ Id.Namespace.Abstract.fresh ()) [] ty
 
-let fresh_ac_name ty =
-  mk_term (Sy.name ~ns:Fresh_ac @@ Id.Namespace.Internal.fresh ()) [] ty
-
-let is_fresh_ac_name t =
-  match t with
-  | { f = Name { ns = Fresh_ac; _ }; xs = []; _ } -> true
-  | _ -> false
-
 let positive_int i = mk_term (Sy.int i) [] Ty.Tint
 
 let int i =
diff --git a/src/lib/structures/expr.mli b/src/lib/structures/expr.mli
index 8c639480c..a68714e67 100644
--- a/src/lib/structures/expr.mli
+++ b/src/lib/structures/expr.mli
@@ -254,12 +254,6 @@ val real : string -> t
 val bitv : string -> Ty.t -> t
 val fresh_name : Ty.t -> t
 
-(** Special names used for AC(X) abstraction.
-    These corresponds to the K sort in the AC(X) paper. *)
-
-val fresh_ac_name : Ty.t -> t
-val is_fresh_ac_name : t -> bool
-
 val mk_abstract : Ty.t -> t
 (** [mk_abstract ty] creates an abstract model term of type [ty].
     This function is intended to be used only in models. *)
diff --git a/src/lib/structures/symbols.ml b/src/lib/structures/symbols.ml
index 3b00b1e45..e443d2ce6 100644
--- a/src/lib/structures/symbols.ml
+++ b/src/lib/structures/symbols.ml
@@ -75,7 +75,7 @@ type form =
 
 type name_kind = Ac | Other
 
-type name_space = User | Internal | Fresh | Fresh_ac | Skolem | Abstract
+type name_space = User | Internal | Fresh | Skolem | Abstract
 
 let compare_name_space ns1 ns2 =
   match ns1, ns2 with
@@ -91,10 +91,6 @@ let compare_name_space ns1 ns2 =
   | Fresh, _ -> -1
   | _, Fresh -> 1
 
-  | Fresh_ac, Fresh_ac -> 0
-  | Fresh_ac, _ -> -1
-  | _, Fresh_ac -> 1
-
   | Skolem, Skolem -> 0
   | Skolem, _ -> -1
   | _, Skolem -> 1
@@ -132,7 +128,6 @@ let mangle ns s =
   | User -> s
   | Internal -> ".!" ^ s
   | Fresh -> ".k" ^ s
-  | Fresh_ac -> ".K" ^ s
   | Skolem -> ".?__" ^ s
   | Abstract -> "@a" ^ s
 
diff --git a/src/lib/structures/symbols.mli b/src/lib/structures/symbols.mli
index 0aedea950..8611d1dcf 100644
--- a/src/lib/structures/symbols.mli
+++ b/src/lib/structures/symbols.mli
@@ -104,28 +104,11 @@ type name_space =
       that was introduced during solving as part of some kind of purification
       or abstraction procedure.
 
-      In order to correctly implement AC(X) in the presence of distributive
-      symbols, symbols generated for AC(X) abstraction use a special
-      namespace, [Fresh_ac] below.
-
       To ensure uniqueness, fresh names must always be generated using
       [Id.Namespace.Internal.fresh ()].
 
       In particular, fresh names are only used to denote constants, not
       arbitrary functions. *)
-  | Fresh_ac
-  (** This symbol has been introduced as part of the AC(X) abstraction process.
-      This is notably used by some parts of AC(X) that check if terms contains
-      fresh symbols (see [contains_a_fresh_alien] in the [Arith] module for an
-      example).
-
-      These correspond to the K sort in the AC(X) paper. They use a different
-      name space from other fresh symbols because we need to be able to know
-      whether a fresh symbol comes from the AC(X) abstraction procedure in order
-      to prevent loops.
-
-      To ensure uniqueness, AC abstraction names must always be generated using
-      [Id.Namespace.Internal.fresh ()]. *)
   | Skolem
   (** This symbol has been introduced as part of skolemization, and represents
       the (dependent) variable of an existential quantifier. Skolem names can