diff --git a/src/sat/smt/array_model.cpp b/src/sat/smt/array_model.cpp
index 0fbc4364ac8..33ad8e48405 100644
--- a/src/sat/smt/array_model.cpp
+++ b/src/sat/smt/array_model.cpp
@@ -120,7 +120,6 @@ namespace array {
     bool solver::must_have_different_model_values(theory_var v1, theory_var v2) {
         euf::enode* else1 = nullptr, * else2 = nullptr;
         euf::enode* n1 = var2enode(v1), *n2 = var2enode(v2);
-        euf::enode* r1 = n1->get_root(), * r2 = n2->get_root();
         expr* e1 = n1->get_expr();
         if (!a.is_array(e1))
             return true;
diff --git a/src/sat/smt/q_mam.cpp b/src/sat/smt/q_mam.cpp
index b1432a5eeca..7999ecea9e4 100644
--- a/src/sat/smt/q_mam.cpp
+++ b/src/sat/smt/q_mam.cpp
@@ -2070,7 +2070,6 @@ namespace q {
         enode * n = m_registers[j2->m_reg]->get_root();
         if (n->num_parents() == 0)
             return nullptr;
-        unsigned num_args = n->num_args();
         enode_vector * v  = mk_enode_vector();
         for (enode* p : euf::enode_parents(n)) {
             if (p->get_decl() == j2->m_decl &&
diff --git a/src/tactic/ufbv/macro_finder_tactic.cpp b/src/tactic/ufbv/macro_finder_tactic.cpp
index 2c0a529e682..86c60653816 100644
--- a/src/tactic/ufbv/macro_finder_tactic.cpp
+++ b/src/tactic/ufbv/macro_finder_tactic.cpp
@@ -17,6 +17,7 @@ Module Name:
 
 --*/
 #include "tactic/tactical.h"
+#include "ast/recfun_decl_plugin.h"
 #include "ast/macros/macro_manager.h"
 #include "ast/macros/macro_finder.h"
 #include "tactic/generic_model_converter.h"
@@ -42,6 +43,12 @@ class macro_finder_tactic : public tactic {
             tactic_report report("macro-finder", *g);
             TRACE("macro-finder", g->display(tout););
 
+            recfun::util rec(m());
+            if (!rec.get_rec_funs().empty()) {
+                result.push_back(g.get());
+                return;
+            }
+
             bool produce_proofs = g->proofs_enabled();
             bool unsat_core_enabled = g->unsat_core_enabled();
             macro_manager mm(m_manager);