diff options
Diffstat (limited to 'src/rewrites.ml')
| -rw-r--r-- | src/rewrites.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/rewrites.ml b/src/rewrites.ml index b47650b7..5a70a721 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -4012,12 +4012,13 @@ let rewrite_defs_remove_superfluous_letbinds env = | _ -> E_aux (exp,annot) end | E_internal_plet (_, E_aux (E_throw e, a), _) -> E_aux (E_throw e, a) - | E_internal_plet (_, E_aux (E_assert (c, msg), a), _) -> + | E_internal_plet (pat, (E_aux (E_assert (c, msg), a) as assert_exp), _) -> begin match typ_of c with | Typ_aux (Typ_app (Id_aux (Id "atom_bool", _), [A_aux (A_bool nc, _)]), _) when prove __POS__ (env_of c) (nc_not nc) -> (* Drop rest of block after an 'assert(false)' *) - E_aux (E_exit (infer_exp (env_of c) (mk_lit_exp L_unit)), a) + let exit_exp = E_aux (E_exit (infer_exp (env_of c) (mk_lit_exp L_unit)), a) in + E_aux (E_internal_plet (pat, assert_exp, exit_exp), annot) | _ -> E_aux (exp, annot) end |