From 78571b9a5178ddcaa42ef1a68a1e5036a9ad90ab Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 27 Apr 2021 09:30:00 -0700
Subject: [PATCH] fix #5219

---
 src/sat/smt/dt_solver.cpp | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/sat/smt/dt_solver.cpp b/src/sat/smt/dt_solver.cpp
index 892ba2f58..9ab23ebc8 100644
--- a/src/sat/smt/dt_solver.cpp
+++ b/src/sat/smt/dt_solver.cpp
@@ -703,9 +703,11 @@ namespace dt {
     }
 
     bool solver::add_dep(euf::enode* n, top_sort<euf::enode>& dep) {
-        theory_var v = n->get_th_var(get_id());
         if (!is_datatype(n->get_expr()))
             return true;
+        theory_var v = n->get_th_var(get_id());
+        if (v == euf::null_theory_var) 
+            return true;        
         euf::enode* con = m_var_data[m_find.find(v)]->m_constructor;
         if (con->num_args() == 0)
             dep.insert(n, nullptr);