diff --git a/src/lib/dune b/src/lib/dune
index 23c57e936..cdad79151 100644
--- a/src/lib/dune
+++ b/src/lib/dune
@@ -40,7 +40,7 @@
     Fun_sat Inequalities Bitv_rel Th_util Adt Adt_rel
     Instances IntervalCalculus Intervals Ite_rel Ite Matching Matching_types
     Polynome Records Records_rel Satml_frontend_hybrid Satml_frontend Satml
-    Sat_solver Sat_solver_sig Sig Sig_rel Theory Uf Use
+    Sat_solver Sat_solver_sig Sig Sig_rel Theory Uf Use Rel_utils
     ; structures
     Commands Errors Explanation Fpa_rounding
     Parsed Profiling Satml_types Symbols
diff --git a/src/lib/reasoners/adt.ml b/src/lib/reasoners/adt.ml
index 686acd288..6f9bd472e 100644
--- a/src/lib/reasoners/adt.ml
+++ b/src/lib/reasoners/adt.ml
@@ -236,6 +236,15 @@ module Shostak (X : ALIEN) = struct
          List.fold_left (fun sx x -> SX.add x sx) sx (X.leaves r)
       )SX.empty l
 
+  let is_constant r =
+    let l = match r with
+      | Alien r -> [Hs.empty, r]
+      | Constr { c_args ; _ } ->  c_args
+      | Select { d_arg  ; _ } -> [Hs.empty, d_arg]
+      | Tester { t_arg  ; _ } -> [Hs.empty, t_arg]
+    in
+    List.for_all (fun (_, r) -> X.is_constant r) l
+
   [@@ocaml.ppwarning "TODO: not sure"]
   let fully_interpreted _ =
     false (* not sure *)
diff --git a/src/lib/reasoners/arith.ml b/src/lib/reasoners/arith.ml
index 4a1168126..87ec2bbf5 100644
--- a/src/lib/reasoners/arith.ml
+++ b/src/lib/reasoners/arith.ml
@@ -492,6 +492,8 @@ module Shostak
 
   let leaves p = P.leaves p
 
+  let is_constant p = Option.is_some (P.is_const p)
+
   let subst x t p =
     let p = P.subst x (embed t) p in
     let ty = P.type_info p in
diff --git a/src/lib/reasoners/arrays.ml b/src/lib/reasoners/arrays.ml
index 881f92613..624dbd91e 100644
--- a/src/lib/reasoners/arrays.ml
+++ b/src/lib/reasoners/arrays.ml
@@ -53,6 +53,7 @@ module Shostak (X : ALIEN) = struct
   let equal _ _      = assert false
   let hash _         = assert false
   let leaves _       = assert false
+  let is_constant _  = assert false
   let subst _ _ _    = assert false
   let make _         = assert false
   let term_extract _ = None, false
diff --git a/src/lib/reasoners/bitv.ml b/src/lib/reasoners/bitv.ml
index 49016adae..85ed96bbc 100644
--- a/src/lib/reasoners/bitv.ml
+++ b/src/lib/reasoners/bitv.ml
@@ -102,6 +102,34 @@ let equal_simple_term eq = equal_alpha_term (equal_simple_term_aux eq)
 
 type 'a abstract =  'a simple_term list
 
+let rec to_Z_opt_aux acc = function
+  | [] -> Some acc
+  | { bv = Cte false; sz } :: sts ->
+    to_Z_opt_aux Z.(acc lsl sz) sts
+  | { bv = Cte true; sz } :: sts ->
+    to_Z_opt_aux Z.((acc lsl sz) + (~$1 lsl sz) - ~$1) sts
+  | _ -> None
+
+let to_Z_opt r = to_Z_opt_aux Z.zero r
+
+let int2bv_const n z =
+  (* If [z] is out of the [0 .. 2^n] range (including if [z] is negative),
+     considering only the first [n] bits is equivalent to computing [z mod 2^n],
+     so we just do that and don't bother computing the modulus. *)
+  let acc = ref [] in
+  for i = 0 to n - 1 do
+    match Z.testbit z i, !acc with
+    | false, { bv = Cte false; sz } :: rst ->
+      acc := { bv = Cte false; sz = sz + 1 } :: rst
+    | false, rst ->
+      acc := { bv = Cte false; sz = 1 } :: rst
+    | true, { bv = Cte true; sz } :: rst ->
+      acc := { bv = Cte true; sz = sz + 1 } :: rst
+    | true, rst ->
+      acc := { bv = Cte true; sz = 1 } :: rst
+  done;
+  !acc
+
 let equal_abstract eq = Lists.equal (equal_simple_term eq)
 
 (* for the solver *)
@@ -332,19 +360,8 @@ module Shostak(X : ALIEN) = struct
     and vmake ~neg tv ctx =
       match tv.descr with
       | Vcte z ->
-        let acc = ref [] in
-        for i = 0 to tv.size - 1 do
-          match Z.testbit z i, !acc with
-          | false, { bv = Cte b; sz } :: rst when Bool.equal b neg ->
-            acc := { bv = Cte b; sz = sz + 1 } :: rst
-          | false, rst ->
-            acc := { bv = Cte neg; sz = 1 } :: rst
-          | _, { bv = Cte b; sz } :: rst when Bool.equal b (not neg) ->
-            acc := { bv = Cte b; sz = sz + 1 } :: rst
-          | _, rst ->
-            acc := { bv = Cte (not neg); sz = 1 } :: rst
-        done;
-        !acc, ctx
+        let z = if neg then Z.lognot z else z in
+        int2bv_const tv.size z, ctx
       | Vother t -> other ~neg t tv.size ctx
       | Vextract (t', i, j) ->
         run ctx @@ vextract ~neg i j (view t')
@@ -1151,6 +1168,12 @@ module Shostak(X : ALIEN) = struct
          | Other t | Ext(t,_,_,_) -> (X.leaves t)@acc
       ) [] bitv
 
+  let is_constant bitv =
+    List.for_all (fun x ->
+        match x.bv with
+        | Cte _ -> true
+        | Other r | Ext (r, _, _, _) -> X.is_constant r) bitv
+
   let is_mine_opt = function [{ bv = Other r; _ }] -> Some r | _ -> None
 
   let is_mine bv =
diff --git a/src/lib/reasoners/bitv.mli b/src/lib/reasoners/bitv.mli
index 8f57a3a9c..f0d38c8ed 100644
--- a/src/lib/reasoners/bitv.mli
+++ b/src/lib/reasoners/bitv.mli
@@ -30,6 +30,16 @@
 
 type 'a abstract
 
+(** [to_Z_opt r] evaluates [r] to an integer if possible. *)
+val to_Z_opt : 'a abstract -> Z.t option
+
+(** [int2bv_const n z] evaluates [z] as a constant [n]-bits bitvector.
+
+    If [z] is out of the [0 .. 2^n] range, only the first [n] bits of [z] in
+    binary representation are considered, i.e.  [int2bv_const n z] is always
+    equal to [int2bv_const n (erem z (1 lsl n))]. *)
+val int2bv_const : int -> Z.t -> 'a abstract
+
 module type ALIEN = sig
   include Sig.X
   val embed : r abstract -> r
diff --git a/src/lib/reasoners/bitv_rel.ml b/src/lib/reasoners/bitv_rel.ml
index b390ba936..9ce823f69 100644
--- a/src/lib/reasoners/bitv_rel.ml
+++ b/src/lib/reasoners/bitv_rel.ml
@@ -28,14 +28,50 @@
 (*                                                                        *)
 (**************************************************************************)
 
-type t = unit
+type t = { delayed : Rel_utils.Delayed.t }
 
-let empty _ = ()
-let assume _ _ _ =
-  (), { Sig_rel.assume = []; remove = []}
+(* Currently we only compute, but in the future we may want to perform the same
+   simplifications as in [Bitv.make]. We currently don't, because we don't
+   really have a way to share code that uses polynome between the theory and the
+   relations without touching the Shostak [module rec].
+
+   Note that if we *do* want to compute here, the check for [X.is_constant] in
+   [Rel_utils.update] needs to be removed, which may have (small) performance
+   implications. *)
+let bv2nat _op bv =
+  match Bitv.to_Z_opt bv with
+  | Some n -> Some (Shostak.Polynome.create [] (Q.of_bigint n) Tint)
+  | None -> None
+
+(* [int2bv] is in the bitvector theory rather than the arithmetic theory because
+   we treat the arithmetic as more "primitive" than bit-vectors. *)
+let int2bv op p =
+  match op, Shostak.Polynome.is_const p with
+  | Symbols.Int2BV n, Some q ->
+    assert (Z.equal (Q.den q) Z.one);
+    let m = Q.to_bigint q in
+    Some (Bitv.int2bv_const n m)
+  | Int2BV _, None -> None
+  | _ -> assert false
+
+let delay1 = Rel_utils.delay1
+
+let dispatch = function
+  | Symbols.BV2Nat ->
+    Some (delay1 Shostak.Bitv.embed Shostak.Arith.is_mine bv2nat)
+  | Int2BV _ ->
+    Some (delay1 Shostak.Arith.embed Shostak.Bitv.is_mine int2bv)
+  | _ -> None
+
+let empty _ = { delayed = Rel_utils.Delayed.create dispatch }
+let assume env uf la =
+  let delayed, result = Rel_utils.Delayed.assume env.delayed uf la in
+  { delayed }, result
 let query _ _ _ = None
 let case_split _ _ ~for_model:_ = []
-let add env _ _ _ = env, []
+let add env uf r t =
+  let delayed, eqs = Rel_utils.Delayed.add env.delayed uf r t in
+  { delayed }, eqs
 let new_terms _ = Expr.Set.empty
 let instantiate ~do_syntactic_matching:_ _ env _ _ = env, []
 
diff --git a/src/lib/reasoners/ccx.ml b/src/lib/reasoners/ccx.ml
index a7d6a7123..265700244 100644
--- a/src/lib/reasoners/ccx.ml
+++ b/src/lib/reasoners/ccx.ml
@@ -451,7 +451,7 @@ module Main : S = struct
            LRE.add (LR.make ra, aopt) e mp
         ) LRE.empty sa
     in
-    LRE.fold (fun _ e acc -> e::acc)mp []
+    LRE.fold (fun _ e acc -> e::acc) mp []
 
   let replay_atom env sa =
     Options.exec_thread_yield ();
diff --git a/src/lib/reasoners/enum.ml b/src/lib/reasoners/enum.ml
index 7366b0ab6..500fa43bc 100644
--- a/src/lib/reasoners/enum.ml
+++ b/src/lib/reasoners/enum.ml
@@ -127,6 +127,8 @@ module Shostak (X : ALIEN) = struct
 
   let leaves _ = []
 
+  let is_constant _ = true
+
   let subst p v c =
     let cr = is_mine c in
     if X.equal p cr then v
diff --git a/src/lib/reasoners/intervalCalculus.ml b/src/lib/reasoners/intervalCalculus.ml
index bad39f9b1..45826b1ab 100644
--- a/src/lib/reasoners/intervalCalculus.ml
+++ b/src/lib/reasoners/intervalCalculus.ml
@@ -75,15 +75,8 @@ module EM = Matching.Make
       let term_repr env t ~init_term:_ = Uf.term_repr env t
     end)
 
-type r = P.r
 module LR = Uf.LX
 
-module MR = Map.Make(
-  struct
-    type t = r L.view
-    let compare a b = LR.compare (LR.make a) (LR.make b)
-  end)
-
 let alien_of p = Shostak.Arith.is_mine p
 
 let poly_of r = Shostak.Arith.embed r
@@ -107,15 +100,11 @@ end
 
 module Sim = OcplibSimplex.Basic.Make(SimVar)(Numbers.Q)(Explanation)
 
-type used_by = {
-  pow : SE.t;
-}
-
 type t = {
   inequations : P.t Inequalities.t MPL.t;
   monomes: (I.t * SX.t) MX0.t;
   polynomes : I.t MP0.t;
-  used_by : used_by MX0.t;
+  delayed : Rel_utils.Delayed.t;
   known_eqs : SX.t;
   improved_p : SP.t;
   improved_x : SX.t;
@@ -564,9 +553,13 @@ module Debug = struct
 
   let implied_equalities l =
     if get_debug_fm () then
-      let print fmt (ra, _, ex, _) =
+      let pp_literal ppf = function
+        | Sig_rel.LTerm e -> Expr.print ppf e
+        | LSem ra -> LR.print ppf (LR.make ra)
+      in
+      let print fmt (ra, ex, _) =
         fprintf fmt "@,%a %a"
-          LR.print (LR.make ra)
+          pp_literal ra
           Explanation.print ex
       in
       print_dbg
@@ -654,11 +647,49 @@ module Debug = struct
 end
 (*BISECT-IGNORE-END*)
 
+let calc_pow a b ty uf =
+  let ra, expl_a = Uf.find uf a in
+  let rb, expl_b = Uf.find uf b in
+  let pa = poly_of ra in
+  let pb = poly_of rb in
+  try
+    match P.is_const pb with
+    | Some c_y ->
+      let res =
+        (* x ** 1 -> x *)
+        if Q.equal c_y Q.one then
+          ra
+          (* x ** 0 -> 1 *)
+        else if Q.equal c_y Q.zero then
+          alien_of (P.create [] Q.one ty)
+        else
+          match P.is_const pa with
+          | Some c_x ->
+            (* x ** y *)
+            let res = Arith.calc_power c_x c_y ty  in
+            alien_of (P.create [] res ty)
+          | None -> raise Exit
+      in
+      Some (res,Ex.union expl_a expl_b)
+    | None -> None
+  with Exit -> None
+
+let delayed_pow uf _op = function
+  | [ a; b ] -> calc_pow a b (E.type_info a) uf
+  | _ -> assert false
+
+(* These are the partially interpreted functions that we know how to compute.
+   They will be computed immediately if possible, or as soon as we learn the
+   value of their arguments. *)
+let dispatch = function
+  | Symbols.Pow -> Some delayed_pow
+  | _ -> None
+
 let empty classes = {
   inequations = MPL.empty;
   monomes = MX.empty ;
   polynomes = MP.empty ;
-  used_by = MX0.empty;
+  delayed = Rel_utils.Delayed.create dispatch;
   known_eqs = SX.empty ;
   improved_p = SP.empty ;
   improved_x = SX.empty ;
@@ -1445,18 +1476,6 @@ let normal_form a = match a with
 
   | _ -> a
 
-let remove_trivial_eqs eqs la =
-  let la =
-    List.fold_left (fun m ((a, _, _, _) as e) -> MR.add a e m) MR.empty la
-  in
-  let eqs, _ =
-    List.fold_left
-      (fun ((eqs, m) as acc) ((sa, _, _, _) as e) ->
-         if MR.mem sa m then acc else e :: eqs, MR.add sa e m
-      )([], la) eqs
-  in
-  eqs
-
 let equalities_from_polynomes env eqs =
   let known, eqs =
     MP.fold
@@ -1560,56 +1579,6 @@ let rec loop_update_intervals are_eq env cpt =
   then env
   else loop_update_intervals are_eq env cpt
 
-let calc_pow a b ty uf =
-  let ra, expl_a = Uf.find uf a in
-  let rb, expl_b = Uf.find uf b in
-  let pa = poly_of ra in
-  let pb = poly_of rb in
-  try
-    match P.is_const pb with
-    | Some c_y ->
-      let res =
-        (* x ** 1 -> x *)
-        if Q.equal c_y Q.one then
-          ra
-          (* x ** 0 -> 1 *)
-        else if Q.equal c_y Q.zero then
-          alien_of (P.create [] Q.one ty)
-        else
-          match P.is_const pa with
-          | Some c_x ->
-            (* x ** y *)
-            let res = Arith.calc_power c_x c_y ty  in
-            alien_of (P.create [] res ty)
-          | None -> raise Exit
-      in
-      Some (res,Ex.union expl_a expl_b)
-    | None -> None
-  with Exit -> None
-
-(** Update and compute value of terms in relation with r1 if it is possible *)
-let update_used_by_pow env r1 p2 orig  eqs =
-  try
-    if orig != Th_util.Subst then raise Exit;
-    if P.is_const p2 == None then raise Exit;
-    let s = (MX0.find r1 env.used_by).pow in
-    SE.fold (fun t eqs ->
-        match E.term_view t with
-        | { E.f = (Sy.Op Sy.Pow); xs = [a; b]; ty; _ } ->
-          begin
-            match calc_pow a b ty env.new_uf with
-              None -> eqs
-            | Some (y,ex) ->
-              let eq = L.Eq (X.term_embed t,y) in
-              (eq, None, ex, Th_util.Other) :: eqs
-          end
-        | _ ->
-          Printer.print_err
-            "Expected a 'power' term with two arguments, but got %a" E.print t;
-          assert false
-      ) s eqs
-  with Exit | Not_found -> eqs
-
 let assume ~query env uf la =
   let module Oracle = (val get_oracle ()) in
   Oracle.incr_age ();
@@ -1689,7 +1658,9 @@ let assume ~query env uf la =
              in
              let env, eqs = add_equality are_eq env eqs p expl in
              let env = tighten_eq_bounds env r1 r2 p1 p2 orig expl in
-             let eqs = update_used_by_pow env r1 p2 orig eqs in
+             let eqs =
+               Rel_utils.Delayed.update env.delayed env.new_uf r1 r2 orig eqs
+             in
              env, eqs, new_ineqs, rm
 
            | _ -> acc
@@ -1716,12 +1687,8 @@ let assume ~query env uf la =
       let env, eqs = equalities_from_intervals env eqs in
 
       Debug.env env;
-      let eqs = remove_trivial_eqs eqs la in
-      Debug.implied_equalities eqs;
-      let to_assume =
-        List.rev_map (fun (sa, _, ex, orig) ->
-            (Sig_rel.LSem sa, ex, orig)) eqs
-      in
+      let to_assume = Rel_utils.assume_nontrivial_eqs eqs la in
+      Debug.implied_equalities to_assume;
       env, {Sig_rel.assume = to_assume; remove = to_remove}
   with I.NotConsistent expl ->
     Debug.inconsistent_interval expl ;
@@ -1845,36 +1812,6 @@ let default_case_split env uf ~for_model =
     end
   | res -> res
 
-(** Add relation between term x and the terms in it. This can allow use to track
-    if x is computable when its subterms values are known.
-    This is currently only done for power *)
-let add_used_by t r env =
-  match E.term_view t with
-  | { E.f = (Sy.Op Sy.Pow); xs = [a; b]; ty; _ } ->
-    begin
-      match calc_pow a b ty env.new_uf with
-      | Some (res,ex) ->
-        if X.equal res r then
-          (* in this case, Arith.make already reduced "t" to a constant "r" *)
-          env, []
-        else
-          env, [L.Eq(res, r), ex]
-      | None ->
-        let ra = Uf.make env.new_uf a in
-        let rb = Uf.make env.new_uf b in
-        let sra =
-          try (MX0.find ra env.used_by).pow
-          with Not_found -> SE.empty in
-        let used_by_ra = MX0.add ra {pow = (SE.add t sra)} env.used_by in
-        let srb =
-          try (MX0.find rb used_by_ra).pow
-          with Not_found -> SE.empty in
-        let used_by_rb = MX0.add rb {pow = (SE.add t srb)} used_by_ra in
-        {env with used_by = used_by_rb}, []
-    end
-  | _ -> env, []
-         [@ocaml.ppwarning "TODO: add other terms such as div!"]
-
 let add =
   let are_eq t1 t2 =
     if E.equal t1 t2 then Some (Explanation.empty, []) else None
@@ -1889,7 +1826,10 @@ let add =
         let env =
           init_monomes_of_poly are_eq env p SX.empty Explanation.empty
         in
-        add_used_by t r env
+        let delayed, eqs =
+          Rel_utils.Delayed.add env.delayed env.new_uf r t
+        in
+        { env with delayed }, eqs
       else env, []
     with I.NotConsistent expl ->
       Debug.inconsistent_interval expl;
diff --git a/src/lib/reasoners/ite.ml b/src/lib/reasoners/ite.ml
index a4daa5c68..a60151288 100644
--- a/src/lib/reasoners/ite.ml
+++ b/src/lib/reasoners/ite.ml
@@ -53,6 +53,7 @@ module Shostak (X : ALIEN) = struct
   let equal _ _      = assert false
   let hash _         = assert false
   let leaves _       = assert false
+  let is_constant _  = assert false
   let subst _ _ _    = assert false
   let make _         = assert false
   let term_extract _ = None, false
@@ -61,4 +62,3 @@ module Shostak (X : ALIEN) = struct
   let assign_value _ _ _ = assert false
   let choose_adequate_model _ _ _ = assert false
 end
-
diff --git a/src/lib/reasoners/records.ml b/src/lib/reasoners/records.ml
index c87883850..cd75c0ea8 100644
--- a/src/lib/reasoners/records.ml
+++ b/src/lib/reasoners/records.ml
@@ -214,6 +214,15 @@ module Shostak (X : ALIEN) = struct
     in
     XS.elements (leaves t)
 
+  let is_constant =
+    let rec is_constant t =
+      match normalize t with
+      | Record (lbs, _) ->
+        List.for_all (fun (_, x) -> is_constant x) lbs
+      | Access (_, x, _) -> is_constant x
+      | Other (x, _) -> X.is_constant x
+    in is_constant
+
   let rec hash  = function
     | Record (lbs, ty) ->
       List.fold_left
diff --git a/src/lib/reasoners/rel_utils.ml b/src/lib/reasoners/rel_utils.ml
new file mode 100644
index 000000000..b31d0391c
--- /dev/null
+++ b/src/lib/reasoners/rel_utils.ml
@@ -0,0 +1,215 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     Alt-Ergo: The SMT Solver For Software Verification                 *)
+(*     Copyright (C) 2013-2023 --- OCamlPro SAS                           *)
+(*                                                                        *)
+(*     This file is distributed under the terms of OCamlPro               *)
+(*     Non-Commercial Purpose License, version 1.                         *)
+(*                                                                        *)
+(*     As an exception, Alt-Ergo Club members at the Gold level can       *)
+(*     use this file under the terms of the Apache Software License       *)
+(*     version 2.0.                                                       *)
+(*                                                                        *)
+(*     More details can be found in the directory licenses/               *)
+(*                                                                        *)
+(**************************************************************************)
+
+module X = Shostak.Combine
+module MXH = Shostak.MXH
+module L = Xliteral
+module LR = Uf.LX
+module SR = Set.Make(
+  struct
+    type t = X.r L.view
+    let compare a b = LR.compare (LR.make a) (LR.make b)
+  end)
+
+(** [assume_nontrivial_eqs eqs la] can be used by theories to remove from the
+    equations [eqs] both duplicates and those that are implied by the
+    assumptions in [la]. *)
+let assume_nontrivial_eqs
+    (eqs : X.r Sig_rel.input list)
+    (la : X.r Sig_rel.input list)
+  : X.r Sig_rel.fact list =
+  let la =
+    List.fold_left (fun m (a, _, _, _) -> SR.add a m) SR.empty la
+  in
+  let eqs, _ =
+    List.fold_left
+      (fun ((eqs, m) as acc) ((sa, _, _, _) as e) ->
+         if SR.mem sa m then acc else e :: eqs, SR.add sa m
+      )([], la) eqs
+  in
+  List.rev_map (fun (sa, _, ex, orig) -> Sig_rel.LSem sa, ex, orig) eqs
+
+(* The type of delayed functions. A delayed function is given an [Uf.t] instance
+   for resolving expressions to semantic values, the operator to compute, and a
+   list of expressions as argument.
+
+   It returns a semantic value, and an explanation for why the operator applied
+   to the arguments is equal to the result (usually derived from the
+   explanations from [Uf.find]). *)
+type delayed_fn =
+  Uf.t -> Symbols.operator -> Expr.t list -> (X.r * Explanation.t) option
+
+let delay1 embed is_mine f uf op = function
+  | [ t ] -> (
+      let r, ex = Uf.find uf t in
+      match f op (embed r) with
+      | Some v -> Some (is_mine v, ex)
+      | None -> None
+    )
+  | _ -> assert false
+
+let delay2 embed is_mine f uf op = function
+  | [ t1; t2 ] -> (
+      let r1, ex1 = Uf.find uf t1 in
+      let r2, ex2 = Uf.find uf t2 in
+      match f op (embed r1) (embed r2) with
+      | Some v -> Some (is_mine v, Explanation.union ex1 ex2)
+      | None -> None
+    )
+  | _ -> assert false
+
+(** The [Delayed] module can be used by relations that deal with partially
+    interpreted functions. It will introduce the equalities between a function
+    and its interpreted value as soon as the value of its arguments become
+    known.
+
+    To avoid issues with eager splitting, functions are not computed
+    on case splits unless model generation is enabled. *)
+module Delayed : sig
+  type t
+
+  (** [create dispatch] creates a new delayed structure for the symbols handled
+      by [dispatch].
+
+      [dispatch] must be pure. *)
+  val create : (Symbols.operator -> delayed_fn option) -> t
+
+  (** [add env uf r t] checks whether the term [t] is a delayed function and if
+      so either adds it to the structure or evaluates it immediately if
+      possible, in which case a new equality with corresponding explanation is
+      returned.
+
+      [r] must be the semantic value associated with [t].
+
+      [add] can be called directly with the arguments passed to a relation's
+      [add] function. *)
+  val add : t -> Uf.t -> X.r -> Expr.t -> t * (X.r L.view * Explanation.t) list
+
+  (** [update env uf r orig eqs] checks whether [r] is an argument of a
+      registered delayed function and, if so, tries to compute the corresponding
+      delayed function. If all the function's arguments are constants, the
+      resulting equality is accumulated into [eqs].
+
+      [update] should be called with the left-hand side of [Eq] literals that
+      are [assume]d by a relation. *)
+  val update :
+    t -> Uf.t -> X.r -> X.r -> Th_util.lit_origin ->
+    X.r Sig_rel.input list -> X.r Sig_rel.input list
+
+  (** [assume] is a simple wrapper for [update] that is compatible with the
+      [assume] signature of a relation. *)
+  val assume : t -> Uf.t -> X.r Sig_rel.input list -> t * X.r Sig_rel.result
+end = struct
+  module OMap = Map.Make(struct
+      type t = Symbols.operator
+
+      let compare = Symbols.compare_operators
+    end)
+
+  type t = {
+    dispatch : Symbols.operator -> delayed_fn option ;
+    used_by : Expr.Set.t OMap.t MXH.t ;
+  }
+
+  let create dispatch = { dispatch; used_by = MXH.empty }
+
+  let add ({ dispatch; used_by } as env) uf r t =
+    (* Note: we dispatch on [Op] symbols, but it could make sense to dispatch on
+       a separate constructor for explicitely delayed terms. *)
+    match Expr.term_view t with
+    | { f = Op f; xs; _ } -> (
+        match dispatch f with
+        | None -> env, []
+        | Some fn ->
+          match fn uf f xs with
+          | Some (r', ex) ->
+            if X.equal r' r then
+              (* already simplified by [X.make] *)
+              env, []
+            else
+              env, [L.Eq(r', r), ex]
+          | None ->
+            let used_by =
+              List.fold_left (fun used_by x ->
+                  MXH.update (Uf.make uf x) (fun sm ->
+                      let sm = Option.value ~default:OMap.empty sm in
+                      Option.some @@
+                      OMap.update f (fun se ->
+                          let se = Option.value ~default:Expr.Set.empty se in
+                          Some (Expr.Set.add t se)) sm) used_by) used_by xs
+            in { env with used_by }, []
+      )
+    | _ -> env, []
+
+  let update { dispatch; used_by } uf r1 eqs =
+    match MXH.find r1 used_by with
+    | exception Not_found -> eqs
+    | sm ->
+      OMap.fold (fun sy se eqs ->
+          let fn =
+            (* The [fn] must be present because we only add symbols to
+               [used_by] if they are in the dispatch table. *)
+            Option.get (dispatch sy)
+          in
+          Expr.Set.fold (fun t eqs ->
+              let { Expr.xs; f; _ } = Expr.term_view t in
+              assert (Symbols.equal (Op sy) f);
+              match fn uf sy xs with
+              | Some (r, ex) ->
+                (L.Eq (X.term_embed t, r), None, ex, Th_util.Other) :: eqs
+              | None -> eqs) se eqs) sm eqs
+
+  let update env uf r1 r2 orig eqs =
+    (* The `Subst` origin is used when `r1 -> r2` is added in the
+        union-find. The `CS _` and `NCS _` origins are used for case splits. In
+        both cases, we want to be propagating the constant.
+
+        Note that equalities of `Subst` origins are oriented: for `Subst`, `r2`
+        is the (new) normal form for `r1.
+
+        Usually, this would be true of case-split equalities as well (of the
+        form `r = v` where `v` is the chosen value), but this is not true for
+        the case splits that come from the arrays theory (in fact, the array
+        theory produces *dis*equality case splits, and the equality ends up in
+        the `NCS` instead), so we don't try to be smart and pay the (small)
+        performance cost.
+
+        `Other` cases should (I believe...) be subsumed by `Subst`. The original
+        code in the arithmetic theory that this is lifted from from was only
+        considering `Subst`, and was allowing possibly incorrect models.
+
+        Note that we need to handle `CS` and `NCS` here to produce correct
+        models, but also this can cause eager enumeration, so by excess of
+        caution we only use it when model generation has been requested. It is
+        unknown whether eager enumeration would be an actual problem in
+        practice. *)
+    match orig with
+    | Th_util.Subst when X.is_constant r2 -> update env uf r1 eqs
+    | CS _ | NCS _ when Options.get_interpretation () ->
+      update env uf r2 (update env uf r1 eqs)
+    | _ -> eqs
+
+
+  let assume env uf la =
+    let eqs =
+      List.fold_left (fun eqs (a, _root, _expl, orig) ->
+          match a with
+          | Xliteral.Eq (r1, r2) -> update env uf r1 r2 orig eqs
+          | _ -> eqs
+        ) [] la
+    in
+    env, { Sig_rel.assume = assume_nontrivial_eqs eqs la; remove = [] }
+end
diff --git a/src/lib/reasoners/shostak.ml b/src/lib/reasoners/shostak.ml
index d2f02b2bb..a2d72d6ea 100644
--- a/src/lib/reasoners/shostak.ml
+++ b/src/lib/reasoners/shostak.ml
@@ -357,6 +357,17 @@ struct
     | Ac t -> r :: (AC.leaves t)
     | Term _ -> [r]
 
+  let is_constant r =
+    match r.v with
+    | Arith t -> ARITH.is_constant t
+    | Records t -> RECORDS.is_constant t
+    | Bitv t -> BITV.is_constant t
+    | Arrays t -> ARRAYS.is_constant t
+    | Enum t -> ENUM.is_constant t
+    | Adt t -> ADT.is_constant t
+    | Ite t -> ITE.is_constant t
+    | Ac _ | Term _ -> false
+
   let subst p v r =
     if equal p v then r
     else match r.v with
diff --git a/src/lib/reasoners/sig.mli b/src/lib/reasoners/sig.mli
index 6b673e2dc..32b0aeb16 100644
--- a/src/lib/reasoners/sig.mli
+++ b/src/lib/reasoners/sig.mli
@@ -61,6 +61,14 @@ module type SHOSTAK = sig
 
   (** Give the leaves of a term of the theory *)
   val leaves : t -> r list
+
+  (** Determines whether the term is a constant. [is_constant t] is equivalent
+      to [leaves t == []], but is more efficient.
+
+      Note that for some theories (e.g. records, arrays) the constant may not be
+      pure: it may involve nested (constant) terms of other theories. *)
+  val is_constant : t -> bool
+
   val subst : r -> r -> t -> r
 
   val compare : r -> r -> int
@@ -116,6 +124,8 @@ module type X = sig
 
   val leaves : r -> r list
 
+  val is_constant : r -> bool
+
   val subst : r -> r -> r -> r
 
   val solve : r -> r ->  (r * r) list
diff --git a/src/lib/structures/symbols.mli b/src/lib/structures/symbols.mli
index 11da4792f..859ff06d3 100644
--- a/src/lib/structures/symbols.mli
+++ b/src/lib/structures/symbols.mli
@@ -117,6 +117,7 @@ val is_internal : t -> bool
 val equal : t -> t -> bool
 val compare : t -> t -> int
 val compare_bounds : bound -> bound -> int
+val compare_operators : operator -> operator -> int
 val hash : t -> int
 
 val to_string : t -> string
diff --git a/tests/bitv/testfile-array-cs.dolmen.expected b/tests/bitv/testfile-array-cs.dolmen.expected
new file mode 100644
index 000000000..6f99ff0f4
--- /dev/null
+++ b/tests/bitv/testfile-array-cs.dolmen.expected
@@ -0,0 +1,2 @@
+
+unsat
diff --git a/tests/bitv/testfile-array-cs.dolmen.smt2 b/tests/bitv/testfile-array-cs.dolmen.smt2
new file mode 100644
index 000000000..8ad600952
--- /dev/null
+++ b/tests/bitv/testfile-array-cs.dolmen.smt2
@@ -0,0 +1,10 @@
+(set-logic ALL)
+; We need produce-models to propagate `int2bv` when learning `0 = y`
+(set-option :produce-models true)
+(declare-const a (Array Int Int))
+(declare-const x Int)
+(declare-const y Int)
+(assert (= (select a 4) 1))
+(assert (= (select (store a y 0) 4) 0))
+(assert (= ((_ int2bv 2) y) #b11))
+(check-sat)
diff --git a/tests/bitv/testfile-bv2nat-delayed.dolmen.expected b/tests/bitv/testfile-bv2nat-delayed.dolmen.expected
new file mode 100644
index 000000000..6f99ff0f4
--- /dev/null
+++ b/tests/bitv/testfile-bv2nat-delayed.dolmen.expected
@@ -0,0 +1,2 @@
+
+unsat
diff --git a/tests/bitv/testfile-bv2nat-delayed.dolmen.smt2 b/tests/bitv/testfile-bv2nat-delayed.dolmen.smt2
new file mode 100644
index 000000000..463832ae2
--- /dev/null
+++ b/tests/bitv/testfile-bv2nat-delayed.dolmen.smt2
@@ -0,0 +1,5 @@
+(set-logic ALL)
+(declare-const x (_ BitVec 32))
+(assert (distinct (bv2nat x) 2))
+(assert (= x #b00000000000000000000000000000010))
+(check-sat)
diff --git a/tests/bitv/testfile-bv2nat-immediate.dolmen.expected b/tests/bitv/testfile-bv2nat-immediate.dolmen.expected
new file mode 100644
index 000000000..6f99ff0f4
--- /dev/null
+++ b/tests/bitv/testfile-bv2nat-immediate.dolmen.expected
@@ -0,0 +1,2 @@
+
+unsat
diff --git a/tests/bitv/testfile-bv2nat-immediate.dolmen.smt2 b/tests/bitv/testfile-bv2nat-immediate.dolmen.smt2
new file mode 100644
index 000000000..467c210cc
--- /dev/null
+++ b/tests/bitv/testfile-bv2nat-immediate.dolmen.smt2
@@ -0,0 +1,5 @@
+(set-logic ALL)
+(declare-const x (_ BitVec 32))
+(assert (= x #b00000000000000000000000000000010))
+(assert (distinct (bv2nat x) 2))
+(check-sat)
diff --git a/tests/bitv/testfile-bv2nat-models.dolmen.expected b/tests/bitv/testfile-bv2nat-models.dolmen.expected
new file mode 100644
index 000000000..a37f6f187
--- /dev/null
+++ b/tests/bitv/testfile-bv2nat-models.dolmen.expected
@@ -0,0 +1,5 @@
+
+unknown
+(
+  (define-fun x () (_ BitVec 4) #b0111)
+)
diff --git a/tests/bitv/testfile-bv2nat-models.dolmen.smt2 b/tests/bitv/testfile-bv2nat-models.dolmen.smt2
new file mode 100644
index 000000000..459ea52d7
--- /dev/null
+++ b/tests/bitv/testfile-bv2nat-models.dolmen.smt2
@@ -0,0 +1,6 @@
+(set-logic ALL)
+(set-option :produce-models true)
+(declare-const x (_ BitVec 4))
+(assert (= (bv2nat x) 7))
+(check-sat)
+(get-model)
diff --git a/tests/bitv/testfile-int2bv-delayed.dolmen.expected b/tests/bitv/testfile-int2bv-delayed.dolmen.expected
new file mode 100644
index 000000000..6f99ff0f4
--- /dev/null
+++ b/tests/bitv/testfile-int2bv-delayed.dolmen.expected
@@ -0,0 +1,2 @@
+
+unsat
diff --git a/tests/bitv/testfile-int2bv-delayed.dolmen.smt2 b/tests/bitv/testfile-int2bv-delayed.dolmen.smt2
new file mode 100644
index 000000000..347264770
--- /dev/null
+++ b/tests/bitv/testfile-int2bv-delayed.dolmen.smt2
@@ -0,0 +1,5 @@
+(set-logic ALL)
+(declare-const x Int)
+(assert (distinct ((_ int2bv 4) x) #b0101))
+(assert (= x 5))
+(check-sat)
diff --git a/tests/bitv/testfile-int2bv-immediate.dolmen.expected b/tests/bitv/testfile-int2bv-immediate.dolmen.expected
new file mode 100644
index 000000000..6f99ff0f4
--- /dev/null
+++ b/tests/bitv/testfile-int2bv-immediate.dolmen.expected
@@ -0,0 +1,2 @@
+
+unsat
diff --git a/tests/bitv/testfile-int2bv-immediate.dolmen.smt2 b/tests/bitv/testfile-int2bv-immediate.dolmen.smt2
new file mode 100644
index 000000000..6abca1303
--- /dev/null
+++ b/tests/bitv/testfile-int2bv-immediate.dolmen.smt2
@@ -0,0 +1,5 @@
+(set-logic ALL)
+(declare-const x Int)
+(assert (= x 5))
+(assert (distinct ((_ int2bv 4) x) #b0101))
+(check-sat)
diff --git a/tests/dune.inc b/tests/dune.inc
index 5ef5b2b99..3b21d9a7f 100644
--- a/tests/dune.inc
+++ b/tests/dune.inc
@@ -120739,6 +120739,48 @@
 
 ; Auto-generated part begin
 (subdir bitv
+  (rule
+   (target testfile-int2bv-immediate.dolmen_dolmen.output)
+   (deps (:input testfile-int2bv-immediate.dolmen.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             %{input})))))))
+  (rule
+   (deps testfile-int2bv-immediate.dolmen_dolmen.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff testfile-int2bv-immediate.dolmen.expected testfile-int2bv-immediate.dolmen_dolmen.output)))
+  (rule
+   (target testfile-int2bv-delayed.dolmen_dolmen.output)
+   (deps (:input testfile-int2bv-delayed.dolmen.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             %{input})))))))
+  (rule
+   (deps testfile-int2bv-delayed.dolmen_dolmen.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff testfile-int2bv-delayed.dolmen.expected testfile-int2bv-delayed.dolmen_dolmen.output)))
   (rule
    (target testfile-bvnot.dolmen_dolmen.output)
    (deps (:input testfile-bvnot.dolmen.smt2))
@@ -120781,6 +120823,69 @@
      (package alt-ergo)
       (action
        (diff testfile-bvnot-term.dolmen.expected testfile-bvnot-term.dolmen_dolmen.output)))
+  (rule
+   (target testfile-bv2nat-models.dolmen_dolmen.output)
+   (deps (:input testfile-bv2nat-models.dolmen.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             %{input})))))))
+  (rule
+   (deps testfile-bv2nat-models.dolmen_dolmen.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff testfile-bv2nat-models.dolmen.expected testfile-bv2nat-models.dolmen_dolmen.output)))
+  (rule
+   (target testfile-bv2nat-immediate.dolmen_dolmen.output)
+   (deps (:input testfile-bv2nat-immediate.dolmen.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             %{input})))))))
+  (rule
+   (deps testfile-bv2nat-immediate.dolmen_dolmen.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff testfile-bv2nat-immediate.dolmen.expected testfile-bv2nat-immediate.dolmen_dolmen.output)))
+  (rule
+   (target testfile-bv2nat-delayed.dolmen_dolmen.output)
+   (deps (:input testfile-bv2nat-delayed.dolmen.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             %{input})))))))
+  (rule
+   (deps testfile-bv2nat-delayed.dolmen_dolmen.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff testfile-bv2nat-delayed.dolmen.expected testfile-bv2nat-delayed.dolmen_dolmen.output)))
   (rule
    (target testfile-bitv023_ci_cdcl_no_minimal_bj.output)
    (deps (:input testfile-bitv023.ae))
@@ -126990,7 +127095,28 @@
     (alias runtest-quick)
      (package alt-ergo)
       (action
-       (diff testfile-bitv001.expected testfile-bitv001_fpa.output))))
+       (diff testfile-bitv001.expected testfile-bitv001_fpa.output)))
+  (rule
+   (target testfile-array-cs.dolmen_dolmen.output)
+   (deps (:input testfile-array-cs.dolmen.smt2))
+   (package alt-ergo)
+   (action
+    (chdir %{workspace_root}
+     (with-stdout-to %{target}
+      (ignore-stderr
+       (with-accepted-exit-codes 0
+        (run %{bin:alt-ergo}
+             --timelimit=2
+             --enable-assertions
+             --output=smtlib2
+             --frontend dolmen
+             %{input})))))))
+  (rule
+   (deps testfile-array-cs.dolmen_dolmen.output)
+    (alias runtest-quick)
+     (package alt-ergo)
+      (action
+       (diff testfile-array-cs.dolmen.expected testfile-array-cs.dolmen_dolmen.output))))
 ; Auto-generated part end
 ; File auto-generated by gentests