Fix infinite loop: bv2nat has type int

OCamlPro · Jul 12, 2023 · be3da73 · be3da73
1 parent df14d0f
commit be3da73
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml
@@ -2958,7 +2958,8 @@ module BV = struct
     (* Note: arith.ml calls [int2bv] in [make]. If additional simplifications
        are added here, arith.ml must be updated as well. *)
     match term_view t with
-    | { f = Op BV2Nat; xs = [ t ]; ty = Tbitv m; _ } ->
+    | { f = Op BV2Nat; xs = [ t ]; _ } ->
+      let m = match type_info t with Tbitv m -> m | _ -> assert false in
       if m > n then
         extract (n - 1) 0 t
       else