fix #5303

Z3Prover · May 25, 2021 · 322531e · 322531e
1 parent 36ca98c
commit 322531e
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp
@@ -21,6 +21,7 @@ Module Name:
 #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;