diff options
| -rw-r--r-- | src/nl_flow.ml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/nl_flow.ml b/src/nl_flow.ml index 24ef73fa..bf99f869 100644 --- a/src/nl_flow.ml +++ b/src/nl_flow.ml @@ -67,6 +67,11 @@ let rec returns (E_aux (aux, _)) = | E_block exps -> returns (List.hd (List.rev exps)) | _ -> false +let is_assert (E_aux (aux, _)) = + match aux with + | E_assert _ -> true + | _ -> false + let is_bitvector_literal (L_aux (aux, _)) = match aux with | L_bin _ | L_hex _ -> true @@ -120,7 +125,7 @@ let analyze' exps = | _ -> exps end | (E_aux (E_if (cond, then_exp, _), (l, _)) as exp) :: next :: rest - when returns then_exp -> + when returns then_exp && not (is_assert next) -> let msg = mk_lit_exp (L_string "") in let not_cond = locate (fun _ -> gen_loc l) (mk_exp (E_app (mk_id "not_bool", [cond]))) in let assertion = locate (fun _ -> gen_loc l) (mk_exp (E_assert (not_cond, msg))) in |