diff --git a/src/sat/smt/recfun_solver.cpp b/src/sat/smt/recfun_solver.cpp
index b908297ad..c88138d3f 100644
--- a/src/sat/smt/recfun_solver.cpp
+++ b/src/sat/smt/recfun_solver.cpp
@@ -333,6 +333,11 @@ namespace recfun {
         return found;
     }
 
+    bool solver::is_beta_redex(euf::enode* p, euf::enode* n) const {
+        return is_defined(p) || is_case_pred(p);
+    }
+
+
     bool solver::add_dep(euf::enode* n, top_sort<euf::enode>& dep) {
         if (n->num_args() == 0)
             dep.insert(n, nullptr);
diff --git a/src/sat/smt/recfun_solver.h b/src/sat/smt/recfun_solver.h
index 69b799b4c..d469b7437 100644
--- a/src/sat/smt/recfun_solver.h
+++ b/src/sat/smt/recfun_solver.h
@@ -108,6 +108,7 @@ namespace recfun {
         bool is_shared(euf::theory_var v) const override { return true; }
         void init_search() override {}
         bool should_research(sat::literal_vector const& core) override;
+        bool is_beta_redex(euf::enode* p, euf::enode* n) const;
         void add_assumptions(sat::literal_set& assumptions) override;
         bool tracking_assumptions() override { return true; }
     };
diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp
index 782510681..c18e5577b 100644
--- a/src/smt/theory_recfun.cpp
+++ b/src/smt/theory_recfun.cpp
@@ -467,6 +467,15 @@ namespace smt {
         return found;
     }
 
+    /**
+     * n is an argument of p, if p is a function definition or case predicate,
+     * then there is no reason for the solver to enforce that equality on n is 
+     * fully determined. It is a beta-redex with respect to expanding p.
+     */
+    bool theory_recfun::is_beta_redex(enode* p, enode* n) const {
+        return is_defined(p) || is_case_pred(p);
+    }
+
     void theory_recfun::display(std::ostream & out) const {
         out << "recfun\n";
         out << "disabled guards:\n" << m_disabled_guards << "\n";
diff --git a/src/smt/theory_recfun.h b/src/smt/theory_recfun.h
index 097181d22..2e576a29a 100644
--- a/src/smt/theory_recfun.h
+++ b/src/smt/theory_recfun.h
@@ -99,6 +99,7 @@ namespace smt {
         bool can_propagate() override;
         void propagate() override;
         bool should_research(expr_ref_vector &) override;
+        bool is_beta_redex(enode* p, enode* n) const override;
 
         void new_eq_eh(theory_var v1, theory_var v2) override {}
         void new_diseq_eh(theory_var v1, theory_var v2) override {}