From 322531e95cb7da59b4596000ffbc92d792433f17 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 25 May 2021 10:20:20 -0700 Subject: [PATCH] fix #5303 --- src/tactic/core/elim_uncnstr_tactic.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp index f5756bfd4..4df4d1fc4 100644 --- a/src/tactic/core/elim_uncnstr_tactic.cpp +++ b/src/tactic/core/elim_uncnstr_tactic.cpp @@ -21,6 +21,7 @@ Notes: #include "ast/rewriter/rewriter_def.h" #include "ast/arith_decl_plugin.h" #include "ast/bv_decl_plugin.h" +#include "ast/recfun_decl_plugin.h" #include "ast/array_decl_plugin.h" #include "ast/datatype_decl_plugin.h" #include "tactic/core/collect_occs.h" @@ -784,7 +785,7 @@ class elim_uncnstr_tactic : public tactic { m_vars.reset(); collect_occs p; p(*g, m_vars); - if (m_vars.empty()) { + if (m_vars.empty() || recfun::util(m()).has_defs()) { result.push_back(g.get()); // did not increase depth since it didn't do anything. return;