From 91b59a2f12057d25aaa17e1ce05e18bba797d74e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 29 Oct 2018 14:41:12 -0700 Subject: [PATCH] fix(library/compiler/extract_closed): do not extract `is_enf_unreachable` --- src/library/compiler/extract_closed.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/library/compiler/extract_closed.cpp b/src/library/compiler/extract_closed.cpp index ad6d43b7a6..d47a26d1c9 100644 --- a/src/library/compiler/extract_closed.cpp +++ b/src/library/compiler/extract_closed.cpp @@ -235,7 +235,7 @@ class extract_closed_fn { expr mk_aux_constant(expr const & e0) { expr e = find(e0); - if (is_enf_neutral(e)) { + if (is_enf_neutral(e) || is_enf_unreachable(e)) { return e0; } if (is_constant(e) && arity_eq_0(const_name(e))) {