From a17b95acc772f3dd4be1e97f96c071a5addddbb2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 30 Sep 2018 08:25:06 -0700 Subject: [PATCH] feat(library/compiler/erase_irrelevant): add support for lc_unreachable --- src/library/compiler/erase_irrelevant.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/library/compiler/erase_irrelevant.cpp b/src/library/compiler/erase_irrelevant.cpp index db5b88d2a6..10196920e4 100644 --- a/src/library/compiler/erase_irrelevant.cpp +++ b/src/library/compiler/erase_irrelevant.cpp @@ -82,6 +82,8 @@ class erase_irrelevant_fn : public compiler_step_visitor { virtual expr visit_constant(expr const & e) override { if (is_comp_irrelevant(e)) { return *g_neutral_expr; + } else if (const_name(e) == get_lc_unreachable_name()) { + return *g_unreachable_expr; } else { /* Erase universe level information */ return mk_constant(const_name(e)); @@ -395,6 +397,8 @@ class erase_irrelevant_fn : public compiler_step_visitor { return visit_subtype_mk(args); } else if (n == get_subtype_val_name()) { return visit_subtype_val(args); + } else if (n == get_lc_unreachable_name()) { + return *g_unreachable_expr; } } return compiler_step_visitor::visit_app(e);