From ecc9014d82662bf81a0b17fcb07db1a666e61ca9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 11 May 2016 16:06:21 -0700 Subject: [PATCH] fix(library/compiler/simp_inductive): check ignore predicate at visit_constant --- src/library/compiler/simp_inductive.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/library/compiler/simp_inductive.cpp b/src/library/compiler/simp_inductive.cpp index 0a8f215185..44d5cd2eb2 100644 --- a/src/library/compiler/simp_inductive.cpp +++ b/src/library/compiler/simp_inductive.cpp @@ -176,7 +176,7 @@ class simp_inductive_fn : public compiler_step_visitor { virtual expr visit_constant(expr const & e) override { name const & n = const_name(e); - if (inductive::is_intro_rule(env(), n)) { + if (inductive::is_intro_rule(env(), n) && !ignore(n)) { return mk_cnstr(get_constructor_idx(env(), n)); } else { return e;