Hack to strip _Bool cast from assert refinement in base and relation

Author: sim642

src/analyses/baseInvariant.ml

@@ -855,6 +855,12 @@ struct
         inv_exp (Float ftv) exp st
 
   let invariant man st exp tv =
+    (* TODO: this cast should be supported generally somewhere above *)
+    let exp =
+      match exp with
+      | CastE (TInt (IBool, _), exp) -> exp
+      | exp -> exp
+    in
     (* The computations that happen here are not computations that happen in the programs *)
     (* Any overflow during the forward evaluation will already have been flagged here *)
     GobRef.wrap AnalysisState.executing_speculative_computations true

src/cdomains/apron/sharedFunctions.apron.ml

@@ -511,6 +511,12 @@ struct
 
   (** Assert any expression. *)
   let assert_inv ask d e negate no_ov =
+    (* TODO: this cast should be supported generally somewhere above? *)
+    let e =
+      match e with
+      | CastE (TInt (IBool, _), e) -> e
+      | e -> e
+    in
     let e' =
       if exp_is_constraint e then
         e