From 8ff1e44a9593d729a028bc93996a2b9032e5faeb Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 6 Nov 2022 11:58:21 -0800
Subject: [PATCH] add discriminator to whether context contains recursive
 functions to avoid enabling recursive function solver when there are just
 macros

---
 src/ast/recfun_decl_plugin.cpp | 1 +
 src/ast/recfun_decl_plugin.h   | 4 ++++
 2 files changed, 5 insertions(+)

diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp
index bf865b393..755a3eccd 100644
--- a/src/ast/recfun_decl_plugin.cpp
+++ b/src/ast/recfun_decl_plugin.cpp
@@ -473,6 +473,7 @@ namespace recfun {
         }
         
         void plugin::set_definition(replace& r, promise_def & d, bool is_macro, unsigned n_vars, var * const * vars, expr * rhs) {
+            m_has_rec_defs |= !is_macro;
             u().set_definition(r, d, is_macro, n_vars, vars, rhs);
             for (case_def & c : d.get_def()->get_cases()) 
                 m_case_defs.insert(c.get_decl(), &c);
diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h
index 8e1279c0a..c369e2827 100644
--- a/src/ast/recfun_decl_plugin.h
+++ b/src/ast/recfun_decl_plugin.h
@@ -165,6 +165,7 @@ namespace recfun {
             mutable scoped_ptr<util> m_util;
             def_map                  m_defs;       // function->def
             case_def_map             m_case_defs;  // case_pred->def
+            bool                     m_has_rec_defs = false;
             
             ast_manager & m() { return *m_manager; }
 
@@ -200,6 +201,7 @@ namespace recfun {
 
             bool has_def(func_decl* f) const { return m_defs.contains(f); }
             bool has_defs() const;
+            bool has_rec_defs() const { return m_has_rec_defs; }
             def const& get_def(func_decl* f) const { return *(m_defs[f]); }
             promise_def get_promise_def(func_decl* f) const { return promise_def(&u(), m_defs[f]); }
             def& get_def(func_decl* f) { return *(m_defs[f]); }
@@ -249,6 +251,8 @@ namespace recfun {
         //<! don't use native theory if recursive function declarations are not populated with defs
         bool has_defs() const { return m_plugin->has_defs(); }
 
+        bool has_rec_defs() const { return m_plugin->has_rec_defs(); }
+
         //<! add a function declaration
         def * decl_fun(symbol const & s, unsigned n_args, sort *const * args, sort * range, bool is_generated);