From 6672c1a94eceb900e70f3976f6ac58968cdb971e Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 24 Jul 2023 17:33:04 +0200 Subject: [PATCH 1/2] 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 e36c682cf..e18f11a09 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) From 66cb47b36ebacb6c27838238dd8a03858dfdc1f7 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Tue, 25 Jul 2023 11:04:31 +0200 Subject: [PATCH 2/2] Add link --- src/lib/frontend/d_cnf.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml index e18f11a09..d73fbcb5c 100644 --- a/src/lib/frontend/d_cnf.ml +++ b/src/lib/frontend/d_cnf.ml @@ -1087,7 +1087,8 @@ let rec mk_expr 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. *) + 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