From 3b16f129bb32908bda1d1030a4b8008c317216fe Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 29 Dec 2019 21:29:39 -0800
Subject: [PATCH] fix #2803

---
 src/smt/theory_recfun.cpp | 3 +++
 1 file changed, 3 insertions(+)

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;
     }