diff --git a/alt-ergo-lib.opam b/alt-ergo-lib.opam
index a1f4a97c48..aa63956fe3 100644
--- a/alt-ergo-lib.opam
+++ b/alt-ergo-lib.opam
@@ -59,3 +59,18 @@ license: [
   "LicenseRef-OCamlpro-Non-Commercial"
   "Apache-2.0"
 ]
+
+pin-depends: [
+  [
+  "dolmen.dev"
+  "git+https://github.com/Gbury/dolmen.git#8e6887481019978c2ad5be762540c09dc8bc619b"
+  ]
+  [
+  "dolmen_loop.dev"
+  "git+https://github.com/Gbury/dolmen.git#8e6887481019978c2ad5be762540c09dc8bc619b"
+  ]
+  [
+  "dolmen_type.dev"
+  "git+https://github.com/Gbury/dolmen.git#8e6887481019978c2ad5be762540c09dc8bc619b"
+  ]
+]
diff --git a/alt-ergo-lib.opam.locked b/alt-ergo-lib.opam.locked
index f6a052ac85..5860c83b89 100644
--- a/alt-ergo-lib.opam.locked
+++ b/alt-ergo-lib.opam.locked
@@ -8,8 +8,8 @@ This is the core library used in the Alt-Ergo SMT solver.
 Alt-Ergo is an automatic theorem prover of mathematical formulas. It was developed at LRI, and is now maintained at OCamlPro.
 
 See more details on http://alt-ergo.ocamlpro.com/"""
-maintainer: "Alt-Ergo developers"
-authors: "Alt-Ergo developers"
+maintainer: "Alt-Ergo developers <alt-ergo@ocamlpro.com>"
+authors: "Alt-Ergo developers <alt-ergo@ocamlpro.com>"
 license: ["LicenseRef-OCamlpro-Non-Commercial" "Apache-2.0"]
 tags: "org:OCamlPro"
 homepage: "https://alt-ergo.ocamlpro.com/"
@@ -17,7 +17,6 @@ doc: "https://ocamlpro.github.io/alt-ergo"
 bug-reports: "https://github.com/OCamlPro/alt-ergo/issues"
 depends: [
   "base-bigarray" {= "base"}
-  "base-bytes" {= "base"}
   "base-threads" {= "base"}
   "base-unix" {= "base"}
   "camlzip" {= "1.11"}
@@ -26,19 +25,14 @@ depends: [
   "conf-pkg-config" {= "3"}
   "conf-zlib" {= "1"}
   "cppo" {= "1.6.9"}
-  "csexp" {= "1.5.2"}
-  "dolmen" {= "0.9"}
-  "dolmen_loop" {= "0.9"}
-  "dolmen_type" {= "0.9"}
+  "dolmen" {= "dev"}
+  "dolmen_loop" {= "dev"}
+  "dolmen_type" {= "dev"}
   "dune" {= "3.10.0"}
   "dune-build-info" {= "3.10.0"}
-  "dune-configurator" {= "3.10.0"}
   "fmt" {= "0.9.0"}
   "gen" {= "1.1"}
-  "js_of_ocaml" {= "5.4.0"}
-  "js_of_ocaml-compiler" {= "5.4.0"}
   "logs" {= "0.7.0"}
-  "lwt" {= "5.6.1"}
   "menhir" {= "20230608"}
   "menhirLib" {= "20230608"}
   "menhirSdk" {= "20230608"}
@@ -46,20 +40,19 @@ depends: [
   "ocaml-compiler-libs" {= "v0.12.4"}
   "ocamlbuild" {= "0.14.2"}
   "ocamlfind" {= "1.9.6"}
-  "ocplib-endian" {= "1.2"}
   "ocplib-simplex" {= "0.5"}
   "pp_loc" {= "2.1.0"}
   "ppx_blob" {= "0.7.2"}
   "ppx_derivers" {= "1.2.1"}
+  "ppx_deriving" {= "5.2.1"}
   "ppxlib" {= "0.30.0"}
-  "sedlex" {= "3.2"}
+  "result" {= "1.5"}
   "seq" {= "base"}
-  "sexplib0" {= "v0.15.1"}
+  "sexplib0" {= "v0.16.0"}
   "spelll" {= "0.4"}
   "stdlib-shims" {= "0.3.0"}
   "topkg" {= "1.0.7"}
   "uutf" {= "1.0.3"}
-  "yojson" {= "2.1.0"}
   "zarith" {= "1.13"}
 ]
 build: [
@@ -78,4 +71,22 @@ build: [
   ]
   ["dune" "install" "-p" name "--create-install-files" name]
 ]
-dev-repo: "git+https://github.com/OCamlPro/alt-ergo.git"
\ No newline at end of file
+dev-repo: "git+https://github.com/OCamlPro/alt-ergo.git"
+conflicts: [
+  "ppxlib" {< "0.30.0"}
+  "result" {< "1.5"}
+]
+pin-depends: [
+  [
+    "dolmen.dev"
+    "git+https://github.com/Gbury/dolmen.git#7c7050bda83a86da7d81c088e4e5eba3cc58b948"
+  ]
+  [
+    "dolmen_loop.dev"
+    "git+https://github.com/Gbury/dolmen.git#7c7050bda83a86da7d81c088e4e5eba3cc58b948"
+  ]
+  [
+    "dolmen_type.dev"
+    "git+https://github.com/Gbury/dolmen.git#7c7050bda83a86da7d81c088e4e5eba3cc58b948"
+  ]
+]
\ No newline at end of file
diff --git a/alt-ergo-lib.opam.template b/alt-ergo-lib.opam.template
index cde1fa1b89..223c1b6b93 100644
--- a/alt-ergo-lib.opam.template
+++ b/alt-ergo-lib.opam.template
@@ -6,3 +6,18 @@ license: [
   "LicenseRef-OCamlpro-Non-Commercial"
   "Apache-2.0"
 ]
+
+pin-depends: [
+  [
+  "dolmen.dev"
+  "git+https://github.com/Gbury/dolmen.git#8e6887481019978c2ad5be762540c09dc8bc619b"
+  ]
+  [
+  "dolmen_loop.dev"
+  "git+https://github.com/Gbury/dolmen.git#8e6887481019978c2ad5be762540c09dc8bc619b"
+  ]
+  [
+  "dolmen_type.dev"
+  "git+https://github.com/Gbury/dolmen.git#8e6887481019978c2ad5be762540c09dc8bc619b"
+  ]
+]
diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml
index 7ab12cb451..95ab994900 100644
--- a/src/lib/frontend/d_cnf.ml
+++ b/src/lib/frontend/d_cnf.ml
@@ -193,24 +193,17 @@ type _ DStd.Builtin.t +=
   (* Internal use for semantic triggers -- do not expose outside of theories *)
   | Not_theory_constant | Is_theory_constant | Linear_dependency
 
-let with_cache ~cache f x =
-  try Hashtbl.find cache x
-  with Not_found ->
-    let res = f x in
-    Hashtbl.add cache x res;
-    res
-
 module Const = struct
   open DE
 
   let bv2nat =
-    with_cache ~cache:(Hashtbl.create 13) (fun n ->
+    with_cache (fun n ->
         let name = "bv2nat" in
         Id.mk ~name ~builtin:(BV2Nat n)
           (DStd.Path.global name) Ty.(arrow [bitv n] int))
 
   let int2bv =
-    with_cache ~cache:(Hashtbl.create 13) (fun n ->
+    with_cache (fun n ->
         let name = "int2bv" in
         Id.mk ~name ~builtin:(Int2BV n)
           (DStd.Path.global name) Ty.(arrow [int] (bitv n)))