diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp
index d4f34f359..226b6b00a 100644
--- a/src/smt/theory_recfun.cpp
+++ b/src/smt/theory_recfun.cpp
@@ -75,6 +75,9 @@ namespace smt {
             bool_var v = ctx().mk_bool_var(atom);
             ctx().set_var_theory(v, get_id());
         }
+        if (!ctx().relevancy() && u().is_defined(atom)) {
+            push_case_expand(alloc(case_expansion, u(), atom));
+        }
         return true;
     }