diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h
index 206b2c951..b51717c1d 100644
--- a/src/ast/recfun_decl_plugin.h
+++ b/src/ast/recfun_decl_plugin.h
@@ -239,6 +239,7 @@ namespace recfun {
         th_rewriter & get_th_rewriter() { return m_th_rw; }
         bool is_case_pred(app * e) const { return is_app_of(e, m_family_id, OP_FUN_CASE_PRED); }
         bool is_defined(app * e) const { return is_app_of(e, m_family_id, OP_FUN_DEFINED); }
+        bool is_depth_limit(app * e) const { return is_app_of(e, m_family_id, OP_DEPTH_LIMIT); }
         bool owns_app(app * e) const { return e->get_family_id() == m_family_id; }
 
         //<! add a function declaration
diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp
index 3bafaf925..1aa3e433e 100644
--- a/src/smt/theory_recfun.cpp
+++ b/src/smt/theory_recfun.cpp
@@ -193,14 +193,14 @@ namespace smt {
             app_ref dlimit = m_util->mk_depth_limit_pred(get_max_depth());
             ctx.internalize(dlimit, false);
             c.push_back(~ ctx.get_literal(dlimit));
-            //SASSERT(ctx.get_assignment(ctx.get_literal(dlimit)) == l_true);
+            SASSERT(ctx.get_assignment(ctx.get_literal(dlimit)) == l_true);
         }
         for (auto& kv : m_guards) {
             expr * g = & kv.get_key();
             c.push_back(~ ctx.get_literal(g));
         }
         DEBUG("max-depth limit: add clause " << pp_lits(ctx, c.size(), c.c_ptr()));
-        //SASSERT(std::all_of(c.begin(), c.end(), [&](literal & l) { return ctx.get_assignment(l) == l_false; })); // conflict
+        SASSERT(std::all_of(c.begin(), c.end(), [&](literal & l) { return ctx.get_assignment(l) == l_false; })); // conflict
 
         m_q_clauses.push_back(std::move(c));
     }
@@ -373,6 +373,16 @@ namespace smt {
         assumptions.push_back(dlimit);
     }
 
+
+    // if `dlimit` occurs in unsat core, return "unknown"
+    lbool theory_recfun::validate_unsat_core(expr_ref_vector & unsat_core) {
+        for (auto & e : unsat_core) {
+            if (is_app(e) && m_util->is_depth_limit(to_app(e)))
+                return l_undef;
+        }
+        return l_false;
+    }
+
     void theory_recfun::display(std::ostream & out) const {
         out << "recfun{}";
     }
diff --git a/src/smt/theory_recfun.h b/src/smt/theory_recfun.h
index 2439c07ff..e73b43a7d 100644
--- a/src/smt/theory_recfun.h
+++ b/src/smt/theory_recfun.h
@@ -136,6 +136,7 @@ namespace smt {
         void restart_eh() override;
         bool can_propagate() override;
         void propagate() override;
+        lbool validate_unsat_core(expr_ref_vector &) override;
 
         void new_eq_eh(theory_var v1, theory_var v2) override {}
         void new_diseq_eh(theory_var v1, theory_var v2) override {}