Also remove impossible if-branches

2 files changed, 11 insertions, 2 deletions

diff --git a/src/constant_propagation.ml b/src/constant_propagation.ml
index c3e00753..d0b524ed 100644
--- a/src/constant_propagation.ml
+++ b/src/constant_propagation.ml
@@ -860,9 +860,17 @@ let remove_impossible_int_cases _ =
       | _ -> true
     in aux exp p
   in
-  let rewrite_e_case (exp,cases) =
+  let e_case (exp,cases) =
     E_case (exp, List.filter (must_keep_case exp) cases)
   in
+  let e_if (cond, e_then, e_else) =
+    match destruct_atom_bool (env_of cond) (typ_of cond) with
+    | Some nc ->
+       if prove __POS__ (Env.add_constraint nc (env_of cond)) nc_false
+       then unaux_exp e_else
+       else E_if (cond, e_then, e_else)
+    | _ -> E_if (cond, e_then, e_else)
+  in
   let open Rewriter in
-  let rewrite_exp _ = fold_exp { id_exp_alg with e_case = rewrite_e_case } in
+  let rewrite_exp _ = fold_exp { id_exp_alg with e_case = e_case; e_if = e_if } in
   rewrite_defs_base { rewriters_base with rewrite_exp = rewrite_exp }
diff --git a/src/rewrites.ml b/src/rewrites.ml
index d9bcec04..f6a004b3 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -5077,6 +5077,7 @@ let rewrite_defs_lem = [
   ("rewrite_undefined", rewrite_undefined_if_gen false);
   ("rewrite_defs_vector_string_pats_to_bit_list", rewrite_defs_vector_string_pats_to_bit_list);
   ("remove_not_pats", rewrite_defs_not_pats);
+  ("remove_impossible_int_cases", Constant_propagation.remove_impossible_int_cases);
   ("pat_lits", rewrite_defs_pat_lits rewrite_lit_lem);
   ("vector_concat_assignments", rewrite_vector_concat_assignments);
   ("tuple_assignments", rewrite_tuple_assignments);