From 2befa3b66c9e566ff8ed95fcb35fb4ca279d8e48 Mon Sep 17 00:00:00 2001
From: Pierre Villemot <tiky.halbaroth@gmail.com>
Date: Mon, 24 Jul 2023 17:33:04 +0200
Subject: [PATCH] Temporary fix

---
 src/lib/frontend/d_cnf.ml | 19 ++++++++++++++++++-
 1 file changed, 18 insertions(+), 1 deletion(-)

diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml
index e36c682cf1..e18f11a09a 100644
--- a/src/lib/frontend/d_cnf.ml
+++ b/src/lib/frontend/d_cnf.ml
@@ -1080,7 +1080,24 @@ let rec mk_expr
             semantic_trigger ~loc ?var trigger
 
           (* Unary functions from FixedSizeBitVectors theory *)
-          | B.Bitv_extract { i; j; _ }, [ x ] -> E.BV.extract i j (mk x)
+          | 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. *)
+              match E.type_info t with
+              | Tbitv m ->
+                if m <= i then
+                  Util.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_not _, [ x ] -> E.BV.bvnot (mk x)
           | B.Bitv_neg _, [ x ] -> E.BV.bvneg (mk x)