From cfb4d289b8b2e210c1bf6d4ae07dbefe193ea363 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 11 Jul 2019 10:34:35 +0100 Subject: [PATCH] fix #2325 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_recfun.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp index cc7ec0e36..d4f34f359 100644 --- a/src/smt/theory_recfun.cpp +++ b/src/smt/theory_recfun.cpp @@ -88,7 +88,11 @@ namespace smt { // the internalization of the arguments may have triggered the internalization of term. if (!ctx().e_internalized(term)) { ctx().mk_enode(term, false, false, true); + if (!ctx().relevancy() && u().is_defined(term)) { + push_case_expand(alloc(case_expansion, u(), term)); + } } + return true; } @@ -117,8 +121,8 @@ namespace smt { */ void theory_recfun::relevant_eh(app * n) { SASSERT(ctx().relevancy()); + TRACEFN("relevant_eh: (defined) " << u().is_defined(n) << " " << mk_pp(n, m)); if (u().is_defined(n) && u().has_defs()) { - TRACEFN("relevant_eh: (defined) " << mk_pp(n, m)); push_case_expand(alloc(case_expansion, u(), n)); } }