diff --git a/src/bitwuzla_mappings.default.ml b/src/bitwuzla_mappings.default.ml
index f1f320cd..feed9763 100644
--- a/src/bitwuzla_mappings.default.ml
+++ b/src/bitwuzla_mappings.default.ml
@@ -18,6 +18,7 @@
 
 include Mappings_intf
 
+(* Hack: this was a hack to try and run bitwuzla in Owi *)
 let leak =
   let leaky_list = ref [] in
   let mutex = Mutex.create () in
@@ -48,6 +49,8 @@ module Fresh_bitwuzla (B : Bitwuzla_cxx.S) : M = struct
   (* Not supported *)
   type func_decl = unit
 
+  let caches_consts = false
+
   let true_ = mk_true ()
 
   let false_ = mk_false ()
diff --git a/src/cvc5_mappings.default.ml b/src/cvc5_mappings.default.ml
index 0af2db74..4d98492a 100644
--- a/src/cvc5_mappings.default.ml
+++ b/src/cvc5_mappings.default.ml
@@ -36,6 +36,8 @@ module Fresh_cvc5 () = struct
 
   type func_decl = unit
 
+  let caches_consts = true
+
   let tm = TermManager.mk_tm ()
 
   let true_ = Term.mk_true tm
diff --git a/src/mappings.ml b/src/mappings.ml
index accaa947..27183791 100644
--- a/src/mappings.ml
+++ b/src/mappings.ml
@@ -79,14 +79,16 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
         Fmt.failwith "Unsupported theory: %a@." Ty.pp ty
 
     let make_symbol (ctx : symbol_ctx) (s : Symbol.t) : symbol_ctx * M.term =
-      match Smap.find_opt s ctx with
-      | Some sym -> (ctx, sym)
-      | None ->
-        let name =
-          match s.name with Simple name -> name | _ -> assert false
-        in
+      let name = match s.name with Simple name -> name | _ -> assert false in
+      if M.caches_consts then
         let sym = M.const name (get_type s.ty) in
         (Smap.add s sym ctx, sym)
+      else
+        match Smap.find_opt s ctx with
+        | Some sym -> (ctx, sym)
+        | None ->
+          let sym = M.const name (get_type s.ty) in
+          (Smap.add s sym ctx, sym)
 
     module Bool_impl = struct
       let true_ = M.true_
diff --git a/src/mappings.nop.ml b/src/mappings.nop.ml
index 5cd04ed2..8c0b913a 100644
--- a/src/mappings.nop.ml
+++ b/src/mappings.nop.ml
@@ -34,6 +34,8 @@ module Nop = struct
 
     type func_decl = unit
 
+    let caches_consts = false
+
     let true_ = ()
 
     let false_ = ()
diff --git a/src/mappings_intf.ml b/src/mappings_intf.ml
index 428eda02..f209c373 100644
--- a/src/mappings_intf.ml
+++ b/src/mappings_intf.ml
@@ -39,6 +39,8 @@ module type M = sig
 
   type func_decl
 
+  val caches_consts : bool
+
   val true_ : term
 
   val false_ : term
diff --git a/src/z3_mappings.default.ml b/src/z3_mappings.default.ml
index df9ab997..91a74a17 100644
--- a/src/z3_mappings.default.ml
+++ b/src/z3_mappings.default.ml
@@ -17,77 +17,74 @@
 (***************************************************************************)
 
 include Mappings_intf
-module P = Params
-module Sym = Symbol
-module Stats = Statistics
 
 module M = struct
   module Make () = struct
-    open Z3
+    type ty = Z3.Sort.sort
 
-    type ty = Sort.sort
-
-    type term = Expr.expr
+    type term = Z3.Expr.expr
 
     type interp = term
 
-    type model = Model.model
+    type model = Z3.Model.model
+
+    type solver = Z3.Solver.solver
 
-    type solver = Solver.solver
+    type handle = Z3.Optimize.handle
 
-    type handle = Optimize.handle
+    type optimizer = Z3.Optimize.optimize
 
-    type optimizer = Optimize.optimize
+    type func_decl = Z3.FuncDecl.func_decl
 
-    type func_decl = FuncDecl.func_decl
+    let caches_consts = true
 
-    let ctx = mk_context []
+    let ctx = Z3.mk_context []
 
-    let true_ = Boolean.mk_true ctx
+    let true_ = Z3.Boolean.mk_true ctx
 
-    let false_ = Boolean.mk_false ctx
+    let false_ = Z3.Boolean.mk_false ctx
 
-    let int i = Arithmetic.Integer.mk_numeral_i ctx i
+    let int i = Z3.Arithmetic.Integer.mk_numeral_i ctx i
 
-    let real f = Arithmetic.Real.mk_numeral_s ctx (Float.to_string f)
+    let real f = Z3.Arithmetic.Real.mk_numeral_s ctx (Float.to_string f)
 
-    let const sym ty = Expr.mk_const_s ctx sym ty
+    let const sym ty = Z3.Expr.mk_const_s ctx sym ty
 
-    let not_ e = Boolean.mk_not ctx e
+    let not_ e = Z3.Boolean.mk_not ctx e
 
-    let and_ e1 e2 = Boolean.mk_and ctx [ e1; e2 ]
+    let and_ e1 e2 = Z3.Boolean.mk_and ctx [ e1; e2 ]
 
-    let or_ e1 e2 = Boolean.mk_or ctx [ e1; e2 ]
+    let or_ e1 e2 = Z3.Boolean.mk_or ctx [ e1; e2 ]
 
-    let logand es = Boolean.mk_and ctx es
+    let logand es = Z3.Boolean.mk_and ctx es
 
-    let logor es = Boolean.mk_or ctx es
+    let logor es = Z3.Boolean.mk_or ctx es
 
-    let xor e1 e2 = Boolean.mk_xor ctx e1 e2
+    let xor e1 e2 = Z3.Boolean.mk_xor ctx e1 e2
 
-    let eq e1 e2 = Boolean.mk_eq ctx e1 e2
+    let eq e1 e2 = Z3.Boolean.mk_eq ctx e1 e2
 
-    let distinct es = Boolean.mk_distinct ctx es
+    let distinct es = Z3.Boolean.mk_distinct ctx es
 
-    let ite cond e1 e2 = Boolean.mk_ite ctx cond e1 e2
+    let ite cond e1 e2 = Z3.Boolean.mk_ite ctx cond e1 e2
 
     module Types = struct
-      let int = Arithmetic.Integer.mk_sort ctx
+      let int = Z3.Arithmetic.Integer.mk_sort ctx
 
-      let real = Arithmetic.Real.mk_sort ctx
+      let real = Z3.Arithmetic.Real.mk_sort ctx
 
-      let bool = Boolean.mk_sort ctx
+      let bool = Z3.Boolean.mk_sort ctx
 
-      let string = Seq.mk_string_sort ctx
+      let string = Z3.Seq.mk_string_sort ctx
 
-      let bitv n = BitVector.mk_sort ctx n
+      let bitv n = Z3.BitVector.mk_sort ctx n
 
-      let float eb sb = FloatingPoint.mk_sort ctx eb sb
+      let float eb sb = Z3.FloatingPoint.mk_sort ctx eb sb
 
-      let ty term = Expr.get_sort term
+      let ty term = Z3.Expr.get_sort term
 
       let to_ety sort =
-        match Sort.get_sort_kind sort with
+        match Z3.Sort.get_sort_kind sort with
         | Z3enums.INT_SORT -> Ty.Ty_int
         | Z3enums.REAL_SORT -> Ty.Ty_real
         | Z3enums.BOOL_SORT -> Ty.Ty_bool
@@ -101,48 +98,49 @@ module M = struct
     end
 
     module Interp = struct
-      let to_int interp = Z.to_int @@ Arithmetic.Integer.get_big_int interp
+      let to_int interp = Z.to_int @@ Z3.Arithmetic.Integer.get_big_int interp
 
-      let to_real interp = Q.to_float @@ Arithmetic.Real.get_ratio interp
+      let to_real interp = Q.to_float @@ Z3.Arithmetic.Real.get_ratio interp
 
       let to_bool interp =
-        match Boolean.get_bool_value interp with
+        match Z3.Boolean.get_bool_value interp with
         | Z3enums.L_TRUE -> true
         | Z3enums.L_FALSE -> false
         | Z3enums.L_UNDEF ->
           Fmt.failwith "Z3_mappings2: to_bool: something went terribly wrong!"
 
-      let to_string interp = Seq.get_string ctx interp
+      let to_string interp = Z3.Seq.get_string ctx interp
 
       let to_bitv interp _n =
-        assert (Expr.is_numeral interp);
+        assert (Z3.Expr.is_numeral interp);
         let set (s : string) (i : int) (n : char) =
           let bs = Bytes.of_string s in
           Bytes.set bs i n;
           Bytes.to_string bs
         in
-        Int64.of_string (set (Expr.to_string interp) 0 '0')
+        Int64.of_string (set (Z3.Expr.to_string interp) 0 '0')
 
       let to_float fp _eb _sb =
-        assert (Expr.is_numeral fp);
-        if FloatingPoint.is_numeral_nan ctx fp then Float.nan
-        else if FloatingPoint.is_numeral_inf ctx fp then
-          if FloatingPoint.is_numeral_negative ctx fp then Float.neg_infinity
+        assert (Z3.Expr.is_numeral fp);
+        if Z3.FloatingPoint.is_numeral_nan ctx fp then Float.nan
+        else if Z3.FloatingPoint.is_numeral_inf ctx fp then
+          if Z3.FloatingPoint.is_numeral_negative ctx fp then Float.neg_infinity
           else Float.infinity
-        else if FloatingPoint.is_numeral_zero ctx fp then
-          if FloatingPoint.is_numeral_negative ctx fp then Float.neg Float.zero
+        else if Z3.FloatingPoint.is_numeral_zero ctx fp then
+          if Z3.FloatingPoint.is_numeral_negative ctx fp then
+            Float.neg Float.zero
           else Float.zero
         else
-          let sort = Expr.get_sort fp in
-          let ebits = FloatingPoint.get_ebits ctx sort in
-          let sbits = FloatingPoint.get_sbits ctx sort in
-          let _, sign = FloatingPoint.get_numeral_sign ctx fp in
+          let sort = Z3.Expr.get_sort fp in
+          let ebits = Z3.FloatingPoint.get_ebits ctx sort in
+          let sbits = Z3.FloatingPoint.get_sbits ctx sort in
+          let _, sign = Z3.FloatingPoint.get_numeral_sign ctx fp in
           (* true => biased exponent *)
           let _, exponent =
-            FloatingPoint.get_numeral_exponent_int ctx fp true
+            Z3.FloatingPoint.get_numeral_exponent_int ctx fp true
           in
           let _, significand =
-            FloatingPoint.get_numeral_significand_uint ctx fp
+            Z3.FloatingPoint.get_numeral_significand_uint ctx fp
           in
           let fp_bits =
             Int64.(
@@ -159,248 +157,250 @@ module M = struct
     end
 
     module Int = struct
-      let neg e = Arithmetic.mk_unary_minus ctx e
+      let neg e = Z3.Arithmetic.mk_unary_minus ctx e
 
-      let to_real e = Arithmetic.Integer.mk_int2real ctx e
+      let to_real e = Z3.Arithmetic.Integer.mk_int2real ctx e
 
-      let add e1 e2 = Arithmetic.mk_add ctx [ e1; e2 ]
+      let add e1 e2 = Z3.Arithmetic.mk_add ctx [ e1; e2 ]
 
-      let sub e1 e2 = Arithmetic.mk_sub ctx [ e1; e2 ]
+      let sub e1 e2 = Z3.Arithmetic.mk_sub ctx [ e1; e2 ]
 
-      let mul e1 e2 = Arithmetic.mk_mul ctx [ e1; e2 ]
+      let mul e1 e2 = Z3.Arithmetic.mk_mul ctx [ e1; e2 ]
 
-      let div e1 e2 = Arithmetic.mk_div ctx e1 e2
+      let div e1 e2 = Z3.Arithmetic.mk_div ctx e1 e2
 
-      let rem e1 e2 = Arithmetic.Integer.mk_rem ctx e1 e2
+      let rem e1 e2 = Z3.Arithmetic.Integer.mk_rem ctx e1 e2
 
-      let pow e1 e2 = Arithmetic.mk_power ctx e1 e2
+      let pow e1 e2 = Z3.Arithmetic.mk_power ctx e1 e2
 
-      let lt e1 e2 = Arithmetic.mk_lt ctx e1 e2
+      let lt e1 e2 = Z3.Arithmetic.mk_lt ctx e1 e2
 
-      let le e1 e2 = Arithmetic.mk_le ctx e1 e2
+      let le e1 e2 = Z3.Arithmetic.mk_le ctx e1 e2
 
-      let gt e1 e2 = Arithmetic.mk_gt ctx e1 e2
+      let gt e1 e2 = Z3.Arithmetic.mk_gt ctx e1 e2
 
-      let ge e1 e2 = Arithmetic.mk_ge ctx e1 e2
+      let ge e1 e2 = Z3.Arithmetic.mk_ge ctx e1 e2
     end
 
     module Real = struct
-      let neg e = Arithmetic.mk_unary_minus ctx e
+      let neg e = Z3.Arithmetic.mk_unary_minus ctx e
 
-      let to_int e = Arithmetic.Real.mk_real2int ctx e
+      let to_int e = Z3.Arithmetic.Real.mk_real2int ctx e
 
-      let add e1 e2 = Arithmetic.mk_add ctx [ e1; e2 ]
+      let add e1 e2 = Z3.Arithmetic.mk_add ctx [ e1; e2 ]
 
-      let sub e1 e2 = Arithmetic.mk_sub ctx [ e1; e2 ]
+      let sub e1 e2 = Z3.Arithmetic.mk_sub ctx [ e1; e2 ]
 
-      let mul e1 e2 = Arithmetic.mk_mul ctx [ e1; e2 ]
+      let mul e1 e2 = Z3.Arithmetic.mk_mul ctx [ e1; e2 ]
 
-      let div e1 e2 = Arithmetic.mk_div ctx e1 e2
+      let div e1 e2 = Z3.Arithmetic.mk_div ctx e1 e2
 
-      let pow e1 e2 = Arithmetic.mk_power ctx e1 e2
+      let pow e1 e2 = Z3.Arithmetic.mk_power ctx e1 e2
 
-      let lt e1 e2 = Arithmetic.mk_lt ctx e1 e2
+      let lt e1 e2 = Z3.Arithmetic.mk_lt ctx e1 e2
 
-      let le e1 e2 = Arithmetic.mk_le ctx e1 e2
+      let le e1 e2 = Z3.Arithmetic.mk_le ctx e1 e2
 
-      let gt e1 e2 = Arithmetic.mk_gt ctx e1 e2
+      let gt e1 e2 = Z3.Arithmetic.mk_gt ctx e1 e2
 
-      let ge e1 e2 = Arithmetic.mk_ge ctx e1 e2
+      let ge e1 e2 = Z3.Arithmetic.mk_ge ctx e1 e2
     end
 
     module String = struct
-      let v s = Seq.mk_string ctx s
+      let v s = Z3.Seq.mk_string ctx s
 
-      let length e = Seq.mk_seq_length ctx e
+      let length e = Z3.Seq.mk_seq_length ctx e
 
-      let to_code e = Seq.mk_string_to_code ctx e
+      let to_code e = Z3.Seq.mk_string_to_code ctx e
 
-      let of_code e = Seq.mk_string_from_code ctx e
+      let of_code e = Z3.Seq.mk_string_from_code ctx e
 
-      let to_int e = Seq.mk_str_to_int ctx e
+      let to_int e = Z3.Seq.mk_str_to_int ctx e
 
-      let of_int e = Seq.mk_int_to_str ctx e
+      let of_int e = Z3.Seq.mk_int_to_str ctx e
 
-      let at str ~pos = Seq.mk_seq_at ctx str pos
+      let at str ~pos = Z3.Seq.mk_seq_at ctx str pos
 
-      let concat es = Seq.mk_seq_concat ctx es
+      let concat es = Z3.Seq.mk_seq_concat ctx es
 
-      let is_prefix e1 ~prefix = Seq.mk_seq_prefix ctx e1 prefix
+      let is_prefix e1 ~prefix = Z3.Seq.mk_seq_prefix ctx e1 prefix
 
-      let is_suffix e1 ~suffix = Seq.mk_seq_suffix ctx e1 suffix
+      let is_suffix e1 ~suffix = Z3.Seq.mk_seq_suffix ctx e1 suffix
 
-      let lt a b = Seq.mk_str_lt ctx a b
+      let lt a b = Z3.Seq.mk_str_lt ctx a b
 
-      let le a b = Seq.mk_str_le ctx a b
+      let le a b = Z3.Seq.mk_str_le ctx a b
 
-      let contains e1 ~sub = Seq.mk_seq_contains ctx e1 sub
+      let contains e1 ~sub = Z3.Seq.mk_seq_contains ctx e1 sub
 
-      let sub str ~pos ~len = Seq.mk_seq_extract ctx str pos len
+      let sub str ~pos ~len = Z3.Seq.mk_seq_extract ctx str pos len
 
-      let index_of e1 ~sub ~pos = Seq.mk_seq_index ctx e1 sub pos
+      let index_of e1 ~sub ~pos = Z3.Seq.mk_seq_index ctx e1 sub pos
 
-      let replace e1 ~pattern ~with_ = Seq.mk_seq_replace ctx e1 pattern with_
+      let replace e1 ~pattern ~with_ =
+        Z3.Seq.mk_seq_replace ctx e1 pattern with_
     end
 
     module Bitv = struct
-      let v bv bitwidth = BitVector.mk_numeral ctx bv bitwidth
+      let v bv bitwidth = Z3.BitVector.mk_numeral ctx bv bitwidth
 
-      let neg e = BitVector.mk_neg ctx e
+      let neg e = Z3.BitVector.mk_neg ctx e
 
-      let lognot e = BitVector.mk_not ctx e
+      let lognot e = Z3.BitVector.mk_not ctx e
 
-      let add e1 e2 = BitVector.mk_add ctx e1 e2
+      let add e1 e2 = Z3.BitVector.mk_add ctx e1 e2
 
-      let sub e1 e2 = BitVector.mk_sub ctx e1 e2
+      let sub e1 e2 = Z3.BitVector.mk_sub ctx e1 e2
 
-      let mul e1 e2 = BitVector.mk_mul ctx e1 e2
+      let mul e1 e2 = Z3.BitVector.mk_mul ctx e1 e2
 
-      let div e1 e2 = BitVector.mk_sdiv ctx e1 e2
+      let div e1 e2 = Z3.BitVector.mk_sdiv ctx e1 e2
 
-      let div_u e1 e2 = BitVector.mk_udiv ctx e1 e2
+      let div_u e1 e2 = Z3.BitVector.mk_udiv ctx e1 e2
 
-      let logor e1 e2 = BitVector.mk_or ctx e1 e2
+      let logor e1 e2 = Z3.BitVector.mk_or ctx e1 e2
 
-      let logand e1 e2 = BitVector.mk_and ctx e1 e2
+      let logand e1 e2 = Z3.BitVector.mk_and ctx e1 e2
 
-      let logxor e1 e2 = BitVector.mk_xor ctx e1 e2
+      let logxor e1 e2 = Z3.BitVector.mk_xor ctx e1 e2
 
-      let shl e1 e2 = BitVector.mk_shl ctx e1 e2
+      let shl e1 e2 = Z3.BitVector.mk_shl ctx e1 e2
 
-      let ashr e1 e2 = BitVector.mk_ashr ctx e1 e2
+      let ashr e1 e2 = Z3.BitVector.mk_ashr ctx e1 e2
 
-      let lshr e1 e2 = BitVector.mk_lshr ctx e1 e2
+      let lshr e1 e2 = Z3.BitVector.mk_lshr ctx e1 e2
 
-      let rem e1 e2 = BitVector.mk_srem ctx e1 e2
+      let rem e1 e2 = Z3.BitVector.mk_srem ctx e1 e2
 
-      let rem_u e1 e2 = BitVector.mk_urem ctx e1 e2
+      let rem_u e1 e2 = Z3.BitVector.mk_urem ctx e1 e2
 
-      let rotate_left e1 e2 = BitVector.mk_ext_rotate_left ctx e1 e2
+      let rotate_left e1 e2 = Z3.BitVector.mk_ext_rotate_left ctx e1 e2
 
-      let rotate_right e1 e2 = BitVector.mk_ext_rotate_right ctx e1 e2
+      let rotate_right e1 e2 = Z3.BitVector.mk_ext_rotate_right ctx e1 e2
 
-      let lt e1 e2 = BitVector.mk_slt ctx e1 e2
+      let lt e1 e2 = Z3.BitVector.mk_slt ctx e1 e2
 
-      let lt_u e1 e2 = BitVector.mk_ult ctx e1 e2
+      let lt_u e1 e2 = Z3.BitVector.mk_ult ctx e1 e2
 
-      let le e1 e2 = BitVector.mk_sle ctx e1 e2
+      let le e1 e2 = Z3.BitVector.mk_sle ctx e1 e2
 
-      let le_u e1 e2 = BitVector.mk_ule ctx e1 e2
+      let le_u e1 e2 = Z3.BitVector.mk_ule ctx e1 e2
 
-      let gt e1 e2 = BitVector.mk_sgt ctx e1 e2
+      let gt e1 e2 = Z3.BitVector.mk_sgt ctx e1 e2
 
-      let gt_u e1 e2 = BitVector.mk_ugt ctx e1 e2
+      let gt_u e1 e2 = Z3.BitVector.mk_ugt ctx e1 e2
 
-      let ge e1 e2 = BitVector.mk_sge ctx e1 e2
+      let ge e1 e2 = Z3.BitVector.mk_sge ctx e1 e2
 
-      let ge_u e1 e2 = BitVector.mk_uge ctx e1 e2
+      let ge_u e1 e2 = Z3.BitVector.mk_uge ctx e1 e2
 
-      let concat e1 e2 = BitVector.mk_concat ctx e1 e2
+      let concat e1 e2 = Z3.BitVector.mk_concat ctx e1 e2
 
-      let extract e ~high ~low = BitVector.mk_extract ctx high low e
+      let extract e ~high ~low = Z3.BitVector.mk_extract ctx high low e
 
-      let zero_extend n e = BitVector.mk_zero_ext ctx n e
+      let zero_extend n e = Z3.BitVector.mk_zero_ext ctx n e
 
-      let sign_extend n e = BitVector.mk_sign_ext ctx n e
+      let sign_extend n e = Z3.BitVector.mk_sign_ext ctx n e
     end
 
     module Float = struct
       module Rounding_mode = struct
-        let rne = FloatingPoint.RoundingMode.mk_rne ctx
+        let rne = Z3.FloatingPoint.RoundingMode.mk_rne ctx
 
-        let rna = FloatingPoint.RoundingMode.mk_rna ctx
+        let rna = Z3.FloatingPoint.RoundingMode.mk_rna ctx
 
-        let rtp = FloatingPoint.RoundingMode.mk_rtp ctx
+        let rtp = Z3.FloatingPoint.RoundingMode.mk_rtp ctx
 
-        let rtn = FloatingPoint.RoundingMode.mk_rtn ctx
+        let rtn = Z3.FloatingPoint.RoundingMode.mk_rtn ctx
 
-        let rtz = FloatingPoint.RoundingMode.mk_rtz ctx
+        let rtz = Z3.FloatingPoint.RoundingMode.mk_rtz ctx
       end
 
-      let v f eb sb = FloatingPoint.mk_numeral_f ctx f (Types.float eb sb)
+      let v f eb sb = Z3.FloatingPoint.mk_numeral_f ctx f (Types.float eb sb)
 
-      let neg e = FloatingPoint.mk_neg ctx e
+      let neg e = Z3.FloatingPoint.mk_neg ctx e
 
-      let abs e = FloatingPoint.mk_abs ctx e
+      let abs e = Z3.FloatingPoint.mk_abs ctx e
 
-      let sqrt ~rm e = FloatingPoint.mk_sqrt ctx rm e
+      let sqrt ~rm e = Z3.FloatingPoint.mk_sqrt ctx rm e
 
-      let is_nan e = FloatingPoint.mk_is_nan ctx e
+      let is_nan e = Z3.FloatingPoint.mk_is_nan ctx e
 
-      let round_to_integral ~rm e = FloatingPoint.mk_round_to_integral ctx rm e
+      let round_to_integral ~rm e =
+        Z3.FloatingPoint.mk_round_to_integral ctx rm e
 
-      let add ~rm e1 e2 = FloatingPoint.mk_add ctx rm e1 e2
+      let add ~rm e1 e2 = Z3.FloatingPoint.mk_add ctx rm e1 e2
 
-      let sub ~rm e1 e2 = FloatingPoint.mk_sub ctx rm e1 e2
+      let sub ~rm e1 e2 = Z3.FloatingPoint.mk_sub ctx rm e1 e2
 
-      let mul ~rm e1 e2 = FloatingPoint.mk_mul ctx rm e1 e2
+      let mul ~rm e1 e2 = Z3.FloatingPoint.mk_mul ctx rm e1 e2
 
-      let div ~rm e1 e2 = FloatingPoint.mk_div ctx rm e1 e2
+      let div ~rm e1 e2 = Z3.FloatingPoint.mk_div ctx rm e1 e2
 
-      let min e1 e2 = FloatingPoint.mk_min ctx e1 e2
+      let min e1 e2 = Z3.FloatingPoint.mk_min ctx e1 e2
 
-      let max e1 e2 = FloatingPoint.mk_max ctx e1 e2
+      let max e1 e2 = Z3.FloatingPoint.mk_max ctx e1 e2
 
-      let rem e1 e2 = FloatingPoint.mk_rem ctx e1 e2
+      let rem e1 e2 = Z3.FloatingPoint.mk_rem ctx e1 e2
 
-      let eq e1 e2 = FloatingPoint.mk_eq ctx e1 e2
+      let eq e1 e2 = Z3.FloatingPoint.mk_eq ctx e1 e2
 
-      let lt e1 e2 = FloatingPoint.mk_lt ctx e1 e2
+      let lt e1 e2 = Z3.FloatingPoint.mk_lt ctx e1 e2
 
-      let le e1 e2 = FloatingPoint.mk_leq ctx e1 e2
+      let le e1 e2 = Z3.FloatingPoint.mk_leq ctx e1 e2
 
-      let gt e1 e2 = FloatingPoint.mk_gt ctx e1 e2
+      let gt e1 e2 = Z3.FloatingPoint.mk_gt ctx e1 e2
 
-      let ge e1 e2 = FloatingPoint.mk_geq ctx e1 e2
+      let ge e1 e2 = Z3.FloatingPoint.mk_geq ctx e1 e2
 
       let to_fp eb sb ~rm fp =
-        FloatingPoint.mk_to_fp_float ctx rm fp (Types.float eb sb)
+        Z3.FloatingPoint.mk_to_fp_float ctx rm fp (Types.float eb sb)
 
       let sbv_to_fp eb sb ~rm bv =
-        FloatingPoint.mk_to_fp_signed ctx rm bv (Types.float eb sb)
+        Z3.FloatingPoint.mk_to_fp_signed ctx rm bv (Types.float eb sb)
 
       let ubv_to_fp eb sb ~rm bv =
-        FloatingPoint.mk_to_fp_unsigned ctx rm bv (Types.float eb sb)
+        Z3.FloatingPoint.mk_to_fp_unsigned ctx rm bv (Types.float eb sb)
 
-      let to_ubv n ~rm fp = FloatingPoint.mk_to_ubv ctx rm fp n
+      let to_ubv n ~rm fp = Z3.FloatingPoint.mk_to_ubv ctx rm fp n
 
-      let to_sbv n ~rm fp = FloatingPoint.mk_to_sbv ctx rm fp n
+      let to_sbv n ~rm fp = Z3.FloatingPoint.mk_to_sbv ctx rm fp n
 
       let of_ieee_bv eb sb bv =
-        FloatingPoint.mk_to_fp_bv ctx bv (Types.float eb sb)
+        Z3.FloatingPoint.mk_to_fp_bv ctx bv (Types.float eb sb)
 
-      let to_ieee_bv fp = FloatingPoint.mk_to_ieee_bv ctx fp
+      let to_ieee_bv fp = Z3.FloatingPoint.mk_to_ieee_bv ctx fp
     end
 
     module Func = struct
-      let make name params ret = FuncDecl.mk_func_decl_s ctx name params ret
+      let make name params ret = Z3.FuncDecl.mk_func_decl_s ctx name params ret
 
-      let apply f params = FuncDecl.apply f params
+      let apply f params = Z3.FuncDecl.apply f params
     end
 
     module Model = struct
       let get_symbols model =
         List.map
           (fun const ->
-            let x = Symbol.to_string (FuncDecl.get_name const) in
-            let t = Types.to_ety (FuncDecl.get_range const) in
-            Sym.make t x )
-          (Model.get_const_decls model)
+            let x = Z3.Symbol.to_string (Z3.FuncDecl.get_name const) in
+            let t = Types.to_ety (Z3.FuncDecl.get_range const) in
+            Symbol.make t x )
+          (Z3.Model.get_const_decls model)
 
       let eval ?(completion = false) model term =
-        Model.eval model term completion
+        Z3.Model.eval model term completion
     end
 
-    let pp_entry fmt (entry : Statistics.Entry.statistics_entry) =
-      let key = Statistics.Entry.get_key entry in
-      let value = Statistics.Entry.to_string_value entry in
+    let pp_entry fmt (entry : Z3.Statistics.Entry.statistics_entry) =
+      let key = Z3.Statistics.Entry.get_key entry in
+      let value = Z3.Statistics.Entry.to_string_value entry in
       Fmt.pf fmt "(%s %s)" key value
 
-    let pp_statistics fmt (stats : Statistics.statistics) =
-      let entries = Statistics.get_entries stats in
+    let pp_statistics fmt (stats : Z3.Statistics.statistics) =
+      let entries = Z3.Statistics.get_entries stats in
       Fmt.list ~sep:(fun fmt () -> Fmt.pf fmt "@\n") pp_entry fmt entries
 
-    let get_statistics (stats : Statistics.statistics) =
+    let get_statistics (stats : Z3.Statistics.statistics) =
       let statistics = Z3.Statistics.get_entries stats in
       let add_entry map entry =
         let key = Z3.Statistics.Entry.get_key entry in
@@ -412,19 +412,19 @@ module M = struct
             `Float (Z3.Statistics.Entry.get_float entry)
           end
         in
-        Stats.Map.add key value map
+        Statistics.Map.add key value map
       in
-      List.fold_left add_entry Stats.Map.empty statistics
+      List.fold_left add_entry Statistics.Map.empty statistics
 
-    let set_params (params : P.t) =
+    let set_params (params : Params.t) =
       Z3.set_global_param "smt.ematching"
-        (string_of_bool @@ P.get params Ematching);
+        (string_of_bool @@ Params.get params Ematching);
       Z3.Params.update_param_value ctx "timeout"
-        (string_of_int @@ P.get params Timeout);
+        (string_of_int @@ Params.get params Timeout);
       Z3.Params.update_param_value ctx "model"
-        (string_of_bool @@ P.get params Model);
+        (string_of_bool @@ Params.get params Model);
       Z3.Params.update_param_value ctx "unsat_core"
-        (string_of_bool @@ P.get params Unsat_core)
+        (string_of_bool @@ Params.get params Unsat_core)
 
     module Solver = struct
       (* TODO: parameters *)
@@ -437,71 +437,71 @@ module M = struct
         in
         Z3.Solver.mk_solver ctx logic
 
-      let clone solver = Solver.translate solver ctx
+      let clone solver = Z3.Solver.translate solver ctx
 
-      let push solver = Solver.push solver
+      let push solver = Z3.Solver.push solver
 
-      let pop solver n = Solver.pop solver n
+      let pop solver n = Z3.Solver.pop solver n
 
-      let reset solver = Solver.reset solver
+      let reset solver = Z3.Solver.reset solver
 
-      let add solver terms = Solver.add solver terms
+      let add solver terms = Z3.Solver.add solver terms
 
       let check solver ~assumptions =
-        match Solver.check solver assumptions with
-        | Solver.UNKNOWN -> `Unknown
-        | Solver.SATISFIABLE -> `Sat
-        | Solver.UNSATISFIABLE -> `Unsat
+        match Z3.Solver.check solver assumptions with
+        | Z3.Solver.UNKNOWN -> `Unknown
+        | Z3.Solver.SATISFIABLE -> `Sat
+        | Z3.Solver.UNSATISFIABLE -> `Unsat
 
-      let model solver = Solver.get_model solver
+      let model solver = Z3.Solver.get_model solver
 
       let add_simplifier solver =
-        let simplify = Simplifier.mk_simplifier ctx "simplify" in
-        let solver_eqs = Simplifier.mk_simplifier ctx "solve-eqs" in
+        let simplify = Z3.Simplifier.mk_simplifier ctx "simplify" in
+        let solver_eqs = Z3.Simplifier.mk_simplifier ctx "solve-eqs" in
         let then_ =
           List.map
-            (Simplifier.mk_simplifier ctx)
+            (Z3.Simplifier.mk_simplifier ctx)
             [ "elim-unconstrained"; "propagate-values"; "simplify" ]
         in
-        Simplifier.and_then ctx simplify solver_eqs then_
-        |> Solver.add_simplifier ctx solver
+        Z3.Simplifier.and_then ctx simplify solver_eqs then_
+        |> Z3.Solver.add_simplifier ctx solver
 
-      let interrupt () = Tactic.interrupt ctx
+      let interrupt () = Z3.Tactic.interrupt ctx
 
       let get_statistics solver =
         get_statistics (Z3.Solver.get_statistics solver)
 
       let pp_statistics fmt solver =
-        pp_statistics fmt @@ Solver.get_statistics solver
+        pp_statistics fmt @@ Z3.Solver.get_statistics solver
     end
 
     module Optimizer = struct
-      let make () = Optimize.mk_opt ctx
+      let make () = Z3.Optimize.mk_opt ctx
 
-      let push opt = Optimize.push opt
+      let push opt = Z3.Optimize.push opt
 
-      let pop opt = Optimize.pop opt
+      let pop opt = Z3.Optimize.pop opt
 
-      let add opt terms = Optimize.add opt terms
+      let add opt terms = Z3.Optimize.add opt terms
 
       let check opt =
-        match Optimize.check opt with
+        match Z3.Optimize.check opt with
         | Z3.Solver.UNKNOWN -> `Unknown
         | Z3.Solver.SATISFIABLE -> `Sat
         | Z3.Solver.UNSATISFIABLE -> `Unsat
 
-      let model opt = Optimize.get_model opt
+      let model opt = Z3.Optimize.get_model opt
 
-      let maximize opt term = Optimize.maximize opt term
+      let maximize opt term = Z3.Optimize.maximize opt term
 
-      let minimize opt term = Optimize.minimize opt term
+      let minimize opt term = Z3.Optimize.minimize opt term
 
-      let interrupt () = Tactic.interrupt ctx
+      let interrupt () = Z3.Tactic.interrupt ctx
 
-      let get_statistics opt = get_statistics (Optimize.get_statistics opt)
+      let get_statistics opt = get_statistics (Z3.Optimize.get_statistics opt)
 
       let pp_statistics fmt opt =
-        pp_statistics fmt @@ Optimize.get_statistics opt
+        pp_statistics fmt @@ Z3.Optimize.get_statistics opt
     end
 
     module Smtlib = struct