Bump the version of Dolmen to 0.10

The new version of Dolmen has been released yesterday! This commit updates the lock file and remove the hotfix for the issue OCamlPro#747 as the appropriate fix is included in the last release of Dolmen.
Halbaroth · Jun 18, 2024 · 5b641bf · 5b641bf
1 parent 2fc8d60
commit 5b641bf
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 35 deletions.
diff --git a/alt-ergo-lib.opam.locked b/alt-ergo-lib.opam.locked
@@ -27,9 +27,9 @@ depends: [
   "conf-zlib" {= "1"}
   "cppo" {= "1.6.9"}
   "csexp" {= "1.5.2"}
-  "dolmen" {= "dev"}
-  "dolmen_loop" {= "dev"}
-  "dolmen_type" {= "dev"}
+  "dolmen" {= "0.10"}
+  "dolmen_loop" {= "0.10"}
+  "dolmen_type" {= "0.10"}
   "dune" {= "3.11.1"}
   "dune-build-info" {= "3.11.1"}
   "dune-configurator" {= "3.11.1"}
@@ -84,19 +84,7 @@ conflicts: [
   "ppxlib" {< "0.30.0"}
   "result" {< "1.5"}
 ]
-pin-depends: [
-  [
-    "dolmen.dev"
-    "git+https://github.com/Gbury/dolmen.git#5e22e653ec376336bbbed50aca4946db8edbc90f"
-  ]
-  [
-    "dolmen_loop.dev"
-    "git+https://github.com/Gbury/dolmen.git#5e22e653ec376336bbbed50aca4946db8edbc90f"
-  ]
-  [
-    "dolmen_type.dev"
-    "git+https://github.com/Gbury/dolmen.git#5e22e653ec376336bbbed50aca4946db8edbc90f"
-  ]
+[
   [
     "js_of_ocaml.5.4.0"
     "https://github.com/ocsigen/js_of_ocaml/releases/download/5.4.0/js_of_ocaml-5.4.0.tbz"

diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml
@@ -1083,25 +1083,7 @@ let rec mk_expr
             semantic_trigger ~loc ?var trigger
 
           (* Unary functions from FixedSizeBitVectors theory *)
-          | B.Bitv_extract { i; j; _ }, [ x ] ->
-            let t = mk x in
-            let _ =
-              (* This temporary fix throws aways ill-typed expression produced
-                 by Dolmen 0.9. See issue
-                 https://github.com/Gbury/dolmen/issues/174.
-                 This code will be removed as soon as the next version of
-                 Dolmen has been released. See issue
-                 https://github.com/OCamlPro/alt-ergo/issues/748. *)
-              match E.type_info t with
-              | Tbitv m ->
-                if m <= i then
-                  Fmt.failwith
-                    "%alength of bitvector extraction exceeds the length\
-                     of its argument."
-                    Loc.report loc
-              | _ -> assert false
-            in
-            E.BV.extract i j t
+          | B.Bitv_extract { i; j; _ }, [ x ] -> E.BV.extract i j (mk x)
           | B.Bitv_not _, [ x ] -> E.BV.bvnot (mk x)
           | B.Bitv_neg _, [ x ] -> E.BV.bvneg (mk x)