From 658460e3fc9a8c51ff81f48f6bb0db2db696ffbe Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 1 Sep 2023 14:14:21 +0100 Subject: [PATCH] Remove some unnecessary (and ill-typed) checks in bitvector cast addition These were benign (the Z3 errors were ignored), but undesirable. --- src/lib/monomorphise.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/lib/monomorphise.ml b/src/lib/monomorphise.ml index 111f9fc38..92994053f 100644 --- a/src/lib/monomorphise.ml +++ b/src/lib/monomorphise.ml @@ -4141,7 +4141,9 @@ module BitvectorSizeCasts = struct | exception _ -> insts ) in - let insts = KidSet.fold check_inst (tyvars_of_constraint nc) KBindings.empty in + let is_Int kid = match Env.get_typ_var kid env with K_int -> true | _ -> false in + let kids_to_check = KidSet.filter is_Int (tyvars_of_constraint nc) in + let insts = KidSet.fold check_inst kids_to_check KBindings.empty in if KBindings.is_empty insts then h :: aux t else begin (* Propagate new instantiations and insert casts *)